Discrimination and trie removed.

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index a558001a5ee0746a0b87e0ddc366bbb696473917..6ee45f235478a78db8a6a682ed77eacb175a55c9 100644 (file)
--- 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;;