Support purification inside rewrite each.

Author: gebner

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -264,7 +264,7 @@ let rec as_subst (p : list (term & term))
 
 
 
-let rewrite_all (is_source:bool) (g:env) (p: list (term & term)) (t:term) tac_opt : T.Tac (term & term) =
+let rewrite_all (is_source:bool) (g:env) (p: list (term & term)) (t:term) pre elaborated tac_opt : T.Tac (term & term) =
   (* We only use the rewrites_to substitution if there is no tactic attached to the
   rewrite. Otherwise, tactics may become brittle as the goal is changed unexpectedly
   by other things in the context. See tests/Match.fst. *)
@@ -275,7 +275,10 @@ let rewrite_all (is_source:bool) (g:env) (p: list (term & term)) (t:term) tac_op
     let t = dfst <| Pulse.Checker.Prover.normalize_slprop g t use_rwr in
     t
   in
+  let maybe_purify t = if elaborated then t else purify_term g {ctxt_now=pre;ctxt_old=None} t in
   let elab_pair (lhs rhs : R.term) : T.Tac (R.term & R.term) =
+    let lhs = maybe_purify lhs in
+    let rhs = maybe_purify rhs in
     let lhs, lhs_typ = Pulse.Checker.Pure.instantiate_term_implicits g lhs None true in
     let rhs, rhs_typ = Pulse.Checker.Pure.instantiate_term_implicits g rhs (Some lhs_typ) true in
     let lhs = norm lhs in
@@ -304,7 +307,7 @@ let check_renaming
     })
 : T.Tac st_term
 = let Tm_ProofHintWithBinders ht = st.term in
-  let { hint_type=RENAME { pairs; goal; tac_opt }; binders=bs; t=body } = ht in
+  let { hint_type=RENAME { pairs; goal; tac_opt; elaborated }; binders=bs; t=body } = ht in
   match bs, goal with
   | _::_, None ->
    //if there are binders, we must have a goal
@@ -324,7 +327,7 @@ let check_renaming
 
   | [], None ->
     // if there is no goal, take the goal to be the full current pre
-    let lhs, rhs = rewrite_all (T.unseal st.source) g pairs pre tac_opt in
+    let lhs, rhs = rewrite_all (T.unseal st.source) g pairs pre pre elaborated tac_opt in
     let t = { st with term = Tm_Rewrite { t1 = lhs; t2 = rhs; tac_opt; elaborated = true };
                       source = Sealed.seal false; } in
     { st with
@@ -334,7 +337,7 @@ let check_renaming
 
   | [], Some goal -> (
       let goal, _ = PC.instantiate_term_implicits g goal None false in
-      let lhs, rhs = rewrite_all (T.unseal st.source) g pairs goal tac_opt in
+      let lhs, rhs = rewrite_all (T.unseal st.source) g pairs goal pre elaborated tac_opt in
       let t = { st with term = Tm_Rewrite { t1 = lhs; t2 = rhs; tac_opt; elaborated = true };
                         source = Sealed.seal false; } in
       { st with term = Tm_Bind { binder = as_binder tm_unit; head = t; body };

src/checker/Pulse.Checker.If.fst

@@ -77,7 +77,7 @@ let check
       let t =
         mk_term (Tm_ProofHintWithBinders {
           binders = [];
-          hint_type = RENAME { pairs = [(b, eq_v)]; goal=None; tac_opt=None; };
+          hint_type = RENAME { pairs = [(b, eq_v)]; goal=None; tac_opt=None; elaborated=true };
           t = br;
         }) br.range
       in

src/checker/Pulse.Checker.Match.fst

@@ -286,7 +286,8 @@ let check_branch
                    binders = [];
                    hint_type = RENAME { pairs = [(sc, elab_p_tm)];
                                         goal = None;
-                                        tac_opt = Some Pulse.Reflection.Util.match_rewrite_tac_tm; };
+                                        tac_opt = Some Pulse.Reflection.Util.match_rewrite_tac_tm;
+                                        elaborated = true };
                    t = e; })
                 e.range
       in

src/checker/Pulse.Syntax.Base.fst

