Merge pull request #3250 from mtzguido/misc

Misc fixes

src/syntax/FStar.Syntax.Hash.fst

@@ -549,7 +549,10 @@ and equal_meta m1 m2 =
     Ident.lid_equals n1 n2 &&
     equal_term t1 t2
 
-and equal_lazyinfo l1 l2 = l1 = l2
+and equal_lazyinfo l1 l2 =
+  (* We cannot really compare the blobs. Just try physical
+  equality (first matching kinds). *)
+  l1.lkind = l1.lkind && BU.physical_equality l1.blob l2.blob
 
 and equal_quoteinfo q1 q2 =
   q1.qkind = q2.qkind &&

src/typechecker/FStar.TypeChecker.Core.fst

@@ -857,12 +857,12 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ)
         | Tm_app _ ->
           let head = U.leftmost_head t in
           (match (Subst.compress head).n with
-           | Tm_abs _ -> N.normalize [Env.Beta; Env.Iota] g.tcenv t
+           | Tm_abs _ -> N.normalize [Env.Beta; Env.Iota; Env.Primops] g.tcenv t
            | _ -> t)
 
         | Tm_let _
         | Tm_match _ ->
-          N.normalize [Env.Beta;Env.Iota] g.tcenv t
+          N.normalize [Env.Beta;Env.Iota;Env.Primops] g.tcenv t
 
         | Tm_refine _ ->
           U.flatten_refinement t

src/typechecker/FStar.TypeChecker.Rel.fst

@@ -2137,6 +2137,10 @@ let gamma_has_free_uvars (g:list binding) : bool =
   List.existsb (function Binding_var bv -> has_free_uvars bv.sort
                        | _ -> false) g
 
+type reveal_hide_t =
+  | Hide of (universe & typ & term)
+  | Reveal of (universe & typ & term)
+
 (******************************************************************************************************)
 (* Main solving algorithm begins here *)
 (******************************************************************************************************)
@@ -3779,17 +3783,15 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
                     | _ -> None
                 in
                 let is_reveal_or_hide t =
-                  // Returns Inl (u, ty, t) for reveal u#u #ty t
-                  // Returns Inr (u, ty, t) for hide u#u #ty t
                   let h, args = U.head_and_args t in
                   if U.is_fvar PC.reveal h
                   then match payload_of_hide_reveal h args with
                        | None -> None
-                       | Some t -> Some (Inl t)
+                       | Some t -> Some (Reveal t)
                   else if U.is_fvar PC.hide h
                   then match payload_of_hide_reveal h args with
                        | None -> None
-                       | Some t -> Some (Inr t)
+                       | Some t -> Some (Hide t)
                   else None
                 in
                 let mk_fv_app lid u args r =
@@ -3798,44 +3800,31 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
                   S.mk_Tm_app head args r
                 in
                 match is_reveal_or_hide t1, is_reveal_or_hide t2 with
