X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=c933aec0b48c3c11115d8d8346302f1144c93892;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=d8019cae8d280fefaab4235bc83c1a8cda2abb52;hpb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index d8019cae8..c933aec0b 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -34,7 +34,7 @@ let maxmeta = ref 0;;
 
 type result =
   | Failure
-  | Success of Cic.term option * environment
+  | Success of Inference.equality option * environment
 ;;
 
 
@@ -44,7 +44,7 @@ let symbols_of_equality (_, (_, left, 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
@@ -64,17 +64,6 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) =
 ;;
 
 
-let weight_of_equality (_, (ty, left, right, _), _, _) =
-  let meta_number = ref 0 in
-  let weight_of t =
-    let weight, ml =  weight_of_term t in
-    meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
-    weight
-  in
-  (weight_of ty) + (weight_of left) + (weight_of right), meta_number
-;;
-
-
 module OrderedEquality = struct
   type t = Inference.equality
 
@@ -82,17 +71,25 @@ module OrderedEquality = struct
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let _, (ty, left, right, _), _, _ = eq1
-        and _, (ty', left', right', _), _, _ = eq2 in
-(*         let w1, m1 = weight_of_equality eq1 *)
-(*         and w2, m2 = weight_of_equality 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
+        let w1, _, (ty, left, right, _), _, a = eq1
+        and w2, _, (ty', left', right', _), _, a' = 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 *)
         match Pervasives.compare w1 w2 with
-        | 0 -> Pervasives.compare eq1 eq2
-(*             let res = Pervasives.compare m1 m2 in *)
-(*             if res = 0 then Pervasives.compare eq1 eq2 else res *)
+        | 0 ->
+            let res = (List.length a) - (List.length a') in
+            if res <> 0 then res else (
+              try
+                let res = Pervasives.compare (List.hd a) (List.hd a') in
+                if res <> 0 then res else Pervasives.compare eq1 eq2
+              with _ -> Pervasives.compare eq1 eq2
+(*               match a, a' with *)
+(*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
+(*                   let res = Pervasives.compare i j in *)
+(*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
+(*               | _, _ -> Pervasives.compare eq1 eq2 *)
+            )
         | res -> res
 end
 
@@ -415,13 +412,13 @@ let infer env sign current (active_list, active_table) =
 let contains_empty env (negative, positive) =
   let metasenv, context, ugraph = env in
   try
-    let (proof, _, _, _) =
+    let found =
       List.find
-        (fun (proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m, a) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
-    true, Some proof
+    true, Some found
   with Not_found ->
     false, None
 ;;
@@ -461,7 +458,8 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
       Indexing.demodulation !maxmeta env table current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
-      if sign = Negative then Some (sign, newcurrent) else None
+      if sign = Negative then Some (sign, newcurrent)
+      else None
     else
       Some (sign, newcurrent)
   in
@@ -490,7 +488,8 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
         match passive_table with
         | None -> res
         | Some passive_table ->
-            if Indexing.in_index passive_table c then None else res
+            if Indexing.in_index passive_table c then None
+            else res
 
 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
 
@@ -571,7 +570,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let new_pos_set =
     List.fold_left
       (fun s e ->
-         if not (Inference.is_identity env e) then EqualitySet.add e s else s)
+         if not (Inference.is_identity env e) then
+           if EqualitySet.mem e s then s
+           else EqualitySet.add e s
+         else s)
       EqualitySet.empty new_pos
   in
   let new_pos = EqualitySet.elements new_pos_set in
@@ -602,10 +604,12 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
 
   let is_duplicate =
     match passive_table with
-    | None -> (fun e -> not (Indexing.in_index active_table e))
+    | None ->
+        (fun e -> not (Indexing.in_index active_table e))
     | Some passive_table ->
-        (fun e -> not ((Indexing.in_index active_table e) ||
-                         (Indexing.in_index passive_table e)))
+        (fun e ->
+           not ((Indexing.in_index active_table e) ||
+                  (Indexing.in_index passive_table e)))
   in
   new_neg, List.filter is_duplicate new_pos
 
@@ -639,16 +643,20 @@ let backward_simplify_active env new_pos new_table active =
   let active, newa =
     List.fold_right
       (fun (s, eq) (res, tbl) ->
-         if (is_identity env eq) || (find eq res) then
+         if List.mem (s, eq) res then
+           res, tbl
+         else if (is_identity env eq) || (find eq res) then (
            res, tbl
+         ) (* else if (find eq res) then *)
+(*            res, tbl *)
          else
            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
       active_list ([], Indexing.empty_table ()),
     List.fold_right
       (fun (s, eq) (n, p) ->
-         if (s <> Negative) && (is_identity env eq) then
+         if (s <> Negative) && (is_identity env eq) then (
            (n, p)
-         else
+         ) else
            if s = Negative then eq::n, p
            else n, eq::p)
       newa ([], [])
@@ -750,8 +758,7 @@ let rec given_clause env passive active =
             Printf.printf "OK!!! %s %s" (string_of_sign sign)
               (string_of_equality ~env current);
             print_newline ();
-            let proof, _, _, _ = current in
-            Success (Some proof, env)
+            Success (Some current, env)
           ) else (            
             print_endline "\n================================================";
             Printf.printf "selected: %s %s"
@@ -763,9 +770,9 @@ let rec given_clause env passive active =
             let t2 = Unix.gettimeofday () in
             infer_time := !infer_time +. (t2 -. t1);
             
-            let res, proof = contains_empty env new' in
+            let res, goal = contains_empty env new' in
             if res then
-              Success (proof, env)
+              Success (goal, env)
             else 
               let t1 = Unix.gettimeofday () in
               let new' = forward_simplify_new env new' (* ~passive *) active in
@@ -839,8 +846,8 @@ let rec given_clause env passive active =
 (*                              (EqualitySet.elements ps)))); *)
 (*                   print_newline (); *)
                   given_clause env passive active
-              | true, proof ->
-                  Success (proof, env)
+              | true, goal ->
+                  Success (goal, env)
           )
 ;;
 
@@ -886,8 +893,7 @@ let rec given_clause_fullred env passive active =
             Printf.printf "OK!!! %s %s" (string_of_sign sign)
               (string_of_equality ~env current);
             print_newline ();
-            let proof, _, _, _ = current in
-            Success (Some proof, env)
+            Success (Some current, env)
           ) else (
             print_endline "\n================================================";
             Printf.printf "selected: %s %s"
@@ -958,8 +964,8 @@ let rec given_clause_fullred env passive active =
             | false, _ -> 
                 let passive = add_to_passive passive new' in
                 given_clause_fullred env passive active
-            | true, proof ->
-                Success (proof, env)
+            | true, goal ->
+                Success (goal, env)
           )
 ;;
 
@@ -1000,7 +1006,7 @@ 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, ordering), _, _ = term_equality in
+    let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
     let active = make_active () in
     let passive = make_passive [term_equality] equalities in
     Printf.printf "\ncurrent goal: %s\n"
@@ -1025,14 +1031,11 @@ let main () =
       match res with
       | Failure ->
           Printf.printf "NO proof found! :-(\n\n"
-      | Success (Some proof, env) ->
-          Printf.printf "OK, found a proof!:\n%s\n%.9f\n"
-            (PP.pp proof (names_of_context context))
-            (finish -. start);
-(*         Printf.printf ("forward_simpl_details:\n  build_all: %.9f\n" ^^ *)
-(*                          "  demodulate: %.9f\n  subsumption: %.9f\n") *)
-(*           fs_time_info.build_all fs_time_info.demodulate *)
-(*           fs_time_info.subsumption; *)
+      | Success (Some goal, env) ->
+          Printf.printf "OK, found a proof!\n";
+          let proof = Inference.build_term_proof goal in
+          print_endline (PP.pp proof (names_of_context context));
+          print_endline (string_of_float (finish -. start));
       | Success (None, env) ->
           Printf.printf "Success, but no proof?!?\n\n"
     in