1. tactical "try_tacticals" renamed to "first"

2. tacticals are now implemented as a functor to abstract the type of
   the tactic
3. tacticals are now activated in matita. Their arguments are parsed in the
   right context.

diff --git a/helm/matita/library/nat.ma b/helm/matita/library/nat.ma
index 066018d9e0defaa009cb7ea7c359a7b4b3bf1689..3ab39d9e485883e51868263d0b47c64cb42aebff 100644 (file)
--- a/helm/matita/library/nat.ma
+++ b/helm/matita/library/nat.ma
@@ -30,21 +30,21 @@ definition pred: nat \to nat \def
 
 theorem pred_Sn : \forall n:nat.
 (eq nat n (pred (S n))).
-intros.reflexivity.
+intros; reflexivity.
 qed.
 
 theorem injective_S : \forall n,m:nat. 
 (eq nat (S n) (S m)) \to (eq nat n m).
-intros.
-rewrite > pred_Sn n.
-rewrite > pred_Sn m.
-apply f_equal. assumption.
+intros;
+rewrite > pred_Sn n;
+rewrite > pred_Sn m;
+apply f_equal; assumption.
 qed.
 
 theorem not_eq_S  : \forall n,m:nat. 
 Not (eq nat n m) \to Not (eq nat (S n) (S m)).
-intros. simplify.intros.
-apply H.apply injective_S.assumption.
+intros; simplify; intros;
+apply H; apply injective_S; assumption.
 qed.
 
 definition not_zero : nat \to Prop \def
@@ -54,9 +54,8 @@ definition not_zero : nat \to Prop \def
   | (S p) \Rightarrow True ].
 
 theorem O_S : \forall n:nat. Not (eq nat O (S n)).
-intros.simplify.intros.
-cut (not_zero O).exact Hcut.rewrite > H.
-exact I.
+intros; simplify; intros;
+cut (not_zero O); [ exact Hcut | rewrite > H; exact I ].
 qed.
 
 theorem n_Sn : \forall n:nat. Not (eq nat n (S n)).
@@ -69,8 +68,9 @@ let rec plus n m \def
  | (S p) \Rightarrow S (plus p m) ].
 
 theorem plus_n_O: \forall n:nat. eq nat n (plus n O).
-intros.elim n.simplify.reflexivity.
-simplify.apply f_equal.assumption.
+intros;elim n;
+ [ simplify;reflexivity
+ | simplify;apply f_equal;assumption ].
 qed.
 
 theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n  m)) (plus n (S m)).

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 67f724ce0a71f30351b84996f528d682e3d396c6..0fac57ec97e69a226e59498c7464650267821367 100644 (file)
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -114,6 +114,14 @@
     <keyword>whd</keyword>
   </keyword-list>
 
+  <keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
+    <keyword>try</keyword>
+    <keyword>solve</keyword>
+    <keyword>do</keyword>
+    <keyword>repeat</keyword>
+    <keyword>first</keyword>
+  </keyword-list>
+
 
   <keyword-list _name = "Matita Macro" style = "Others 3" case-sensitive="TRUE">
     <keyword>print</keyword>

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 7f70736abbe22a30cbae66fcaf8db893429e49c2..b20755d870bb4a87def160f7f57d05e9ee7c12e4 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -93,40 +93,209 @@ let tactic_of_ast = function
   | TacticAst.Symmetry _ -> Tactics.symmetry
   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
 
