helm/software/components/ng_paramodulation/paramod.ml

   1 let nparamod metasenv subst context t table =
   2   let module C = struct
   3     let metasenv = metasenv
   4     let subst = subst
   5     let context = context
   6   end
   7   in
   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
  14 (*
  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
  21     | _ -> assert false
  22   in
  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)
  28 *)
  29   let mk_clause maxvar t =
  30     let ty = B.embed t in
  31     let proof = B.embed (NCic.Rel ~-1) in
  32     Utils.mk_unit_clause maxvar ty proof
  33   in
  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 =
  39     List.fold_left
  40       (fun (cl,maxvar) t ->
  41          let c, m = mk_clause maxvar t in
  42          c::cl, m)
  43       ([],maxvar) table
  44   in
  45   let table =
  46     List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
  47   in
  48   let bag, maxvar, newclauses =
  49     Sup.superposition_right_with_table bag maxvar clause table
  50   in
  51   prerr_endline "Output clauses :";
  52   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
  53 ;;