removed bad guard that was always false (assert false in the line above)

[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 11966ef8d016ef7eb8dba7a7e4a2cda72d3882eb..b52e074fd1f5317e096322e43b9e46bd6f3ae0cd 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -438,21 +438,22 @@ let check_for_deep_subsumption env active_table eq =
 
 (** simplifies current using active and passive *)
 let forward_simplify bag eq_uri env current (active_list, active_table) =
+  prerr_endline (Equality.string_of_equality ~env current);
   let _, context, _ = env in
   let demodulate table current = 
     let newmeta, newcurrent =
       Indexing.demodulation_equality bag eq_uri !maxmeta env table current
     in
     maxmeta := newmeta;
-    if Equality.is_identity env newcurrent then None else Some newcurrent
+    if Equality.is_weak_identity newcurrent then None else Some newcurrent
   in
-  let rec demod current =
+  let demod current =
     if Utils.debug_metas then
       ignore (Indexing.check_target bag context current "demod0");
     let res = demodulate active_table current in
-      if Utils.debug_metas then
-        ignore ((function None -> () | Some x -> 
-                   ignore (Indexing.check_target bag context x "demod1");()) res);
+    if Utils.debug_metas then
+      ignore ((function None -> () | Some x -> 
+      ignore (Indexing.check_target bag context x "demod1");()) res);
     res
   in 
   let res = demod current in
@@ -556,7 +557,7 @@ let backward_simplify_active
       (fun eq ((res,pruned), tbl) ->
          if List.mem eq res then
            (res, (id_of_eq eq)::pruned),tbl 
-         else if (Equality.is_identity env eq) || (find eq res) then (
+         else if (Equality.is_weak_identity eq) || (find eq res) then (
            (res, (id_of_eq eq)::pruned),tbl
          ) 
          else
@@ -746,7 +747,10 @@ let rec simpl bag eq_uri env e others others_simpl =
          if Equality.is_weak_identity e then t else Indexing.index t e) 
       Indexing.empty active
   in
-  let res = forward_simplify bag eq_uri env e (active, tbl) in
+  let res = 
+    if Equality.is_weak_identity e then None else 
+      forward_simplify bag eq_uri env e (active, tbl) 
+  in
     match others with
       | hd::tl -> (
           match res with
@@ -846,7 +850,7 @@ let check_if_goal_is_identity env = function
     (let _,context,_ = env in
     try 
      let s,m,_ = 
-       Inference.unification m m context left right CicUniv.empty_ugraph 
+       Founif.unification m m context left right CicUniv.empty_ugraph 
      in
       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
       let m = Subst.apply_subst_metasenv s m in
@@ -1077,6 +1081,7 @@ let given_clause
           ParamodulationSuccess p
       | None -> 
 *)
+
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
@@ -1084,6 +1089,7 @@ let given_clause
                   let goals = 
                     infer_goal_set_with_current bag env current goals active 
                   in
+
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
 (*                   prerr_endline "fwd/back simpl"; *)
                   let rec simplify new' active passive =
@@ -1103,6 +1109,7 @@ let given_clause
                   let active, passive, new' = 
                     simplify new' active passive
                   in
+
 (*                   prerr_endline "simpl goal with new"; *)
                   let goals = 
                     let a,b,_ = build_table new' in
@@ -1360,13 +1367,13 @@ let find_equalities dbd status smart_flag ?auto cache =
   let env = (metasenv, context, CicUniv.empty_ugraph) in 
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm, cache = 
-    Inference.find_equalities 0 bag ?auto context proof cache
+    Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache
   in
   prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
   List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
   prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
   let lib_eq_uris, library_equalities, maxm, cache =
-    Inference.find_library_equalities bag
+    Equality_retrieval.find_library_equalities bag
       ?auto smart_flag dbd context (proof, goalno) (maxm+2)
       cache
   in
@@ -1394,15 +1401,23 @@ let saturate_more bag active maxmeta status smart_flag ?auto cache =
   let eq_uri = eq_of_goal type_of_goal in 
   let env = (metasenv, context, CicUniv.empty_ugraph) in 
   let eq_indexes, equalities, maxm, cache = 
-    Inference.find_equalities maxmeta bag ?auto context proof cache
+    Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache
   in
+  prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+    string_of_int maxm);
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) 
+    equalities;
+  prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
   let equalities = 
-(*
     HExtlib.filter_map 
       (fun e -> forward_simplify bag eq_uri env e active)
-*)
     equalities
   in
+  prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+  List.iter
+    (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
+  prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
   bag, equalities, cache, maxm
 
 let saturate 
@@ -1424,7 +1439,7 @@ let saturate
   let env = (metasenv, context, ugraph) in 
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   let bag, equalities, cache, maxm = 
-    find_equalities dbd status smart_flag ?auto AutoTypes.cache_empty 
+    find_equalities dbd status smart_flag ?auto AutoCache.cache_empty 
   in
   let res, time =
     maxmeta := maxm+2;
@@ -1508,6 +1523,10 @@ let given_clause
   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   let env = metasenv,context,CicUniv.empty_ugraph in
+  prerr_endline ">>>>>> ACTIVES >>>>>>>>"; 
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+  active_l;
+  prerr_endline ">>>>>>>>>>>>>>"; 
   let goals = make_goal_set goal in
   match 
     given_clause bag eq_uri env goals passive active 
@@ -1530,10 +1549,10 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
   let eq_uri = eq_of_goal ty in
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm, cache = 
-    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
   in
   let lib_eq_uris, library_equalities, maxm, cache =
-    Inference.find_library_equalities bag 
+    Equality_retrieval.find_library_equalities bag 
       false dbd context (proof, goal) (maxm+2)  cache 
   in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
@@ -1611,7 +1630,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   let names = Utils.names_of_context context in
   let bag = Equality.mk_equality_bag () in
   let eq_index, equalities, maxm,cache  = 
-    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty 
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty 
   in
   let eq_what = 
     let what = find_in_ctx 1 target context in
@@ -1693,7 +1712,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
 
 let get_stats () = "" 
 (*
-  <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
+  <:show<Saturation.>> ^ Indexing.get_stats () ^ Founif.get_stats () ^
   Equality.get_stats ()
 ;;
 *)
@@ -1716,12 +1735,12 @@ let retrieve_and_print dbd term metasenv ugraph =
   let eq_uri = eq_of_goal type_of_goal in
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm,cache = 
-    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.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, cache =
-    Inference.find_library_equalities bag
+    Equality_retrieval.find_library_equalities bag
       false dbd context (proof, goal') (maxm+2)  cache
   in 
   let t2 = Unix.gettimeofday () in
@@ -1800,9 +1819,9 @@ let main_demod_equalities dbd term metasenv ugraph =
   let eq_uri = eq_of_goal goal in 
   let bag = Equality.mk_equality_bag () in
   let eq_indexes, equalities, maxm,  cache = 
-    Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+    Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
   let lib_eq_uris, library_equalities, maxm,cache =
-    Inference.find_library_equalities bag
+    Equality_retrieval.find_library_equalities bag
       false dbd context (proof, goal') (maxm+2)  cache
   in
   let library_equalities = List.map snd library_equalities in