X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteEngine.ml;h=f587d2defcaa207b53eb6c6afd075c1ea5ce967e;hb=cf9784a6b94fa9045810d8559509b54dc9e65a4a;hp=7cf1520ab549c661bb7b3060c2716bcc6d615034;hpb=f38af523cd051d4c1d0dceeb59ce2fbbfc87367d;p=helm.git diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 7cf1520ab..f587d2def 100644 --- 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