X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=e38179c77cb83af42a52c32872c6b7173f9306a1;hb=a19551fd50df93951d78eea4c163d434f844047c;hp=86a964c1487f36a7f72deb0c8f2608f621ec2aac;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_paramodulation/paramod.ml b/matita/components/ng_paramodulation/paramod.ml
index 86a964c14..e38179c77 100644
--- a/matita/components/ng_paramodulation/paramod.ml
+++ b/matita/components/ng_paramodulation/paramod.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 let print s = prerr_endline (Lazy.force s) ;; 
-let noprint s = ();;  
+let noprint _s = ();;  
 let debug = noprint;;
 
 let monster = 100;;
@@ -65,7 +65,7 @@ module type Paramod =
 
 module Paramod (B : Orderings.Blob) = struct
   module Pp = Pp.Pp (B) 
-  module FU = FoUnif.Founif(B) 
+  (*module FU = FoUnif.Founif(B)*)
   module IDX = Index.Index(B) 
   module Sup = Superposition.Superposition(B) 
   module Utils = FoUtils.Utils(B) 
@@ -293,14 +293,22 @@ module Paramod (B : Orderings.Blob) = struct
      * new = supright e'' A'' *
      * new'= demod A'' new    *
      * P' = P + new'          *)
-    debug (lazy "Forward infer step...");
+    debug (lazy ("Forward infer step for "^ (Pp.pp_unit_clause current)));
     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
     noprint (lazy (pp_clauses actives passives));
+    let _ = noprint
+      (lazy 
+	 ("Actives before simplification:" ^ (String.concat ";\n" 
+	    (List.map Pp.pp_unit_clause (fst actives))))) in 
     match Sup.keep_simplified current actives bag maxvar
     with
-      | _,None -> s
+      | _,None -> debug(lazy("None")); s
       | bag,Some (current,actives) ->
     debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
+    let _ = noprint
+      (lazy 
+	 ("Actives after simplification:" ^ (String.concat ";\n" 
+	    (List.map Pp.pp_unit_clause (fst actives))))) in 
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
@@ -355,7 +363,7 @@ module Paramod (B : Orderings.Blob) = struct
     debug (lazy("Last chance " ^ string_of_float
 		  (Unix.gettimeofday())));
     let actives_l, active_t = actives in
-    let passive_t,wset,_ = passives in
+    let passive_t,_wset,_ = passives in
     let _ = noprint
       (lazy 
 	 ("Actives :" ^ (String.concat ";\n" 
@@ -485,12 +493,12 @@ module Paramod (B : Orderings.Blob) = struct
     let newstatus = 
       List.fold_left
 	(fun acc g ->
-	   let bag,maxvar,actives,passives,g_actives,g_passives = acc in
-	   let g_passives =
+	   let _bag,_maxvar,_actives,_passives,_g_actives,g_passives = acc in
+	   let _g_passives =
 	     remove_passive_goal g_passives g in
 	   let current = snd g in
 	   let _ = 
-	     debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) 
+	     debug (lazy("Selected goal gn: " ^ Pp.pp_unit_clause current)) 
 	   in
 	     (* we work both on the original goal and the demodulated one*)
 	   let acc = check_and_infer ~no_demod:false iterno acc current
@@ -503,7 +511,7 @@ module Paramod (B : Orderings.Blob) = struct
       let l =
         let rec traverse ongoal (accg,acce) i =
           match Terms.get_from_bag 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,_,_,_)),_,_ ->
@@ -565,8 +573,8 @@ module Paramod (B : Orderings.Blob) = struct
   ;;
 
 let demod s goal =
-  let bag,maxvar,actives,passives,g_actives,g_passives = s in
-  let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+  let bag,maxvar,actives,_passives,_g_actives,_g_passives = s in
+  let (bag,_maxvar), g = mk_goal (bag,maxvar) goal in
   let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
     if g1 = g then GaveUp else compute_result bag i []
 (*
@@ -576,7 +584,7 @@ let demod s goal =
 
 let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
-  if is_passive_g_set_empty g_passives then Error "not an equation"
+  if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology)
   else
   try 
     goal_narrowing 0 2 None s
@@ -590,7 +598,7 @@ let fast_eq_check s goal =
 let nparamod ~useage ~max_steps ?timeout s goal =
   let bag,maxvar,actives,passives,g_actives,g_passives
       = initialize_goal s goal in
-  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  if is_passive_g_set_empty g_passives then (Error "not an equation" : szsontology)
   else
     try given_clause ~useage ~noinfer:false
       bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives