X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=5eb591c0b1450c80036f9f904e313157dd7d8238;hb=b1bad322d0daf6c25f95a82c4349f057a753ab7c;hp=a558001a5ee0746a0b87e0ddc366bbb696473917;hpb=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index a558001a5..5eb591c0b 100644
--- 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;;