X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=f040241223bf3996f0972f3df4a4fcc8acbb89be;hb=0d1ecc789c6d57a3eef47a028634d316905ef317;hp=e2f85fa2b4acce69dfa6604b1c92799234771bf1;hpb=50844b0116c863862434c7c673c5caaf6ff78cdf;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index e2f85fa2b..f04024122 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
@@ -70,7 +70,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   let lookup = Subst.lookup_subst in
   let rec occurs_check subst what where =
     match where with
-    | t when what = t -> true
+    | Cic.Meta(i,_) when i = what -> true
     | C.Appl l -> List.exists (occurs_check subst what) l
     | C.Meta _ ->
         let t = lookup where subst in
@@ -84,6 +84,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     in
     match s, t with
     | s, t when s = t -> subst, menv
+    (* sometimes the same meta has different local contexts; this
+       could create "cyclic" substitutions *)
+    | C.Meta (i, _), C.Meta (j, _) when i=j ->  subst, menv
     | C.Meta (i, _), C.Meta (j, _) 
         when (locked locked_menv i) &&(locked locked_menv j) ->
         raise
@@ -92,7 +95,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
         unif subst menv t s
     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
         unif subst menv t s
-    | C.Meta _, t when occurs_check subst s t ->
+    | C.Meta (i,_), t when occurs_check subst i t ->
         raise
           (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t when (locked locked_menv i) -> 
@@ -240,7 +243,8 @@ let find_equalities context proof =
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
-                    let w = compute_equality_weight stat in
+                    (* let w = compute_equality_weight stat in *)
+                    let w = 0 in 
                     let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
@@ -316,10 +320,10 @@ let equations_blacklist =
 let equations_blacklist = UriManager.UriSet.empty;;
 
 let tty_of_u u = 
-  let _ = <:start<tty_of_u>> in
+(*   let _ = <:start<tty_of_u>> in *)
   let t = CicUtil.term_of_uri u in
   let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-  let _ = <:stop<tty_of_u>> in
+(*   let _ = <:stop<tty_of_u>> in *)
   t, ty
 ;;
 
@@ -328,13 +332,39 @@ let utty_of_u u =
   u, t, ty
 ;;
 
-let find_library_equalities dbd context status maxmeta = 
+let find_library_equalities caso_strano dbd context status maxmeta = 
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _ = <:start<equations_for_goal>> in
-  let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
-  let _ = <:stop<equations_for_goal>> in
+(*   let _ = <:start<equations_for_goal>> in *)
+  let signature = 
+    if caso_strano then
+      begin
+        let proof, goalno = status in
+        let _,metasenv,_,_ = proof in
+        let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
+        match ty with
+        | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
+            (let mainl, sigl = MetadataConstraints.signature_of l in
+            let mainr, sigr = MetadataConstraints.signature_of r in
+            match mainl,mainr with
+            | Some (uril,tyl), Some (urir, tyr) 
+                when LibraryObjects.is_eq_URI uril && 
+                     LibraryObjects.is_eq_URI urir && 
+                     tyl = tyr ->
+                  Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
+            | _ -> 
+                let u = (UriManager.uri_of_string
+                  (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
+                let main = Some (u, []) in
+                Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
+        | _ -> assert false
+      end
+    else
+      None
+  in
+  let eqs = (MetadataQuery.equations_for_goal ~dbd ?signature status) in
+(*   let _ = <:stop<equations_for_goal>> in *)
   let candidates =
     List.fold_left
       (fun l uri ->
@@ -490,4 +520,4 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
-let get_stats () = <:show<Inference.>> ;;
+let get_stats () = "" (*<:show<Inference.>>*) ;;