-let eval_tactical status tac =
-  let apply_tactic tactic =
-    let (proof, goals) =
-      ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
-    in
-    let new_status =
-      match goals with
-      | [] -> 
-          let (_,metasenv,_,_) = proof in
-          (match metasenv with
-          | [] -> Proof proof
-          | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
-      | ng::_ -> Incomplete_proof (proof, ng)
-    in
-    { status with proof_status = new_status }
+let disambiguate_term status term =
+  let (aliases, metasenv, cic, _) =
+    match
+      MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+        ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
+        ~metasenv:(MatitaMisc.get_proof_metasenv status) term
+    with
+    | [x] -> x
+    | _ -> assert false
+  in
+  let proof_status =
+    match status.proof_status with
+    | No_proof -> Intermediate metasenv
+    | Incomplete_proof ((uri, _, proof, ty), goal) ->
+        Incomplete_proof ((uri, metasenv, proof, ty), goal)
+    | Intermediate _ -> Intermediate metasenv 
+    | Proof _ -> assert false
+  in
+  let status = { status with proof_status = proof_status } in
+  let status = MatitaSync.set_proof_aliases status aliases in
+  status, cic
+  
+let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
+  let interp path = Disambiguate.interpretate_path [] status.aliases path in
+  let goal_path = interp goal_path in
+  let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+  let status,wanted =
+   match wanted with
+      None -> status,None
+    | Some wanted ->
+       let status,wanted = disambiguate_term status wanted in
+        status, Some wanted
   in
-  let rec tactical_of_ast = function
-    | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
+   status, (wanted, hyp_paths ,goal_path)
+  
+let disambiguate_tactic status = function
+  | TacticAst.Apply (loc, term) ->
+      let status, cic = disambiguate_term status term in
+      status, TacticAst.Apply (loc, cic)
+  | TacticAst.Absurd (loc, term) -> 
+      let status, cic = disambiguate_term status term in
+      status, TacticAst.Absurd (loc, cic)
+  | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
+  | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
+  | TacticAst.Change (loc, pattern, with_what) -> 
+      let status, with_what = disambiguate_term status with_what in
+      let status, pattern = disambiguate_pattern status pattern in
+      status, TacticAst.Change (loc, pattern, with_what)
+  | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
+  | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
+  | TacticAst.Compare (loc,term) ->
+      let status, term = disambiguate_term status term in
+      status, TacticAst.Compare (loc,term)
+  | TacticAst.Constructor (loc,n) ->
+      status, TacticAst.Constructor (loc,n)
+  | TacticAst.Contradiction loc ->
+      status, TacticAst.Contradiction loc
+  | TacticAst.Cut (loc, ident, term) -> 
+      let status, cic = disambiguate_term status term in
+      status, TacticAst.Cut (loc, ident, cic)
+  | TacticAst.DecideEquality loc ->
+      status, TacticAst.DecideEquality loc
+  | TacticAst.Decompose (loc,term) ->
+      let status,term = disambiguate_term status term in
+      status, TacticAst.Decompose(loc,term)
+  | TacticAst.Discriminate (loc,term) ->
+      let status,term = disambiguate_term status term in
+      status, TacticAst.Discriminate(loc,term)
+  | TacticAst.Exact (loc, term) -> 
+      let status, cic = disambiguate_term status term in
+      status, TacticAst.Exact (loc, cic)
+  | TacticAst.Elim (loc, what, Some using, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      let status, using = disambiguate_term status using in
+      status, TacticAst.Elim (loc, what, Some using, depth, idents)
+  | TacticAst.Elim (loc, what, None, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      status, TacticAst.Elim (loc, what, None, depth, idents)
+  | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      let status, using = disambiguate_term status using in
+      status, TacticAst.ElimType (loc, what, Some using, depth, idents)
+  | TacticAst.ElimType (loc, what, None, depth, idents) ->
+      let status, what = disambiguate_term status what in
+      status, TacticAst.ElimType (loc, what, None, depth, idents)
+  | TacticAst.Exists loc -> status, TacticAst.Exists loc 
+  | TacticAst.Fail loc -> status,TacticAst.Fail loc
+  | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
+     let status, pattern = disambiguate_pattern status pattern in
+     let status, term = disambiguate_term status term in
+     status, TacticAst.Fold (loc,reduction_kind, term, pattern)
+  | TacticAst.FwdSimpl (loc, hyp, names) ->
+     status, TacticAst.FwdSimpl (loc, hyp, names)  
+  | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
+  | TacticAst.Generalize (loc,pattern,ident) ->
+      let status, pattern = disambiguate_pattern status pattern in
+      status, TacticAst.Generalize(loc,pattern,ident)
+  | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
+  | TacticAst.IdTac loc -> status,TacticAst.IdTac loc
+  | TacticAst.Injection (loc,term) ->
+      let status, term = disambiguate_term status term in
+      status, TacticAst.Injection (loc,term)
+  | TacticAst.Intros (loc, num, names) ->
+      status, TacticAst.Intros (loc, num, names)
+  | TacticAst.LApply (loc, depth, to_what, what, ident) ->
+     let f term (status, to_what) =
+        let status, term = disambiguate_term status term in
+        status, term :: to_what
+     in
+     let status, to_what = List.fold_right f to_what (status, []) in 
+     let status, what = disambiguate_term status what in
+     status, TacticAst.LApply (loc, depth, to_what, what, ident)
+  | TacticAst.Left loc -> status, TacticAst.Left loc
+  | TacticAst.LetIn (loc, term, name) ->
+      let status, term = disambiguate_term status term in
+      status, TacticAst.LetIn (loc,term,name)
+  | TacticAst.Reduce (loc, reduction_kind, pattern) ->
+      let status, pattern = disambiguate_pattern status pattern in
+      status, TacticAst.Reduce(loc, reduction_kind, pattern)
+  | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
+  | TacticAst.Replace (loc, pattern, with_what) -> 
+      let status, pattern = disambiguate_pattern status pattern in
+      let status, with_what = disambiguate_term status with_what in
+      status, TacticAst.Replace (loc, pattern, with_what)
+  | TacticAst.Rewrite (loc, dir, t, pattern) ->
+      let status, term = disambiguate_term status t in
+      let status, pattern = disambiguate_pattern status pattern in
+      status, TacticAst.Rewrite (loc, dir, term, pattern)
+  | TacticAst.Right loc -> status, TacticAst.Right loc
+  | TacticAst.Ring loc -> status, TacticAst.Ring loc
+  | TacticAst.Split loc -> status, TacticAst.Split loc
+  | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
+  | TacticAst.Transitivity (loc, term) -> 
+      let status, cic = disambiguate_term status term in
+      status, TacticAst.Transitivity (loc, cic)
+
+let apply_tactic tactic status =
+ let status,tactic = disambiguate_tactic status tactic in
+ let tactic = tactic_of_ast tactic in
+ let (proof, goals) =
+  ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in
+ let dummy = -1 in
+  { status with
+     proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals
+
+module MatitaStatus =
+ struct
+  type input_status = MatitaTypes.status
+  type output_status = MatitaTypes.status * ProofEngineTypes.goal list
+  type tactic = input_status -> output_status
+
+  let focus (status,_) goal =
+   let proof,_ = MatitaMisc.get_proof_status status in
+    {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)}
+
+  let goals (_,goals) = goals
+
+  let set_goals (status,_) goals = status,goals
+
+  let id_tac status = apply_tactic (TacticAst.IdTac CicAst.dummy_floc) status
+
+  let mk_tactic tac = tac
+
+  let apply_tactic tac = tac
+
+ end
+
+module MatitaTacticals = Tacticals.Make(MatitaStatus)
+
+let eval_tactical status tac =
+ let rec tactical_of_ast tac =
+  match tac with
+    | TacticAst.Tactic (loc, tactic) -> apply_tactic tactic
+    | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
+       MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals)
     | TacticAst.Do (loc, num, tactical) ->
-        Tacticals.do_tactic num (tactical_of_ast tactical)
+        MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical)
     | TacticAst.Repeat (loc, tactical) ->
-        Tacticals.repeat_tactic (tactical_of_ast tactical)
-    | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
-        Tacticals.seq (List.map tactical_of_ast tacticals)
+        MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical)
     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
