From: Ferruccio Guidi Date: Fri, 2 Nov 2007 17:36:33 +0000 (+0000) Subject: - tacticals: new tactical ifs added: uses thens where if_ uses then_ X-Git-Tag: 0.4.95@7852~67 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cf9784a6b94fa9045810d8559509b54dc9e65a4a - tacticals: new tactical ifs added: uses thens where if_ uses then_ - ProofEngineHelpers: namer_of exported from GrafiteEngine --- 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 diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml index b5db34d17..246751b32 100644 --- a/components/tactics/proofEngineHelpers.ml +++ b/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/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli index 39fb69b0d..cc13d1ad7 100644 --- a/components/tactics/proofEngineHelpers.mli +++ b/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/components/tactics/tacticals.ml b/components/tactics/tacticals.ml index d5ec8acfb..f647ebcca 100644 --- a/components/tactics/tacticals.ml +++ b/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/components/tactics/tacticals.mli b/components/tactics/tacticals.mli index 800991bb5..44a6ab4d9 100644 --- a/components/tactics/tacticals.mli +++ b/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