Extended the equality case to non ground terms

[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 3206ff7d20bf0977752fa3cac36173cb73c6a2a5..13b1d7270bc3fd1f785d8831a97ac284ec0b0bce 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,4 +1,5 @@
-let nparamod metasenv subst context t =
+let nparamod metasenv subst context t table =
+  prerr_endline "========================================";
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -7,19 +8,50 @@ let nparamod metasenv subst context t =
   in
   let module B = NCicBlob.NCicBlob(C) in
   let module Pp = Pp.Pp (B) in
-  let res,vars = B.embed t in
-  let module FU = Founif.Founif(B) in
-  let test_unification vars = function
+  let module FU = FoUnif.Founif(B) in
+  let module IDX = Index.Index(B) in
+  let module Sup = Superposition.Superposition(B) in
+  let module Utils = FoUtils.Utils(B) in
+(*
+  let test_unification _ = function
     | Terms.Node [_; _; lhs; rhs] ->
        prerr_endline "Unification test :";
        prerr_endline (Pp.pp_foterm lhs);
        prerr_endline (Pp.pp_foterm rhs);
-       FU.unification vars [] lhs rhs
+        FU.unification [] [] lhs rhs
     | _ -> assert false
   in
-  let subst,vars = test_unification vars res in
+  let subst,vars = test_unification [] res in
     prerr_endline "Result :";
     prerr_endline (Pp.pp_foterm res);
     prerr_endline "Substitution :";
     prerr_endline (Pp.pp_substitution subst)
+*)
+  let mk_clause maxvar t =
+    let ty = B.embed t in
+    let proof = B.embed (NCic.Rel ~-1) in
+    Utils.mk_unit_clause maxvar ty proof 
+  in
+  let clause, maxvar = mk_clause 0 t in
+  prerr_endline "Input clause :";
+  prerr_endline (Pp.pp_unit_clause clause);
+  let bag = Utils.empty_bag in
+  let active_clauses, maxvar = 
+    List.fold_left
+      (fun (cl,maxvar) t -> 
+         let c, m = mk_clause maxvar t in
+         c::cl, m)
+      ([],maxvar) table 
+  in
+  let table =  
+    List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
+  in
+  prerr_endline "Active table:";
+  List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
+  let bag, maxvar, _, newclauses = 
+    Sup.superposition_right bag maxvar clause (active_clauses, table)
+  in
+  prerr_endline "Output clauses :";
+  List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
+  prerr_endline "========================================";
 ;;