Merge pull request #395 from FStarLang/_nik_slprop_equiv_profiling

Profiling and revising slprop_equiv checking for fold and unfold

Author: nikswamy

lib/common/Pulse.Lib.Core.fsti

@@ -591,6 +591,22 @@ than SMT. This tactic is also used by the checker when elaborating fold/unfold.
 let slprop_equiv_norm (_:unit) : T.Tac unit =
     T.mapply (`slprop_equiv_refl)
 
+
+let slprop_equiv_unfold (head_sym:string) (_:unit) : T.Tac unit =
+    T.mapply (`slprop_equiv_trans);
+    T.norm [hnf; zeta; delta_only [head_sym]];
+    T.norm [hnf; iota; primops];
+    T.mapply (`slprop_equiv_refl);
+    T.mapply (`slprop_equiv_refl)
+
+let slprop_equiv_fold (head_sym:string) (_:unit) : T.Tac unit =
+    T.mapply (`slprop_equiv_trans);
+    T.flip();
+    T.norm [hnf; zeta; delta_only [head_sym]];
+    T.norm [hnf; iota; primops];
+    T.mapply (`slprop_equiv_refl);
+    T.mapply (`slprop_equiv_refl)
+    
 let slprop_equiv_ext' (p1 p2:slprop) (_: squash (p1 == p2))
   : slprop_equiv p1 p2 = slprop_equiv_refl p1
 

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -142,14 +142,15 @@ let def_of_fv (g:T.env) (fv:R.fv)
       | R.Sg_Inductive _nm _univs params typ _ -> None
 
 let unfold_head (g : env) (t:term)
-  : T.Tac term
+  : T.Tac (term & string)
   = let rg = elab_env g in
     match T.hua t with
     | Some (fv, u, args) -> (
       (* zeta to allow unfolding recursive definitions. Should be only once
       unless it appears on the head of its own definition.. which should be impossible? *)
-      let t = T.norm_term_env rg [hnf; zeta; delta_only [T.implode_qn (T.inspect_fv fv)]] t in
-      t
+      let head_symbol = T.implode_qn (T.inspect_fv fv) in
+      let t = T.norm_term_env rg [hnf; zeta; delta_only [head_symbol]] t in
+      t, head_symbol
       (* Something like this would be better, but we need to instantiate
          the universes, and we don't have a good way to do that yet.
       match def_of_fv rg fv with
@@ -166,16 +167,22 @@ let unfold_head (g : env) (t:term)
       fail g (Some (RU.range_of_term t))
         (Printf.sprintf "Cannot unfold %s, the head is not an fvar" (T.term_to_string t))
 
-let unfold_defs (g:env) (defs:option (list string)) (t:term)
-  : T.Tac term
-  = let t = unfold_head g t in
+let unfold_defs' (g:env) (defs:option (list string)) (t:term)
+  : T.Tac (term & string)
+  = let t, head_sym = unfold_head g t in
     let t =
       match defs with
       | None -> t
       | Some defs -> unfold_all g defs t
     in
     let t = T.norm_term_env (elab_env g) [hnf; iota; primops] t in
-    t
+    t, head_sym
+
+let unfold_defs (g:env) (defs:option (list string)) (t:term)
+: T.Tac (term & string)
+= RU.profile (fun () -> unfold_defs' g defs t) 
+             (T.moduleof (fstar_env g))
+            "Pulse.Checker.Unfold"
 
 let check_unfoldable g (v:term) : T.Tac unit =
   match inspect_term v with
@@ -445,8 +452,8 @@ let check
     (| x, x_ty, pre'', g2, k_elab_trans k_frame k |)
 
 
-  | UNFOLD { names; p=v }
-  | FOLD { names; p=v } ->
+  | UNFOLD { p=v }
+  | FOLD { p=v } ->
 
     let (| uvs, v_opened, body_opened |) =
       let bs = infer_binder_types g bs v in
@@ -461,14 +468,15 @@ let check
         add_rem_uvs (push_env g uvs) t_rem (mk_env (fstar_env g)) v_opened in
       push_env uvs uvs_rem, v_opened in
 
-    let lhs, rhs =
+    let lhs, rhs, tac =
       match hint_type with      
       | UNFOLD _ ->
-        v_opened,
-        unfold_defs (push_env g uvs) None v_opened
+        let rhs, head_sym = unfold_defs (push_env g uvs) None v_opened in
+        v_opened, rhs, Pulse.Reflection.Util.slprop_equiv_unfold_tm head_sym
       | FOLD { names=ns } -> 
-        unfold_defs (push_env g uvs) ns v_opened,
-        v_opened in
+        let lhs, head_sym = unfold_defs (push_env g uvs) ns v_opened in
+        lhs, v_opened, Pulse.Reflection.Util.slprop_equiv_fold_tm head_sym
+    in
 
     let uvs_bs = uvs |> bindings_with_ppname |> L.rev in
     let uvs_closing = uvs_bs |> closing in
@@ -491,8 +499,7 @@ let check
       ] in
       info_doc_env g (Some st.range) msg
     end;
-
-    let rw = mk_term (Tm_Rewrite { t1 = lhs; t2 = rhs; tac_opt = Some Pulse.Reflection.Util.slprop_equiv_norm_tm }) st.range in
+    let rw = mk_term (Tm_Rewrite { t1 = lhs; t2 = rhs; tac_opt = Some tac }) st.range in
     let rw = { rw with effect_tag = as_effect_hint STT_Ghost } in
 
     let st = mk_term (Tm_Bind { binder = as_binder (wr (`unit) st.range); head = rw; body }) st.range in

