]> matita.cs.unibo.it Git - helm.git/commitdiff
Universe is used only locally to tactics/
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Apr 2009 09:46:57 +0000 (09:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Apr 2009 09:46:57 +0000 (09:46 +0000)
AutomationCache.cache is part of grafite_status and will
contain tables too

16 files changed:
helm/software/components/binaries/transcript/.depend.opt
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli
helm/software/components/syntax_extensions/.depend
helm/software/components/tactics/.depend
helm/software/components/tactics/Makefile
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/automationCache.ml [new file with mode: 0644]
helm/software/components/tactics/automationCache.mli [new file with mode: 0644]
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/declarative.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/matitaScript.ml

index efadc681eee16cb3cd170845fdd1c7549fbb89b0..f17459162ce81c0ad9c5352cca5e9d99f43cb81c 100644 (file)
@@ -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 
index 354413f1b9464307172ae2c18b3124887d3a07cd..1f32e8c9e2db06944bf86b6e4ca8938940093fca 100644 (file)
@@ -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
index 5a746f41c8ee727e9346bc7daec2eaaee61f63e0..999d961369324bd1c3be5df1661e244982cce0f1 100644 (file)
@@ -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;
   }
index fc81efcaf29bbffe8fc428799a135c62d900a304..66da43c8f36259edc8111f14014a658a42755f4b 100644 (file)
@@ -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;
 }
index 22386ebbf9b8a2c0a2753f6d7a400d30e29d2ff6..e75c8aa3c565913032cb096127693052380df6c5 100644 (file)
@@ -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;
 }
index f3c6a8bd17a7351e99ce8e59905fda76a37cbf08..25e67131fca0487c4390d310d8307722b5058067 100644 (file)
@@ -1,2 +1,5 @@
+utf8Macro.cmi: 
+utf8MacroTable.cmo: 
+utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
index a278f6f0836f66a12becb40648662f44c709a1e6..9dca5c5fbeb7d5098d990edb4c241476bccb73da 100644 (file)
@@ -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 \
index 7c9f00db5f42d10f25d851cca0e6d3df09fbd1a3..ecc21a5db402b75730053217392c4bbf4996e06d 100644 (file)
@@ -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 \
index f78dbce75976c26416cccd679af13af08694bbf9..a01ca86913eedfbe9789997c54d3e9c0576bfb24 100644 (file)
@@ -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;;
 
index a45083f390da6b1521606bfb424149f286b3f428..d5297e7b84eddfe62e7bd995356be43045b81e00 100644 (file)
@@ -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 (file)
index 0000000..84d4c84
--- /dev/null
@@ -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 (file)
index 0000000..00fb516
--- /dev/null
@@ -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
+
index be4724b55509124678137083d36c040e519d8dab..79e627409ed5794f451f23b40c13316bde7e3379 100644 (file)
 
 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
index 987663e15ebb929c346b66a59d848f7009539cef..21e49b8e2e3ef40bfe290ce76e6c22c321800374 100644 (file)
@@ -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] ->
index 927ae8102e06c4f05a18f0bf04fb09616f873876..fa9d4ed8bfa5e059ca19bc5c9a4b2c341e28e4ff 100644 (file)
@@ -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
index 3ff2d034901f15bbf175e2630dc993d90d3356f8..a941bf0883476f87144b7fdafcb3dab8ff59725d 100644 (file)
@@ -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 =