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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index a558001a5..6ee45f235 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -27,7 +27,6 @@ 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) ->
@@ -375,6 +374,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 +547,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;;