From 92d100db14a01e3fb70a7d5151ac1e60d5a782a0 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 19 May 2005 13:12:56 +0000
Subject: [PATCH] added lpo term-ordering

---
 helm/ocaml/paramodulation/utils.ml  | 120 ++++++++++++++++++++++++----
 helm/ocaml/paramodulation/utils.mli |  10 ++-
 2 files changed, 112 insertions(+), 18 deletions(-)

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 7f0a8ba55..b0aa00e89 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -222,7 +222,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
 
@@ -289,21 +289,111 @@ 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;;
diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 235085ab1..1adf90e50 100644
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -19,11 +19,15 @@ val compare_weights: ?normalize:bool -> weight -> weight -> comparison
 
 val nonrec_kbo: Cic.term -> Cic.term -> comparison
 
-val string_of_equality:
-  ?env:Inference.environment -> Inference.equality -> string
-
 val nonrec_kbo_w: (Cic.term * weight) -> (Cic.term * weight) -> comparison
 
 val names_of_context: Cic.context -> (Cic.name option) list
 
+module TermMap: Map.S with type key = Cic.term
+
+val symbols_of_term: Cic.term -> int TermMap.t
+
+val lpo: Cic.term -> Cic.term -> comparison
 
+(** term-ordering function settable by the user *)
+val compare_terms: (Cic.term -> Cic.term -> comparison) ref
-- 
2.39.2