X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=c1c9086de1ccf4db4570125ea0f2963bcfd1495f;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=8d97e0c4bbb8ca198d2ecf9fb449527432edac13;hpb=6cce91267c785d7790e9377717a13d0546bb68e1;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 8d97e0c4b..c1c9086de 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -1,3 +1,8 @@
+let debug = true;;
+
+let debug_print = if debug then prerr_endline else ignore;;
+
+
 let print_metasenv metasenv =
   String.concat "\n--------------------------\n"
     (List.map (fun (i, context, term) ->
@@ -7,8 +12,8 @@ let print_metasenv metasenv =
 ;;
 
 
-let print_subst subst =
-  String.concat "\n"
+let print_subst ?(prefix="\n") subst =
+  String.concat prefix
     (List.map
        (fun (i, (c, t, ty)) ->
           Printf.sprintf "?%d -> %s : %s" i
@@ -27,20 +32,21 @@ let string_of_weight (cw, mw) =
   Printf.sprintf "[%d; %s]" cw s
 
 
-let weight_of_term term =
+let weight_of_term ?(consider_metas=true) term =
   (* ALB: what to consider as a variable? I think "variables" in our case are
      Metas and maybe Rels... *)
   let module C = Cic in
   let vars_dict = Hashtbl.create 5 in
   let rec aux = function
-    | C.Meta (metano, _) ->
+    | C.Meta (metano, _) when consider_metas ->
         (try
            let oldw = Hashtbl.find vars_dict metano in
            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...*)
+                  
     | C.Var (_, ens)
     | C.Const (_, ens)
     | C.MutInd (_, _, ens)
@@ -82,6 +88,33 @@ let weight_of_term term =
 ;;
 
 
+module OrderedInt = struct
+  type t = int
+
+  let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make(OrderedInt)
+
+let compute_equality_weight ty left right =
+(*   let metasw = ref IntSet.empty in *)
+  let metasw = ref 0 in
+  let weight_of t =
+    let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
+(*     let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
+(*     metasw := !metasw + mw; *)
+    metasw := !metasw + (2 * (List.length m));
+(*     metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw 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
+  w + !metasw
+(*     (4 * IntSet.cardinal !metasw) *)
+;;
+
+
 (* returns a "normalized" version of the polynomial weight wl (with type
  * weight list), i.e. a list sorted ascending by meta number,
  * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
@@ -124,6 +157,7 @@ let normalize_weights (cw1, wl1) (cw2, wl2) =
     | (m, w)::tl1, [] ->
         let res1, res2 = aux tl1 [] in
         (m, w)::res1, (m, 0)::res2
+    | _, _ -> assert false
   in
   let cmp (m, _) (n, _) = compare m n in
   let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
@@ -203,10 +237,11 @@ let compare_weights ?(normalize=false)
         if (- diffs) >= hdiff then Ge else Incomparable
   | (m, _, n) when m > 0 && n > 0 ->
       Incomparable
+  | _ -> assert false
 ;;
 
 
-let rec aux_ordering t1 t2 =
+let rec aux_ordering ?(recursion=true) t1 t2 =
   let module C = Cic in
   let compare_uris u1 u2 =
     let res =
@@ -221,7 +256,7 @@ let rec aux_ordering t1 t2 =
 
   | t1, t2 when t1 = t2 -> Eq
 
-  | C.Rel n, C.Rel m -> if n > m then Lt else Gt (* ALB: changed < to > *)
+  | C.Rel n, C.Rel m -> if n > m then Lt else Gt
   | C.Rel _, _ -> Lt
   | _, C.Rel _ -> Gt
 
@@ -238,7 +273,7 @@ let rec aux_ordering t1 t2 =
   | C.MutConstruct _, _ -> Lt
   | _, C.MutConstruct _ -> Gt
 
-  | C.Appl l1, C.Appl l2 ->
+  | C.Appl l1, C.Appl l2 when recursion ->
       let rec cmp t1 t2 =
         match t1, t2 with
         | [], [] -> Eq
@@ -250,10 +285,13 @@ let rec aux_ordering t1 t2 =
             else o
       in
       cmp l1 l2
+  | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
+      aux_ordering h1 h2
         
   | t1, t2 ->
-      Printf.printf "These two terms are not comparable:\n%s\n%s\n\n"
-        (CicPp.ppterm t1) (CicPp.ppterm t2);
+      debug_print (
+        Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
+          (CicPp.ppterm t1) (CicPp.ppterm t2));
       Incomparable
 ;;
 
@@ -279,6 +317,68 @@ let nonrec_kbo t1 t2 =
 ;;
 
 
+let rec kbo t1 t2 =
+(*   debug_print ( *)
+(*     Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *)
+(*   if t1 = t2 then *)
+(*     Eq *)
+(*   else *)
+    let aux = aux_ordering ~recursion:false in
+    let w1 = weight_of_term t1
+    and w2 = weight_of_term t2 in
+    let rec cmp t1 t2 =
+      match t1, t2 with
+      | [], [] -> Eq
+      | _, [] -> Gt
+      | [], _ -> Lt
+      | hd1::tl1, hd2::tl2 ->
+          let o =
+(*             debug_print ( *)
+(*               Printf.sprintf "recursion kbo on %s %s" *)
+(*                 (CicPp.ppterm hd1) (CicPp.ppterm hd2)); *)
+            kbo hd1 hd2
+          in
+          if o = Eq then cmp tl1 tl2
+          else o
+    in
+    let comparison = compare_weights ~normalize:true w1 w2 in
+(*     debug_print ( *)
+(*       Printf.sprintf "Weights are: %s %s: %s" *)
+(*         (string_of_weight w1) (string_of_weight w2) *)
+(*         (string_of_comparison comparison)); *)
+    match comparison with
+    | Le ->
+        let r = aux t1 t2 in
+(*         debug_print ("HERE! " ^ (string_of_comparison r)); *)
+        if r = Lt then Lt
+        else if r = Eq then (
+          match t1, t2 with
+          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+              if cmp tl1 tl2 = Lt then Lt else Incomparable
+          | _, _ ->  Incomparable
+        ) else Incomparable
+    | Ge ->
+        let r = aux t1 t2 in
+        if r = Gt then Gt
+        else if r = Eq then (
+          match t1, t2 with
+          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+              if cmp tl1 tl2 = Gt then Gt else Incomparable
+          | _, _ ->  Incomparable
+        ) else Incomparable
+    | Eq ->
+        let r = aux t1 t2 in
+        if r = Eq then (
+          match t1, t2 with
+          | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+(*               if cmp tl1 tl2 = Gt then Gt else Incomparable *)
+              cmp tl1 tl2
+          | _, _ ->  Incomparable
+        ) else r 
+    | res -> res
+;;
+          
+
 let names_of_context context = 
   List.map
     (function
@@ -288,21 +388,127 @@ let names_of_context context =
 ;;
 
 
-let string_of_equality ?env =
-  match env with
-  | None -> (
-      function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
-              (CicPp.ppterm left) (CicPp.ppterm right)
-    )
-  | Some (_, context, _) -> (
-      let names = names_of_context context in
-      function
-        | _, (ty, left, right), _, _ ->
-            Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
-              (CicPp.pp left names) (CicPp.pp right names)
+module OrderedTerm =
+struct
+  type t = Cic.term
+      
+  let compare = Pervasives.compare
+end
+
+module TermSet = Set.Make(OrderedTerm);;
+module TermMap = Map.Make(OrderedTerm);;
+
+let symbols_of_term term =
+  let module C = Cic in
+  let rec aux map = function
+    | C.Meta _ -> map
+    | C.Appl l ->
+        List.fold_left (fun res t -> (aux res t)) map l
+    | t ->
+        let map = 
+          try
+            let c = TermMap.find t map in
+            TermMap.add t (c+1) map
+          with Not_found ->
+            TermMap.add t 1 map
+        in
+        map
+  in
+  aux TermMap.empty term
+;;
+
+
+let metas_of_term term =
+  let module C = Cic in
+  let rec aux = function
+    | C.Meta _ as t -> TermSet.singleton t
+    | C.Appl l ->
+        List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l
+    | t -> TermSet.empty (* TODO: maybe add other cases? *)
+  in
+  aux term
+;;
+
+
+let rec lpo t1 t2 =
+  let module C = Cic in
+  match t1, t2 with
+  | t1, t2 when t1 = t2 -> Eq
+  | t1, (C.Meta _ as m) ->
+      if TermSet.mem m (metas_of_term t1) then Gt else Incomparable
+  | (C.Meta _ as m), t2 ->
+      if TermSet.mem m (metas_of_term t2) then Lt else Incomparable
+  | C.Appl (hd1::tl1), C.Appl (hd2::tl2) -> (
+      let res =
+        let f o r t =
+          if r then true else
+            match lpo t o with
+            | Gt | Eq -> true
+            | _ -> false
+        in
+        let res1 = List.fold_left (f t2) false tl1 in
+        if res1 then Gt
+        else let res2 = List.fold_left (f t1) false tl2 in
+        if res2 then Lt
+        else Incomparable
+      in
+      if res <> Incomparable then
+        res
+      else
+        let f o r t =
+          if not r then false else
+            match lpo o t with
+            | Gt -> true
+            | _ -> false
+        in
+        match aux_ordering hd1 hd2 with
+        | Gt ->
+            let res = List.fold_left (f t1) false tl2 in
+            if res then Gt
+            else Incomparable
+        | Lt ->
+            let res = List.fold_left (f t2) false tl1 in
+            if res then Lt
+            else Incomparable
+        | Eq -> (
+            let lex_res =
+              try
+                List.fold_left2
+                  (fun r t1 t2 -> if r <> Eq then r else lpo t1 t2)
+                  Eq tl1 tl2
+              with Invalid_argument _ ->
+                Incomparable
+            in
+            match lex_res with
+            | Gt ->
+                if List.fold_left (f t1) false tl2 then Gt
+                else Incomparable
+            | Lt ->
+                if List.fold_left (f t2) false tl1 then Lt
+                else Incomparable
+            | _ -> Incomparable
+          )
+        | _ -> Incomparable
     )
+  | t1, t2 -> aux_ordering t1 t2
+;;
+
+
+(* settable by the user... *)
+let compare_terms = ref nonrec_kbo;;
+
+
+type equality_sign = Negative | Positive;;
+
+let string_of_sign = function
+  | Negative -> "Negative"
+  | Positive -> "Positive"
 ;;
 
 
+type pos = Left | Right 
+
+let string_of_pos = function
+  | Left -> "Left"
+  | Right -> "Right"
+;;