Changed auto from implicit to option and renamed a few functions.

[helm.git] / components / tactics / paramodulation / equality_retrieval.ml

diff --git a/components/tactics/paramodulation/equality_retrieval.ml b/components/tactics/paramodulation/equality_retrieval.ml
index 4637a1a4342a1a389a45a6a504d719fd57146b9b..886cc7ffe2e1ca03840279ea0d71d115d2c7cfd6 100644 (file)
--- a/components/tactics/paramodulation/equality_retrieval.ml
+++ b/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 _ _ _ _ _ = [],AutoCache.cache_empty,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 use_auto, auto =
+    match auto with
+      | None -> false, default_auto
+      | Some auto -> true, 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 ->
@@ -218,11 +224,11 @@ let find_context_equalities
              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
         let do_find context term =
           match term with
-          | C.Prod (name, s, t) when is_an_equality t ->
+          | C.Prod (name, s, t) when (is_an_equality t && use_auto) ->
               (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 use_auto, auto =
+    match auto with
+      | None -> false, default_auto
+      | Some auto -> true, 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 ->
@@ -305,10 +317,10 @@ let find_library_equalities bag
                 (CicPp.ppterm term) (CicPp.ppterm termty)));
         let res, newmeta, cache = 
           match termty with
-          | C.Prod (name, s, t) ->
+          | C.Prod (name, s, t) when use_auto ->
               (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,8 +339,9 @@ let find_library_equalities bag
                    ([],newmeta) saturated
                 in
                  eqs, newmeta , cache
-              with UnableToSaturate (cache,newmeta) ->
+               with AutoFailure (cache,newmeta) ->
                 [], newmeta , cache)
+          | C.Prod _ ->  [], newmeta, cache
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> 
               let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
               [e], newmeta+1, cache