-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
in
let module B = NCicBlob.NCicBlob(C) in
let module Pp = Pp.Pp (B) in
- let res = B.embed t in
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 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 "========================================";
;;