added (but not yet used) remove_local_context

[helm.git] / components / tactics / paramodulation / utils.ml

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index b212d0faba862c580355b4db09b98ef6142120b7..a25ba8e2d7cda49cb9ac8cfede5cb14ea2aef99d 100644 (file)
--- 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
@@ -100,6 +103,13 @@ let metas_of_term term =
   aux term
 ;;
 
+let rec remove_local_context =
+  function
+    | Cic.Meta (i,_) -> Cic.Meta (i,[])
+    | Cic.Appl l ->
+       Cic.Appl(List.map remove_local_context l)
+    | t -> t 
+
 
 (************************* rpo ********************************)
 let number = [
@@ -227,7 +237,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 +247,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 +299,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
+      (max w1 w2)+(max (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 +436,6 @@ let compare_weights ?(normalize=false)
   | (m, _, n) when m > 0 && n > 0 ->
       Incomparable
   | _ -> assert false 
-
 ;;
 
 
@@ -697,11 +731,7 @@ let string_of_pos = function
   | Right -> "Right"
 ;;
 
+let metas_of_term t = 
+  List.map fst (CicUtil.metas_of_term t)
+;;
 
-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_XURI () =
-  let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
-  UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())