proof reconstruction almost OK

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 8903ec02fc1c24082fe54d53ddbb32006ec761c4..f0cd03758594d92411284fd0e1945d86d21a3967 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -165,27 +165,42 @@ let nparamod rdb metasenv subst context t table =
           Set.Make(struct type t=int let compare=Pervasives.compare end)
         in
         let all id = 
-          let rec traverse acc i =
+          let rec traverse ongoal (accg,acce) i =
             match Terms.M.find i bag with
-            | (_,_,_,Terms.Exact _) -> acc
+            | (_,_,_,Terms.Exact _) -> accg, acce
             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> 
-               traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2    
+               let accg, acce = 
+                 if ongoal then C.add i1 accg, acce
+                 else accg, C.add i1 acce
+               in
+               let acce = C.add i2 acce in
+                 traverse false (traverse ongoal (accg,acce) i1) i2    
           in
-           C.elements (traverse C.empty id)
+            traverse true (C.empty,C.empty) id
         in
-        S.topological_sort (all i) all
+        let esteps = 
+          S.topological_sort (C.elements (snd (all i))) 
+           (fun i -> C.elements (snd (all i)))
+        in
+        let gsteps = 
+          S.topological_sort (C.elements (fst (all i))) 
+           (fun i -> C.elements (fst (all i)))
+        in
+        let gsteps = List.rev gsteps in
+        esteps@gsteps
       in
       prerr_endline "YES!";
       prerr_endline "Proof:"; 
       List.iter (fun x -> 
               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
-      let proofterm = B.mk_proof bag l in
+      let proofterm = B.mk_proof bag i l in
       prerr_endline
        (NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context
          proofterm); 
       let _metasenv, _subst, _proofterm, _prooftype = 
         NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None
       in
+      prerr_endline "REFINED!";
       ()
   | Failure _ -> prerr_endline "FAILURE";
 ;;