Simple tactics in proof-terms.

Simple tactics (//, //#, /#) can now been used in proof-terms.

Author: strub

src/ecCoreGoal.ml

@@ -48,12 +48,14 @@ type proofterm =
   | PTQuant of binding * proofterm
 
 and pt_head =
-| PTCut    of EcFol.form
+| PTCut    of EcFol.form * cutsolve option
 | PTHandle of handle
 | PTLocal  of EcIdent.t
 | PTGlobal of EcPath.path * (ty list)
 | PTTerm   of proofterm
 
+and cutsolve = [`Done | `Smt | `DoneSmt]
+
 and pt_arg =
 | PAFormula of EcFol.form
 | PAMemory  of EcMemory.memory
@@ -88,8 +90,8 @@ let ptlocal ?(args = []) x =
 let pthandle ?(args = []) x =
   PTApply { pt_head = PTHandle x; pt_args = args; }
 
-let ptcut ?(args = []) f =
-  PTApply { pt_head = PTCut f; pt_args = args; }
+let ptcut ?(args = []) ?(cutsolve : cutsolve option) f =
+  PTApply { pt_head = PTCut (f, cutsolve); pt_args = args; }
 
 (* -------------------------------------------------------------------- *)
 let paglobal ?args ~tys p =

src/ecCoreGoal.mli

@@ -50,12 +50,14 @@ type proofterm =
   | PTQuant of binding * proofterm
 
 and pt_head =
-| PTCut    of EcFol.form
+| PTCut    of EcFol.form * cutsolve option
 | PTHandle of handle
 | PTLocal  of EcIdent.t
 | PTGlobal of EcPath.path * (ty list)
 | PTTerm   of proofterm
 
+and cutsolve = [`Done | `Smt | `DoneSmt]
+
 and pt_arg =
 | PAFormula of EcFol.form
 | PAMemory  of EcMemory.memory
@@ -88,7 +90,7 @@ val pahandle  : ?args:pt_arg list -> handle -> pt_arg
 val ptglobal  : ?args:pt_arg list -> tys:ty list -> EcPath.path -> proofterm
 val ptlocal   : ?args:pt_arg list -> EcIdent.t -> proofterm
 val pthandle  : ?args:pt_arg list -> handle -> proofterm
-val ptcut     : ?args:pt_arg list -> EcFol.form -> proofterm
+val ptcut     : ?args:pt_arg list -> ?cutsolve:cutsolve -> EcFol.form -> proofterm
 
 (* -------------------------------------------------------------------- *)
 val ptapply : proofterm -> pt_arg list -> proofterm

src/ecHiGoal.ml

@@ -28,7 +28,7 @@ module LG  = EcCoreLib.CI_Logic
 
 (* -------------------------------------------------------------------- *)
 type ttenv = {
-  tt_provers   : EcParsetree.pprover_infos -> EcProvers.prover_infos;
+  tt_provers   : EcParsetree.pprover_infos option -> EcProvers.prover_infos;
   tt_smtmode   : [`Admit | `Strict | `Sloppy | `Report];
   tt_implicits : bool;
   tt_oldip     : bool;
@@ -150,7 +150,7 @@ let process_smt ?loc (ttenv : ttenv) pi (tc : tcenv1) =
 (* -------------------------------------------------------------------- *)
 
 let process_coq ~loc ~name (ttenv : ttenv) coqmode  pi (tc : tcenv1) =
-  let pi = ttenv.tt_provers pi in
+  let pi = ttenv.tt_provers (Some pi) in
 
   match ttenv.tt_smtmode with
   | `Admit ->
@@ -841,7 +841,7 @@ let process_rewrite1_r ttenv ?target ri tc =
             ptenv.pte_ev := MEV.add x `Form !(ptenv.pte_ev)
           );
 
-          let pt = PTApply { pt_head = PTCut f; pt_args = []; } in
+          let pt = PTApply { pt_head = PTCut (f, None); pt_args = []; } in
           let pt = { ptev_env = ptenv; ptev_pt = pt; ptev_ax = f; } in
 
           process_rewrite1_core ~mode ?target (theside, prw, o) pt tc
@@ -872,10 +872,10 @@ let process_rewrite1_r ttenv ?target ri tc =
   end
 
   | RWSmt (false, info) ->
-     process_smt ~loc:ri.pl_loc ttenv info tc
+     process_smt ~loc:ri.pl_loc ttenv (Some info) tc
 
   | RWSmt (true, info) ->
-     t_or process_done (process_smt ~loc:ri.pl_loc ttenv info) tc
+     t_or process_done (process_smt ~loc:ri.pl_loc ttenv (Some info)) tc
 
   | RWApp fp -> begin
       let implicits = ttenv.tt_implicits in
@@ -1404,10 +1404,10 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
       | None -> process_trivial
     in t tc
 
-  and intro1_smt (_ : ST.state) ((dn, pi) : _ * pprover_infos) (tc : tcenv1) =
+  and intro1_smt (_ : ST.state) (dn : bool) (pi : pprover_infos) (tc : tcenv1) =
     if dn then
-      t_or process_done (process_smt ttenv pi) tc
-    else process_smt ttenv pi tc
+      t_or process_done (process_smt ttenv (Some pi)) tc
+    else process_smt ttenv (Some pi) tc
 
   and intro1_simplify (_ : ST.state) logic tc =
     t_simplify_lg ~delta:`IfApplied (ttenv, logic) tc
@@ -1575,8 +1575,8 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
         | `Done b ->
             (nointro, rl (t_onall (intro1_done st b)) gs)
 
-        | `Smt pi ->
-            (nointro, rl (t_onall (intro1_smt st pi)) gs)
+        | `Smt (b, pi) ->
+            (nointro, rl (t_onall (intro1_smt st b pi)) gs)
 
         | `Simpl b ->
             (nointro, rl (t_onall (intro1_simplify st b)) gs)
@@ -1938,6 +1938,9 @@ let process_cut ?(mode = `Have) engine ttenv ((ip, phi, t) : cut_t) tc =
 (* -------------------------------------------------------------------- *)
 type cutdef_t = intropattern * pcutdef
 
