helm/software/components/binaries/matitaprover/matitaprover.ml

   1 let main () =
   2   let problem_file = ref "" in
   3   Arg.parse [
   4    ] (fun x -> problem_file := x) "matitaprover [problemfile]";
   5   let hypotheses, goal = Tptp_cnf.parse !problem_file in
   6   let module B : Terms.Blob = struct
   7         type t = Ast.atom
   8         let eq a b = a = b
   9         let compare = Pervasives.compare
  10         let eqP = Ast.True
  11         let pp x = ""
  12         let embed x = Terms.Var 0
  13         let saturate x y = Terms.Var 0,Terms.Var 0
  14   end
  15   in
  16   let module P = Paramod.Paramod(B) in
  17   let bag = Terms.M.empty, 0 in
  18   let g_passives = assert false in
  19   let passives = assert false in
  20   ignore(P.paramod bag ~g_passives ~passives);
  21   ()
  22 ;;
  23
  24 main ()