2 let trans_atom ~neg = function
3 | Ast.True | Ast.False | Ast.Predicate _ | Ast.Proposition _ -> assert false
4 | Ast.Eq _ when neg -> assert false
5 | Ast.Eq (a,b) -> Ast.Function ("==",[Ast.Constant "_"; a; b])
6 | Ast.NotEq (a,b) when neg -> Ast.Function ("==",[Ast.Constant "_"; a; b])
7 | Ast.NotEq _ -> assert false
10 let trans_formulae ~neg = function
11 | Ast.Disjunction _ -> assert false
12 | Ast.Atom a -> trans_atom ~neg a
13 | Ast.NegAtom _ -> assert false
18 let resolve ~tptppath s =
20 if tptppath = "/" then s else
21 if Filename.check_suffix s ".p" then
22 (assert (String.length s > 5);
23 let prefix = String.sub s 0 3 in
24 tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
28 if HExtlib.is_regular resolved_name then
32 prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
38 let parse ~tptppath filename =
39 let rec aux = function
41 | (Ast.Inclusion (file,_)) :: tl ->
42 let file = resolve ~tptppath file in
43 let lexbuf = Lexing.from_channel (open_in file) in
44 let statements = Parser.main Lexer.yylex lexbuf in
46 | hd::tl -> hd :: aux tl
48 let statements = aux [Ast.Inclusion (filename,[])] in
49 let positives, negatives =
50 let rec aux p n = function
52 | Ast.Comment _ :: tl -> aux p n tl
53 | Ast.AnnotatedFormula (name, (Ast.Axiom | Ast.Hypothesis), f,_,_) :: tl->
54 aux (p@[Ast.Constant name,trans_formulae ~neg:false f]) n tl
55 | Ast.AnnotatedFormula (name, Ast.Negated_conjecture, f,_,_) :: tl ->
57 aux p (n@[Ast.Constant name, trans_formulae ~neg:true f]) tl
58 | _ -> prerr_endline "bad syntax"; assert false