added stdlib_dir entry

[helm.git] / helm / ocaml / paramodulation / utils.ml

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index a558001a5ee0746a0b87e0ddc366bbb696473917..5eb591c0b1450c80036f9f904e313157dd7d8238 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -23,11 +23,12 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 let debug = true;;
 
 let debug_print s = if debug then prerr_endline (Lazy.force s);;
 
-
 let print_metasenv metasenv =
   String.concat "\n--------------------------\n"
     (List.map (fun (i, context, term) ->
@@ -106,7 +107,7 @@ let weight_of_term ?(consider_metas=true) term =
   let compare w1 w2 = 
     match w1, w2 with
     | (m1, _), (m2, _) -> m2 - m1 
-  in
+  in 
   (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
 ;;
 
@@ -234,17 +235,23 @@ let compare_weights ?(normalize=false)
       else if hdiff > 0 then Gt
       else Eq (* Incomparable *)
   | (m, _, 0) ->
+      if diffs < (- hdiff) then Lt
+      else if diffs = (- hdiff) then Le else Incomparable
+(*
       if hdiff <= 0 then 
         if m > 0 || hdiff < 0 then Lt
         else if diffs >= (- hdiff) then Le else Incomparable
       else 
-        if diffs >= (- hdiff) then Le else Incomparable
+        if diffs >= (- hdiff) then Le else Incomparable *)
   | (0, _, m) ->
+      if (- hdiff) < diffs then Gt
+      else if (- hdiff) = diffs then Ge else Incomparable
+(*
       if hdiff >= 0 then 
         if m > 0 || hdiff > 0 then Gt
         else if (- diffs) >= hdiff then Ge else Incomparable
       else
-        if (- diffs) >= hdiff then Ge else Incomparable
+        if (- diffs) >= hdiff then Ge else Incomparable *)
   | (m, _, n) when m > 0 && n > 0 ->
       Incomparable
   | _ -> assert false
@@ -320,6 +327,10 @@ let nonrec_kbo_w (t1, w1) (t2, w2) =
 let nonrec_kbo t1 t2 =
   let w1 = weight_of_term t1 in
   let w2 = weight_of_term t2 in
+  (* 
+  prerr_endline ("weight1 :"^(string_of_weight w1));
+  prerr_endline ("weight2 :"^(string_of_weight w2)); 
+  *)
   match compare_weights ~normalize:true w1 w2 with
   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
@@ -375,6 +386,62 @@ let rec kbo t1 t2 =
   | res -> res
 ;;
           
+let rec ao t1 t2 =
+  let get_hd t =
+    match t with
+       Cic.MutConstruct(uri,tyno,cno,_) -> Some(uri,tyno,cno)
+      | Cic.Appl(Cic.MutConstruct(uri,tyno,cno,_)::_) -> 
+         Some(uri,tyno,cno)
+      | _ -> None in
+  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 =
+          ao hd1 hd2
+        in
+        if o = Eq then cmp tl1 tl2
+        else o
+  in
+  match get_hd t1, get_hd t2 with
+      Some(_),None -> Lt
+    | None,Some(_) -> Gt
+    | _ ->
+       let comparison = compare_weights ~normalize:true w1 w2 in
+         match comparison with
+           | Le ->
+               let r = aux t1 t2 in
+                 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 ->
+                         cmp tl1 tl2
+                     | _, _ ->  Incomparable
+                 ) else r 
+           | res -> res
+;;
 
 let names_of_context context = 
   List.map
@@ -492,8 +559,17 @@ let rec lpo t1 t2 =
 
 
 (* settable by the user... *)
-let compare_terms = ref nonrec_kbo;;
-
+let compare_terms = ref nonrec_kbo;; 
+(* let compare_terms = ref ao;; *)
+
+let guarded_simpl context t =
+  let t' = ProofEngineReduction.simpl context t in
+  let simpl_order = !compare_terms t t' in
+  if simpl_order = Gt then 
+    (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *)
+  t'
+  else t
+;;
 
 type equality_sign = Negative | Positive;;