- tacticals: new tactical ifs added: uses thens where if_ uses then_

- ProofEngineHelpers: namer_of exported from GrafiteEngine

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7cf1520ab549c661bb7b3060c2716bcc6d615034..f587d2defcaa207b53eb6c6afd075c1ea5ce967e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -25,6 +25,8 @@
 
 (* $Id$ *)
 
+module PEH = ProofEngineHelpers
+
 exception Drop
 (* mo file name, ma file name *)
 exception IncludedFileNotCompiled of string * string 
@@ -40,23 +42,6 @@ type options = {
   clean_baseuri: bool
 }
 
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
-  * names as long as they are available, then it fallbacks to name generation
-  * using FreshNamesGenerator module *)
-let namer_of names =
-  let len = List.length names in
-  let count = ref 0 in
-  fun metasenv context name ~typ ->
-    if !count < len then begin
-      let name = match List.nth names !count with
-         | Some s -> Cic.Name s
-        | None   -> Cic.Anonymous
-      in
-      incr count;
-      name
-    end else
-      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
 let rec tactic_of_ast status ast =
   let module PET = ProofEngineTypes in
   match ast with
@@ -90,7 +75,7 @@ let rec tactic_of_ast status ast =
       Tactics.auto ~params ~dbd:(LibraryDb.instance ()) 
        ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Cases (_, what, (howmany, names)) ->
-      Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
+      Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(PEH.namer_of names)
         what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
@@ -98,24 +83,24 @@ let rec tactic_of_ast status ast =
   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
   | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) -> 
       Tactics.compose times t1 t2 ?howmany
-        ~mk_fresh_name_callback:(namer_of names)
+        ~mk_fresh_name_callback:(PEH.namer_of names)
   | GrafiteAst.Contradiction _ -> Tactics.contradiction
   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
   | GrafiteAst.Cut (_, ident, term) ->
      let names = match ident with None -> [] | Some id -> [Some id] in
-     Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
+     Tactics.cut ~mk_fresh_name_callback:(PEH.namer_of names) term
   | GrafiteAst.Decompose (_, names) ->
-      let mk_fresh_name_callback = namer_of names in
+      let mk_fresh_name_callback = PEH.namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ()
   | GrafiteAst.Demodulate _ -> 
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
-      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
         ~pattern what
   | GrafiteAst.ElimType (_, what, using, (depth, names)) ->
-      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
         what
   | GrafiteAst.Exact (_, term) -> Tactics.exact term
   | GrafiteAst.Exists _ -> Tactics.exists
@@ -140,24 +125,24 @@ let rec tactic_of_ast status ast =
       Tactics.fold ~reduction ~term ~pattern
   | GrafiteAst.Fourier _ -> Tactics.fourier
   | GrafiteAst.FwdSimpl (_, hyp, names) -> 
-     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(PEH.namer_of names)
       ~dbd:(LibraryDb.instance ()) hyp
   | GrafiteAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [Some id] in
-     Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
+     Tactics.generalize ~mk_fresh_name_callback:(PEH.namer_of names) pattern 
   | GrafiteAst.IdTac _ -> Tactics.id
   | GrafiteAst.Intros (_, (howmany, names)) ->
       PrimitiveTactics.intros_tac ?howmany
-        ~mk_fresh_name_callback:(namer_of names) ()
+        ~mk_fresh_name_callback:(PEH.namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
   | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
       let names = match ident with None -> [] | Some id -> [Some id] in
-      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
+      Tactics.lapply ~mk_fresh_name_callback:(PEH.namer_of names) 
         ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
-      Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name])
+      Tactics.letin term ~mk_fresh_name_callback:(PEH.namer_of [Some name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
         | `Normalize -> Tactics.normalize ~pattern
@@ -170,7 +155,7 @@ let rec tactic_of_ast status ast =
      Tactics.replace ~pattern ~with_what
   | GrafiteAst.Rewrite (_, direction, t, pattern, names) ->
      EqualityTactics.rewrite_tac ~direction ~pattern t 
-(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *)
+(* to be replaced with ~mk_fresh_name_callback:(PEH.namer_of names) *)
      (List.map (function Some s -> s | None -> assert false) names)
   | GrafiteAst.Right _ -> Tactics.right
   | GrafiteAst.Ring _ -> Tactics.ring

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index b5db34d17c8b852bdd2ca9988f10dd46feb4ed0b..246751b32785f52b49cad40cff47f7172fffe469 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -707,3 +707,19 @@ let sort_metasenv (m : Cic.metasenv) =
   (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
 ;;
   
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+  * names as long as they are available, then it fallbacks to name generation
+  * using FreshNamesGenerator module *)
+let namer_of names =
+  let len = List.length names in
+  let count = ref 0 in
+  fun metasenv context name ~typ ->
+    if !count < len then begin
+      let name = match List.nth names !count with
+         | Some s -> Cic.Name s
+        | None   -> Cic.Anonymous
+      in
+      incr count;
+      name
+    end else
+      FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 39fb69b0d1067370a408c62be07cc495331516c1..cc13d1ad780bf067e7df4ca65ee77ef4bd447ca2 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/components/tactics/proofEngineHelpers.mli
@@ -128,3 +128,8 @@ val split_with_whd: Cic.context * Cic.term ->
                     (Cic.context * Cic.term) list * int
 val split_with_normalize: Cic.context * Cic.term -> 
                           (Cic.context * Cic.term) list * int
+
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+  * names as long as they are available, then it fallbacks to name generation
+  * using FreshNamesGenerator module *)
+val namer_of: string option list -> ProofEngineTypes.mk_fresh_name_type

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index d5ec8acfb8be6c9edee7f353ba9f5368f8314511..f647ebccaa9d199181761b2233c59f00ace13f1d 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -201,6 +201,23 @@ let if_ ~start ~continuation ~fail =
    in
    PET.mk_tactic if_
 
+let ifs ~start ~continuations ~fail =
+   let ifs status =
+      let xoutput = 
+         try
+           let result = PET.apply_tactic start status in
+           info (lazy ("Tacticals.ifs: succedeed!!!"));
+           Some result 
+        with PET.Fail _ -> None
+      in
+      let tactic = match xoutput with
+         | Some res -> thens ~start:(const_tac res) ~continuations
+        | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic ifs
+
 let first ~tactics =
   let rec first ~(tactics: tactic list) status =
     info (lazy "in Tacticals.first");

diff --git a/helm/software/components/tactics/tacticals.mli b/helm/software/components/tactics/tacticals.mli
index 800991bb560fa9abd4da4e79399192333352694b..44a6ab4d9cffb0160bd1deaa1ae64359725e4363 100644 (file)
--- a/helm/software/components/tactics/tacticals.mli
+++ b/helm/software/components/tactics/tacticals.mli
@@ -31,6 +31,7 @@ val fail_tac: tactic
 val first: tactics: tactic list -> tactic
 val thens: start: tactic -> continuations: tactic list -> tactic
 val then_: start: tactic -> continuation: tactic -> tactic
+val ifs: start: tactic -> continuations: tactic list -> fail: tactic -> tactic
 val if_: start: tactic -> continuation: tactic -> fail: tactic -> tactic
 val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
 val repeat_tactic: tactic: tactic -> tactic