+let cutsolver (ttenv : ttenv) =
+  { smt = process_smt ttenv None; done_ = process_trivial; }
+
 let process_cutdef ttenv (ip, pt) (tc : tcenv1) =
   let pt = {
       fp_mode = `Implicit;
@@ -1953,7 +1956,7 @@ let process_cutdef ttenv (ip, pt) (tc : tcenv1) =
   let pt, ax = PT.concretize pt in
 
   FApi.t_sub
-    [EcLowGoal.t_apply pt; process_intros_1 ttenv ip]
+    [EcLowGoal.t_apply ~cutsolver:(cutsolver ttenv) pt; process_intros_1 ttenv ip]
     (t_cut ax tc)
 
 (* -------------------------------------------------------------------- *)

src/ecHiGoal.mli

@@ -9,7 +9,7 @@ open EcProofTerm
 
 (* -------------------------------------------------------------------- *)
 type ttenv = {
-  tt_provers   : EcParsetree.pprover_infos -> EcProvers.prover_infos;
+  tt_provers   : EcParsetree.pprover_infos option -> EcProvers.prover_infos;
   tt_smtmode   : [`Admit | `Strict | `Sloppy | `Report];
   tt_implicits : bool;
   tt_oldip     : bool;
@@ -72,7 +72,7 @@ val process_genintros   : ?cf:bool -> ttenv -> introgenpattern list -> backward
 val process_generalize  : ?doeq:bool -> genpattern list -> backward
 val process_move        : ?doeq:bool -> ppterm list -> prevert -> backward
 val process_clear       : psymbol list -> backward
-val process_smt         : ?loc:EcLocation.t -> ttenv -> pprover_infos -> backward
+val process_smt         : ?loc:EcLocation.t -> ttenv -> pprover_infos option -> backward
 val process_coq         : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward
 val process_apply       : implicits:bool -> apply_t * prevert option -> backward
 val process_delta       : und_delta:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward

src/ecHiTacticals.ml

@@ -128,7 +128,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) =
     match unloc t with
     | Preflexivity        -> process_reflexivity
     | Passumption         -> process_assumption
-    | Psmt pi             -> process_smt ~loc:(loc t) ttenv pi
+    | Psmt pi             -> process_smt ~loc:(loc t) ttenv (Some pi)
     | Psplit              -> process_split
     | Pfield st           -> process_algebra `Solve `Field st
     | Pring st            -> process_algebra `Solve `Ring  st

src/ecLowGoal.ml

@@ -1,5 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
+open EcMaps
 open EcLocation
 open EcIdent
 open EcSymbols
@@ -99,17 +100,21 @@ module LowApply = struct
    in List.for_all h_eqs ld1.h_local
 
   (* ------------------------------------------------------------------ *)
-  let rec check_pthead (pt : pt_head) (tc : ckenv) =
+  let rec check_pthead (pt : pt_head) (subgoals : _) (tc : ckenv) =
     let hyps = hyps_of_ckenv tc in
 
     match pt with
-    | PTCut f -> begin
+    | PTCut (f, cutsolve) -> begin
         match tc with
-        | `Hyps ( _, _) -> (PTCut f, f)
+        | `Hyps ( _, _) -> (PTCut (f, None), f, subgoals) (* FIXME *)
         | `Tc   (tc, _) ->
             (* cut - create a dedicated subgoal *)
             let handle = RApi.newgoal tc ~hyps f in
-            (PTHandle handle, f)
+            let subgoals =
+              ofold
+                (fun cutsolve subgoals -> DMap.add handle cutsolve subgoals)
+                subgoals cutsolve
+            in (PTHandle handle, f, subgoals)
     end
 
     | PTHandle hd -> begin
@@ -121,38 +126,38 @@ module LowApply = struct
         (* proof reuse - fetch corresponding subgoal*)
         if not (sub_hyps subgoal.g_hyps (hyps_of_ckenv tc)) then
           raise InvalidProofTerm;
-        (pt, subgoal.g_concl)
+        (pt, subgoal.g_concl, subgoals)
     end
 
     | PTLocal x -> begin
         let hyps = hyps_of_ckenv tc in
-        try  (pt, LDecl.hyp_by_id x hyps)
+        try  (pt, LDecl.hyp_by_id x hyps, subgoals)
         with LDecl.LdeclError _ -> raise InvalidProofTerm
     end
 
     | PTGlobal (p, tys) ->
         (* FIXME: poor API ==> poor error recovery *)
         let env = LDecl.toenv (hyps_of_ckenv tc) in
-        (pt, EcEnv.Ax.instanciate p tys env)
+        (pt, EcEnv.Ax.instanciate p tys env, subgoals)
 
     | PTTerm pt ->
-      let pt, ax = check `Elim pt tc in
-      (PTTerm pt, ax)
+      let pt, ax, subgoals = check_ `Elim pt subgoals tc in
+      (PTTerm pt, ax, subgoals)
 
   (* ------------------------------------------------------------------ *)
-  and check (mode : [`Intro | `Elim]) (pt : proofterm) (tc : ckenv) =
+  and check_ (mode : [`Intro | `Elim]) (pt : proofterm) (subgoals : _) (tc : ckenv) =
     let hyps = hyps_of_ckenv tc in
     let env  = LDecl.toenv hyps in
 
-    let rec check_args (sbt, ax, nargs) args =
+    let rec check_args (sbt, ax, nargs) subgoals args =
       match args with
-      | [] -> (Fsubst.f_subst sbt ax, List.rev nargs)
+      | [] -> (Fsubst.f_subst sbt ax, List.rev nargs, subgoals)
 
       | arg :: args ->
-          let ((sbt, ax), narg) = check_arg (sbt, ax) arg in
-          check_args (sbt, ax, narg :: nargs) args
+          let ((sbt, ax), narg, subgoals) = check_arg (sbt, ax) subgoals arg in
+          check_args (sbt, ax, narg :: nargs) subgoals args
 
-    and check_arg (sbt, ax) arg =
+    and check_arg (sbt, ax) subgoals arg =
       let check_binder (x, xty) f =
         let xty = Fsubst.gty_subst sbt xty in
 
@@ -186,43 +191,53 @@ module LowApply = struct
                 | None       -> EcCoreGoal.ptcut f1
                 | Some subpt -> subpt
               in
-              let subpt, subax = check mode subpt tc in
+              let subpt, subax, subgoals = check_ mode subpt subgoals tc in
                 if not (EcReduction.is_conv hyps f1 subax) then
                   raise InvalidProofTerm;
-                ((sbt, f2), PASub (Some subpt))
+                ((sbt, f2), PASub (Some subpt), subgoals)
 
           | Some (`Forall (x, xty, f)), _ ->
-              (check_binder (x, xty) f, arg)
+              (check_binder (x, xty) f, arg, subgoals)
 
           | _, _ ->
               if Fsubst.is_subst_id sbt then
                 raise InvalidProofTerm;
-              check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) arg
+              check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) subgoals arg
       end
 
       | `Intro -> begin
           match TTC.destruct_exists hyps ax with
-          | Some (`Exists (x, xty, f)) -> (check_binder (x, xty) f, arg)
+          | Some (`Exists (x, xty, f)) ->
+              (check_binder (x, xty) f, arg, subgoals)
           | None ->
               if Fsubst.is_subst_id sbt then
                 raise InvalidProofTerm;
-              check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) arg
+              check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) subgoals arg
       end
     in
 
     match pt with
     | PTApply pt ->
