Merge pull request #482 from FStarLang/gebner_purify_rw

Support purification inside rewrite and unfold.

Author: gebner

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -19,6 +19,7 @@ module Pulse.Checker.AssertWithBinders
 open Pulse.Syntax
 open Pulse.Typing
 open Pulse.Checker.Base
+open Pulse.Checker.ImpureSpec
 open Pulse.Elaborate.Pure
 open Pulse.Typing.Env
 
@@ -263,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. *)
@@ -274,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
@@ -303,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
@@ -323,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
@@ -333,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 };
@@ -486,6 +490,7 @@ let check
 
     check_unfoldable g v;
 
+    let v_opened = purify_term g { ctxt_now = pre; ctxt_old = None } v_opened in
     let v_opened, t_rem = PC.instantiate_term_implicits (push_env g uvs) v_opened None false in
 
     let uvs, v_opened =

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.ImpureSpec.fst

@@ -30,7 +30,6 @@ open Pulse.Readback
 open Pulse.Syntax.Naming
 open Pulse.Reflection.Util
 open Pulse.PP
-open Pulse.Checker.Prover.Substs
 open Pulse.Show
 
 let old_lid = Pulse.Reflection.Util.mk_pulse_lib_core_lid "old"
@@ -433,6 +432,11 @@ let run_elim_ctxt (g: env) (ctxt: ctxt) =
       g, ys, Some old in
   g, xs @ ys, { ctxt_old = old; ctxt_now = now }
 
+let purify_term (g: env) (ctxt: ctxt) (t: term) : T.Tac term =
+  let g', xs, ctxt = run_elim_ctxt g ctxt in
+  let _, t = symb_eval_subterms g ctxt t in
+  t
+
 let purify_spec (g: env) (ctxt: ctxt) (t0: slprop) : T.Tac slprop =
   let t = t0 in
   let g', xs, ctxt = run_elim_ctxt g ctxt in

src/checker/Pulse.Checker.ImpureSpec.fsti

@@ -25,6 +25,8 @@ noeq type ctxt = {
   ctxt_old: option slprop;
 }
 
+val purify_term (g: env) (ctxt: ctxt) (t: term) : T.Tac term
+
 val purify_spec (g: env) (ctxt: ctxt) (t: slprop) :
   T.Tac slprop
 

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.Checker.Rewrite.fst

@@ -21,6 +21,7 @@ open Pulse.Typing
 open Pulse.Checker.Pure
 open Pulse.Checker.Base
 open Pulse.Checker.Prover
+open Pulse.Checker.ImpureSpec
 open Pulse.PP
 module T = FStar.Tactics.V2
 module R = FStar.Reflection.V2
@@ -118,6 +119,12 @@ let check
 
   let g = push_context "check_rewrite" t.range g in
   let Tm_Rewrite {t1=p; t2=q; tac_opt; elaborated} = t.term in
+  let p, q =
+    if elaborated then
+      p, q
+    else
+      let ctxt = { ctxt_now = pre; ctxt_old = None } in
+      purify_term g ctxt p, purify_term g ctxt q in
   let (| p, p_typing |), (| q, q_typing |) =
     check_slprop g p, check_slprop g q 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;