2 let problem_file = ref "no-file-given" in
3 let tptppath = ref "./" in
5 "--tptppath", Arg.String (fun p -> tptppath := p), "[path] TPTP lib root"
6 ] (fun x -> problem_file := x) "matitaprover [problemfile]";
7 let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
8 let goal = match goals with [x] -> x | _ -> assert false in
9 let module B : Terms.Blob with type t = Ast.term = struct
12 let compare = Pervasives.compare
13 let eqP = Ast.Constant "=="
16 | Ast.Variable _ -> assert false
17 | Ast.Function _ -> assert false
20 let rec aux m = function
21 | Ast.Variable name ->
22 (try m, List.assoc name m
24 let t = Terms.Var (List.length m) in
26 | Ast.Constant _ as t -> m, Terms.Leaf t
27 | Ast.Function (name,args) ->
30 (fun x _ m -> aux m x) m args
32 m, Terms.Node (Terms.Leaf (Ast.Constant name):: args)
37 let vars, ty = embed ty in
38 let _, bo = embed bo in
39 let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
42 let embed t = snd(embed t);;
46 let module P = Paramod.Paramod(B) in
47 let module Pp = Pp.Pp(B) in
48 let bag = Terms.M.empty, 0 in
49 let bag, g_passives = P.mk_goal bag goal in
51 HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses
53 prerr_endline "Facts";
54 prerr_endline (String.concat "\n" (List.map Pp.pp_unit_clause passives));
56 prerr_endline (Pp.pp_unit_clause g_passives);
57 ignore(P.paramod bag ~g_passives:[g_passives] ~passives);