@@ -150,10 +150,11 @@ let eq_hint_type (ht1 ht2:proof_hint_type)
     | UNFOLD { names=ns1; p=p1}, UNFOLD { names=ns2; p=p2 } ->
       eq_opt (eq_list (fun n1 n2 -> n1 = n2)) ns1 ns2 &&
       eq_tm p1 p2
-    | RENAME { pairs=ps1; goal=p1; tac_opt=t1 }, RENAME { pairs=ps2; goal=p2; tac_opt=t2 } ->
+    | RENAME { pairs=ps1; goal=p1; tac_opt=t1; elaborated=e1 }, RENAME { pairs=ps2; goal=p2; tac_opt=t2; elaborated=e2 } ->
       eq_list (fun (x1, y1) (x2, y2) -> eq_tm x1 x2 && eq_tm y1 y2) ps1 ps2 &&
       eq_opt eq_tm p1 p2 &&
-      eq_tm_opt t1 t2
+      eq_tm_opt t1 t2 &&
+      e1 = e2
     | REWRITE { t1; t2; tac_opt; elaborated=e1 }, REWRITE { t1=s1; t2=s2; tac_opt=tac_opt2; elaborated=e2 } ->
       eq_tm t1 s1 &&
       eq_tm t2 s2 &&

src/checker/Pulse.Syntax.Base.fsti

@@ -179,6 +179,7 @@ type proof_hint_type =
       pairs:list (term & term);
       goal: option term;
       tac_opt : option term; (* optional tactic *)
+      elaborated: bool; (* internally created by the checker, don't purify *)
     }
   | REWRITE {
       t1:slprop;

src/checker/Pulse.Syntax.Builder.fst

@@ -60,7 +60,7 @@ let tm_assert_with_binders bs p t = Tm_ProofHintWithBinders { hint_type=ASSERT {
 let mk_assert_hint_type p = ASSERT { p; elaborated=false }
 let mk_unfold_hint_type names p = UNFOLD { names; p }
 let mk_fold_hint_type names p = FOLD { names; p }
-let mk_rename_hint_type pairs goal tac_opt = RENAME { pairs; goal; tac_opt=map_opt tac_opt thunk }
+let mk_rename_hint_type pairs goal tac_opt = RENAME { pairs; goal; tac_opt=map_opt tac_opt thunk; elaborated=false }
 let mk_rewrite_hint_type t1 t2 tac_opt = REWRITE { t1; t2; tac_opt=map_opt tac_opt thunk; elaborated=false }
 let mk_fn_defn id isrec us bs comp meas body : decl' = FnDefn { id; isrec; us; bs; comp; meas; body }
 let mk_fn_decl id us bs comp : decl' = FnDecl { id; us; bs; comp; }

src/checker/Pulse.Syntax.Naming.fsti

@@ -470,10 +470,11 @@ let subst_proof_hint (ht:proof_hint_type) (ss:subst)
     | ASSERT { p; elaborated } -> ASSERT { p=subst_term p ss; elaborated }
     | UNFOLD { names; p } -> UNFOLD {names; p=subst_term p ss}
     | FOLD { names; p } -> FOLD { names; p=subst_term p ss }
-    | RENAME { pairs; goal; tac_opt } ->
+    | RENAME { pairs; goal; tac_opt; elaborated } ->
       RENAME { pairs=subst_term_pairs pairs ss;
                goal=subst_term_opt goal ss;
                tac_opt=subst_term_opt tac_opt ss;
+               elaborated;
              }
     | REWRITE { t1; t2; tac_opt; elaborated } ->
       REWRITE { t1=subst_term t1 ss;

src/ml/PulseSyntaxExtension_SyntaxWrapper.ml

@@ -125,7 +125,7 @@ let tm_abs (b:binder)
            (body:st_term)
            r
   : st_term 
-  = let asc = { annotated = c; elaborated2 = None } in
+  = let asc = { annotated = c; elaborated3 = None } in
     PSB.(with_range (tm_abs b q asc body) r)
 
 let tm_st (head:term) (args:st_term list) r : st_term =

test/ImpureSpec.fst

@@ -120,4 +120,11 @@ fn test13 ()
   let mut y = x;
   fold p13 (!y);
   unfold p13 (!y);
+}
+
+fn test14 ()
+{
+  let mut x = 42;
+  assert live x ** pure (!x == 42);
+  rewrite each !x as 42;
 }