-      let (nhd, ax) = check_pthead pt.pt_head tc in
-      let ax, nargs = check_args (Fsubst.f_subst_id, ax, []) pt.pt_args in
-      (PTApply { pt_head = nhd; pt_args = nargs }, ax)
+      let (nhd, ax, subgoals) = check_pthead pt.pt_head subgoals tc in
+      let ax, nargs, subgoals =
+        check_args (Fsubst.f_subst_id, ax, []) subgoals pt.pt_args in
+      (PTApply { pt_head = nhd; pt_args = nargs }, ax, subgoals)
 
     | PTQuant (bd, pt) -> begin
         match mode with
         | `Intro -> raise InvalidProofTerm
         | `Elim  ->
-          let pt, ax = check `Elim pt tc in
-          (PTQuant (bd, pt), f_forall [bd] ax)
+          let pt, ax, subgoals = check_ `Elim pt subgoals tc in
+          (PTQuant (bd, pt), f_forall [bd] ax, subgoals)
       end
+
+  let check_with_cutsolve (mode : [`Intro | `Elim]) (pt : proofterm) (tc : ckenv) =
+    check_ mode pt DMap.empty tc
+
+  let check (mode : [`Intro | `Elim]) (pt : proofterm) (tc : ckenv) =
+    let pt, f, subgoals = check_ mode pt DMap.empty tc in
+    assert (DMap.is_empty subgoals);
+    (pt, f)
 end
 
 (* -------------------------------------------------------------------- *)
