tests/test_tptp.ml

   1
   2
   3 open Why3
   4 open Tptp_ast
   5 open Format
   6
   7 let pr_kind fmt k =
   8   match k with
   9   | TFF -> fprintf fmt "TFF"
  10   | FOF -> fprintf fmt "FOF"
  11   | CNF -> fprintf fmt "CNF"
  12
  13 let pr_role fmt r =
  14   match r with
  15   | Axiom -> fprintf fmt "Axiom"
  16   | Hypothesis -> fprintf fmt "Hypothesis"
  17   | Definition -> fprintf fmt "Definition"
  18   | Assumption -> fprintf fmt "Assumption"
  19   | Corollary -> fprintf fmt "Corollary"
  20   | Lemma -> fprintf fmt "Lemma"
  21   | Theorem -> fprintf fmt "Theorem"
  22   | Conjecture -> fprintf fmt "Conjecture"
  23   | Negated_conjecture -> fprintf fmt "Negated_conjecture"
  24   | Type -> fprintf fmt "Type"
  25
  26 let pr_op fmt op =
  27   match op with
  28   | BOequ -> fprintf fmt "equ"
  29   | BOnequ -> fprintf fmt "nequ"
  30   | BOimp -> fprintf fmt "imp"
  31   | BOpmi -> fprintf fmt "pmi"
  32   | BOand -> fprintf fmt "and"
  33   | BOor -> fprintf fmt "or"
  34   | BOnand -> fprintf fmt "nand"
  35   | BOnor -> fprintf fmt "nor"
  36
  37 let rec pr_expr fmt e =
  38   match e.e_node with
  39   | Elet(e1,e2) -> fprintf fmt "Elet(...)"
  40   | Eite(e1,e2,e3) -> fprintf fmt "Eite(...)"
  41   | Eqnt(q,vl,e) -> fprintf fmt "Eqnt(...)"
  42   | Ebin(op,e1,e2) ->
  43     fprintf fmt "Ebin(%a,%a,%a)" pr_op op pr_expr e1 pr_expr e2
  44   | Enot e -> fprintf fmt "Enot(%a)" pr_expr e
  45   | Eequ(e1,e2) -> fprintf fmt "Equ(%a,%a)" pr_expr e1 pr_expr e2
  46   | Eapp(w,el) ->
  47     fprintf fmt "Eapp(%s,[%a])" w (Pp.print_list Pp.comma pr_expr) el
  48   | Edef(w,el) -> fprintf fmt "Edef(...)"
  49   | Evar v -> fprintf fmt "Evar(%s)" v
  50   | Edob d -> fprintf fmt "Edob(...)"
  51   | Enum n -> fprintf fmt "Enum(...)"
  52
  53 let pr_top_formula fmt f =
  54   match f with
  55   | LogicFormula e -> fprintf fmt "LogicFormula(%a)" pr_expr e
  56   | TypedAtom(a,t) -> fprintf fmt "TypedAtom"
  57   | Sequent(l1,l2) -> fprintf fmt "Sequent"
  58
  59 let pr_decl fmt d =
  60   match d with
  61   | Formula(kind,name,role,top_formula,loc) ->
  62     fprintf fmt "@[<hov 2>{ kind = %a,@ name = '%s',@ role = %a,@ form = %a }@]"
  63       pr_kind kind name pr_role role pr_top_formula top_formula
  64   | Include(file,namelist,loc) ->
  65     fprintf fmt "include file '%s'" file
  66
  67 let pr_file fmt a =
  68   Pp.print_list Pp.newline pr_decl fmt a
  69
  70 exception Unsupported of string
  71
  72 let unsupported s = raise (Unsupported s)
  73
  74 let check_op op =
  75   match op with
  76   | BOequ -> unsupported "BOequ"
  77   | BOnequ -> unsupported "BOnequ"
  78   | BOimp -> ()
  79   | BOpmi -> unsupported "BOpmi"
  80   | BOand -> ()
  81   | BOor -> ()
  82   | BOnand -> ()
  83   | BOnor -> ()
  84
  85 let rec check_expr e = match e.e_node with
  86   | Elet(e1,e2) -> unsupported "let"
  87   | Eite(e1,e2,e3) -> unsupported "ite"
  88   | Eqnt(q,vl,e) -> check_expr e
  89   | Ebin(op,e1,e2) -> check_op op; check_expr e1; check_expr e2
  90   | Enot e -> check_expr e
  91   | Eequ(e1,e2) -> unsupported "equ"
  92   | Eapp(w,el) -> List.iter check_expr el
  93   | Edef(w,el) -> unsupported "def"
  94   | Evar v -> ()
  95   | Edob d -> unsupported "dob"
  96   | Enum n -> unsupported "num"
  97
  98 let check_top_formula f =
  99   match f with
 100   | LogicFormula e -> check_expr e
 101   | TypedAtom _ -> unsupported "TypedAtom"
 102   | Sequent _ -> unsupported "Sequent"
 103
 104 let check_role r =
 105   match r with
 106   | Axiom -> ()
 107   | Hypothesis -> ()
 108   | Definition -> unsupported "Definition"
 109   | Assumption -> ()
 110   | Corollary -> ()
 111   | Lemma -> ()
 112   | Theorem -> ()
 113   | Conjecture -> ()
 114   | Negated_conjecture -> ()
 115   | Type -> unsupported "Type"
 116
 117
 118 let check_kind k =
 119   match k with
 120   | TFF -> unsupported "TFF"
 121   | FOF -> ()
 122   | CNF -> ()
 123
 124 let check_decl d =
 125   match d with
 126   | Include _ -> unsupported "Include"
 127   | Formula(kind,_,role,top_formula,_) ->
 128     check_kind kind; check_role role; check_top_formula top_formula
 129
 130 let check_file a = List.iter check_decl a
 131
 132 let () =
 133   if Array.length Sys.argv <> 2 then
 134     begin
 135       eprintf "Usage: %s <file>@." Sys.argv.(0);
 136       exit 2
 137     end
 138   else
 139     let file = Sys.argv.(1) in
 140     try
 141       let ast = Tptp_lexer.load file in
 142       check_file ast;
 143       (* printf "%a@." pr_file ast; *)
 144       printf "File '%s' is OK.@." file;
 145       exit 0
 146     with
 147     | Tptp_lexer.FileNotFound f ->
 148       eprintf "File not found: %s@." f; exit 2
 149     | Unsupported s ->
 150       eprintf "File %s: '%s' is not supported@." file s; exit 1
 151     | e ->
 152       eprintf "Parsing error: %a@." Exn_printer.exn_printer e;
 153       exit 2