-        Tacticals.thens (tactical_of_ast tactical)
-          (List.map tactical_of_ast tacticals)
-    | TacticAst.Tries (loc, tacticals) ->
-        Tacticals.try_tactics
-          (List.map (fun t -> "", tactical_of_ast t) tacticals)
+        MatitaTacticals.thens ~start:(tactical_of_ast tactical)
+          ~continuations:(List.map tactical_of_ast tacticals)
+    | TacticAst.First (loc, tacticals) ->
+        MatitaTacticals.first
+          ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals)
     | TacticAst.Try (loc, tactical) ->
-        Tacticals.try_tactic (tactical_of_ast tactical)
+        MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical)
+    | TacticAst.Solve (loc, tacticals) ->
+        MatitaTacticals.solve_tactics
+         ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals)
+ in
+  let status,goals = tactical_of_ast tac status in
+  let proof,_ = MatitaMisc.get_proof_status status in
+  let new_status =
+   match goals with
+   | [] -> 
+       let (_,metasenv,_,_) = proof in
+       (match metasenv with
+       | [] -> Proof proof
+       | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
+   | ng::_ -> Incomplete_proof (proof, ng)
   in
-  apply_tactic (tactical_of_ast tac)
+   { status with proof_status = new_status }
 
 let eval_coercion status coercion = 
   let coer_uri,coer_ty =
@@ -234,7 +403,48 @@ let generate_projections uri fields status =
 (* to avoid a long list of recursive functions *)
 let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
  
+let disambiguate_obj status obj =
+  let uri =
+   match obj with
+      TacticAst.Inductive (_,(name,_,_,_)::_)
+    | TacticAst.Record (_,name,_,_) ->
+       Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
+    | TacticAst.Inductive _ -> assert false
+    | _ -> None in
+  let (aliases, metasenv, cic, _) =
+    match
+      MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+        ~aliases:(status.aliases) ~uri obj
+    with
+    | [x] -> x
+    | _ -> assert false
+  in
+  let proof_status =
+    match status.proof_status with
+    | No_proof -> Intermediate metasenv
+    | Incomplete_proof _
+    | Intermediate _
+    | Proof _ -> assert false
+  in
+  let status = { status with proof_status = proof_status } in
+  let status = MatitaSync.set_proof_aliases status aliases in
+  status, cic
+  
+let disambiguate_command status = function
+  | TacticAst.Default _
+  | TacticAst.Alias _
+  | TacticAst.Include _ as cmd  -> status,cmd
+  | TacticAst.Coercion (loc, term) ->
+      let status, term = disambiguate_term status term in
+      status, TacticAst.Coercion (loc,term)
+  | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
+      status, cmd
+  | TacticAst.Obj (loc,obj) ->
+      let status,obj = disambiguate_obj status obj in
+       status, TacticAst.Obj (loc,obj)
+
 let eval_command status cmd =
+ let status,cmd = disambiguate_command status cmd in
   match cmd with
   | TacticAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
@@ -341,261 +551,15 @@ let eval_executable status ex =
   | TacticAst.Command (_, cmd) -> eval_command status cmd
   | TacticAst.Macro (_, mac) -> 
       command_error (sprintf "The macro %s can't be in a script" 
-        (TacticAstPp.pp_macro_cic mac))
+        (TacticAstPp.pp_macro_ast mac))
 
 let eval_comment status c = status
             
-let eval status st =
+let eval_ast status st =
   match st with
   | TacticAst.Executable (_,ex) -> eval_executable status ex
   | TacticAst.Comment (_,c) -> eval_comment status c
 
