From b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 16 Apr 2009 09:46:57 +0000 Subject: [PATCH] Universe is used only locally to tactics/ AutomationCache.cache is part of grafite_status and will contain tables too --- .../binaries/transcript/.depend.opt | 5 ++ .../grafite_engine/grafiteEngine.ml | 27 ++++++----- .../components/grafite_engine/grafiteSync.ml | 7 +-- .../components/grafite_engine/grafiteTypes.ml | 2 +- .../grafite_engine/grafiteTypes.mli | 2 +- .../components/syntax_extensions/.depend | 3 ++ helm/software/components/tactics/.depend | 16 +++++++ helm/software/components/tactics/Makefile | 1 + helm/software/components/tactics/auto.ml | 46 ++++++++++++------- helm/software/components/tactics/auto.mli | 10 ++-- .../components/tactics/automationCache.ml | 36 +++++++++++++++ .../components/tactics/automationCache.mli | 33 +++++++++++++ .../components/tactics/declarative.ml | 30 ++++++------ .../components/tactics/declarative.mli | 10 ++-- helm/software/components/tactics/tactics.mli | 10 ++-- helm/software/matita/matitaScript.ml | 3 +- 16 files changed, 178 insertions(+), 63 deletions(-) create mode 100644 helm/software/components/tactics/automationCache.ml create mode 100644 helm/software/components/tactics/automationCache.mli diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 354413f1b..1f32e8c9e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -86,11 +86,11 @@ let rec tactic_of_ast status ast = | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term | GrafiteAst.ApplyS (_, term, params) -> Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ()) - ~universe:status.GrafiteTypes.universe + ~automation_cache:status.GrafiteTypes.automation_cache | GrafiteAst.Assumption _ -> Tactics.assumption | GrafiteAst.AutoBatch (_,params) -> Tactics.auto ~params ~dbd:(LibraryDb.instance ()) - ~universe:status.GrafiteTypes.universe + ~automation_cache:status.GrafiteTypes.automation_cache | GrafiteAst.Cases (_, what, pattern, (howmany, names)) -> Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names) ~pattern what @@ -112,7 +112,7 @@ let rec tactic_of_ast status ast = | GrafiteAst.Demodulate (_, params) -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~params - ~universe:status.GrafiteTypes.universe + ~automation_cache:status.GrafiteTypes.automation_cache | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) @@ -183,12 +183,12 @@ let rec tactic_of_ast status ast = | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1 | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) -> Declarative.by_just_we_proved ~dbd:(LibraryDb.instance()) - ~universe:status.GrafiteTypes.universe just ty id t1 + ~automation_cache:status.GrafiteTypes.automation_cache just ty id t1 | GrafiteAst.We_need_to_prove (_, t, id, t2) -> Declarative.we_need_to_prove t id t2 | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) - ~universe:status.GrafiteTypes.universe t + ~automation_cache:status.GrafiteTypes.automation_cache t | GrafiteAst.We_proceed_by_cases_on (_, t, t1) -> Declarative.we_proceed_by_cases_on t t1 | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> @@ -197,14 +197,14 @@ let rec tactic_of_ast status ast = | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) -> Declarative.existselim ~dbd:(LibraryDb.instance()) - ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2 + ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2 | GrafiteAst.Case (_,id,params) -> Declarative.case id params | GrafiteAst.AndElim(_,just,id1,t1,id2,t2) -> Declarative.andelim ~dbd:(LibraryDb.instance ()) - ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2 + ~automation_cache:status.GrafiteTypes.automation_cache just id1 t1 id2 t2 | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) - ~universe:status.GrafiteTypes.universe termine t1 t2 cont + ~automation_cache:status.GrafiteTypes.automation_cache termine t1 t2 cont let classify_tactic tactic = match tactic with @@ -631,9 +631,14 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteAst.Index (loc,None,uri) -> assert false (* TODO: for user input *) | GrafiteAst.Index (loc,Some key,uri) -> - let universe = Universe.index - status.GrafiteTypes.universe key (CicUtil.term_of_uri uri) in - let status = {status with GrafiteTypes.universe = universe} in + let universe = + status.GrafiteTypes.automation_cache.AutomationCache.univ + in + let universe = Universe.index universe key (CicUtil.term_of_uri uri) in + let cache = { + status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } + in + let status = { status with GrafiteTypes.automation_cache = cache } in (* debug let msg = let candidates = Universe.get_candidates status.GrafiteTypes.universe key in diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 5a746f41c..999d96136 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -77,12 +77,13 @@ let add_obj ~pack_coercion_obj uri obj status = in let universe,status = List.fold_left add_to_universe - (status.GrafiteTypes.universe,status) + (status.GrafiteTypes.automation_cache.AutomationCache.univ,status) uris_to_index in + let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in {status with GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects; - GrafiteTypes.universe = universe}, + GrafiteTypes.automation_cache = cache }, lemmas let add_coercion ~pack_coercion_obj ~add_composites status uri arity @@ -120,7 +121,7 @@ let initial_status lexicon_status baseuri = { proof_status = GrafiteTypes.No_proof; objects = []; coercions = CoercDb.empty_coerc_db; - universe = Universe.empty; + automation_cache = AutomationCache.empty; baseuri = baseuri; ng_status = GrafiteTypes.CommandMode lexicon_status; } diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index fc81efcaf..66da43c8f 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -53,7 +53,7 @@ type status = { proof_status: proof_status; objects: UriManager.uri list; coercions: CoercDb.coerc_db; - universe:Universe.universe; + automation_cache:AutomationCache.cache; baseuri: string; ng_status: ng_status; } diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index 22386ebbf..e75c8aa3c 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -51,7 +51,7 @@ type status = { proof_status: proof_status; objects: UriManager.uri list; coercions: CoercDb.coerc_db; - universe:Universe.universe; + automation_cache:AutomationCache.cache; baseuri: string; ng_status: ng_status; } diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index f3c6a8bd1..25e67131f 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,2 +1,5 @@ +utf8Macro.cmi: +utf8MacroTable.cmo: +utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index a278f6f08..9dca5c5fb 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,11 +1,19 @@ +proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi +proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi +hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi +universe.cmi: autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: +paramodulation/utils.cmi: +closeCoercionGraph.cmi: +paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -16,6 +24,7 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/indexing.cmi paramodulation/equality.cmi +automationCache.cmi: universe.cmi paramodulation/saturation.cmi variousTactics.cmi: proofEngineTypes.cmi compose.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi @@ -25,10 +34,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: universe.cmi proofEngineTypes.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi +inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi +fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi +history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi @@ -106,6 +118,10 @@ paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ paramodulation/indexing.cmx paramodulation/founif.cmx \ paramodulation/equality.cmx paramodulation/saturation.cmi +automationCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ + automationCache.cmi +automationCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \ + automationCache.cmi variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ variousTactics.cmi variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index 7c9f00db5..ecc21a5db 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/components/tactics/Makefile @@ -17,6 +17,7 @@ INTERFACE_FILES = \ paramodulation/equality_indexing.mli\ paramodulation/indexing.mli \ paramodulation/saturation.mli \ + automationCache.mli \ variousTactics.mli \ compose.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index f78dbce75..a01ca8691 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -689,10 +689,10 @@ let universe_of_params metasenv context universe tl = (***************** applyS *******************) let new_metasenv_and_unify_and_t - dbd flags universe proof goal ?tables newmeta' metasenv' + dbd flags automation_cache proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity = - let ppterm = ppterm context in +(* let ppterm = ppterm context in *) let (consthead,newmetasenv,arguments,_) = TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let term'' = @@ -728,6 +728,8 @@ let new_metasenv_and_unify_and_t (PrimitiveTactics.apply_tac term'') (proof''',goal) in + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in let (active, passive,bag), cache, maxm = init_cache_and_tables ~dbd flags.use_library false (* was true *) true false universe @@ -764,7 +766,7 @@ let rec count_prods context ty = | _ -> 0 let apply_smart - ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) + ~dbd ~term ~subst ~automation_cache ?tables ~params:(univ,params) (proof, goal) = let module T = CicTypeChecker in let module R = CicReduction in @@ -772,7 +774,11 @@ let apply_smart let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params ~for_applyS:true () in + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in let universe = universe_of_params metasenv context universe univ in + let automation_cache = { automation_cache with AutomationCache.univ = universe } in + let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -813,7 +819,7 @@ let apply_smart let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in let goal_arity = count_prods context ty in let proof, gl, active, passive = - new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables + new_metasenv_and_unify_and_t dbd flags automation_cache proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity in proof, gl, active, passive @@ -1635,12 +1641,12 @@ let auto flags metasenv tables universe cache context metasenv gl = None,cache ;; -let applyS_tac ~dbd ~term ~params ~universe = +let applyS_tac ~dbd ~term ~params ~automation_cache = ProofEngineTypes.mk_tactic (fun status -> try let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~params ~universe status + apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status in proof, gl with @@ -1648,10 +1654,12 @@ let applyS_tac ~dbd ~term ~params ~universe = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) -let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = +let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) = let _,metasenv,_subst,_,_, _ = proof in let _,context,goalty = CicUtil.lookup_meta goal metasenv in let flags = flags_of_params params () in + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in let universe = universe_of_params metasenv context universe univ in let use_library = flags.use_library in let tables,cache,newmeta = @@ -1689,8 +1697,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; -let auto_tac ~dbd ~params ~universe = - ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);; +let auto_tac ~dbd ~params ~automation_cache = + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);; let eq_of_goal = function | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri -> @@ -1700,10 +1708,12 @@ let eq_of_goal = function (* performs steps of rewrite with the universe, obtaining if possible * a trivial goal *) -let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= +let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)= let _,metasenv,_subst,_,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let steps = int_of_string (string params "steps" "1") in + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in let universe = universe_of_params metasenv context universe univ in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = @@ -1736,8 +1746,8 @@ let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= (ProofEngineTypes.Fail (lazy ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) ;; -let solve_rewrite_tac ~params ~universe () = - ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params) +let solve_rewrite_tac ~params ~automation_cache () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params) ;; (* Demodulate thorem *) @@ -1796,7 +1806,7 @@ let is_subsumed univ context ty = ) None candidates ;; -let demodulate_theorem ~universe uri = +let demodulate_theorem ~automation_cache uri = let eq_uri = match LibraryObjects.eq_URI () with | Some (uri) -> uri @@ -1819,6 +1829,8 @@ let demodulate_theorem ~universe uri = MetadataQuery.close_with_types set [] context in (* retrieve equations from the universe universe *) + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in let equations = retrieve_equations true signature universe AutoCache.cache_empty context [] in @@ -1879,9 +1891,11 @@ let demodulate_theorem ~universe uri = (* NEW DEMODULATE *) -let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= +let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + (* XXX automation_cache *) + let universe = automation_cache.AutomationCache.univ in let universe = universe_of_params metasenv context universe univ in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let initgoal = [], metasenv, ty in @@ -1933,8 +1947,8 @@ let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd ~params ~universe = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);; +let demodulate_tac ~dbd ~params ~automation_cache = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);; let pp_proofterm = Equality.pp_proofterm;; diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index a45083f39..d5297e7b8 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -28,30 +28,30 @@ type auto_params = Cic.term list * (string * string) list val auto_tac: dbd:HSql.dbd -> params:auto_params -> - universe:Universe.universe -> + automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic val applyS_tac: dbd:HSql.dbd -> term: Cic.term -> params:auto_params -> - universe:Universe.universe -> + automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic val demodulate_tac : dbd:HSql.dbd -> params:auto_params -> - universe:Universe.universe -> + automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic val demodulate_theorem : - universe:Universe.universe -> + automation_cache:AutomationCache.cache -> UriManager.uri -> Cic.term * Cic.term val solve_rewrite_tac: params:auto_params -> - universe:Universe.universe -> + automation_cache:AutomationCache.cache -> unit -> ProofEngineTypes.tactic type auto_status = diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml new file mode 100644 index 000000000..84d4c8448 --- /dev/null +++ b/helm/software/components/tactics/automationCache.ml @@ -0,0 +1,36 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type cache = { + univ : Universe.universe; + tables : Saturation.active_table * Saturation.passive_table; +} + + +let empty = { + univ = Universe.empty; + tables = (Saturation.make_active [], Saturation.make_passive []); +} + diff --git a/helm/software/components/tactics/automationCache.mli b/helm/software/components/tactics/automationCache.mli new file mode 100644 index 000000000..00fb516e2 --- /dev/null +++ b/helm/software/components/tactics/automationCache.mli @@ -0,0 +1,33 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type cache = { + univ : Universe.universe; + tables : Saturation.active_table * Saturation.passive_table; +} + + +val empty : cache + diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index be4724b55..79e627409 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -25,11 +25,11 @@ type just = [ `Term of Cic.term | `Auto of Auto.auto_params ] -let mk_just ~dbd ~universe = +let mk_just ~dbd ~automation_cache = function `Auto (l,params) -> Tactics.auto ~dbd - ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~universe + ~params:(l,("skip_trie_filtering","1")::("skip_context","1")::params) ~automation_cache | `Term t -> Tactics.apply t ;; @@ -55,8 +55,8 @@ let suppose t id ty = (fun _ metasenv ugraph -> ty,metasenv,ugraph)) ;; -let by_just_we_proved ~dbd ~universe just ty id ty' = - let just = mk_just ~dbd ~universe just in +let by_just_we_proved ~dbd ~automation_cache just ty id ty' = + let just = mk_just ~dbd ~automation_cache just in match id with None -> (match ty' with @@ -89,8 +89,8 @@ let by_just_we_proved ~dbd ~universe just ty id ty' = ~continuations:[ Tacticals.id_tac ; continuation ] ;; -let bydone ~dbd ~universe just = - mk_just ~dbd ~universe just +let bydone ~dbd ~automation_cache just = + mk_just ~dbd ~automation_cache just ;; let we_need_to_prove t id ty = @@ -128,7 +128,7 @@ let we_need_to_prove t id ty = ProofEngineTypes.mk_tactic aux ;; -let existselim ~dbd ~universe just id1 t1 id2 t2 = +let existselim ~dbd ~automation_cache just id1 t1 id2 t2 = let aux (proof, goal) = let (n,metasenv,_subst,bo,ty,attrs) = proof in let metano,context,_ = CicUtil.lookup_meta goal metasenv in @@ -144,13 +144,13 @@ let existselim ~dbd ~universe just id1 t1 id2 t2 = fun _ _ _ ~typ -> incr i; if !i = 1 then Cic.Name id1 else Cic.Name id2) ; - (mk_just ~dbd ~universe just) + (mk_just ~dbd ~automation_cache just) ]) (proof', goal) in ProofEngineTypes.mk_tactic aux ;; -let andelim ~dbd ~universe just id1 t1 id2 t2 = +let andelim ~dbd ~automation_cache just id1 t1 id2 t2 = Tacticals.thens ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/And.ind", 0, []); t1 ; t2])) ~continuations: @@ -160,10 +160,10 @@ let andelim ~dbd ~universe just id1 t1 id2 t2 = fun _ _ _ ~typ -> incr i; if !i = 1 then Cic.Name id1 else Cic.Name id2) ; - (mk_just ~dbd ~universe just) ] + (mk_just ~dbd ~automation_cache just) ] ;; -let rewritingstep ~dbd ~universe lhs rhs just last_step = +let rewritingstep ~dbd ~automation_cache lhs rhs just last_step = let aux ((proof,goal) as status) = let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in let _,context,gty = CicUtil.lookup_meta goal metasenv in @@ -189,14 +189,14 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = else params in if params = params' then - Tactics.auto ~dbd ~params:(univ, params) ~universe + Tactics.auto ~dbd ~params:(univ, params) ~automation_cache else Tacticals.first - [Tactics.auto ~dbd ~params:(univ, params) ~universe ; - Tactics.auto ~dbd ~params:(univ, params') ~universe] + [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ; + Tactics.auto ~dbd ~params:(univ, params') ~automation_cache] | `Term just -> Tactics.apply just | `SolveWith term -> - Tactics.solve_rewrite ~universe ~params:([term],["steps","1"]) () + Tactics.solve_rewrite ~automation_cache ~params:([term],["steps","1"]) () | `Proof -> Tacticals.id_tac in diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli index 987663e15..21e49b8e2 100644 --- a/helm/software/components/tactics/declarative.mli +++ b/helm/software/components/tactics/declarative.mli @@ -30,11 +30,11 @@ val assume : string -> Cic.term -> ProofEngineTypes.tactic val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic val by_just_we_proved : - dbd:HSql.dbd -> universe:Universe.universe -> + dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> just -> Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic -val bydone : dbd:HSql.dbd -> universe:Universe.universe -> +val bydone : dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> just -> ProofEngineTypes.tactic val we_need_to_prove : @@ -51,15 +51,15 @@ val thesisbecomes : Cic.term -> ProofEngineTypes.tactic val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic val existselim : - dbd:HSql.dbd -> universe:Universe.universe -> just -> + dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> just -> string -> Cic.term -> string -> Cic.lazy_term -> ProofEngineTypes.tactic val andelim : - dbd:HSql.dbd -> universe:Universe.universe -> just -> + dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> just -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic val rewritingstep : - dbd:HSql.dbd -> universe:Universe.universe -> + dbd:HSql.dbd -> automation_cache:AutomationCache.cache -> (string option * Cic.term) option -> Cic.term -> [ `Term of Cic.term | `Auto of Auto.auto_params | `Proof | `SolveWith of Cic.term] -> diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 927ae8102..fa9d4ed8b 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jul 2 19:37:38 CEST 2008 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 16 11:28:06 CEST 2009 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyP : term:Cic.term -> ProofEngineTypes.tactic @@ -6,12 +6,12 @@ val applyS : dbd:HSql.dbd -> term:Cic.term -> params:Auto.auto_params -> - universe:Universe.universe -> ProofEngineTypes.tactic + automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic val auto : dbd:HSql.dbd -> params:Auto.auto_params -> - universe:Universe.universe -> ProofEngineTypes.tactic + automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic val cases_intros : ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> @@ -35,7 +35,7 @@ val decompose : val demodulate : dbd:HSql.dbd -> params:Auto.auto_params -> - universe:Universe.universe -> ProofEngineTypes.tactic + automation_cache:AutomationCache.cache -> ProofEngineTypes.tactic val destruct : Cic.term list option -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> @@ -100,7 +100,7 @@ val ring : ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val solve_rewrite : params:Auto.auto_params -> - universe:Universe.universe -> unit -> ProofEngineTypes.tactic + automation_cache:AutomationCache.cache -> unit -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 3ff2d0349..a941bf088 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -512,7 +512,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let (_,menv,subst,_,_,_), _ = ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params - ~universe:grafite_status.GrafiteTypes.universe) proof_status + ~automation_cache:grafite_status.GrafiteTypes.automation_cache) + proof_status in let proof_term = let irl = -- 2.39.2