Make Set[T] contravariant in T (as it should be)

nyu-acsys · Dec 5, 2024 · ccd1e31 · ccd1e31
1 parent ffa32f5
commit ccd1e31
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 9 deletions.
diff --git a/lib/ast/astDef.ml b/lib/ast/astDef.ml
@@ -444,8 +444,6 @@ module Type = struct
     match (t1, t2) with
     | App (Bot, [], _), t | t, App (Bot, [], _) -> t
     | App (t1, [], a1), App (t2, [], _) -> App (join_constr t1 t2, [], a1)
-    | App (Map, [t1; App (Bool, [], a0)], a1), App (Map, [t2; App (Bool, [], _)], _a2) ->
-      App (Map, [join t1 t2; App (Bool, [], a0)], a1)
     | App (Map, [ti1; to1], a1), App (Map, [ti2; to2], _) -> App (Map, [meet ti1 ti2; join to1 to2], a1)
     | App (Prod, ts1, a1), App (Prod, ts2, _a2) ->
       (List.map2 ~f:join ts1 ts2 |> function
@@ -459,8 +457,6 @@ module Type = struct
     match (t1, t2) with
     | App (Any, [], _), t | t, App (Any, [], _) -> t
     | App (t1, [], a1), App (t2, [], _) -> App (meet_constr t1 t2, [], a1)
-    | App (Map, [t1; App (Bool, [], a0)], a1), App (Map, [t2; App (Bool, [], _)], _a2) ->
-      App (Map, [meet t1 t2; App (Bool, [], a0)], a1)
     | App (Map, [ti1; to1], a1), App (Map, [ti2; to2], _) -> App (Map, [join ti1 ti2; meet to1 to2], a1)
     | App (Prod, ts1, a1), App (Prod, ts2, _a2) ->
       (List.map2 ~f:meet ts1 ts2 |> function

diff --git a/lib/frontend/typing.ml b/lib/frontend/typing.ml
@@ -171,8 +171,8 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
             | Int _ -> (Type.int, Type.int)
             | Bool _ -> (Type.bool, Type.bool)
             | Empty ->
-                ( Type.(mk_set (Expr.to_loc expr) bot),
-                  Type.(mk_set (Expr.to_loc expr) any) )
+                ( Type.(mk_set (Expr.to_loc expr) any),
+                  Type.(mk_set (Expr.to_loc expr) bot) )
             | _ -> assert false
           in
           check_and_set expr given_type_lb given_type_ub expected_typ
@@ -245,8 +245,8 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
             | TupleLookUp -> Type.(any)
             | MapLookUp -> Type.(map bot expected_typ)
             | Diff | Union | Inter ->
-                Type.meet expected_typ Type.(set_typed any)
-            | Subseteq -> Type.(set_typed any)
+                Type.meet expected_typ Type.(set_typed bot)
+            | Subseteq -> Type.(set_typed bot)
             | Plus | Minus | Mult | Div | Mod | Gt | Lt | Geq | Leq -> Type.num
             | And | Or -> Type.perm
             | Impl -> Type.bool (* antecedent must be pure *)
@@ -320,7 +320,7 @@ let rec process_expr (expr : expr) (expected_typ : type_expr) : expr Rewriter.t
                 let typ = expr1 |> Expr.to_type |> Type.map_codom in
                 (typ, typ)
             | Diff | Union | Inter ->
-                (Type.(set_typed bot), Type.(set_typed any))
+                (Type.(set_typed any), Type.(set_typed bot))
             | Plus | Minus | Mult | Div | Mod ->
                 let typ = expr1 |> Expr.to_type in
                 (typ, typ)