@@ -619,10 +634,16 @@ let t_intro_sx_seq id tt tc =
   FApi.t_focus (tt id) tc
 
 (* -------------------------------------------------------------------- *)
-let tt_apply (pt : proofterm) (tc : tcenv) =
+type cutsolver = {
+  smt   : FApi.backward;
+  done_ : FApi.backward;
+}
+  
+(* -------------------------------------------------------------------- *)
+let tt_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv) =
   let (hyps, concl) = FApi.tc_flat tc in
-  let tc, (pt, ax)  =
-    RApi.to_pure (fun tc -> LowApply.check `Elim pt (`Tc (tc, None))) tc in
+  let tc, (pt, ax, subgoals)  =
+    RApi.to_pure (fun tc -> LowApply.check_with_cutsolve `Elim pt (`Tc (tc, None))) tc in
 
   if not (EcReduction.is_conv hyps ax concl) then begin
     (*
@@ -636,7 +657,25 @@ let tt_apply (pt : proofterm) (tc : tcenv) =
     raise InvalidGoalShape
   end;
 
-  FApi.close tc (VApply pt)
+  let tc = FApi.close tc (VApply pt) in
+
+  match cutsolver with
+  | None ->
+    assert (DMap.is_empty subgoals);
+    tc
+
+  | Some cutsolver -> begin
+    Format.eprintf "%d@." (DMap.cardinal subgoals);
+    FApi.t_onall (fun tc ->
+      let tactic =
+        match  DMap.find_opt (FApi.tc1_handle tc) subgoals with
+        | Some `Smt     -> cutsolver.smt
+        | Some `Done    -> cutsolver.done_
+        | Some `DoneSmt -> FApi.t_seq cutsolver.done_ cutsolver.smt
+        | None          -> t_id in
+      tactic tc
+    ) tc
+  end
 
 (* -------------------------------------------------------------------- *)
 let tt_apply_hyp (x : EcIdent.t) ?(args = []) ?(sk = 0) tc =
@@ -663,8 +702,8 @@ let tt_apply_hd (hd : handle) ?(args = []) ?(sk = 0) tc =
   tt_apply pt tc
 
 (* -------------------------------------------------------------------- *)
-let t_apply (pt : proofterm) (tc : tcenv1) =
-  tt_apply pt (FApi.tcenv_of_tcenv1 tc)
+let t_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv1) =
+  tt_apply ?cutsolver pt (FApi.tcenv_of_tcenv1 tc)
 
 (* -------------------------------------------------------------------- *)
 let t_apply_hyp (x : EcIdent.t) ?args ?sk tc =