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 Filename.check_suffix s ".p" then
  21       (assert (String.length s > 5);
  22       let prefix = String.sub s 0 3 in
  23       tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
  24     else
  25       tptppath ^ "/" ^ s
  26   in
  27   if HExtlib.is_regular resolved_name then
  28     resolved_name
  29   else
  30     begin
  31       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
  32       exit 1
  33     end
  34 ;;
  35
  36 (* MAIN *)
  37 let parse ~tptppath filename =
  38   let rec aux = function
  39     | [] -> []
  40     | (Ast.Inclusion (file,_)) :: tl ->
  41         let file = resolve ~tptppath file in
  42         let lexbuf = Lexing.from_channel (open_in file) in
  43         let statements = Parser.main Lexer.yylex lexbuf in
  44         aux (statements @ tl)
  45     | hd::tl -> hd :: aux tl
  46   in
  47   let statements = aux [Ast.Inclusion (filename,[])] in
  48   let positives, negatives =
  49     let rec aux p n = function
  50       | [] -> p,n
  51       | Ast.Comment _ :: tl -> aux p n tl
  52       | Ast.AnnotatedFormula (name, (Ast.Axiom | Ast.Hypothesis), f,_,_) :: tl->
  53           aux (p@[Ast.Constant name,trans_formulae ~neg:false f]) n tl
  54       | Ast.AnnotatedFormula (name, Ast.Negated_conjecture, f,_,_) :: tl ->
  55           assert (n = []);
  56           aux p (n@[Ast.Constant name, trans_formulae ~neg:true f]) tl
  57       | _ -> prerr_endline "bad syntax"; assert false
  58     in
  59       aux [] [] statements
  60   in
  61   positives, negatives
  62 ;;
  63