first proof reconstruction attempt, still bugged since it

[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 b301e800547aa40aa0e2c61a98af0916f2a8ccca..36adca45413def9a1fa5214571a84c92edcbfbca 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -2,7 +2,7 @@ let debug s = ()
 (*  prerr_endline s *)
 ;;
 
-let nparamod metasenv subst context t table =
+let nparamod rdb metasenv subst context t table =
   let nb_iter = ref 100 in
   prerr_endline "========================================";
   let module C = struct
@@ -148,9 +148,37 @@ let nparamod metasenv subst context t table =
   in
   let actives = [], IDX.DT.empty in
   try given_clause bag maxvar actives passives g_actives g_passives
-  with Sup.Success (bag, _, mp) ->
-    prerr_endline "YES!";
-    prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp)
-    (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *)
-    | Failure _ -> prerr_endline "FAILURE"
+  with 
+  | Sup.Success (bag, _, (i,_,_,_)) ->
+      let l =
+        let module S  = 
+          HTopoSort.Make(struct type t=int let compare=Pervasives.compare end)
+        in
+        let module C : Set.S with type elt = int = 
+          Set.Make(struct type t=int let compare=Pervasives.compare end)
+        in
+        let all id = 
+          let rec traverse acc i =
+            match Terms.M.find i bag with
+            | (_,_,_,Terms.Exact _) -> acc
+            | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> 
+               traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2    
+          in
+           C.elements (traverse C.empty id)
+        in
+        S.topological_sort (all i) all
+      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
+      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
+      ()
+  | Failure _ -> prerr_endline "FAILURE";
 ;;