args removed from equalities.

[helm.git] / components / tactics / paramodulation / saturation.ml

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b6678683d5d73688473e9d91b9849d429030df57..bf9f8ba57dde43b7bcbbdf6b9fa0cb73a2940fc6 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -32,7 +32,7 @@ open Utils;;
 (*
 for debugging 
 let check_equation env equation msg =
-  let w, proof, (eq_ty, left, right, order), metas, args = equation in
+  let w, proof, (eq_ty, left, right, order), metas = equation in
   let metasenv, context, ugraph = env in
   let metasenv' = metasenv @ metas in
     try
@@ -101,7 +101,7 @@ type goal = proof * Cic.metasenv * Cic.term;;
 
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
-let symbols_of_equality (_, _, (_, left, right, _), _, _) =
+let symbols_of_equality (_, _, (_, left, right, _), _) =
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -116,26 +116,57 @@ let symbols_of_equality (_, _, (_, left, right, _), _, _) =
   m
 ;;
 
-module OrderedEquality = struct
+(* griggio *)
+module OrderedEquality = struct 
   type t = Inference.equality
 
   let compare eq1 eq2 =
     match meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let w1, _, (ty, left, right, _), _, a = eq1
-        and w2, _, (ty', left', right', _), _, a' = eq2 in
+        let w1, _, (ty, left, right, _), m1 = eq1
+        and w2, _, (ty', left', right', _), m2 = eq2 in
         match Pervasives.compare w1 w2 with
+        | 0 -> 
+           let res = (List.length m1) - (List.length m2) in 
+            if res <> 0 then res else Pervasives.compare eq1 eq2
+        | res -> res 
+end 
+
+(*
+module OrderedEquality = struct
+  type t = Inference.equality
+
+  let minor eq =
+    let w, _, (ty, left, right, o), _ = eq in
+      match o with
+        | Lt -> Some left
+        | Le -> assert false
+        | Gt -> Some right
+        | Ge -> assert false
+        | Eq 
+        | Incomparable -> None
+            
+  let compare eq1 eq2 =
+    let w1, _, (ty, left, right, o1), m1 = eq1
+    and w2, _, (ty', left', right', o2), m2 = eq2 in
+      match Pervasives.compare w1 w2 with
         | 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 Failure "hd" -> Pervasives.compare eq1 eq2
-            )
-        | res -> res
+           (match minor eq1, minor eq2 with
+             | Some t1, Some t2 ->
+                 fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
+             | Some _, None -> -1
+             | None, Some _ -> 1
+             | _,_ -> 
+                 (List.length m2) - (List.length m1) )
+       | res ->  res
+  
+  let compare eq1 eq2 =
+    match compare eq1 eq2 with
+       0 -> Pervasives.compare eq1 eq2
+      | res -> res 
 end 
+*)
 
 module EqualitySet = Set.Make(OrderedEquality);;
 
@@ -208,7 +239,7 @@ let rec select env goals passive (active, _) =
           (Negative, hd),
           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
       | [], (hd:EqualitySet.elt)::tl ->
-          let w,_,_,_,_ = hd in
+          let w,_,_,_ = hd in
           let passive_table =
            Indexing.remove_index passive_table hd
           in  (Positive, hd),
@@ -261,7 +292,7 @@ let rec select env goals passive (active, _) =
   | _ ->
       symbols_counter := !symbols_ratio;
       let set_selection set = EqualitySet.min_elt set in 
-      (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *)
+      (* let set_selection l = min_elt (fun (w,_,_,_) -> w) l in *)
       if EqualitySet.is_empty neg_set then
         let current = set_selection pos_set in
         let passive =
@@ -546,7 +577,7 @@ let contains_empty env (negative, positive) =
   try
     let found =
       List.find
-        (fun (w, proof, (ty, left, right, ordering), m, a) ->
+        (fun (w, proof, (ty, left, right, ordering), m) ->
            fst (CicReduction.are_convertible context left right ugraph))
         negative
     in
@@ -733,7 +764,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
   let active_list, newa = 
     List.fold_right
       (fun (s, equality) (res, newn) ->
-         let ew, _, _, _, _ = equality in
+         let ew, _, _, _ = equality in
          if ew < min_weight then
            (s, equality)::res, newn
          else
@@ -779,7 +810,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
 let backward_simplify_passive env new_pos new_table min_weight passive =
   let (nl, ns), (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
-    let ew, _, _, _, _ = equality in
+    let ew, _, _, _ = equality in
     if ew < min_weight then
       equality::resl, ress, newn
     else
@@ -808,7 +839,7 @@ let backward_simplify env new' ?passive active =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
-         let ew, _, _, _, _ = e in
+         let ew, _, _, _ = e in
          (Positive, e)::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) (snd new')
   in
@@ -830,7 +861,7 @@ let close env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
-         let ew, _, _, _, _ = e in
+         let ew, _, _, _ = e in
          (Positive, e)::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) (snd new')
   in
@@ -842,7 +873,7 @@ let close env new' given =
 ;;
 
 let is_commutative_law eq =
-  let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+  let w, proof, (eq_ty, left, right, order), metas = snd eq in
     match left,right with
        Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], 
        Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
@@ -1041,7 +1072,7 @@ let apply_equality_to_goal env equality goal =
   let module HL = HelmLibraryObjects in
   let module I = Inference in
   let metasenv, context, ugraph = env in
-  let _, proof, (ty, left, right, _), metas, args = equality in
+  let _, proof, (ty, left, right, _), metas = equality in
   let eqterm =
     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
@@ -1630,7 +1661,7 @@ and given_clause_aux dbd env goals theorems passive active =
             debug_print
               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                        (string_of_equality ~env current)));
-            let _, proof, _, _, _  = current in
+            let _, proof, _, _ = current in
             ParamodulationSuccess (Some proof, env)
           ) else (           
             debug_print
@@ -1648,7 +1679,7 @@ and given_clause_aux dbd env goals theorems passive active =
             if res then
               let proof =
                 match goal' with
-                | Some goal -> let _, proof, _, _, _ = goal in Some proof
+                | Some goal -> let _, proof, _, _ = goal in Some proof
                 | None -> None
               in
               ParamodulationSuccess (proof, env)
@@ -1700,7 +1731,7 @@ and given_clause_aux dbd env goals theorems passive active =
                   let proof =
                     match goal with
                     | Some goal ->
-                        let _, proof, _, _, _ = goal in Some proof
+                        let _, proof, _, _ = goal in Some proof
                     | None -> None
                   in
                   ParamodulationSuccess (proof, env)
@@ -1740,6 +1771,7 @@ let rec given_clause_fullred dbd env goals theorems passive active =
         | _ -> assert false
       in
       ( prerr_endline "esco qui";
+        (*
        let s = Printf.sprintf "actives:\n%s\n"
          (String.concat "\n"
              ((List.map
@@ -1752,7 +1784,7 @@ let rec given_clause_fullred dbd env goals theorems passive active =
                (string_of_equality ~env)
                (let x,y,_ = passive in (fst x)@(fst y)))) in
          prerr_endline s;
-         prerr_endline sp;
+         prerr_endline sp; *)
       ParamodulationSuccess (proof, env))
     else
       given_clause_fullred_aux dbd env goals theorems passive active
@@ -1778,6 +1810,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                  " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
                 " #ACTIVES: " ^ string_of_int (size_of_active active) ^
                  " #PASSIVES: " ^ string_of_int (size_of_passive passive));
+(*
   if (size_of_active active) mod 50 = 0 then
     (let s = Printf.sprintf "actives:\n%s\n"
       (String.concat "\n"
@@ -1791,7 +1824,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
              (string_of_equality ~env)
              (let x,y,_ = passive in (fst x)@(fst y)))) in
       prerr_endline s;
-      prerr_endline sp);
+      prerr_endline sp); *)
   let time1 = Unix.gettimeofday () in
   let (_,context,_) = env in
   let selection_estimate = get_selection_estimate () in
@@ -1839,7 +1872,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
             debug_print
               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                        (string_of_equality ~env current)));
-            let _, proof, _, _, _ = current in 
+            let _, proof, _, _ = current in 
             ParamodulationSuccess (Some proof, env)
           ) else (
             debug_print
@@ -1954,7 +1987,7 @@ end prova *)
             | true, goal ->
                 let proof =
                   match goal with
-                  | Some goal -> let _, proof, _, _, _ = goal in Some proof
+                  | Some goal -> let _, proof, _, _ = goal in Some proof
                   | None -> None
                 in
                 ParamodulationSuccess (proof, env)
@@ -2132,7 +2165,7 @@ let main dbd full term metasenv ugraph =
             print_endline (PP.pp proof names);
             let newmetasenv =
               List.fold_left
-                (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
+                (fun m (_, _, _, menv) -> m @ menv) metasenv equalities
             in
             let _ =
               (*try*)