-let disambiguate_term status term =
-  let (aliases, metasenv, cic, _) =
-    match
-      MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
-        ~metasenv:(MatitaMisc.get_proof_metasenv status) term
-    with
-    | [x] -> x
-    | _ -> assert false
-  in
-  let proof_status =
-    match status.proof_status with
-    | No_proof -> Intermediate metasenv
-    | Incomplete_proof ((uri, _, proof, ty), goal) ->
-        Incomplete_proof ((uri, metasenv, proof, ty), goal)
-    | Intermediate _ -> Intermediate metasenv 
-    | Proof _ -> assert false
-  in
-  let status = { status with proof_status = proof_status } in
-  let status = MatitaSync.set_proof_aliases status aliases in
-  status, cic
-  
-let disambiguate_obj status obj =
-  let uri =
-   match obj with
-      TacticAst.Inductive (_,(name,_,_,_)::_)
-    | TacticAst.Record (_,name,_,_) ->
-       Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
-    | TacticAst.Inductive _ -> assert false
-    | _ -> None in
-  let (aliases, metasenv, cic, _) =
-    match
-      MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
-        ~aliases:(status.aliases) ~uri obj
-    with
-    | [x] -> x
-    | _ -> assert false
-  in
-  let proof_status =
-    match status.proof_status with
-    | No_proof -> Intermediate metasenv
-    | Incomplete_proof _
-    | Intermediate _
-    | Proof _ -> assert false
-  in
-  let status = { status with proof_status = proof_status } in
-  let status = MatitaSync.set_proof_aliases status aliases in
-  status, cic
-  
-let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
-  let interp path = Disambiguate.interpretate_path [] status.aliases path in
-  let goal_path = interp goal_path in
-  let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
-  let status,wanted =
-   match wanted with
-      None -> status,None
-    | Some wanted ->
-       let status,wanted = disambiguate_term status wanted in
-        status, Some wanted
-  in
-   status, (wanted, hyp_paths ,goal_path)
-  
-let disambiguate_tactic status = function
-  | TacticAst.Apply (loc, term) ->
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Apply (loc, cic)
-  | TacticAst.Absurd (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Absurd (loc, cic)
-  | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
-  | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
-  | TacticAst.Change (loc, pattern, with_what) -> 
-      let status, with_what = disambiguate_term status with_what in
-      let status, pattern = disambiguate_pattern status pattern in
-      status, TacticAst.Change (loc, pattern, with_what)
-  | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
-  | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
-  | TacticAst.Compare (loc,term) ->
-      let status, term = disambiguate_term status term in
-      status, TacticAst.Compare (loc,term)
-  | TacticAst.Constructor (loc,n) ->
-      status, TacticAst.Constructor (loc,n)
-  | TacticAst.Contradiction loc ->
-      status, TacticAst.Contradiction loc
-  | TacticAst.Cut (loc, ident, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Cut (loc, ident, cic)
-  | TacticAst.DecideEquality loc ->
-      status, TacticAst.DecideEquality loc
-  | TacticAst.Decompose (loc,term) ->
-      let status,term = disambiguate_term status term in
-      status, TacticAst.Decompose(loc,term)
-  | TacticAst.Discriminate (loc,term) ->
-      let status,term = disambiguate_term status term in
-      status, TacticAst.Discriminate(loc,term)
-  | TacticAst.Exact (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Exact (loc, cic)
-  | TacticAst.Elim (loc, what, Some using, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      let status, using = disambiguate_term status using in
-      status, TacticAst.Elim (loc, what, Some using, depth, idents)
-  | TacticAst.Elim (loc, what, None, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      status, TacticAst.Elim (loc, what, None, depth, idents)
-  | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      let status, using = disambiguate_term status using in
-      status, TacticAst.ElimType (loc, what, Some using, depth, idents)
-  | TacticAst.ElimType (loc, what, None, depth, idents) ->
-      let status, what = disambiguate_term status what in
-      status, TacticAst.ElimType (loc, what, None, depth, idents)
-  | TacticAst.Exists loc -> status, TacticAst.Exists loc 
-  | TacticAst.Fail loc -> status,TacticAst.Fail loc
-  | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
-     let status, pattern = disambiguate_pattern status pattern in
-     let status, term = disambiguate_term status term in
-     status, TacticAst.Fold (loc,reduction_kind, term, pattern)
-  | TacticAst.FwdSimpl (loc, hyp, names) ->
-     status, TacticAst.FwdSimpl (loc, hyp, names)  
-  | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
-  | TacticAst.Generalize (loc,pattern,ident) ->
-      let status, pattern = disambiguate_pattern status pattern in
-      status, TacticAst.Generalize(loc,pattern,ident)
-  | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
-  | TacticAst.IdTac loc -> status,TacticAst.IdTac loc
-  | TacticAst.Injection (loc,term) ->
-      let status, term = disambiguate_term status term in
-      status, TacticAst.Injection (loc,term)
-  | TacticAst.Intros (loc, num, names) ->
-      status, TacticAst.Intros (loc, num, names)
-  | TacticAst.LApply (loc, depth, to_what, what, ident) ->
-     let f term (status, to_what) =
-        let status, term = disambiguate_term status term in
-        status, term :: to_what
-     in
-     let status, to_what = List.fold_right f to_what (status, []) in 
-     let status, what = disambiguate_term status what in
-     status, TacticAst.LApply (loc, depth, to_what, what, ident)
-  | TacticAst.Left loc -> status, TacticAst.Left loc
-  | TacticAst.LetIn (loc, term, name) ->
-      let status, term = disambiguate_term status term in
-      status, TacticAst.LetIn (loc,term,name)
-  | TacticAst.Reduce (loc, reduction_kind, pattern) ->
-      let status, pattern = disambiguate_pattern status pattern in
-      status, TacticAst.Reduce(loc, reduction_kind, pattern)
-  | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
-  | TacticAst.Replace (loc, pattern, with_what) -> 
-      let status, pattern = disambiguate_pattern status pattern in
-      let status, with_what = disambiguate_term status with_what in
-      status, TacticAst.Replace (loc, pattern, with_what)
-  | TacticAst.Rewrite (loc, dir, t, pattern) ->
-      let status, term = disambiguate_term status t in
-      let status, pattern = disambiguate_pattern status pattern in
-      status, TacticAst.Rewrite (loc, dir, term, pattern)
-  | TacticAst.Right loc -> status, TacticAst.Right loc
-  | TacticAst.Ring loc -> status, TacticAst.Ring loc
-  | TacticAst.Split loc -> status, TacticAst.Split loc
-  | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
-  | TacticAst.Transitivity (loc, term) -> 
-      let status, cic = disambiguate_term status term in
-      status, TacticAst.Transitivity (loc, cic)
-
-let rec disambiguate_tactical status = function 
-  | TacticAst.Tactic (loc, tactic) -> 
-      let status, tac = disambiguate_tactic status tactic in
-      status, TacticAst.Tactic (loc, tac)
-  | TacticAst.Do (loc, num, tactical) ->
-      let status, tac = disambiguate_tactical status tactical in
-      status, TacticAst.Do (loc, num, tac)
-  | TacticAst.Repeat (loc, tactical) -> 
-      let status, tac = disambiguate_tactical status tactical in
-      status, TacticAst.Repeat (loc, tac)
-  | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
-      let status, tacticals = disambiguate_tacticals status tacticals in
-      let tacticals = List.rev tacticals in
-      status, TacticAst.Seq (loc, tacticals)
-  | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
-      let status, tactical = disambiguate_tactical status tactical in
-      let status, tacticals = disambiguate_tacticals status tacticals in
-      status, TacticAst.Then (loc, tactical, tacticals)
-  | TacticAst.Tries (loc, tacticals) ->
-      let status, tacticals = disambiguate_tacticals status tacticals in
-      status, TacticAst.Tries (loc, tacticals)
-  | TacticAst.Try (loc, tactical) ->
-      let status, tactical = disambiguate_tactical status tactical in
-      status, TacticAst.Try (loc, tactical)
-
-and disambiguate_tacticals status tacticals =
-  let status, tacticals =
-    List.fold_left
-      (fun (status, tacticals) tactical ->
-        let status, tac = disambiguate_tactical status tactical in
-        status, tac :: tacticals)
-      (status, [])
-      tacticals
-  in
-  let tacticals = List.rev tacticals in
-  status, tacticals
-  
-let disambiguate_command status = function
-  | TacticAst.Default _
-  | TacticAst.Alias _
-  | TacticAst.Include _ as cmd  -> status,cmd
-  | TacticAst.Coercion (loc, term) ->
-      let status, term = disambiguate_term status term in
-      status, TacticAst.Coercion (loc,term)
-  | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
-      status, cmd
-  | TacticAst.Obj (loc,obj) ->
-      let status,obj = disambiguate_obj status obj in
-       status, TacticAst.Obj (loc,obj)
-
-let disambiguate_executable status ex =
-  match ex with
-  | TacticAst.Tactical (loc, tac) ->
-      let status, tac = disambiguate_tactical status tac in
-      status, (TacticAst.Tactical (loc, tac))
-  | TacticAst.Command (loc, cmd) ->
-      let status, cmd = disambiguate_command status cmd in
-      status, (TacticAst.Command (loc, cmd))
-  | TacticAst.Macro (_, mac) -> 
-      command_error (sprintf "The macro %s can't be in a script" 
-        (TacticAstPp.pp_macro_ast mac))
-
-let disambiguate_comment status c = 
-  match c with
-  | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
-  | TacticAst.Code (loc,ex) -> 
-        let status, ex = disambiguate_executable status ex in
-        status, TacticAst.Code (loc,ex)
-        
-let disambiguate_statement status statement =
-  match statement with
-  | TacticAst.Comment (loc,c) -> 
-        let status, c = disambiguate_comment status c in
-        status, TacticAst.Comment (loc,c)
-  | TacticAst.Executable (loc,ex) -> 
-        let status, ex = disambiguate_executable status ex in
-        status, TacticAst.Executable (loc,ex)
-  
-let eval_ast status ast =
-  let status,st = disambiguate_statement status ast in
-  (* this disambiguation step should be deferred to support tacticals *)
-  eval status st
-
 let eval_from_stream status str cb =
   let stl = CicTextualParser2.parse_statements str in
   List.iter

diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli
index 249bad8f487bedc80240b247b3c508445307691c..9311215f3d563c0b6e729c456c133421d71231da 100644 (file)
--- a/helm/matita/matitaEngine.mli
+++ b/helm/matita/matitaEngine.mli
@@ -44,9 +44,4 @@ val eval_ast:
     (CicAst.term,TacticAst.obj,string) TacticAst.statement ->
     MatitaTypes.status
 
-val eval:
-  MatitaTypes.status -> (Cic.term,Cic.obj,string) TacticAst.statement ->
-    MatitaTypes.status
-
 val initial_status: MatitaTypes.status lazy_t
-

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index fd79cdab176374096c76b36ed3ca28bc092447c0..7b0360b9cef2c7f4b4410ddbe568defb3ed167a3 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -477,11 +477,14 @@ EXTEND
   ];
   tactical:
     [ "sequence" LEFTA
-      [ tactical = NEXT -> tactical
-      | tacticals = LIST1 NEXT SEP SYMBOL ";" -> TacticAst.Seq (loc, tacticals)
+      [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
+         match tacticals with
+            [] -> assert false
+          | [tac] -> tac
+          | l -> TacticAst.Seq (loc, l)
       ]
     | "then" NONA
-      [ tac = tactical;
+      [ tac = tactical; SYMBOL ";";
         PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
           (TacticAst.Then (loc, tac, tacs))
       ]
@@ -492,11 +495,14 @@ EXTEND
           TacticAst.Repeat (loc, tac)
       ]
     | "simple" NONA
-      [ IDENT "tries";
-        PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
-          TacticAst.Tries (loc, tacs)
+      [ IDENT "first";
+        PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
+          TacticAst.First (loc, tacs)
       | IDENT "try"; tac = NEXT ->
           TacticAst.Try (loc, tac)
+      | IDENT "solve";
+        PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" ->
+          TacticAst.Solve (loc, tacs)
       | PAREN "("; tac = tactical; PAREN ")" -> tac
       | tac = tactic -> TacticAst.Tactic (loc, tac)
       ]

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 581b44698ef23de18ab618107f16abed5c192d2a..31e2093530f33d6a1c22dd601204c3cafa2b27e3 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -145,9 +145,10 @@ type ('term, 'ident) tactical =
   | Repeat of loc * ('term, 'ident) tactical
   | Seq of loc * ('term, 'ident) tactical list (* sequential composition *)
   | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list
-  | Tries of loc * ('term, 'ident) tactical list
+  | First of loc * ('term, 'ident) tactical list
       (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
   | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
+  | Solve of loc * ('term, 'ident) tactical list
 
 
 type ('term, 'obj, 'ident) code =

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 2c31f3bfcebf9eeae1a096ebdbae5a816cdbe786..bd26fb387492dcc6947b23945d7769a2bd64a03b 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -246,9 +246,10 @@ let rec pp_tactical = function
   | Repeat (_, tac) -> "repeat " ^ pp_tactical tac
   | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
   | Then (_, tac, tacs) ->
-      sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
-  | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
+      sprintf "%s; [%s]" (pp_tactical tac) (pp_tacticals ~sep:" | " tacs)
+  | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
   | Try (_, tac) -> "try " ^ pp_tactical tac
+  | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
 
 and pp_tacticals ~sep tacs =
   String.concat sep (List.map pp_tactical tacs)

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 1c4e40ed3601fa3dbeab5d2cf910ebffca3f93d2..a424987a2de9dc19c1445d28aa9934223d96b3df 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -915,7 +915,7 @@ let assumption_tac (proof,goal)=
         )  
           context 
   in
-  Tacticals.try_tactics ~tactics:tac_list (proof,goal)
+  Tacticals.first ~tactics:tac_list (proof,goal)
 ;;
 *)
 (* Galla: moved in negationTactics.ml
@@ -1162,7 +1162,7 @@ let rec fourier (s_proof,s_goal)=
                    r))
                  ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
-                   Tacticals.try_tactics 
+                   Tacticals.first 
                      ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
                    ])
                ;(*Tacticals.id_tac*)

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index 1d5fd903dead5cc09649faf676e9bb310e080b88..c505807f2ddc24295a060912d90fd3602cb7bfb3 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -483,7 +483,7 @@ let ring_tac status =
       try
         let new_hyps = ref 0 in  (* number of new hypotheses created *)
        ProofEngineTypes.apply_tactic 
-         (Tacticals.try_tactics
+         (Tacticals.first
           ~tactics:[
             "reflexivity", EqualityTactics.reflexivity_tac ;
             "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
@@ -526,7 +526,7 @@ let ring_tac status =
               in
               let status'' =
               ProofEngineTypes.apply_tactic
-                (Tacticals.try_tactics (* try to solve 1st subgoal *)
+                (Tacticals.first (* try to solve 1st subgoal *)
                   ~tactics:[
                     "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
                     "exact sym_eqt su t2 ...",

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index b72e6e24fae7a678caa5a901b49f1c45bbd09b1d..b5a45dae15d9c957a4fe21a14a1c4b177b241076 100644 (file)
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -38,11 +38,6 @@ let warn s =
   if debug then
     debug_print ("TACTICALS WARNING: " ^ s)
 
-
-(** TACTIC{,AL}S *)
-
-  (* not a tactical, but it's used only here (?) *)
-
 let id_tac = 
  let id_tac (proof,goal) = 
   let _, metasenv, _, _ = proof in
@@ -51,24 +46,67 @@ let id_tac =
  in 
   mk_tactic id_tac
 
+let fail_tac =
+ let fail_tac (proof,goal) =
+  let _, metasenv, _, _ = proof in
+  let _, _, _ = CicUtil.lookup_meta goal metasenv in
+   raise (Fail "fail tactical")
+ in
+  mk_tactic fail_tac
+
+module type Status =
+ sig
+   type input_status
+   type output_status
+   type tactic
+   val id_tac : tactic
+   val mk_tactic : (input_status -> output_status) -> tactic
+   val apply_tactic : tactic -> input_status -> output_status
+   val goals : output_status -> ProofEngineTypes.goal list
+   val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
+   val focus : output_status -> ProofEngineTypes.goal -> input_status
+ end
+
+module type T =
+ sig
+  type tactic
+
+  val first: tactics: (string * tactic) list -> tactic
+
+  val thens: start: tactic -> continuations: tactic list -> tactic
+
+  val then_: start: tactic -> continuation: tactic -> tactic
+
+   (** "folding" of then_ *)
+  val seq: tactics: tactic list -> tactic
+
+  val repeat_tactic: tactic: tactic -> tactic
+
+  val do_tactic: n: int -> tactic: tactic -> tactic 
+
+  val try_tactic: tactic: tactic -> tactic 
+
+  val solve_tactics: tactics: (string * tactic) list -> tactic
+ end
+
+module Make (S:Status) : T with type tactic = S.tactic =
+struct
+type tactic = S.tactic
+
   (**
     naive implementation of ORELSE tactical, try a sequence of tactics in turn:
     if one fails pass to the next one and so on, eventually raises (failure "no
     tactics left")
-    TODO warning: not tail recursive due to "try .. with" boxing
-
-    Galla: is this exactly Coq's "First"?
-
   *)
-let try_tactics ~tactics =
- let rec try_tactics ~(tactics: (string * tactic) list) status =
-  warn "in Tacticals.try_tactics";
+let first ~tactics =
+ let rec first ~(tactics: (string * tactic) list) status =
+  warn "in Tacticals.first";
   match tactics with
   | (descr, tac)::tactics ->
-      warn ("Tacticals.try_tactics IS TRYING " ^ descr);
+      warn ("Tacticals.first IS TRYING " ^ descr);
       (try
-        let res = apply_tactic tac status in
-        warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!");
+        let res = S.apply_tactic tac status in
+        warn ("Tacticals.first: " ^ descr ^ " succedeed!!!");
         res
        with
         e ->
@@ -77,46 +115,57 @@ let try_tactics ~tactics =
           | (CicTypeChecker.TypeCheckerFailure _)
           | (CicUnification.UnificationFailure _) ->
               warn (
-                "Tacticals.try_tactics failed with exn: " ^
+                "Tacticals.first failed with exn: " ^
                 Printexc.to_string e);
-              try_tactics ~tactics status
+              first ~tactics status
         | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
       )
-  | [] -> raise (Fail "try_tactics: no tactics left")
+  | [] -> raise (Fail "first: no tactics left")
  in
-  mk_tactic (try_tactics ~tactics)
+  S.mk_tactic (first ~tactics)
 
 
 let thens ~start ~continuations =
  let thens ~start ~continuations status =
- let (proof,new_goals) = apply_tactic start status in
+ let output_status = S.apply_tactic start status in
+ let new_goals = S.goals output_status in
   try
-   List.fold_left2
-    (fun (proof,goals) goal tactic ->
-      let (proof',new_goals') = apply_tactic tactic (proof,goal) in
-       (proof',goals@new_goals')
-    ) (proof,[]) new_goals continuations
+   let output_status,goals =
+    List.fold_left2
+     (fun (output_status,goals) goal tactic ->
+       let status = S.focus output_status goal in
+       let output_status' = S.apply_tactic tactic status in
+       let new_goals' = S.goals output_status' in
+        (output_status',goals@new_goals')
+     ) (output_status,[]) new_goals continuations
+   in
+    S.set_goals output_status goals
   with
    Invalid_argument _ -> 
-(* FG: more debugging information *)
     let debug = Printf.sprintf "thens: expected %i new goals, found %i"
      (List.length continuations) (List.length new_goals)
     in
     raise (Fail debug)
  in
-  mk_tactic (thens ~start ~continuations )
+  S.mk_tactic (thens ~start ~continuations )
 
 
 let then_ ~start ~continuation =
  let then_ ~start ~continuation status =
- let (proof,new_goals) = apply_tactic start status in
-  List.fold_left
-   (fun (proof,goals) goal ->
-     let (proof',new_goals') = apply_tactic continuation (proof,goal) in
-      (proof',goals@new_goals')
-   ) (proof,[]) new_goals
+ let output_status = S.apply_tactic start status in
+ let new_goals = S.goals output_status in
+  let output_status,goals =
+   List.fold_left
+    (fun (output_status,goals) goal ->
+      let status = S.focus output_status goal in
+      let output_status' = S.apply_tactic continuation status in
+      let new_goals' = S.goals output_status' in
+       (output_status',goals@new_goals')
+    ) (output_status,[]) new_goals
+  in
+   S.set_goals output_status goals
  in
-  mk_tactic (then_ ~start ~continuation)
+  S.mk_tactic (then_ ~start ~continuation)
 
 let rec seq ~tactics =
   match tactics with
@@ -133,24 +182,27 @@ let rec seq ~tactics =
 let repeat_tactic ~tactic =
  let rec repeat_tactic ~tactic status =
   warn "in repeat_tactic";
-  try let (proof, goallist) = apply_tactic tactic status in
-   let rec step proof goallist =
+  try
+   let output_status = S.apply_tactic tactic status in
+   let goallist = S.goals output_status in
+   let rec step output_status goallist =
     match goallist with
-       [] -> (proof, [])
+       [] -> output_status,[]
      | head::tail -> 
-        let (proof', goallist') = repeat_tactic ~tactic (proof, head) in
-         let (proof'', goallist'') = step proof' tail in
-          proof'', goallist'@goallist''
+        let status = S.focus output_status head in
+        let output_status' = repeat_tactic ~tactic status in
+        let goallist' = S.goals output_status' in
+         let output_status'',goallist'' = step output_status' tail in
+          output_status'',goallist'@goallist''
    in
-    step proof goallist
+    let output_status,goallist = step output_status goallist in
+     S.set_goals output_status goallist
   with 
    (Fail _) as e ->
     warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
-    apply_tactic id_tac status
+    S.apply_tactic S.id_tac status
  in 
-  mk_tactic (repeat_tactic ~tactic)
-;;
-
+  S.mk_tactic (repeat_tactic ~tactic)
 
 
 (* This tries to apply tactic n times *)
@@ -158,28 +210,30 @@ let do_tactic ~n ~tactic =
  let rec do_tactic ~n ~tactic status =
   warn "in do_tactic";
   try 
-   let (proof, goallist) = 
-    if (n>0) then apply_tactic tactic status 
-             else apply_tactic id_tac status in
+   let output_status = 
+    if (n>0) then S.apply_tactic tactic status 
+             else S.apply_tactic S.id_tac status in
+   let goallist = S.goals output_status in
 (*             else (proof, []) in *)
 (* perche' non va bene questo? stessa questione di ##### ? *)
-   let rec step proof goallist =
+   let rec step output_status goallist =
     match goallist with
-       [] -> (proof, [])
+       [] -> output_status, []
      | head::tail -> 
-        let (proof', goallist') = 
-        do_tactic ~n:(n-1) ~tactic (proof, head) in
-        let (proof'', goallist'') = step proof' tail in
-         proof'', goallist'@goallist''
+        let status = S.focus output_status head in
+        let output_status' = do_tactic ~n:(n-1) ~tactic status in
+        let goallist' = S.goals output_status' in 
+        let (output_status'', goallist'') = step output_status' tail in
+         output_status'', goallist'@goallist''
    in
-    step proof goallist
+    let output_status,goals = step output_status goallist in
+     S.set_goals output_status goals
   with 
    (Fail _) as e ->
     warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ;
-    apply_tactic id_tac status
+    S.apply_tactic S.id_tac status
  in
-  mk_tactic (do_tactic ~n ~tactic)
-;;
+  S.mk_tactic (do_tactic ~n ~tactic)
 
 
 
@@ -188,16 +242,13 @@ let try_tactic ~tactic =
  let rec try_tactic ~tactic status =
   warn "in Tacticals.try_tactic";
   try
-   apply_tactic tactic status
+   S.apply_tactic tactic status
   with
    (Fail _) as e -> 
     warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e);
-    apply_tactic id_tac status
+    S.apply_tactic S.id_tac status
  in
-  mk_tactic (try_tactic ~tactic)
-;;
-
-let fail_tac = mk_tactic (fun _ -> raise (Fail "fail tactical"))
+  S.mk_tactic (try_tactic ~tactic)
 
 (* This tries tactics until one of them doesn't _solve_ the goal *)
 (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
@@ -208,14 +259,15 @@ let solve_tactics ~tactics =
   | (descr, currenttactic)::moretactics ->
       warn ("Tacticals.solve_tactics is trying " ^ descr);
       (try
-        let (proof, goallist) = apply_tactic currenttactic status in
+        let output_status = S.apply_tactic currenttactic status in
+        let goallist = S.goals output_status in
          match goallist with 
             [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ 
                   " solved the goal!!!");
 (* questo significa che non ci sono piu' goal, o che current_tactic non ne 
    ha aperti di nuovi? (la 2a!) ##### 
    nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *)
-                  (proof, goallist)
+                  output_status
           | _ -> warn ("Tacticals.solve_tactics: try the next tactic");
                  solve_tactics ~tactics:(moretactics) status
        with
@@ -225,7 +277,24 @@ let solve_tactics ~tactics =
          solve_tactics ~tactics status
       )
   | [] -> raise (Fail "solve_tactics cannot solve the goal");
-          apply_tactic id_tac status
+          S.apply_tactic S.id_tac status
  in
-  mk_tactic (solve_tactics ~tactics)
-;;
+  S.mk_tactic (solve_tactics ~tactics)
+end
+
+module ProofEngineStatus =
+ struct
+   type input_status = ProofEngineTypes.status
+   type output_status = ProofEngineTypes.proof * ProofEngineTypes.goal list
+   type tactic = ProofEngineTypes.tactic
+   let id_tac = id_tac
+   let mk_tactic = ProofEngineTypes.mk_tactic
+   let apply_tactic = ProofEngineTypes.apply_tactic
+   let goals (_,goals) = goals
+   let set_goals (proof,_) goals = proof,goals
+   let focus (proof,_) goal = proof,goal
+ end
+
+module ProofEngineTacticals = Make(ProofEngineStatus)
+
+include ProofEngineTacticals

diff --git a/helm/ocaml/tactics/tacticals.mli b/helm/ocaml/tactics/tacticals.mli
index ab2f718238aebaab580376085b2b9ada202ed7f6..06afc21dc1755c060f3de4e727844f62baa9fb20 100644 (file)
--- a/helm/ocaml/tactics/tacticals.mli
+++ b/helm/ocaml/tactics/tacticals.mli
@@ -23,35 +23,44 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
 val id_tac : ProofEngineTypes.tactic
+val fail_tac: ProofEngineTypes.tactic
 
- (* tacticals *)
-val try_tactics:
-  tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+module type Status =
+ sig
+   type input_status
+   type output_status
+   type tactic
+   val id_tac : tactic
+   val mk_tactic : (input_status -> output_status) -> tactic
+   val apply_tactic : tactic -> input_status -> output_status
+   val goals : output_status -> ProofEngineTypes.goal list
+   val set_goals: output_status -> ProofEngineTypes.goal list -> output_status
+   val focus : output_status -> ProofEngineTypes.goal -> input_status
+ end
 
-val thens:
- start: ProofEngineTypes.tactic ->
- continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+module type T =
+ sig
+  type tactic
 
-val then_:
- start: ProofEngineTypes.tactic ->
- continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+  val first: tactics: (string * tactic) list -> tactic
 
- (** "folding" of then_ *)
-val seq: tactics: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+  val thens: start: tactic -> continuations: tactic list -> tactic
 
-val repeat_tactic: 
- tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
+  val then_: start: tactic -> continuation: tactic -> tactic
 
-val do_tactic:
- n: int ->
- tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic 
+   (** "folding" of then_ *)
+  val seq: tactics: tactic list -> tactic
 
-val try_tactic:
- tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic 
+  val repeat_tactic: tactic: tactic -> tactic
 
-val solve_tactics:
- tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+  val do_tactic: n: int -> tactic: tactic -> tactic 
 
-val fail_tac: ProofEngineTypes.tactic
+  val try_tactic: tactic: tactic -> tactic 
+
+  val solve_tactics: tactics: (string * tactic) list -> tactic
+ end
+
+module Make (S:Status) : T with type tactic = S.tactic
+
+include T with type tactic = ProofEngineTypes.tactic