-                | None, None -> None
-
-                | Some (Inl _), Some (Inl _)
-                | Some (Inr _), Some (Inr _) ->
-                  //reveal/reveal, or hide/hide; impossible, head_matches_delta
-                  //would have matched
-                  None
-
-                | Some (Inl _), Some (Inr _)
-                | Some (Inr _), Some (Inl _) ->
-                  //reveal/hide, or hide/reveal; inapplicable
-                  None
-
-                (* We only apply these rules when the arg to reveal
+                (* We only apply these first two rules when the arg to reveal
                 is a flex, to avoid loops such as:
                      reveal t1 =?= t2
                   ~> t1        =?= hide t2
                   ~> reveal t1 =?= t2
                 *)
-                | Some (Inl (u, ty, lhs)), None when is_flex lhs ->
+                | Some (Reveal (u, ty, lhs)), None when is_flex lhs ->
                   // reveal (?u _) / _
                   //add hide to rhs and simplify lhs
                   let rhs = mk_fv_app PC.hide u [(ty, S.as_aqual_implicit true); (t2, None)] t2.pos in
                   Some (lhs, rhs)
 
-                | None, Some (Inl (u, ty, rhs)) when is_flex rhs ->
+                | None, Some (Reveal (u, ty, rhs)) when is_flex rhs ->
                   // _ / reveal (?u _)
                   //add hide to lhs and simplify rhs
                   let lhs = mk_fv_app PC.hide u [(ty, S.as_aqual_implicit true); (t1, None)] t1.pos in
                   Some (lhs, rhs)
 
-                | Some (Inr (u, ty, lhs)), None ->
+                | Some (Hide (u, ty, lhs)), None ->
                   // hide _ / _
                   //add reveal to rhs and simplify lhs
                   let rhs = mk_fv_app PC.reveal u [(ty,S.as_aqual_implicit true); (t2, None)] t2.pos in
                   Some (lhs, rhs)
 
-                | None, Some (Inr (u, ty, rhs)) ->
+                | None, Some (Hide (u, ty, rhs)) ->
                   // _ / hide _
                   //add reveal to lhs and simplify rhs
                   let lhs = mk_fv_app PC.reveal u [(ty,S.as_aqual_implicit true); (t1, None)] t1.pos in

tests/tactics/CheckEquiv.fst

@@ -0,0 +1,45 @@
+module CheckEquiv
+
+open FStar.Tactics.V2
+open FStar.Ghost
+
+let g (x:int) : int = x
+
+let must (r:ret_t 'a) : Tac 'a =
+  match r with
+  | Some x, [] -> x
+  | _, issues ->
+    log_issues issues;
+    fail "must failed"
+
+#push-options "--no_smt"
+let _ = assert True by begin
+  let env = cur_env () in
+  let _ = must <| check_equiv env (`1) (`(g 1)) in
+  ()
+end
+
+let _ = assert True by begin
+  let env = cur_env () in
+  let _ = must <| check_equiv env (`1) (`1) in
+  ()
+end
+
+let _ = assert True by begin
+  let env = cur_env () in
+  let _ = must <| check_equiv env (`(1+1)) (`(3-1)) in
+  ()
+end
+
+#pop-options
+
+(* This one creates a guard for:
+
+  1 == (match hide 1 with | 1 -> 1 | _ -> 0)
+
+*)
+let _ = assert True by begin
+  let env = cur_env () in
+  let _ = must <| check_equiv env (`1) (`(reveal u#0 #int (hide u#0 #int 1))) in
+  ()
+end

ulib/FStar.Cardinality.Universes.fst

@@ -6,11 +6,11 @@ open FStar.Cardinality.Cantor
 (* This type is an injection of all powersets of Type u (i.e. Type u -> bool
 functions) into Type (u+1) *)
 noeq
-type type_powerset : (Type u#a -> bool) -> Type u#(a+1) =
+type type_powerset : (Type u#a -> bool) -> Type u#(max (a+1) b) =
   | Mk : f:(Type u#a -> bool) -> type_powerset f
 
 let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
-  : Lemma (requires type_powerset f1 == type_powerset f2)
+  : Lemma (requires type_powerset u#a u#b f1 == type_powerset u#a u#b f2)
           (ensures f1 == f2)
 =
   assert (type_powerset f1 == type_powerset f2);
@@ -22,17 +22,21 @@ let aux_inj_type_powerset (f1 f2 : powerset (Type u#a))
 let inj_type_powerset () : Lemma (is_inj type_powerset) =
   Classical.forall_intro_2 (fun f1 -> Classical.move_requires (aux_inj_type_powerset f1))
 
- (* The general structure of this proof is:
-   1- We know there is an injection of powerset(Type(u)) into Type(u+1) (see type_powerset above)
+(* let u' > u be universes. (u' = max(a+1, b), u=a below)
+   The general structure of this proof is:
+   1- We know there is an injection of powerset(Type(u)) into Type(u') (see type_powerset above)
    2- We know there is NO injection from powerset(Type(u)) into Type(u) (see no_inj_powerset)
-   3- Therefore, there cannot be an injection from Type(u+1) into Type(u), otherwise we would
+   3- Therefore, there cannot be an injection from Type(u') into Type(u), otherwise we would
       compose it with the first injection and obtain the second impossible injection.
 *)
-let no_inj_universes (f : Type u#(a+1) -> Type u#a) : Lemma (~(is_inj f)) =
+let no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a) : Lemma (~(is_inj f)) =
   let aux () : Lemma (requires is_inj f) (ensures False) =
     let comp : powerset (Type u#a) -> Type u#a = fun x -> f (type_powerset x) in
     inj_type_powerset ();
     inj_comp type_powerset f;
     no_inj_powerset _ comp
   in
   Classical.move_requires aux ()
+
+let no_inj_universes_suc (f : Type u#(a+1) -> Type u#a) : Lemma (~(is_inj f)) =
+  no_inj_universes f

ulib/FStar.Cardinality.Universes.fsti

@@ -3,6 +3,12 @@ module FStar.Cardinality.Universes
 open FStar.Functions
 open FStar.Cardinality.Cantor
 
-(* Prove that there can be no injection from Type (u+1) into Type u *)
-val no_inj_universes (f : Type u#(a+1) -> Type u#a)
+(* Prove that there can be no injection from a universe into a strictly smaller
+universe. We use `max (a+1) b` to represent an arbitrary universe strictly larger
+than `a` as we cannot write sums of universe levels. *)
+val no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a)
+  : Lemma (~(is_inj f))
+
+(* A simpler version for the +1 case. *)
+val no_inj_universes_suc (f : Type u#(a+1) -> Type u#a)
   : Lemma (~(is_inj f))