X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Futils.ml;h=c2b1905f89f4f313ae4e2cd230ec301e889f883f;hb=ec7717f5e0dd4c295ba1cfd57a0a6a46170490ef;hp=b212d0faba862c580355b4db09b98ef6142120b7;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index b212d0fab..c2b1905f8 100644
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -25,7 +25,10 @@
 
 (* $Id$ *)
 
-let debug = true;;
+let time = true;;
+let debug = false;;
+let debug_metas = false;; 
+let debug_res = false;;
 
 let debug_print s = if debug then prerr_endline (Lazy.force s);;
 
@@ -38,8 +41,6 @@ let print_metasenv metasenv =
 ;;
 
 
-
-
 let print_subst ?(prefix="\n") subst =
     String.concat prefix
      (List.map
@@ -59,6 +60,8 @@ let string_of_comparison = function
   | Eq -> "="
   | Incomparable -> "I"
 
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
 module OrderedTerm =
 struct
   type t = Cic.term
@@ -227,7 +230,7 @@ let string_of_weight (cw, mw) =
   Printf.sprintf "[%d; %s]" cw s
 
 
-let weight_of_term ?(consider_metas=true) term =
+let weight_of_term ?(consider_metas=true) ?(count_metas_occurrences=false) term =
   let module C = Cic in
   let vars_dict = Hashtbl.create 5 in
   let rec aux = function
@@ -237,15 +240,15 @@ let weight_of_term ?(consider_metas=true) term =
            Hashtbl.replace vars_dict metano (oldw+1)
          with Not_found ->
            Hashtbl.add vars_dict metano 1);
-        0
-    | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*)
-                  
+        if count_metas_occurrences then 1 else 0
+    | C.Meta _ ->  (* "variables" are lighter than constants and functions...*)
+        if count_metas_occurrences then 1 else 0         
     | C.Var (_, ens)
     | C.Const (_, ens)
     | C.MutInd (_, _, ens)
     | C.MutConstruct (_, _, _, ens) ->
         List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens
-          
+         
     | C.Cast (t1, t2)
     | C.Lambda (_, t1, t2)
     | C.Prod (_, t1, t2)
@@ -289,19 +292,44 @@ end
 
 module IntSet = Set.Make(OrderedInt)
 
-let compute_equality_weight ty left right =
+let compute_equality_weight (ty,left,right,o) =
+  let factor = 2 in
+  match o with
+    | Lt -> 
+	let w, m = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false right) in
+	  w + (factor * (List.length m)) ;
+    | Le -> assert false
+    | Gt -> 
+	let w, m = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false left) in
+	  w + (factor * (List.length m)) ;
+  | Ge -> assert false
+  | Eq 
+  | Incomparable -> 
+      let w1, m1 = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false right) in
+      let w2, m2 = (weight_of_term 
+	       ~consider_metas:true ~count_metas_occurrences:false left) in
+      w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
+;;
+
+(* old
+let compute_equality_weight (ty,left,right,o) =
   let metasw = ref 0 in
   let weight_of t =
-    let w, m = (weight_of_term ~consider_metas:true t) in
-    metasw := !metasw + (2 * (List.length m));
+    let w, m = (weight_of_term 
+		  ~consider_metas:true ~count_metas_occurrences:false t) in
+    metasw := !metasw + (1 * (List.length m)) ;
     w
   in
   (* Warning: the following let cannot be expanded since it forces the
      right evaluation order!!!! *)
-  let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+  let w = (weight_of ty) + (weight_of left) + (weight_of right) in 
+  (* let w = weight_of (Cic.Appl [ty;left;right]) in *)
   w + !metasw
 ;;
-
+*)
 
 (* returns a "normalized" version of the polynomial weight wl (with type
  * weight list), i.e. a list sorted ascending by meta number,
@@ -401,7 +429,6 @@ let compare_weights ?(normalize=false)
   | (m, _, n) when m > 0 && n > 0 ->
       Incomparable
   | _ -> assert false 
-
 ;;
 
 
@@ -697,11 +724,20 @@ let string_of_pos = function
   | Right -> "Right"
 ;;
 
+let eq_URI () =
+ match LibraryObjects.eq_URI () with
+    None -> assert false
+  | Some uri -> uri
 
-let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
-let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
-let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(eq_URI ())
 let eq_XURI () =
-  let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+  let s = UriManager.string_of_uri (eq_URI ()) in
   UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(eq_URI ())
+
+let metas_of_term t = 
+  List.map fst (CicUtil.metas_of_term t)
+;;
+