cambiato il tipo equality, aggiunto l'ordinamento tra left e right

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 4c1480d100c86a72a88ee652de5d4dcd5d697a69..5f9ffe33506e7ac4c266c41f5361af6368f20cd6 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -7,21 +7,13 @@ type result =
 ;;
 
 
-type equality_sign = Negative | Positive;;
-
-let string_of_sign = function
-  | Negative -> "Negative"
-  | Positive -> "Positive"
-;;
-
-
 (*
 let symbols_of_equality (_, (_, left, right), _, _) =
   TermSet.union (symbols_of_term left) (symbols_of_term right)
 ;;
 *)
 
-let symbols_of_equality ((_, (_, left, right), _, _) as equality) =
+let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -49,8 +41,8 @@ struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right), _, _ = eq1
-        and _, (ty', left', right'), _, _ = eq2 in
+        let _, (ty, left, right, _), _, _ = eq1
+        and _, (ty', left', right', _), _, _ = eq2 in
         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
@@ -234,7 +226,7 @@ let contains_empty env (negative, positive) =
   try
     let (proof, _, _, _) =
       List.find
-        (fun (proof, (ty, left, right), m, a) ->
+        (fun (proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -663,24 +655,18 @@ let main () =
   let env = (metasenv, context, ugraph) in
   try
     let term_equality = equality_of_term meta_proof goal in
-    let meta_proof, (eq_ty, left, right), _, _ = term_equality in
+    let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = [] in
     let passive = make_passive [term_equality] equalities in
-    Printf.printf "\ncurrent goal: %s ={%s} %s\n"
-      (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
+    Printf.printf "\ncurrent goal: %s\n"
+      (string_of_equality ~env term_equality);
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
-    Printf.printf "\nequalities:\n";
-    List.iter
-      (function (_, (ty, t1, t2), _, _) ->
-         let w1 = weight_of_term t1 in
-         let w2 = weight_of_term t2 in
-         let res = !compare_terms t1 t2 in
-         Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
-           (PP.ppterm t1) (string_of_weight w1)
-           (string_of_comparison res)
-           (PP.ppterm t2) (string_of_weight w2))
-      equalities;
+    Printf.printf "\nequalities:\n%s\n"
+      (String.concat "\n"
+         (List.map
+            (string_of_equality ~env)
+            equalities));
     print_endline "--------------------------------------------------";
     let start = Unix.gettimeofday () in
     print_endline "GO!";