- init_cache_and_tables rewritten using the automation_cache

[helm.git] / helm / software / components / tactics / automationCache.ml

diff --git a/helm/software/components/tactics/automationCache.ml b/helm/software/components/tactics/automationCache.ml
index 84d4c8448e94e29ae4469fefa4f1031ee6019aaa..7d8e7d129d9032406c0e9f30cf6dcbb90fcfd0e3 100644 (file)
--- a/helm/software/components/tactics/automationCache.ml
+++ b/helm/software/components/tactics/automationCache.ml
@@ -23,14 +23,97 @@
  * http://cs.unibo.it/helm/.
  *)
 
+type tables = 
+  Saturation.active_table * Saturation.passive_table * Equality.equality_bag
+
 type cache = {
         univ : Universe.universe;
-        tables : Saturation.active_table * Saturation.passive_table;
+        tables : Saturation.active_table * 
+                 Saturation.passive_table *
+                 Equality.equality_bag;
 }
 
+let empty_tables () =
+  Saturation.make_active [], 
+  Saturation.make_passive [],
+  Equality.mk_equality_bag ()
+;;
 
-let empty = { 
+let empty () = { 
         univ = Universe.empty; 
-        tables = (Saturation.make_active [], Saturation.make_passive []);
+        tables = empty_tables ();
 }
 
+let pump cache steps = 
+  let active, passive, bag = cache.tables in
+  let active, passive, bag = 
+    Saturation.pump_actives 
+      [] bag active passive steps infinity
+  in
+  let tables = active, passive, bag in 
+  { cache with tables = tables }
+;;
+
+let add_term_to_active cache metasenv subst context t ty_opt =
+  let actives, passives, bag = cache.tables in
+  let bag, metasenv, head, t, args, mes, ugraph =
+    match ty_opt with
+    | Some ty -> 
+        bag, metasenv, ty, t, [], (CicUtil.metas_of_term (Cic.Appl [t;ty])),
+        CicUniv.oblivion_ugraph
+    | None -> 
+        let ty, ugraph = 
+          CicTypeChecker.type_of_aux' 
+            ~subst metasenv context t CicUniv.oblivion_ugraph
+        in
+        let bag, head, metasenv, args =
+          Equality.saturate_term bag metasenv context ty
+        in
+        let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
+        let t = if args = [] then t else Cic.Appl (t:: args) in
+        bag, metasenv, head, t, args, mes, ugraph
+  in
+  if List.exists 
+      (function 
+      | Cic.Meta(i,_) -> 
+          (try 
+            let _,mc, mt = CicUtil.lookup_meta i metasenv in
+            let sort, u = 
+               CicTypeChecker.type_of_aux' metasenv mc mt ugraph
+            in
+            fst (CicReduction.are_convertible mc sort (Cic.Sort Cic.Prop) u)
+          with
+          | CicUtil.Meta_not_found _ -> false)
+      | _ -> assert false)
+     args 
+  then
+    cache
+  else
+    let env = metasenv, context, CicUniv.oblivion_ugraph in 
+    let newmetas = 
+      List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv
+    in
+    let tables = 
+      Saturation.add_to_active bag actives passives env head t newmetas
+    in
+    { cache with tables = tables }
+;;
+
+let pp_cache cache =
+  prerr_endline "Automation cache";
+  prerr_endline "----------------------------------------------";
+  prerr_endline "universe:";      
+  Universe.iter cache.univ (fun _ ts ->
+    prerr_endline (" "^
+      String.concat "\n " (List.map CicPp.ppterm ts)));
+  prerr_endline "tables/actives:";      
+  let active, passive, _ = cache.tables in
+  List.iter 
+    (fun e -> prerr_endline (" " ^ Equality.string_of_equality e)) 
+    (Saturation.list_of_active active);
+  prerr_endline "tables/passives:";      
+  List.iter 
+    (fun e -> prerr_endline (" " ^ Equality.string_of_equality e)) 
+    (Saturation.list_of_passive passive);
+  prerr_endline "----------------------------------------------";
+;;