1 let nparamod metasenv subst context t table =
3 let metasenv = metasenv
8 let module B = NCicBlob.NCicBlob(C) in
9 let module Pp = Pp.Pp (B) in
10 let module FU = FoUnif.Founif(B) in
11 let module IDX = Index.Index(B) in
12 let module Sup = Superposition.Superposition(B) in
13 let module Utils = FoUtils.Utils(B) in
15 let test_unification _ = function
16 | Terms.Node [_; _; lhs; rhs] ->
17 prerr_endline "Unification test :";
18 prerr_endline (Pp.pp_foterm lhs);
19 prerr_endline (Pp.pp_foterm rhs);
20 FU.unification [] [] lhs rhs
23 let subst,vars = test_unification [] res in
24 prerr_endline "Result :";
25 prerr_endline (Pp.pp_foterm res);
26 prerr_endline "Substitution :";
27 prerr_endline (Pp.pp_substitution subst)
29 let mk_clause maxvar t =
31 let proof = B.embed (NCic.Rel ~-1) in
32 Utils.mk_unit_clause maxvar ty proof
34 let clause, maxvar = mk_clause 0 t in
35 prerr_endline "Input clause :";
36 prerr_endline (Pp.pp_unit_clause clause);
37 let bag = Utils.empty_bag in
38 let active_clauses, maxvar =
41 let c, m = mk_clause maxvar t in
46 List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
48 let bag, maxvar, newclauses =
49 Sup.superposition_right_with_table bag maxvar clause table
51 prerr_endline "Output clauses :";
52 List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;