From: denes <??>
Date: Thu, 25 Jun 2009 15:24:09 +0000 (+0000)
Subject: Various fixes
X-Git-Tag: make_still_working~3795
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c2b31c242aa81dc6f3c73e7e2a3ec0789a21edd;p=helm.git

Various fixes
---

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 26b7f6fa4..4c99f5b9c 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -130,7 +130,7 @@ module Utils (B : Terms.Blob) = struct
   let add_to_bag bag  (_,lit,vl,proof) =
     let id = mk_id () in
     let clause = (id, lit, vl, proof) in
-    let bag = Terms.M.add id clause bag in
+    let bag = Terms.M.add id (clause,false) bag in
     bag, clause 
    ;;
     
diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 35c3c02b1..1e50999e9 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -113,7 +113,7 @@
        t vl  
     in
     let get_literal id =
-      let _, lit, vl, proof = Terms.M.find id bag in
+      let (_, lit, vl, proof),_ = Terms.M.find id bag in
       let lit =match lit with 
           | Terms.Predicate t -> assert false 
           | Terms.Equation (l,r,ty,_) -> 
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 105f5c86b..47975fb3b 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-(* let debug s = prerr_endline s ;;*)
+ (*let debug s = prerr_endline s ;;*)
  let debug _ = ();;
     
 let max_nb_iter = 999999999 ;;
@@ -174,7 +174,7 @@ module Paramod (B : Terms.Blob) = struct
 
     let rec aux_select passives g_passives =
       let backward,current,passives,g_passives =
-	select ~use_age passives g_passives
+	select ~use_age:false passives g_passives
       in
 	if backward then
 	 match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
@@ -224,10 +224,10 @@ module Paramod (B : Terms.Blob) = struct
         let l =
           let rec traverse ongoal (accg,acce) i =
             match Terms.M.find i bag with
-              | (id,_,_,Terms.Exact _) ->
+              | (id,_,_,Terms.Exact _),_ ->
           	if ongoal then [i],acce else
           	  if (List.mem i acce) then accg,acce else accg,acce@[i]
-              | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
+              | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_ ->
           	if (not ongoal) && (List.mem i acce) then accg,acce
           	else
                     let accg,acce = 
@@ -241,9 +241,9 @@ module Paramod (B : Terms.Blob) = struct
         prerr_endline 
           (Printf.sprintf "Found proof, %fs" 
             (Unix.gettimeofday() -. timeout +. amount_of_time));
-        prerr_endline "Proof:"; 
+        (* prerr_endline "Proof:"; 
         List.iter (fun x -> prerr_endline (string_of_int x);
-                prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+                prerr_endline (Pp.pp_unit_clause (fst (Terms.M.find x bag)))) l;*)
         [ bag, i, l ]
     | Failure (msg,_bag,_maxvar,nb_iter) -> 
         prerr_endline msg;
diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index bba9a26ae..8a74fa762 100644
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -68,8 +68,8 @@ let pp_proof bag ~formatter:f p =
           eq (string_of_rule rule);
 	Format.fprintf f "|%d with %d dir %s))" eq1 eq2
 	  (string_of_direction dir);
-	let (_, _, _, proof1) = Terms.M.find eq1 bag in
-	let (_, _, _, proof2) = Terms.M.find eq2 bag in
+	let (_, _, _, proof1),_ = Terms.M.find eq1 bag in
+	let (_, _, _, proof2),_ = Terms.M.find eq2 bag in
 	  Format.fprintf f "@[<v 2>";
           aux eq1 proof1;	    
           aux eq2 proof2;
@@ -123,7 +123,7 @@ let pp_unit_clause ~formatter:f c =
 let pp_bag ~formatter:f bag = 
   Format.fprintf f "@[<v>";
   Terms.M.iter 
