From: denes <??>
Date: Fri, 3 Jul 2009 16:41:33 +0000 (+0000)
Subject: Ported old implementation of LPO (for test purposes)
X-Git-Tag: make_still_working~3752
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f6040cf168fe0cdcbe8b3c37904a2090d7083a0;p=helm.git

Ported old implementation of LPO (for test purposes)
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index f2e0273c8..b95593df2 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -221,39 +221,146 @@ let compute_goal_weight (_,l, _, _) =
   ;;
 
   let rec lpo s t =
+    let cmp a1 a2 =
+      let res = B.compare a1 a2 in
+	if res = 0 then XEQ else if res < 0 then XLT else XGT
+    in
     match s,t with
-      | Terms.Var i, Terms.Var j when i = j ->
+      | s, t when s = t ->
 	  XEQ
       | Terms.Var _, Terms.Var _ ->
 	  XINCOMPARABLE
+      | Terms.Leaf a1, Terms.Leaf a2 ->
+	  cmp a1 a2
+      | _, Terms.Var i ->
+	  if (List.mem i (Terms.vars_of_term s)) then XGT
+	  else XINCOMPARABLE
       | Terms.Var _, _ ->
+      (*| Terms.Leaf _, Terms.Node _ -> *)
 	  (match lpo t s with
 	    | XGT -> XLT
 	    | XLT -> XGT
 	    | o -> o)
-      | _, Terms.Var i ->
-	  if (List.mem i (Terms.vars_of_term s)) then XGT
-	  else XINCOMPARABLE
-      | Terms.Leaf a1, Terms.Leaf a2 -> 
-          let cmp = B.compare a1 a2 in
-            if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+      (*| Terms.Node (Terms.Leaf a1::tl), Terms.Leaf a2 ->
+	  (match cmp a1 a2 with
+	    | XGT -> XGT
+	    | _ -> 
+		if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl
+		then XGT
+		else XINCOMPARABLE)*)
       | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
-	  (match lpo hd1 hd2 with
-	    | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
-	      else XINCOMPARABLE
-	    | XLT -> if List.for_all (fun x -> lpo s x = XLT) tl2 then XLT
-	      else XINCOMPARABLE
-	    | XEQ -> List.fold_left2
-		(fun acc si ti -> if acc = XEQ then lpo si ti else acc)
-		  XEQ tl1 tl2
-	    | XINCOMPARABLE -> XINCOMPARABLE
-	    | _ -> assert false)
-      | _ -> assert false
+(*	  let lo = List.map (lpo s) tl2 in
+	  let ro = List.map (lpo t) tl1 in
+	    if List.exists (fun x -> x=XGT || x=XEQ) lo
+	    then XGT
+	    else if List.exists (fun x -> x=XGT || x=XEQ) ro
+	    then XLT
+	    else begin
+	      match lpo hd1 hd2 with
+		| XGT -> if List.for_all (fun x -> x=XGT) lo then XGT
+		  else XINCOMPARABLE
+		| XLT -> if List.for_all (fun x -> x=XGT) ro then XLT
+		  else XINCOMPARABLE
+		| XEQ -> List.fold_left2
+		    (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+		      XEQ tl1 tl2
+		| XINCOMPARABLE -> XINCOMPARABLE
+		| _ -> assert false
+	    end*)
+	  if List.exists (fun x -> let o = lpo x t in o=XGT || o=XEQ) tl1
+	  then XGT
+	  else if List.exists (fun x -> let o=lpo s x in o=XLT || o=XEQ) tl2
+	  then XLT
+	  else begin
+	    match lpo hd1 hd2 with
+	      | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+		else XINCOMPARABLE
+	      | XLT -> if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
+		else XINCOMPARABLE
+	      | XEQ -> 
+	       let lex = List.fold_left2
+		 (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+		 XEQ tl1 tl2
+	       in
+		 (match lex with
+		    | XGT ->
+			if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+		      else XINCOMPARABLE
+		    | XLT ->
+			if List.for_all (fun x -> lpo x t = XLT) tl1 then XLT
+		      else XINCOMPARABLE
+		    | o -> o)   
+	      | XINCOMPARABLE -> XINCOMPARABLE
+	      | _ -> assert false
+	  end
+      | _,_ -> aux_ordering s t
 	    
   ;;
 
+let rec lpo_old t1 t2 =
+  match t1, t2 with
+  | t1, t2 when t1 = t2 -> XEQ
+  | t1, (Terms.Var m) ->
+      if List.mem m (Terms.vars_of_term t1) then XGT else XINCOMPARABLE
+  | (Terms.Var m), t2 ->
+      if List.mem m (Terms.vars_of_term t2) then XLT else XINCOMPARABLE
+  | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) -> (
+      let res =
+        let f o r t =
+          if r then true else
+            match lpo_old t o with
+            | XGT | XEQ -> true
+            | _ -> false
+        in
+        let res1 = List.fold_left (f t2) false tl1 in
+        if res1 then XGT
+        else let res2 = List.fold_left (f t1) false tl2 in
+        if res2 then XLT
+        else XINCOMPARABLE
+      in
+      if res <> XINCOMPARABLE then
+        res
+      else
+        let f o r t =
+          if not r then false else
+            match lpo_old o t with
+            | XGT -> true
+            | _ -> false
+        in
+        match aux_ordering hd1 hd2 with
+        | XGT ->
+            let res = List.fold_left (f t1) false tl2 in
+            if res then XGT
+            else XINCOMPARABLE
+        | XLT ->
+            let res = List.fold_left (f t2) false tl1 in
+            if res then XLT
+            else XINCOMPARABLE
+        | XEQ -> (
+            let lex_res =
+              try
+                List.fold_left2
+                  (fun r t1 t2 -> if r <> XEQ then r else lpo_old t1 t2)
+                  XEQ tl1 tl2
+              with Invalid_argument _ ->
+                XINCOMPARABLE
+            in
+            match lex_res with
+            | XGT ->
+                if List.fold_left (f t1) false tl2 then XGT
+                else XINCOMPARABLE
+            | XLT ->
+                if List.fold_left (f t2) false tl1 then XLT
+                else XINCOMPARABLE
+            | _ -> XINCOMPARABLE
+          )
+        | _ -> XINCOMPARABLE
+    )
+  | t1, t2 -> aux_ordering t1 t2
+;;
+
   let compare_terms x y = 
-    match kbo x y with
+    match lpo_old x y with
     | XINCOMPARABLE -> Terms.Incomparable
     | XGT -> Terms.Gt
     | XLT -> Terms.Lt