PHL: make eqobs-in programmatically reusable (split parse/tactic)

src/ecParser.mly

@@ -3359,9 +3359,9 @@ eqobs_in_eqpost:
 
 eqobs_in:
 | pos=eqobs_in_pos? i=eqobs_in_eqinv p=eqobs_in_eqpost? {
-    { sim_pos  = pos;
-      sim_hint = i;
-      sim_eqs  = p; }
+    { psim_pos  = pos;
+      psim_hint = i;
+      psim_eqs  = p; }
 }
 
 pgoptionkw:

src/ecParsetree.ml

@@ -739,10 +739,10 @@ type conseq_contra =
 type conseq_ppterm = (conseq_contra * (conseq_info) option) gppterm
 
 (* -------------------------------------------------------------------- *)
-type sim_info = {
-  sim_pos  : pcodegap1 pair option;
-  sim_hint : (pgamepath option pair * pformula) list * pformula option;
-  sim_eqs  : pformula option
+type psim_info = {
+  psim_pos  : pcodegap1 pair option;
+  psim_hint : (pgamepath option pair * pformula) list * pformula option;
+  psim_eqs  : pformula option
 }
 
 (* -------------------------------------------------------------------- *)
@@ -823,7 +823,7 @@ type phltactic =
   | Pfel           of (pcodegap1 * fel_info)
   | Phoare
   | Pprbounded
-  | Psim           of crushmode option* sim_info
+  | Psim           of crushmode option* psim_info
   | Ptrans_stmt    of trans_info
   | Prw_equiv      of rw_eqv_info
   | Psymmetry

src/phl/ecPhlEqobs.ml

@@ -1,6 +1,9 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
+open EcPath
+open EcParsetree
 open EcAst
+open EcMatching.Position
 open EcTypes
 open EcModules
 open EcFol
@@ -13,6 +16,16 @@ open EcLowPhlGoal
 
 module TTC = EcProofTyping
 
+(* -------------------------------------------------------------------- *)
+type sim_info = {
+  sim_pos  : codegap1 pair option;
+  sim_hint : (xpath option * xpath option * EcPV.Mpv2.t) list * ts_inv option;
+  sim_eqs  : EcPV.Mpv2.t option;
+}
+
+let empty_sim_info : sim_info =
+  { sim_pos = None; sim_hint = ([], None); sim_eqs = None; }
+
 (* -------------------------------------------------------------------- *)
 let extend_body fsig body =
   let arg = pv_arg in
@@ -397,7 +410,7 @@ let t_eqobs_inS_r sim eqo tc =
     tc_error !!tc "cannot apply sim";
 
   let sg = List.map (mk_inv_spec env inv) sim.needed_spec in
-  let concl = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr pre in
+  let concl = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr pre in 
 
   FApi.xmutate1 tc `EqobsIn (sg @ [concl])
 
@@ -423,54 +436,62 @@ let t_eqobs_inF_r sim eqo tc =
 let t_eqobs_inF = FApi.t_low2 "eqobs-in" t_eqobs_inF_r
 
 (* -------------------------------------------------------------------- *)
-let process_eqs env tc f =
-   try
-      Mpv2.of_form env f
-   with Not_found ->
-     tc_error_lazy !!tc (fun fmt ->
-       let ppe = EcPrinting.PPEnv.ofenv env in
-       Format.fprintf fmt
-         "cannot recognize %a as a set of equalities"
-         (EcPrinting.pp_form ppe) f.inv)
+let process_eqs (pe : proofenv) (env : env) (f : ts_inv) =
+  try
+    Mpv2.of_form env f
+  with Not_found ->
+    tc_error_lazy pe (fun fmt ->
+      let ppe = EcPrinting.PPEnv.ofenv env in
+      Format.fprintf fmt
+        "cannot recognize %a as a set of equalities"
+        (EcPrinting.pp_form ppe) f.inv)
 
 (* -------------------------------------------------------------------- *)
-let process_hint ml mr tc hyps (feqs, inv) =
+let process_hint ml mr (pe : proofenv) (hyps : LDecl.hyps) (feqs, inv : _ * _) =
   let env = LDecl.toenv hyps in
   let ienv = LDecl.push_active_ts (EcMemory.abstract ml) (EcMemory.abstract mr) hyps in
-  let doinv pf = {ml;mr;inv=TTC.pf_process_form !!tc ienv tbool pf} in
-  let doeq pf = process_eqs env tc (doinv pf) in
+  let doinv pf = {ml;mr;inv=TTC.pf_process_form pe ienv tbool pf} in 
+  let doeq pf = process_eqs pe env (doinv pf) in
   let dof g = omap (EcTyping.trans_gamepath env) g in
   let geqs =
-    List.map (fun ((f1,f2),geq) -> dof f1, dof f2, doeq geq)
+    List.map
+      (fun ((f1, f2), geq) -> dof f1, dof f2, doeq geq)
       feqs in
-  let ginv = odfl {ml;mr;inv=f_true} (omap doinv inv) in
+  let ginv = (omap doinv inv) in (* FIXME: check *) 
   geqs, ginv
 
 (* -------------------------------------------------------------------- *)
-let process_eqobs_inS info tc =
-  let env, hyps, _ = FApi.tc1_eflat tc in
+let pre_eqobs (cm : crushmode) (tc : tcenv1) =
+  let dt, ts = EcHiGoal.process_crushmode cm in
+  EcPhlConseq.t_conseqauto ~delta:dt ?tsolve:ts tc
+
+(* -------------------------------------------------------------------- *)
+let t_eqobs_inS_ (info : sim_info) (tc : tcenv1) =
+  let env, _, _ = FApi.tc1_eflat tc in
   let es = tc1_as_equivS tc in
-  let ml, mr = fst es.es_ml, fst es.es_mr in
-  let spec, inv = process_hint ml mr tc hyps info.EcParsetree.sim_hint in
+  let spec, inv = info.sim_hint in
+
+  let inv = match inv with
+  | Some inv -> inv
+  | None -> let ml, mr = fst es.es_ml, fst es.es_mr in
+  {ml;mr;inv=f_true}
+  in
+
   let eqo =
-    match info.EcParsetree.sim_eqs with
-    | Some pf ->
-      process_eqs env tc (TTC.tc1_process_prhl_formula tc pf)
-    | None ->
-      try Mpv2.needed_eq env (es_po es)
-      with Not_found -> tc_error !!tc "cannot infer the set of equalities" in
-  let post = Mpv2.to_form_ts_inv eqo inv in
+    match info.sim_eqs with Some eqo -> eqo | None ->
+      try  Mpv2.needed_eq env (es_po es)
+      with _ -> tc_error !!tc "cannot infer the set of equalities" in
+
   let sim = init_sim env spec inv in
+  let post = Mpv2.to_form_ts_inv eqo inv in
+
   let t_main tc =
-    match info.EcParsetree.sim_pos with
+    match info.sim_pos with
     | None ->
       FApi.t_last
         (FApi.t_try (FApi.t_seq EcPhlSkip.t_skip t_trivial))
         (t_eqobs_inS sim eqo tc)
     | Some(p1,p2) ->
-      (* sim positions are gaps: sim applies to instructions after the gap *)
-      let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in
-      let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in
       let _,sl2 = s_split env p1 es.es_sl in
       let _,sr2 = s_split env p2 es.es_sr in
       let _, eqi =
@@ -485,49 +506,110 @@ let process_eqobs_inS info tc =
       ]) tc in
   (EcPhlConseq.t_equivS_conseq (es_pr es) post @+
     [t_trivial;
-     t_trivial;
-     t_main]) tc
+      t_trivial;
+      t_main]) tc
+
+(* -------------------------------------------------------------------- *)
+let t_eqobs_inS (cm : crushmode option) (info : sim_info) (tc : tcenv1) =
+  FApi.t_last (t_eqobs_inS_ info) ((omap pre_eqobs cm |> odfl t_id) tc)
 
 (* -------------------------------------------------------------------- *)
-let process_eqobs_inF info tc =
-  if info.EcParsetree.sim_pos <> None then
-    tc_error !!tc "no positions excepted";
+let process_eqobs_inS (cm : crushmode option) (info : psim_info) (tc : tcenv1) =
   let env, hyps, _ = FApi.tc1_eflat tc in
+  let es = tc1_as_equivS tc in
+  let ml, mr = fst es.es_ml, fst es.es_mr in
+  let sim_hint = process_hint ml mr !!tc hyps info.psim_hint in
+  let sim_eqs =
+    let process pf =
+      process_eqs !!tc env (TTC.tc1_process_prhl_formula tc pf)
+    in Option.map process info.psim_eqs in
+  let sim_pos =
+    info.psim_pos |>
+      Option.map (fun (p1, p2) ->
+        let p1 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left , p1) in
+        let p2 = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Right, p2) in
+        (p1, p2)
+      )
+  in
+
+  let info = { sim_pos; sim_hint; sim_eqs; } in
+
+  t_eqobs_inS cm info tc
+
+(* -------------------------------------------------------------------- *)
+let t_eqobs_inF_ (info : sim_info) (tc : tcenv1) =
+  assert (Option.is_none info.sim_pos);  
+
+  let env, _, _ = FApi.tc1_eflat tc in
   let ef = tc1_as_equivF tc in
-  let ml, mr = ef.ef_ml, ef.ef_mr in
-  let spec, inv = process_hint ml mr tc hyps info.EcParsetree.sim_hint in
   let fl = ef.ef_fl and fr = ef.ef_fr in
+
+  let spec, inv = info.sim_hint in
+
   let eqo =
-    match info.EcParsetree.sim_eqs with
-    | Some pf ->
-      let _,(mle,mre) = Fun.equivF_memenv ml mr fl fr env in
-      let hyps = LDecl.push_active_ts mle mre hyps in
-      process_eqs env tc {ml; mr; inv=TTC.pf_process_form !!tc hyps tbool pf}
-    | None ->
+    match info.sim_eqs with Some eqo -> eqo | None ->
       try Mpv2.needed_eq env (ef_po ef)
       with _ -> tc_error !!tc "cannot infer the set of equalities" in
+
   let eqo = Mpv2.remove env pv_res pv_res eqo in
+
+  let inv = match inv with
+  | Some inv -> inv
+  | None -> let ml, mr = ef.ef_ml, ef.ef_mr in
+    {ml;mr;inv=f_true}
+  in
+
   let sim = init_sim env spec inv in
   let _, eqi =
     try f_eqobs_in fl fr sim eqo
     with EqObsInError -> tc_error !!tc "not able to process" in
   let ef' = destr_equivF (mk_inv_spec2 env inv (fl, fr, eqi, eqo)) in
+
   (EcPhlConseq.t_equivF_conseq (ef_pr ef') (ef_po ef') @+ [
     t_trivial;
     t_trivial;
      t_eqobs_inF sim eqo]) tc
 
 (* -------------------------------------------------------------------- *)
-let process_eqobs_in cm info tc =
-  let prett cm tc =
-    let dt, ts = EcHiGoal.process_crushmode cm in
-      EcPhlConseq.t_conseqauto ~delta:dt ?tsolve:ts tc in
-  let tt tc =
-    let concl = FApi.tc1_goal tc in
-    match concl.f_node with
-    | FequivF _ -> process_eqobs_inF info tc
-    | FequivS _ -> process_eqobs_inS info tc
-    | _ -> tc_error_noXhl ~kinds:[`Equiv `Any] !!tc
-  in
+let t_eqobs_inF (cm : crushmode option) (info : sim_info) (tc : tcenv1) =
+  FApi.t_last (t_eqobs_inF_ info) ((omap pre_eqobs cm |> odfl t_id) tc)
+
+(* -------------------------------------------------------------------- *)
+let process_eqobs_inF (cm : crushmode option) (info : psim_info) (tc : tcenv1) =
+  if Option.is_some info.psim_pos then
+    tc_error !!tc "no positions excepted";
 
-  FApi.t_last tt ((omap prett cm |> odfl t_id) tc)
+  let env, hyps, _ = FApi.tc1_eflat tc in
+  let ef = tc1_as_equivF tc in
+  let ml, mr = ef.ef_ml, ef.ef_mr in
+  let sim_hint = process_hint ml mr !!tc hyps info.psim_hint in
+  let fl = ef.ef_fl and fr = ef.ef_fr in
+  let sim_eqs =
+    let process pf =
+      let _,(mle,mre) = Fun.equivF_memenv ml mr fl fr env in
+      let hyps = LDecl.push_active_ts mle mre hyps in
+      process_eqs !!tc env {ml; mr; inv=TTC.pf_process_form !!tc hyps tbool pf} 
+    in Option.map process info.psim_eqs in
+
+  let info = { sim_pos = None; sim_hint; sim_eqs; } in
+
+  t_eqobs_inF cm info tc
+
+(* -------------------------------------------------------------------- *)
+let process_eqobs_in (cm : crushmode option) (info : psim_info) (tc : tcenv1) =
+  let concl = FApi.tc1_goal tc in
+  match concl.f_node with
+  | FequivF _ -> process_eqobs_inF cm info tc
+  | FequivS _ -> process_eqobs_inS cm info tc
+  | _ -> tc_error_noXhl ~kinds:[`Equiv `Any] !!tc
+
+(* -------------------------------------------------------------------- *)
+let t_eqobs_in_r (cm : crushmode option) (info : sim_info) (tc : tcenv1) =
+  let concl = FApi.tc1_goal tc in
+  match concl.f_node with
+  | FequivF _ -> t_eqobs_inF cm info tc
+  | FequivS _ -> t_eqobs_inS cm info tc
+  | _ -> tc_error_noXhl ~kinds:[`Equiv `Any] !!tc
+
+(* -------------------------------------------------------------------- *)
+let t_eqobs_in = FApi.t_low2 "eqobs-in" t_eqobs_in_r

src/phl/ecPhlEqobs.mli

@@ -1,7 +1,20 @@
 (* -------------------------------------------------------------------- *)
-
+open EcUtils
+open EcPath
 open EcParsetree
+open EcAst
+open EcMatching.Position
 open EcCoreGoal.FApi
 
 (* -------------------------------------------------------------------- *)
-val process_eqobs_in : crushmode option -> sim_info -> backward
+type sim_info = {
+  sim_pos  : codegap1 pair option;
+  sim_hint : (xpath option * xpath option * EcPV.Mpv2.t) list * ts_inv option;
+  sim_eqs  : EcPV.Mpv2.t option;
+}
+
+val empty_sim_info : sim_info
+
+(* -------------------------------------------------------------------- *)
+val t_eqobs_in : crushmode option -> sim_info -> backward
+val process_eqobs_in : crushmode option -> psim_info -> backward

src/phl/ecPhlOutline.ml

@@ -12,7 +12,7 @@ open EcLowPhlGoal
 let t_auto_equiv_sim =
   t_seqs [
     EcPhlInline.process_inline (`ByName (None, None, ([], None)));
-    EcPhlEqobs.process_eqobs_in None {sim_pos = None; sim_hint = ([], None); sim_eqs = None};
+    EcPhlEqobs.process_eqobs_in None {psim_pos = None; psim_hint = ([], None); psim_eqs = None};
     EcPhlAuto.t_auto;
     EcLowGoal.t_crush;
     EcHiGoal.process_done;