Two bugs fixed in the apply tactic:

[helm.git] / helm / ocaml / paramodulation / inference.ml

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 09a0234575e2dc918d116500ea80ba4f981b403e..969d412cef43a28151e995250fdf10d2adc172c4 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -373,8 +373,10 @@ let replace_metas (* context *) term =
   in
   aux term
 ;;
+*)
 
 
+(*
 let restore_metas (* context *) term =
   let module C = Cic in
   let rec aux = function
@@ -413,8 +415,9 @@ let restore_metas (* context *) term =
   in
   aux term
 ;;
+*)
 
-
+(*
 let rec restore_subst (* context *) subst =
   List.map
     (fun (i, (c, t, ty)) ->
@@ -438,6 +441,8 @@ let rec is_simple_term = function
   | Cic.Meta (i, l) -> check_irl 1 l
   | Cic.Rel _ -> true
   | Cic.Const _ -> true
+  | Cic.MutInd (_, _, []) -> true
+  | Cic.MutConstruct (_, _, _, []) -> true
   | _ -> false
 ;;
 
@@ -521,9 +526,12 @@ let unification_simple metasenv context t1 t2 ugraph =
 let unification metasenv context t1 t2 ugraph =
 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
   let subst, menv, ug =
-    if not (is_simple_term t1) || not (is_simple_term t2) then
+    if not (is_simple_term t1) || not (is_simple_term t2) then (
+      debug_print (
+        Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+          (CicPp.ppterm t1) (CicPp.ppterm t2));
       CicUnification.fo_unif metasenv context t1 t2 ugraph
-    else
+    ) else
       unification_simple metasenv context t1 t2 ugraph
   in
   let rec fix_term = function
@@ -1047,7 +1055,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
               let (head, newmetas, args, newmeta) =
                 ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term)
+                  context (S.lift index term) 0
               in
               let p =
                 if List.length args = 0 then
@@ -1109,6 +1117,10 @@ let equations_blacklist =
       "cic:/Coq/Init/Logic/sym_eq.con";
 (*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
 (*       "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
+
+      (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
+         perche' questo cacchio di teorema rompe le scatole :'( *)
+      "cic:/Rocq/SUBST/comparith/mult_n_2.con"; 
     ]
 ;;
 
@@ -1119,6 +1131,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let candidates =
     List.fold_left
       (fun l uri ->
+       let suri = UriManager.string_of_uri uri in
          if UriManager.UriSet.mem uri equations_blacklist then
            l
          else
@@ -1143,12 +1156,12 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
     | (term, termty)::tl ->
         debug_print (
           Printf.sprintf "Examining: %s (%s)"
-            (CicPp.ppterm term) (CicPp.ppterm termty));
+            (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty));
         let res, newmeta = 
           match termty with
           | C.Prod (name, s, t) ->
               let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty
+                ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
               let p =
                 if List.length args = 0 then
@@ -1182,7 +1195,16 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
         | None ->
             aux newmeta tl
   in
-  aux maxmeta candidates
+  let found, maxm = aux maxmeta candidates in
+  (List.fold_left
+     (fun l e ->
+        if List.exists (meta_convertibility_eq e) l then (
+          debug_print (
+            Printf.sprintf "NO!! %s already there!" (string_of_equality e));
+          l
+        )
+        else e::l)
+     [] found), maxm
 ;;