X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality_retrieval.ml;h=962304d41ac8d7c28df9dc9cfffebdd6242aac18;hb=61f3a8a688132be943b81befa5805e27148f2038;hp=4637a1a4342a1a389a45a6a504d719fd57146b9b;hpb=2eaee49a7ff3ed74598a0db84ce4dbc5bca92380;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality_retrieval.ml b/helm/software/components/tactics/paramodulation/equality_retrieval.ml
index 4637a1a43..962304d41 100644
--- a/helm/software/components/tactics/paramodulation/equality_retrieval.ml
+++ b/helm/software/components/tactics/paramodulation/equality_retrieval.ml
@@ -133,12 +133,12 @@ let equations_blacklist =
 *)
 let equations_blacklist = UriManager.UriSet.empty;;
 
-(* {{{ ****************** SATURATION STUFF ***************************)
-exception UnableToSaturate of AutoCache.cache * int
+(*****************************************************************)
+exception AutoFailure of AutoCache.cache * int
 
-let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
+let default_auto maxm _ _ _ c _ = [],c,maxm ;; 
 
-let saturate_term context metasenv oldnewmeta term cache auto fast = 
+let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast = 
   let head, metasenv, args, newmeta =
     ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
   in
@@ -181,7 +181,7 @@ let saturate_term context metasenv oldnewmeta term cache auto fast =
            use_paramod=true;use_only_paramod=false} 
       in
       match auto newmeta flags proof context cache args_for_auto with
-      | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
+      | [],cache,newmeta -> raise (AutoFailure (cache,newmeta))
       | substs,cache,newmeta ->
           List.map 
             (fun subst ->
@@ -202,7 +202,7 @@ let saturate_term context metasenv oldnewmeta term cache auto fast =
 (* }}} ***************************************************************)
 
 let find_context_equalities 
-  maxmeta bag ?(auto = default_auto) context proof cache 
+  maxmeta bag auto context proof cache 
 =
   prerr_endline "find_equalities";
   let module C = Cic in
@@ -210,6 +210,12 @@ let find_context_equalities
   let module T = CicTypeChecker in
   let _,metasenv,_,_ = proof in
   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+  let auto =
+    match auto with
+      | None -> default_auto
+      | Some auto -> auto in
+  (* if use_auto is true, we try to close the hypothesis of equational
+    statements using auto; a naif, and probably wrong approach *)
   let rec aux cache index newmeta = function
     | [] -> [], newmeta,cache
     | (Some (_, C.Decl (term)))::tl ->
@@ -222,7 +228,7 @@ let find_context_equalities
               (try 
                 let term = S.lift index term in
                 let saturated,cache,newmeta = 
-                  saturate_term context metasenv newmeta term 
+                  close_hypothesis_of_term context metasenv newmeta term 
                     cache auto false
                 in
                 let eqs,newmeta = 
@@ -236,7 +242,7 @@ let find_context_equalities
                    ([],newmeta) saturated
                 in
                  eqs, newmeta, cache
-              with UnableToSaturate (cache,newmeta) ->
+              with AutoFailure (cache,newmeta) ->
                 [],newmeta,cache)
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
               when LibraryObjects.is_eq_URI uri ->
@@ -261,7 +267,7 @@ let find_context_equalities
 ;;
 
 let find_library_equalities bag
-  ?(auto = default_auto) caso_strano dbd context status maxmeta cache 
+  auto caso_strano dbd context status maxmeta cache 
 = 
   let module C = Cic in
   let module S = CicSubstitution in
@@ -296,6 +302,12 @@ let find_library_equalities bag
  let candidates = List.map utty_of_u eqs in
  let candidates = List.filter is_monomorphic_eq candidates in
  let candidates = List.filter is_var_free candidates in
+ let auto =
+    match auto with
+      | None -> default_auto
+      | Some auto -> auto in
+  (* if use_auto is true, we try to close the hypothesis of equational
+    statements using auto; a naif, and probably wrong approach *)
  let rec aux cache newmeta = function
     | [] -> [], newmeta, cache
     | (uri, term, termty)::tl ->
@@ -308,7 +320,7 @@ let find_library_equalities bag
           | C.Prod (name, s, t) ->
               (try
                 let saturated,cache,newmeta = 
-                  saturate_term context metasenv newmeta termty 
+                  close_hypothesis_of_term context metasenv newmeta termty 
                     cache auto true
                 in
                 let eqs,newmeta = 
@@ -327,7 +339,7 @@ let find_library_equalities bag
                    ([],newmeta) saturated
                 in
                  eqs, newmeta , cache
-              with UnableToSaturate (cache,newmeta) ->
+               with AutoFailure (cache,newmeta) ->
                 [], newmeta , cache)
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> 
               let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in