Subst improvements

pulse/test/bug-reports/Bug267.fst.output.expected

@@ -3,7 +3,7 @@
   - Tactic failed
   - Expected a total term, but this term has Ghost effect
 
-* Info at Bug267.fst(58,5-58,8):
+* Info at Bug267.fst(58,4-58,5):
   - Expected failure:
   - Could not prove equality between computed type int and expected type nat
   - Assertion failed

src/syntax/FStarC.Syntax.Subst.fst

@@ -64,18 +64,14 @@ let compose_subst (s1 s2 : subst_ts) : subst_ts =
                | _ -> snd s1 in
     (s, ropt)
 
-//apply a delayed substitution s to t,
-//composing it with any other delayed substitution that may already be there
+// Apply a delayed substitution s to t.
+// This may nest Tm_delayed nodes, that is fine. If we coallesce
+// them, that implies composing the substitutions and potentially breaking
+// sharing.
+let delay' (t:term) (s : subst_ts) rng : ML term =
+    mk_Tm_delayed (t, s) rng
 let delay (t:term) (s : subst_ts) : ML term =
- match t.n with
- | Tm_delayed {tm=t'; substs=s'} ->
-    //s' is the subsitution already associated with this node;
-    //s is the new subsitution to add to it
-    //compose substitutions by concatenating them
-    //the order of concatenation is important!
-    mk_Tm_delayed (t', compose_subst s' s) t.pos
- | _ ->
-    mk_Tm_delayed (t, s) t.pos
+    delay' t s t.pos
 
 (*
     force_uvar' (t:term) : term * bool
@@ -198,11 +194,11 @@ let rec subst' (s:subst_ts) (t:term) : ML term =
     | Tm_fvar _ -> tag_with_range t0 s   //fvars are never subject to substitution
 
     | Tm_delayed {tm=t';substs=s'} ->
-        //s' is the subsitution already associated with this node;
-        //s is the new subsitution to add to it
-        //compose substitutions by concatenating them
-        //the order of concatenation is important!
-        mk_Tm_delayed (t', compose_subst s' s) t.pos
+        (* I really just want this:
+           delay t s
+        Or to remove this completely and fall in the default case above.
+        But somehow, that's incredibly bad for ranges. *)
+        delay' t' (compose_subst s' s) t.pos
 
     | Tm_bvar a ->
         apply_until_some_then_map (subst_bv a) (fst s) subst_tail t0
@@ -214,10 +210,7 @@ let rec subst' (s:subst_ts) (t:term) : ML term =
         mk (Tm_type (subst_univ (fst s) u)) (mk_range t0.pos s)
 
     | _ ->
-      //NS: 04/12/2018
-      //    Substitutions on Tm_uvar just gets delayed
-      //    since its solution may eventually end up being an open term
-      mk_Tm_delayed (t0, s) (mk_range t.pos s)
+      delay' t0 s (mk_range t.pos s)
 
 let subst_dec_order' s = function
   | Decreases_lex l -> Decreases_lex (l |> List.map (subst' s))
@@ -337,46 +330,15 @@ let push_subst_lcomp s lopt : ML _ = match lopt with
                  ; residual_flags  = rc.residual_flags } in
         Some rc
 
-let compose_uvar_subst (u:ctx_uvar) (s0:subst_ts) (s:subst_ts) : ML subst_ts =
-    let should_retain x =
-        u.ctx_uvar_binders |> U.for_some (fun b -> S.bv_eq x b.binder_bv)
-    in
-    let rec aux (l:list (list subst_elt)) : ML (list subst_elt) = match l with
-        | [] -> []
-        | hd_subst::rest ->
-          let hd =
-              hd_subst |> List.collect (function
-              | NT(x, t) ->
-                if should_retain x
-                then [NT(x, delay t (rest, NoUseRange))]
-                else []
-              | NM(x, i) ->
-                if should_retain x
-                then let x_i = S.bv_to_tm ({x with index=i}) in
-                     let t = subst' (rest, NoUseRange) x_i in
-                     match t.n with
-                     | Tm_bvar x_j -> [NM(x, x_j.index)]
-                     | _ -> [NT(x, t)]
-                else []
-              | _ -> [])
-          in
-          hd @ aux rest
-    in
-    match aux (fst s0 @ fst s) with
-    | [] -> [], snd s
-    |  s' -> [s'], snd s
-
 //
-// If resolve_uvars is true, it will lookup the unionfind graph
-//   and use uvar solution, if it has already been solved
-//   see the Tm_uvar case in this function
-// Otherwise it will just compose s with the uvar subst
+// Push a substitution one level down.
 // 
-let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
+let rec push_subst (s : subst_ts) (t : term) : ML term =
     //makes a syntax node, setting it's use range as appropriate from s
     let mk t' = Syntax.mk t' (mk_range t.pos s) in
     match t.n with
-    | Tm_delayed _ -> failwith "Impossible (delayed node in push_subst)"
+    | Tm_delayed _ ->
+      push_subst s (compress_subst t)
 
     | Tm_lazy i ->
         begin match i.lkind with
@@ -385,7 +347,7 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
              * The hope is that this does not occur often and so
              * we still get good performance. *)
           let t = Option.must !lazy_chooser i.lkind i in // Can't call Syntax.Util from here
-          push_subst_aux resolve_uvars s t
+          push_subst s t
         | _ ->
             (* All others must be closed, so don't bother *)
             tag_with_range t s
@@ -396,14 +358,7 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
     | Tm_unknown -> tag_with_range t s //these are always closed
 
     | Tm_uvar (uv, s0) ->
-      let fallback () =
-        tag_with_range ({t with n = Tm_uvar(uv, compose_uvar_subst uv s0 s)}) s
-      in
-      if not resolve_uvars
-      then fallback ()
-      else (match (Unionfind.find uv.ctx_uvar_head) with
-            | None -> fallback ()
-            | Some t -> push_subst_aux resolve_uvars (compose_subst s0 s) t)
+      tag_with_range ({t with n = Tm_uvar(uv, compose_subst s0 s)}) s
 
     | Tm_type _
     | Tm_bvar _
@@ -489,20 +444,26 @@ let rec push_subst_aux (resolve_uvars:bool) s t : ML _ =
 
     | Tm_meta {tm=t; meta=m} ->
         mk (Tm_meta {tm=subst' s t; meta=m})
-
-let push_subst s t : ML _ = push_subst_aux true s t
-
 //
 // Only push the pending substitution down,
 //   no resolving uvars
 //
-let compress_subst (t:term) : ML term =
+and compress_subst (t:term) : ML term =
   match t.n with
   | Tm_delayed {tm=t; substs=s} ->
-    let resolve_uvars = false in
-    push_subst_aux resolve_uvars s t
+    push_subst s t
   | _ -> t
 
+let compress_post_check (t:term) : ML unit =
+  match t.n with
+  | Tm_delayed _ -> failwith "compress attempting to return a Tm_delayed"
+  | Tm_uvar ({ctx_uvar_head=uv}, s) -> (
+    match Unionfind.find uv with
+        | Some t' -> failwith "compress attempting to return a solved uvar"
+        | None -> ()
+  )
+  | _ -> ()
+
 (* compress:
       This is used pervasively, throughout the codebase
 
@@ -513,41 +474,21 @@ let compress_subst (t:term) : ML term =
          2. eliminate any top-level (Tm_uvar uv) node,
             when uv has been assigned a solution already
 
-      `compress` should will *not* memoize the result of uvar
-      solutions (since those could be reverted), nor the result
-      of `push_subst` (since it internally uses the unionfind
-      graph too).
-
-      The function is broken into a fast-path where the
-      result can be easily determined and a recursive slow
-      path.
-
-      Warning: if force_uvar changes to operate on inputs other than
-      Tm_uvar then the fastpath out match in compress will need to be
-      updated.
-
-      This function should NEVER return a Tm_delayed. If you do any
-      non-trivial change to it, it would be wise to uncomment the check
-      below and run a full regression build.
+      This function should NEVER return a Tm_delayed, nor a resolved uvar. If
+      you do any non-trivial change to it, it would be wise to uncomment the
+      check below and run a full regression build.
 *)
-let rec compress_slow (t:term) : ML _ =
+let rec compress (t:term) =
+  let r =
     let t = force_uvar t in
     match t.n with
     | Tm_delayed {tm=t'; substs=s} ->
-        compress (push_subst s t')
-    | _ ->
-        t
-and compress (t:term) : ML term =
-  match t.n with
-    | Tm_delayed _ | Tm_uvar _ ->
-        let r = compress_slow t in
-        (* begin match r.n with *)
-        (* | Tm_delayed _ -> failwith "compress attempting to return a Tm_delayed" *)
-        (* | _ -> () *)
-        (* end; *)
-        r
+      compress (push_subst s t')
     | _ ->
-        t
+      t
+  in
+  // compress_post_check r;
+  r
 
 let subst s t : ML _ = subst' ([s], NoUseRange) t
 let set_use_range r t : ML _ = subst' ([], SomeUseRange (Range.set_def_range r (Range.use_range r))) t

src/typechecker/FStarC.TypeChecker.TermEqAndSimplify.fst

@@ -131,6 +131,25 @@ let rec eq_tm (env:env_t) (t1:term) (t2:term) : ML eq_result =
       )
       | _ -> None
     in
+    let eq_subst_elt (e1:subst_elt) (e2:subst_elt) : ML bool =
+      match e1, e2 with
+      | DB (i1, x1), DB (i2, x2) -> i1 = i2 && bv_eq x1 x2
+      | DT (i1, t1), DT (i2, t2) -> i1 = i2 && eq_tm env t1 t2 = Equal
+      | NM (x1, i1), NM (x2, i2) -> bv_eq x1 x2 && i1 = i2
+      | NT (x1, t1), NT (x2, t2) -> bv_eq x1 x2 && eq_tm env t1 t2 = Equal
+      | UN (i1, u1), UN (i2, u2) -> i1 = i2 && eq_univs u1 u2
+      | UD (u1, i1), UD (u2, i2) -> ident_equals u1 u2 && i1 = i2
+      | _ -> false
+    in
+    let eq_subst_ts (_env:env_t) (s1:subst_ts) (s2:subst_ts) : ML bool =
+      let s1l, _r1 = s1 in
+      let s2l, _r2 = s2 in
+      List.length s1l = List.length s2l &&
+      List.forall2 (fun l1 l2 ->
+        List.length l1 = List.length l2 &&
+        List.forall2 eq_subst_elt l1 l2
+      ) s1l s2l
+    in
     let t1 = unmeta t1 in
     let t2 = unmeta t2 in
     match t1.n, t2.n with
@@ -185,8 +204,10 @@ let rec eq_tm (env:env_t) (t1:term) (t2:term) : ML eq_result =
       // updates should be done with care.
       equal_iff (eq_const c d)
 
-    | Tm_uvar (u1, ([], _)), Tm_uvar (u2, ([], _)) ->
-      equal_if (Unionfind.equiv u1.ctx_uvar_head u2.ctx_uvar_head)
+    | Tm_uvar (u1, s1), Tm_uvar (u2, s2) ->
+      if Unionfind.equiv u1.ctx_uvar_head u2.ctx_uvar_head
+      then equal_if (eq_subst_ts env s1 s2)
+      else Unknown
 
     | Tm_app {hd=h1; args=args1}, Tm_app {hd=h2; args=args2} ->
       begin match (un_uinst h1).n, (un_uinst h2).n with

tests/error-messages/TestHasEq.fst.json_output.expected

@@ -1,3 +1,3 @@
 {"msg":["Expected failure:","Failed to prove that the type\n'TestHasEq.t3'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query.","Env = (a : Type0)","VC =\n  forall (x: a).\n    (* - Failed to prove that the type\\n    'TestHasEq.t3'\\n    supports decidable equality because of this argument.\\n  - Add either the 'noeq' or 'unopteq' qualifier *)\n    Prims.hasEq a"],"level":"Info","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":57,"col":0},"end_pos":{"line":58,"col":19}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":58,"col":10},"end_pos":{"line":58,"col":11}}},"number":19,"ctx":["While typechecking the top-level declaration `type TestHasEq.t3`","While typechecking the top-level declaration `[@@expect_failure] type TestHasEq.t3`"]}
-{"msg":["Expected failure:","Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query.","Env =\n  (x : x: TestHasEq.erasable_t{C_erasable_t? x})\n  (y : y: TestHasEq.erasable_t{D_erasable_t? y})","VC =\n  Prims.hasEq TestHasEq.erasable_t /\\\n  (forall (any_result: Type0).\n      x: TestHasEq.erasable_t{C_erasable_t? x \\/ D_erasable_t? x} == any_result ==>\n      (C_erasable_t? x ==> C_erasable_t? x \\/ D_erasable_t? x) /\\\n      (forall (any_result: x: TestHasEq.erasable_t{C_erasable_t? x}).\n          x == any_result ==>\n          (D_erasable_t? y ==> C_erasable_t? y \\/ D_erasable_t? y) /\\\n          (forall (any_result: y: TestHasEq.erasable_t{D_erasable_t? y}).\n              y == any_result ==>\n              (forall (any_result: Prims.bool).\n                  x = y == any_result ==>\n                  (forall (k: Prims.pure_post (n: Prims.int{n == 1})).\n                      (forall (x: n: Prims.int{n == 1}).\n                          {:pattern Prims.guard_free (k x)}\n                          k x) ==>\n                      x = y == true ==> Prims.l_False)))))"],"level":"Info","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":84,"col":12},"end_pos":{"line":84,"col":22}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":84,"col":10},"end_pos":{"line":84,"col":70}}},"number":19,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]}
+{"msg":["Expected failure:","Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query.","Env =\n  (x : x: TestHasEq.erasable_t{C_erasable_t? x})\n  (y : y: TestHasEq.erasable_t{D_erasable_t? y})","VC =\n  Prims.hasEq TestHasEq.erasable_t /\\\n  (forall (any_result: Type0).\n      x: TestHasEq.erasable_t{C_erasable_t? x \\/ D_erasable_t? x} == any_result ==>\n      (C_erasable_t? x ==> C_erasable_t? x \\/ D_erasable_t? x) /\\\n      (forall (any_result: x: TestHasEq.erasable_t{C_erasable_t? x}).\n          x == any_result ==>\n          (D_erasable_t? y ==> C_erasable_t? y \\/ D_erasable_t? y) /\\\n          (forall (any_result: y: TestHasEq.erasable_t{D_erasable_t? y}).\n              y == any_result ==>\n              (forall (any_result: Prims.bool).\n                  x = y == any_result ==>\n                  (forall (k: Prims.pure_post (n: Prims.int{n == 1})).\n                      (forall (x: n: Prims.int{n == 1}).\n                          {:pattern Prims.guard_free (k x)}\n                          k x) ==>\n                      x = y == true ==> Prims.l_False)))))"],"level":"Info","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":84,"col":12},"end_pos":{"line":84,"col":22}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":85,"col":7},"end_pos":{"line":85,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]}
 {"msg":["Expected failure:","Invalid qualifiers for declaration `type TestHasEq.erasable_t2`","The `unopteq` qualifier is not allowed on erasable inductives since they don't\nhave decidable equality."],"level":"Info","range":{"def":{"file_name":"TestHasEq.fst","start_pos":{"line":88,"col":8},"end_pos":{"line":89,"col":30}},"use":{"file_name":"TestHasEq.fst","start_pos":{"line":88,"col":8},"end_pos":{"line":89,"col":30}}},"number":162,"ctx":["While typechecking the top-level declaration `type TestHasEq.erasable_t2`","While typechecking the top-level declaration `[@@expect_failure] type TestHasEq.erasable_t2`"]}

tests/error-messages/TestHasEq.fst.output.expected

@@ -12,7 +12,7 @@
         Prims.hasEq a
   - See also TestHasEq.fst(57,0-58,19)
 
-* Info at TestHasEq.fst(84,10-84,70):
+* Info at TestHasEq.fst(85,7-85,8):
   - Expected failure:
   - Subtyping check failed
   - Expected type Prims.eqtype got type Type0