existential variables in goal supported

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

diff --git a/helm/software/components/tactics/paramodulation/utils.ml b/helm/software/components/tactics/paramodulation/utils.ml
index b212d0faba862c580355b4db09b98ef6142120b7..6a32e25953f5afff5df75c0ce55058c246303a0c 100644 (file)
--- a/helm/software/components/tactics/paramodulation/utils.ml
+++ b/helm/software/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 
-
 ;;
 
 
@@ -705,3 +732,30 @@ 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 ())
+
+let rec metas_of_term = function
+  | Cic.Meta (i, c) -> [i]
+  | Cic.Var (_, ens) 
+  | Cic.Const (_, ens) 
+  | Cic.MutInd (_, _, ens) 
+  | Cic.MutConstruct (_, _, _, ens) ->
+      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+  | Cic.Cast (s, t)
+  | Cic.Prod (_, s, t)
+  | Cic.Lambda (_, s, t)
+  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+  | Cic.MutCase (uri, i, s, t, l) ->
+      (metas_of_term s) @ (metas_of_term t) @
+        (List.flatten (List.map metas_of_term l))
+  | Cic.Fix (i, il) ->
+      List.flatten
+        (List.map (fun (s, i, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | Cic.CoFix (i, il) ->
+      List.flatten
+        (List.map (fun (s, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | _ -> []
+;;      
+