helm/software/components/ng_paramodulation/paramod.ml

   1 let nparamod metasenv subst context t table =
   2   prerr_endline "========================================";
   3   let module C = struct
   4     let metasenv = metasenv
   5     let subst = subst
   6     let context = context
   7   end
   8   in
   9   let module B = NCicBlob.NCicBlob(C) in
  10   let module Pp = Pp.Pp (B) in
  11   let module FU = FoUnif.Founif(B) in
  12   let module IDX = Index.Index(B) in
  13   let module Sup = Superposition.Superposition(B) in
  14   let module Utils = FoUtils.Utils(B) in
  15 (*
  16   let test_unification _ = function
  17     | Terms.Node [_; _; lhs; rhs] ->
  18         prerr_endline "Unification test :";
  19         prerr_endline (Pp.pp_foterm lhs);
  20         prerr_endline (Pp.pp_foterm rhs);
  21         FU.unification [] [] lhs rhs
  22     | _ -> assert false
  23   in
  24   let subst,vars = test_unification [] res in
  25     prerr_endline "Result :";
  26     prerr_endline (Pp.pp_foterm res);
  27     prerr_endline "Substitution :";
  28     prerr_endline (Pp.pp_substitution subst)
  29 *)
  30   let mk_clause maxvar t =
  31     let ty = B.embed t in
  32     let proof = B.embed (NCic.Rel ~-1) in
  33     Utils.mk_unit_clause maxvar ty proof
  34   in
  35   let clause, maxvar = mk_clause 0 t in
  36   prerr_endline "Input clause :";
  37   prerr_endline (Pp.pp_unit_clause clause);
  38   let bag = Utils.empty_bag in
  39   let active_clauses, maxvar =
  40     List.fold_left
  41       (fun (cl,maxvar) t ->
  42          let c, m = mk_clause maxvar t in
  43          c::cl, m)
  44       ([],maxvar) table
  45   in
  46   let table =
  47     List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
  48   in
  49   prerr_endline "Active table:";
  50   List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
  51   let bag, maxvar, _, newclauses =
  52     Sup.infer_right bag maxvar clause (active_clauses, table)
  53   in
  54   prerr_endline "Output clauses :";
  55   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
  56   prerr_endline "Proofs: ";
  57   prerr_endline (Pp.pp_bag bag);
  58   prerr_endline "========================================";
  59 ;;