Commit 0459a044 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

TPTP parser started

parent d57ad4af
......@@ -21,6 +21,7 @@ type loc = Loc.position
type atomic_word = string
type variable = string
type distinct = string
(** TFF type *)
......@@ -60,13 +61,16 @@ type defined_func =
| DFfloor | DFceil
| DFtrunc | DFround
| DFtoint | DFtorat | DFtoreal
| DFunknown of string
type distinct = string
type num_integer = string
type num_rational = string * string
type num_real = string * string option * string option
type number =
| Nint of string
| Nrat of string
| Nreal of string
| Nint of num_integer
| Nrat of num_rational
| Nreal of num_real
type formula_node =
| LFqnt of quant * tyvar list * formula
......@@ -113,7 +117,7 @@ type role =
type input =
| Formula of kind * name * role * top_formula * loc
| Include of file * name list option * loc
| Include of file * name list * loc
type tptp_file = tptp_input list
......@@ -37,6 +37,7 @@
| DoubleDollarWord -> fprintf fmt "system-specifics are not supported"
| _ -> raise e)
(*
let defwords = Hashtbl.create 97
let () = List.iter (fun (x,y) -> Hashtbl.add defwords x y) [
"ceiling", CEILING;
......@@ -77,6 +78,7 @@
"tType", TTYPE;
"uminus", UMINUS;
]
*)
let keywords = Hashtbl.create 97
let () = List.iter (fun (x,y) -> Hashtbl.add keywords x y) [
......@@ -142,23 +144,27 @@ rule token = parse
{ raise DoubleDollarWord }
| '+'? (natural as s)
| '-' natural as s
{ INTEGER s }
{ INTNUM s }
| '+'? (natural as n) '/' (positive as d)
| ('-' natural as n) '/' (positive as d)
{ RATIONAL (n,d) }
{ RATNUM (n,d) }
| '+'? (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('+'? (natural as e)))?
| ('-' natural as i) ('.' (digit+ as f))? (['e' 'E'] ('+'? (natural as e)))?
| '+'? (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('-' natural as e))?
| ('-' natural as i) ('.' (digit+ as f))? (['e' 'E'] ('-' natural as e))?
{ REAL (i,f,e) }
{ REALNUM (i,f,e) }
| "/*/"
{ SLASH_STAR_SLASH }
| "/*"
{ comment_start_loc := loc lexbuf; comment_block lexbuf; token lexbuf }
| "%"
{ comment_start_loc := loc lexbuf; comment_line lexbuf; token lexbuf }
| "."
{ DOT }
| ","
{ COMMA }
| ":"
{ COLON }
| "("
{ LEFTPAR }
| ")"
......@@ -167,8 +173,6 @@ rule token = parse
{ LEFTSQ }
| "]"
{ RIGHTSQ }
| ":"
{ COLON }
| "-->"
{ LONGARROW }
| "<="
......@@ -185,8 +189,6 @@ rule token = parse
{ NBAR }
| "~"
{ TILDE }
| "."
{ DOT }
| "="
{ EQUAL }
| "!="
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment