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

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 7cf1520ab549c661bb7b3060c2716bcc6d615034..f587d2defcaa207b53eb6c6afd075c1ea5ce967e 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/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