-  (fun _ c -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag;
+  (fun _ c,_ -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag;
   Format.fprintf f "@]"
 ;;
 
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 61d6c0589..8e77936c8 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -267,24 +267,24 @@ module Superposition (B : Terms.Blob) =
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       let bag, clause = demodulate bag clause table in
-      if is_identity_clause ~unify:false clause then None
+      if is_identity_clause ~unify:false clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
-	  | None -> Some (bag, clause)
-	  | Some _ -> None
+	  | None -> bag, Some clause
+	  | Some _ -> bag, None
     ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
-	| None -> None (* new_clause has been discarded *)
-	| Some (bag, clause) ->
+	| bag,None -> None (* new_clause has been discarded *)
+	| bag,(Some clause) ->
 	    let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 	    let bag, alist, atable = 
 	      List.fold_left 
 		(fun (bag, alist, atable as acc) c ->
 		   match simplify ctable maxvar bag c with
-		     |None -> acc (* an active clause as been discarded *)
-		     |Some (bag, c1) ->
+		     |bag,None -> acc (* an active clause as been discarded *)
+		     |bag,Some c1 ->
 			bag, c :: alist, IDX.index_unit_clause atable c)
 		(bag,[],IDX.DT.empty) alist
 	    in
@@ -300,8 +300,8 @@ module Superposition (B : Terms.Blob) =
 	 * - actives and cl if new_clause is not cl *
 	 * - only actives otherwise                 *)
 	match simplify atable1 maxvar bag new_clause with
-	  | None -> (Some cl, None) (* new_clause has been discarded *)
-	  | Some (bag, clause) ->
+	  | bag,None -> (Some cl, None) (* new_clause has been discarded *)
+	  | bag,Some clause ->
 	      (* Simplification of each active clause with clause *
 	       * which is the simplified form of new_clause       *)
               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
@@ -309,8 +309,8 @@ module Superposition (B : Terms.Blob) =
 		List.fold_left 
 		  (fun (bag, newa, alist, atable as acc) c ->
 		     match simplify ctable maxvar bag c with
-		       |None -> acc (* an active clause as been discarded *)
-		       |Some (bag, c1) ->
+		       |bag,None -> acc (* an active clause as been discarded *)
+		       |bag,Some c1 ->
 			    if (c1 == c) then 
 			      bag, newa, c :: alist,
 			    IDX.index_unit_clause atable c
@@ -323,10 +323,10 @@ module Superposition (B : Terms.Blob) =
 		else
 		  (* if new_clause is not cl, we simplify cl with clause *)
 		  match simplify ctable maxvar bag cl with
-		    | None ->
+		    | bag,None ->
 			(* cl has been discarded *)
 			(None, Some (clause, (alist,atable), newa, bag))
-		    | Some (bag,cl1) ->
+		    | bag,Some cl1 ->
 			(Some cl1, Some (clause, (alist,atable), newa, bag))
     ;;
 
@@ -492,7 +492,7 @@ module Superposition (B : Terms.Blob) =
 	debug (Printf.sprintf "Demodulating %d clauses"
 		 (List.length new_clauses));
       let bag, new_clauses = 
-        HExtlib.filter_map_acc (simplify atable maxvar) bag new_clauses
+        HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
       in
 	debug "Demodulated new clauses";
       bag, maxvar, (alist, atable), new_clauses
diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index bcfb0091e..e3e2f8b9f 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -42,7 +42,7 @@ module Superposition (B : Terms.Blob) :
           int ->
           B.t Terms.bag ->
           B.t Terms.unit_clause ->
-            (B.t Terms.bag * B.t Terms.unit_clause) option
+            B.t Terms.bag * (B.t Terms.unit_clause option)
 
     (* may raise success *)
     val simplify_goal : 
diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index bcc3bcf7b..f2a3de020 100644
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -56,7 +56,7 @@ module OT =
 module M : Map.S with type key = int 
   = Map.Make(OT) 
 
-type 'a bag = 'a unit_clause M.t
+type 'a bag = ('a unit_clause * bool) M.t
 
 module type Blob =
   sig
diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index c9c99caa1..7c60f0562 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -54,7 +54,7 @@ type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
 
 module M : Map.S with type key = int 
 
-type 'a bag = 'a unit_clause M.t 
+type 'a bag = ('a unit_clause * bool) M.t
 
 module type Blob =
   sig