helm/software/components/ng_paramodulation/paramod.ml

   1 let nparamod metasenv subst context t =
   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 res = B.embed t 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 test_unification _ = function
  15     | Terms.Node [_; _; lhs; rhs] ->
  16         prerr_endline "Unification test :";
  17         prerr_endline (Pp.pp_foterm lhs);
  18         prerr_endline (Pp.pp_foterm rhs);
  19         FU.unification [] [] lhs rhs
  20     | _ -> assert false
  21   in
  22   let subst,vars = test_unification [] res in
  23     prerr_endline "Result :";
  24     prerr_endline (Pp.pp_foterm res);
  25     prerr_endline "Substitution :";
  26     prerr_endline (Pp.pp_substitution subst)
  27 ;;