- ProofEngineHelpers: namer_of moved to GrafiteEngine

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 0d2fb682ed78b98ec293f6e26b6ce94353a7c1e2..afcbf7f26709a0ea6ddd875852b07a5e6a157b06 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -42,6 +42,23 @@ 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
@@ -75,7 +92,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:(PEH.namer_of names)
+      Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
         what
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
@@ -83,24 +100,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:(PEH.namer_of names)
+        ~mk_fresh_name_callback:(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:(PEH.namer_of names) term
+     Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
   | GrafiteAst.Decompose (_, names) ->
-      let mk_fresh_name_callback = PEH.namer_of names in
+      let mk_fresh_name_callback = namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ()
   | GrafiteAst.Demodulate _ -> 
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm
   | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) ->
-      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
+      Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         ~pattern what
   | GrafiteAst.ElimType (_, what, using, (depth, names)) ->
-      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names)
+      Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what
   | GrafiteAst.Exact (_, term) -> Tactics.exact term
   | GrafiteAst.Exists _ -> Tactics.exists
@@ -125,24 +142,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:(PEH.namer_of names)
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(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:(PEH.namer_of names) pattern 
+     Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
   | GrafiteAst.IdTac _ -> Tactics.id
   | GrafiteAst.Intros (_, (howmany, names)) ->
       PrimitiveTactics.intros_tac ?howmany
-        ~mk_fresh_name_callback:(PEH.namer_of names) ()
+        ~mk_fresh_name_callback:(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:(PEH.namer_of names) 
+      Tactics.lapply ~mk_fresh_name_callback:(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:(PEH.namer_of [Some name])
+      Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
         | `Normalize -> Tactics.normalize ~pattern
@@ -155,7 +172,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:(PEH.namer_of names) *)
+(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *)
      (List.map (function Some s -> s | None -> assert false) names)
   | GrafiteAst.Right _ -> Tactics.right
   | GrafiteAst.Ring _ -> Tactics.ring
@@ -204,7 +221,6 @@ let classify_tactic tactic =
   | _ -> false
   
 let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
-  let module PEH = ProofEngineHelpers in
 (*   let print_m name metasenv =
     prerr_endline (">>>>> " ^ name);
     prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)