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

   1
   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
   8 ;;
   9
  10 let trans_formulae ~neg = function
  11   | Ast.Disjunction _ -> assert false
  12   | Ast.Atom a -> trans_atom ~neg a
  13   | Ast.NegAtom _ -> assert false
  14 ;;
  15
  16
  17 (* HELPERS *)
  18 let resolve ~tptppath s =
  19   let resolved_name =
  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)
  25       else
  26         tptppath ^ "/" ^ s
  27   in
  28   if HExtlib.is_regular resolved_name then
  29     resolved_name
  30   else
  31     begin
  32       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
  33       exit 1
  34     end
  35 ;;
  36
  37 (* MAIN *)
  38 let parse ~tptppath filename =
  39   let rec aux = function
  40     | [] -> []
  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
  45         aux (statements @ tl)
  46     | hd::tl -> hd :: aux tl
  47   in
  48   let statements = aux [Ast.Inclusion (filename,[])] in
  49   let positives, negatives =
  50     let rec aux p n = function
  51       | [] -> p,n
  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 ->
  56           assert (n = []);
  57           aux p (n@[Ast.Constant name, trans_formulae ~neg:true f]) tl
  58       | _ -> prerr_endline "bad syntax"; assert false
  59     in
  60       aux [] [] statements
  61   in
  62   positives, negatives
  63 ;;
  64