auto snapshot

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 83588d24d5a7987da65242326adeda5a9bf07567..cf093473c7e77088bbffdb219382cbabfc5d9426 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -745,7 +745,8 @@ let rec simpl eq_uri env e others others_simpl =
   let active = others @ others_simpl in
   let tbl =
     List.fold_left
-      (fun t e -> Indexing.index t e)
+      (fun t e -> 
+        if Equality.is_weak_identity e then t else Indexing.index t e)
       Indexing.empty active
   in
   let res = forward_simplify eq_uri env e (active, tbl) in
@@ -807,7 +808,7 @@ let pp_goal_set msg goals names =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-  let names = Utils.names_of_context ctx in
+(*   let names = Utils.names_of_context ctx in *)
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when LibraryObjects.is_eq_URI uri ->
@@ -1212,7 +1213,7 @@ let eq_and_ty_of_goal = function
 let saturate 
     caso_strano 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) 
-    ?(timeout=600.) status = 
+    ?(timeout=600.) ?auto status = 
   let module C = Cic in
   reset_refs ();
   Indexing.init_index ();
@@ -1226,15 +1227,27 @@ let saturate
   let cleaned_goal = Utils.remove_local_context type_of_goal in
   Utils.set_goal_symbols cleaned_goal;
   let names = Utils.names_of_context context in
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
+  let eq_indexes, equalities, maxm, universe, cache = 
+    Inference.find_equalities ?auto context proof AutoTypes.cache_empty
+  in
+  prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
-    let lib_eq_uris, library_equalities, maxm =
-      Inference.find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
+    let lib_eq_uris, library_equalities, maxm, universe, cache =
+      Inference.find_library_equalities 
+        ?auto caso_strano dbd context (proof, goalno) (maxm+2)
+        ?universe cache
     in
+    prerr_endline ">>>>>>>>>>  gained from the library >>>>>>>>>>>>";
+    List.iter
+      (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) 
+      library_equalities;
+    prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
     let library_equalities = List.map snd library_equalities in
     let t2 = Unix.gettimeofday () in
     maxmeta := maxm+2;
@@ -1246,15 +1259,10 @@ let saturate
          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
     let t1 = Unix.gettimeofday () in
     let theorems =
-      if full then
-        let thms = Inference.find_library_theorems dbd env (proof, goalno) lib_eq_uris in
-        let context_hyp = Inference.find_context_hypotheses env eq_indexes in
-        context_hyp @ thms, []
-      else
-        let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
-        let t = CicUtil.term_of_uri refl_equal in
-        let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-        [(t, ty, [])], []
+      let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
+      let t = CicUtil.term_of_uri refl_equal in
+      let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+      [(t, ty, [])], []
     in
     let t2 = Unix.gettimeofday () in
     let _ =
@@ -1432,12 +1440,15 @@ let retrieve_and_print dbd term metasenv ugraph =
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
+  let eq_indexes, equalities, maxm,universe,cache = 
+    Inference.find_equalities context proof AutoTypes.cache_empty in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in
   let t1 = Unix.gettimeofday () in
-  let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in
+  let lib_eq_uris, library_equalities, maxm, unvierse, cache =
+    Inference.find_library_equalities 
+      false dbd context (proof, goal') (maxm+2) ?universe cache
+  in 
   let t2 = Unix.gettimeofday () in
   maxmeta := maxm+2;
   let equalities = (* equalities @ *) library_equalities in
@@ -1512,9 +1523,11 @@ let main_demod_equalities dbd term metasenv ugraph =
   let _, metasenv, meta_proof, _ = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let eq_uri = eq_of_goal goal in 
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
-  let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities false dbd context (proof, goal') (maxm+2)
+  let eq_indexes, equalities, maxm, universe, cache = 
+    Inference.find_equalities context proof AutoTypes.cache_empty in
+  let lib_eq_uris, library_equalities, maxm,universe,cache =
+    Inference.find_library_equalities 
+      false dbd context (proof, goal') (maxm+2) ?universe cache
   in
   let library_equalities = List.map snd library_equalities in
   maxmeta := maxm+2; (* TODO ugly!! *)
@@ -1589,11 +1602,13 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let eq_uri = eq_of_goal ty in 
-  let eq_indexes, equalities, maxm = 
-    Inference.find_equalities context proof 
+  let eq_indexes, equalities, maxm, universe, cache = 
+    Inference.find_equalities context proof AutoTypes.cache_empty
+  in
+  let lib_eq_uris, library_equalities, maxm, universe, cache =
+    Inference.find_library_equalities 
+      false dbd context (proof, goal) (maxm+2) ?universe cache 
   in
-  let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in
@@ -1668,7 +1683,9 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   let eq_uri,tty = eq_and_ty_of_goal ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let names = Utils.names_of_context context in
-  let eq_index, equalities, maxm = Inference.find_equalities context proof in
+  let eq_index, equalities, maxm,universe,cache  = 
+    Inference.find_equalities context proof AutoTypes.cache_empty 
+  in
   let eq_what = 
     let what = find_in_ctx 1 target context in
     List.nth equalities (position_of 0 what eq_index)