src/checker/Pulse.Checker.Rewrite.fst

@@ -129,7 +129,9 @@ let check
     | None ->
       check_slprop_equiv t.range g p q
     | Some tac ->
-      check_slprop_equiv_tac t.range g p q tac
+      RU.profile (fun () -> check_slprop_equiv_tac t.range g p q tac)
+                 (T.moduleof (fstar_env g))
+                 "Pulse.Checker.Rewrite.check_slprop_equiv_tac"
   in
 	let d = T_Rewrite _ p q p_typing equiv_p_q in
 	prove_post_hint (try_frame_pre false pre_typing (match_comp_res_with_post_hint d post_hint) res_ppname) post_hint t.range

src/checker/Pulse.Reflection.Util.fst

@@ -62,6 +62,16 @@ let seq_create_lid = ["FStar"; "Seq"; "Base"; "create"]
 let tot_lid = ["Prims"; "Tot"]
 
 let slprop_equiv_norm_tm = R.pack_ln (R.Tv_FVar (R.pack_fv (mk_pulse_lib_core_lid "slprop_equiv_norm")))
+let slprop_equiv_fold_tm (s:string) = 
+  let head = R.pack_ln (R.Tv_FVar (R.pack_fv (mk_pulse_lib_core_lid "slprop_equiv_fold"))) in
+  let s = R.pack_ln (R.Tv_Const (R.C_String s)) in
+  let t = R.pack_ln (R.Tv_App head (s, R.Q_Explicit)) in
+  t
+let slprop_equiv_unfold_tm (s:string) =
+  let head = R.pack_ln (R.Tv_FVar (R.pack_fv (mk_pulse_lib_core_lid "slprop_equiv_unfold"))) in
+  let s = R.pack_ln (R.Tv_Const (R.C_String s)) in
+  let t = R.pack_ln (R.Tv_App head (s, R.Q_Explicit)) in
+  t
 let match_rewrite_tac_tm = R.pack_ln (R.Tv_FVar (R.pack_fv (mk_pulse_lib_core_lid "match_rewrite_tac")))
 
 (* The "plicities" *)

src/checker/Pulse.RuntimeUtils.fsti

@@ -81,11 +81,15 @@ val norm_well_typed_term
       Ghost.erased (RT.related g t RT.R_Eq t')
     )
 val add_attribute (x:T.sigelt) (_:R.term) : (y:T.sigelt { x == y })
-val get_attributes (x:T.sigelt) : T.Tac (list R.term)
+val get_attributes (x:T.sigelt) : T.Tac (list R.term) 
+
 val add_noextract_qual (x:T.sigelt) : (y:T.sigelt { x == y })
 
 val must_erase_for_extraction (g:env) (ty:T.term) : bool
 
 val magic : #a: Type -> unit -> GTot a
 (* magic with a string, to at least report an error message if it is hit at runtime *)
 val magic_s: #a: Type -> string -> Tot a
+
+val profile (f:(unit -> Tac 'b)) (module_name:name) (component_name:string)
+: Tac 'b

src/ml/Pulse_RuntimeUtils.ml

@@ -213,3 +213,9 @@ let must_erase_for_extraction (g:FStarC_Reflection_Types.env) (ty:FStarC_Syntax_
   FStarC_TypeChecker_Util.must_erase_for_extraction g ty
 
 let magic_s s = failwith ("Cannot execute magic: " ^ s)
+
+let profile (f: unit -> 'b utac) (module_name:string list) (component_name:string) 
+: 'b utac
+= fun ps ->
+    let name = String.concat "." module_name in
+    FStarC_Profiling.profile (fun () -> f () ps) (Some name) component_name