X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=7893ecba6142ef4a5934d3edc0fd18db3ec51a14;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=fcb4586cb4d8b2e0ecb2e1831797f11a2ef49605;hpb=cfbcef4637ff26ac4dfefe41bf2df29222e80138;p=helm.git

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index fcb4586cb..7893ecba6 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -260,7 +260,7 @@ let open_pred pred =
   match pred with 
   | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) 
      when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
-  | _ -> prerr_endline (CicPp.ppterm pred); assert false   
+  | _ -> Utils.debug_print (lazy (CicPp.ppterm pred)); assert false   
 ;;
 
 let is_not_fixed t =
@@ -290,7 +290,7 @@ let canonical t context menv =
        [] -> List.rev acc
      | (l',p)::tl when l=l' -> 
 if acc <> [] then
-prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
+Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"));
          cut_to_last_duplicate l [l',p] tl
      | (l',p)::tl ->
          cut_to_last_duplicate l ((l',p)::acc) tl
@@ -358,7 +358,7 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
                    Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
                  in
                  let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in
-                 prerr_endline ("CANONICAL " ^ CicPp.ppterm rc);
+                 Utils.debug_print (lazy ("CANONICAL " ^ CicPp.ppterm rc));
                  rc
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
@@ -371,12 +371,12 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
   
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
-    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+  ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
 ;;
 
 let put_in_ctx ctx t = 
   ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+  ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
 ;;
 
 let mk_eq uri ty l r =
@@ -581,8 +581,9 @@ let parametrize_proof p l r =
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(fun t1 t2 -> 
+    ~equality:(fun _ t1 t2 -> 
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
+    ~context:[]
     ~what ~with_what ~where:p
   in
   let ty_of_m _ = Cic.Implicit (Some `Type) in
@@ -1025,7 +1026,6 @@ let meta_convertibility_eq eq1 eq2 =
         false
 ;;
 
-
 let meta_convertibility t1 t2 =
   if t1 = t2 then
     true
@@ -1037,6 +1037,32 @@ let meta_convertibility t1 t2 =
       false
 ;;
 
+let meta_convertibility_subst t1 t2 menv =
+  if t1 = t2 then
+    Some([])
+  else
+    try
+      let (l,_) = meta_convertibility_aux ([],[]) t1 t2 in
+      let subst =
+	List.map
+	  (fun (x,y) ->
+	     try 
+	       let (_,c,t) = CicUtil.lookup_meta x menv in
+	       let irl = 
+		 CicMkImplicit.identity_relocation_list_for_metavariable c in
+	       (y,(c,Cic.Meta(x,irl),t))
+	     with CicUtil.Meta_not_found _ ->
+	       try 
+		 let (_,c,t) = CicUtil.lookup_meta y menv in
+		 let irl =  
+		   CicMkImplicit.identity_relocation_list_for_metavariable c in
+		   (x,(c,Cic.Meta(y,irl),t))
+	       with CicUtil.Meta_not_found _ -> assert false) l in   
+	Some subst
+    with NotMetaConvertible ->
+      None
+;;
+
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
@@ -1197,7 +1223,7 @@ let rec pp_proofterm name t context =
               when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] 
-              when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)->
+              when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)->
                 pp true p
           | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] 
               when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)->
@@ -1327,7 +1353,7 @@ let draw_proof bag names goal_proof proof id =
   let oc = open_out "/tmp/matita_paramod.dot" in
   Buffer.output_buffer oc b;
   close_out oc;
-  prerr_endline "dot!";
+  Utils.debug_print (lazy "dot!");
   ignore(Unix.system 
     "dot -Tps -o /tmp/matita_paramod.eps /tmp/matita_paramod.dot"
 (* "cat /tmp/matita_paramod.dot| tred | dot -Tps -o /tmp/matita_paramod.eps" *)