plugins/tptp/tptp_lexer.mll

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2024 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 {
  13   open Format
  14   open Lexing
  15   open Tptp_ast
  16   open Tptp_parser
  17
  18   open Why3
  19
  20   (* lexical errors *)
  21
  22   exception IllegalLexeme of string
  23   exception UnterminatedComment
  24   exception UnknownDDW of string
  25   exception UnknownDW of string
  26
  27   let () = Exn_printer.register (fun fmt e -> match e with
  28     | IllegalLexeme s -> fprintf fmt "illegal lexeme %s" s
  29     | UnterminatedComment -> pp_print_string fmt "unterminated comment"
  30     | UnknownDDW s -> fprintf fmt "unknown system_word %s" s
  31     | UnknownDW s -> fprintf fmt "unknown defined_word %s" s
  32     | _ -> raise e)
  33
  34   let defwords = Hashtbl.create 97
  35   let () = List.iter (fun (x,y) -> Hashtbl.add defwords x y) [
  36     "ceiling", DWORD (DF DFceil);
  37     "difference", DWORD (DF DFdiff);
  38     "distinct", DWORD (DP DPdistinct);
  39     "false", DWORD (DP DPfalse);
  40     "floor", DWORD (DF DFfloor);
  41     "greater", DWORD (DP DPgreater);
  42     "greatereq", DWORD (DP DPgreatereq);
  43     "i", DWORD (DT DTuniv);
  44     "int", DWORD (DT DTint);
  45     "is_int", DWORD (DP DPisint);
  46     "is_rat", DWORD (DP DPisrat);
  47     "ite_f", ITE_F;
  48     "ite_t", ITE_T;
  49     "iType", DWORD (DT DTuniv);
  50     "let_tt", LET_TT;
  51     "let_ft", LET_FT;
  52     "let_tf", LET_TF;
  53     "let_ff", LET_FF;
  54     "less", DWORD (DP DPless);
  55     "lesseq", DWORD (DP DPlesseq);
  56     "o", DWORD (DT DTprop);
  57     "oType", DWORD (DT DTprop);
  58     "product", DWORD (DF DFprod);
  59     "quotient", DWORD (DF DFquot);
  60     "quotient_e", DWORD (DF DFquot_e);
  61     "quotient_t", DWORD (DF DFquot_t);
  62     "quotient_f", DWORD (DF DFquot_f);
  63     "rat", DWORD (DT DTrat);
  64     "real", DWORD (DT DTreal);
  65     "remainder_e", DWORD (DF DFrem_e);
  66     "remainder_t", DWORD (DF DFrem_t);
  67     "remainder_f", DWORD (DF DFrem_f);
  68     "round", DWORD (DF DFround);
  69     "sum", DWORD (DF DFsum);
  70     "to_int", DWORD (DF DFtoint);
  71     "to_rat", DWORD (DF DFtorat);
  72     "to_real", DWORD (DF DFtoreal);
  73     "true", DWORD (DP DPtrue);
  74     "truncate", DWORD (DF DFtrunc);
  75     "tType", DWORD (DT DTtype);
  76     "uminus", DWORD (DF DFumin);
  77   ]
  78
  79   let keywords = Hashtbl.create 97
  80   let () = List.iter (fun (x,y) -> Hashtbl.add keywords x y) [
  81     "assumption", ASSUMPTION;
  82     "axiom", AXIOM;
  83     "cnf", CNFK;
  84     "conjecture", CONJECTURE;
  85     "corollary", COROLLARY;
  86     "definition", DEFINITION;
  87     "fof", FOFK;
  88     "hypothesis", HYPOTHESIS;
  89     "include", INCLUDE;
  90     "lemma", LEMMA;
  91     "negated_conjecture", NEGATED_CONJECTURE;
  92     "tff", TFFK;
  93     "theorem", THEOREM;
  94     "type", TYPE;
  95   ]
  96
  97   let comment_start_loc = ref Loc.dummy_position
  98
  99   let loc lb = Loc.extract (lexeme_start_p lb, lexeme_end_p lb)
 100 }
 101
 102 let newline = '\n'
 103 let space = [' ' '\t' '\r']
 104
 105 let lalpha = ['a'-'z']
 106 let ualpha = ['A'-'Z']
 107 let digit  = ['0'-'9']
 108 let nzero  = ['1'-'9']
 109
 110 let alnum = lalpha | ualpha | digit | '_'
 111 let lword = lalpha alnum*
 112 let uword = ualpha alnum*
 113
 114 let positive = nzero digit*
 115 let natural  = '0' | positive
 116
 117 let sq_char = [' '-'&' '('-'[' ']'-'~'] | '\\' ['\\' '\'']
 118 let do_char = [' '-'!' '#'-'[' ']'-'~'] | '\\' ['\\' '"']
 119
 120 rule token = parse
 121   | newline
 122       { new_line lexbuf; token lexbuf }
 123   | space+
 124       { token lexbuf }
 125   | lword as id
 126       { try Hashtbl.find keywords id with Not_found -> LWORD id }
 127   | uword as id
 128       { UWORD id }
 129   | '\'' (lword as id) '\''
 130       { LWORD id }
 131   | '\'' sq_char+ '\'' as sq
 132       { SINGLE_QUOTED sq }
 133   | '"' (do_char* as dob) '"'
 134       { DISTINCT_OBJECT dob }
 135   | "$_"
 136       { DWORD (DT DTdummy) }
 137   | '$' (lword as id)
 138       { try Hashtbl.find defwords id with Not_found -> raise (UnknownDW id) }
 139   | "$$" (lword as id)
 140       { raise (UnknownDDW id) }
 141   | '+'? (natural as s)
 142       { INTPOSNUM s }
 143   | '-'  (natural as s)
 144       { INTNEGNUM s }
 145   | '+'? (natural as n) '/' (positive as d)
 146       { RATPOSNUM (n,d) }
 147   | '-'  (natural as n) '/' (positive as d)
 148       { RATNEGNUM (n,d) }
 149   | '+'? (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('+'? (natural as e)))?
 150   | '+'? (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('-'   natural as e))?
 151       { REALPOSNUM (i,f,e) }
 152   | '-'  (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('+'? (natural as e)))?
 153   | '-'  (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('-'   natural as e))?
 154       { REALNEGNUM (i,f,e) }
 155   | "/*/"
 156       { raise (IllegalLexeme "/*/") }
 157   | "/*"
 158       { comment_start_loc := loc lexbuf; comment_block lexbuf; token lexbuf }
 159   | "%"
 160       { comment_start_loc := loc lexbuf; comment_line  lexbuf; token lexbuf }
 161   | "."
 162       { DOT }
 163   | ","
 164       { COMMA }
 165   | ":"
 166       { COLON }
 167   | "("
 168       { LEFTPAR }
 169   | ")"
 170       { RIGHTPAR }
 171   | "["
 172       { LEFTSQ }
 173   | "]"
 174       { RIGHTSQ }
 175   | "-->"
 176       { LONGARROW }
 177   | "<="
 178       { LARROW }
 179   | "=>"
 180       { RARROW }
 181   | "<=>"
 182       { LRARROW }
 183   | "<~>"
 184       { NLRARROW }
 185   | "~&"
 186       { NAMP }
 187   | "~|"
 188       { NBAR }
 189   | "~"
 190       { TILDE }
 191   | "&"
 192       { AMP }
 193   | "|"
 194       { BAR }
 195   | "="
 196       { EQUAL }
 197   | "!="
 198       { NEQUAL }
 199   | "*"
 200       { STAR }
 201   | ">"
 202       { GT }
 203   | "!>"
 204       { PI }
 205   | "!"
 206       { BANG }
 207   | "?"
 208       { QUES }
 209   | eof
 210       { EOF }
 211   | _ as c
 212       { Lexlib.illegal_character c lexbuf }
 213
 214 and comment_block = parse
 215   | "*/"
 216       { () }
 217   | newline
 218       { new_line lexbuf; comment_block lexbuf }
 219   | eof
 220       { raise (Loc.Located (!comment_start_loc, UnterminatedComment)) }
 221   | _
 222       { comment_block lexbuf }
 223
 224 and comment_line = parse
 225   | newline
 226       { new_line lexbuf; () }
 227   | eof
 228       { () }
 229   | _
 230       { comment_line lexbuf }
 231
 232 {
 233
 234 let parse file c =
 235   let lb = Lexing.from_channel c in
 236   Loc.set_file file lb;
 237   Loc.with_location (tptp_file token) lb
 238
 239 exception FileNotFound of string
 240
 241 let load file =
 242   let dir = Filename.dirname file in
 243   let tptplib =
 244     try Some (Sys.getenv "TPTP")
 245     with Not_found -> None
 246   in
 247   let rec aux file =
 248     let ch,file =
 249       try (open_in file, file)
 250       with Sys_error _ ->
 251         if not (Filename.is_relative file) then raise (FileNotFound file) else
 252         try let f = Filename.concat dir file in (open_in f,f)
 253         with Sys_error _ ->
 254           match tptplib with
 255           | None ->
 256             raise (FileNotFound (file ^ " (warning: $TPTP was not set)"))
 257           | Some d ->
 258             try let f = Filename.concat d file in (open_in f,f)
 259             with Sys_error _ -> raise (FileNotFound file)
 260     in
 261     let ast = parse file ch in
 262     close_in ch;
 263     let ast =
 264       List.fold_left
 265         (fun acc d ->
 266           match d with
 267           | Formula _ -> d::acc
 268           | Include(file,_,_) ->
 269             let ast = aux file in
 270             List.rev_append ast acc)
 271         [] ast
 272     in List.rev ast
 273   in aux file
 274
 275   let read_channel env path file c =
 276     let ast = parse file c in
 277     Tptp_typing.typecheck env path ast
 278
 279   let () = Env.register_format Env.base_language "tptp" ["p";"ax"] read_channel
 280     ~desc:"TPTP format (CNF FOF FOFX TFF)"
 281
 282 }
 283
 284 (*
 285 Local Variables:
 286 compile-command: "unset LANG; make -C ../.. test"
 287 End:
 288 *)