X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=43211ccf93cf76f5fa393c5d21511b91fb77399c;hb=18c6848695fbfa97508e0981f6875a6459429a58;hp=b9f165edb2d3c83ef3506357631d3228d0b49726;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index b9f165edb..43211ccf9 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -449,7 +449,7 @@ let unification metasenv context t1 t2 ugraph =
 ;;
 
 
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
 
 exception MatchingFailure;;
 
@@ -590,6 +590,7 @@ let find_equalities context proof =
 ;;
 
 
+(*
 let equations_blacklist =
   List.fold_left
     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
@@ -622,6 +623,9 @@ let equations_blacklist =
       "cic:/matita/logic/equality/eq_rect.con";
     ]
 ;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
 
 let find_library_equalities dbd context status maxmeta = 
   let module C = Cic in
@@ -724,13 +728,13 @@ let find_library_equalities dbd context status maxmeta =
   let uriset, eqlist = 
     (List.fold_left
        (fun (s, l) (u, e) ->
-          if List.exists (meta_convertibility_eq e) l then (
+          if List.exists (meta_convertibility_eq e) (List.map snd l) then (
             debug_print
               (lazy
                  (Printf.sprintf "NO!! %s already there!"
                     (string_of_equality e)));
             (UriManager.UriSet.add u s, l)
-          ) else (UriManager.UriSet.add u s, e::l))
+          ) else (UriManager.UriSet.add u s, (u, e)::l))
        (UriManager.UriSet.empty, []) found)
   in
   uriset, eqlist, maxm
@@ -911,9 +915,38 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 
-let is_identity ((_, context, ugraph) as env) = function
-  | ((_, _, (ty, left, right, _), _, _) as equality) ->
-      (left = right ||
-          (meta_convertibility left right) ||
-          (fst (CicReduction.are_convertible context left right ugraph)))
+let is_identity ((metasenv, context, ugraph) as env) = function
+  | ((_, _, (ty, left, right, _), menv, _) as equality) ->
+      (prerr_endline ("left = "^(CicPp.ppterm left));
+       prerr_endline ("right = "^(CicPp.ppterm right));
+       (left = right ||
+          (* (meta_convertibility left right) || *)
+          (fst (CicReduction.are_convertible 
+		  ~metasenv:(metasenv @ menv) context left right ugraph))))
+;;
+
+
+let term_of_equality equality =
+  let _, _, (ty, left, right, _), menv, args = equality in
+  let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
+  let argsno = List.length args in
+  let t =
+    CicSubstitution.lift argsno
+      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+  in
+  snd (
+    List.fold_right
+      (fun a (n, t) ->
+         match a with
+         | Cic.Meta (i, _) ->
+             let name = Cic.Name ("X" ^ (string_of_int n)) in
+             let _, _, ty = CicUtil.lookup_meta i menv in
+             let t = 
+               ProofEngineReduction.replace
+                 ~equality:eq ~what:[i]
+                 ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
+             in
+             (n-1, Cic.Prod (name, ty, t))
+         | _ -> assert false)
+      args (argsno, t))
 ;;