Commit 18171354 authored by Andrei Paskevich's avatar Andrei Paskevich

finish TPTP parser

parent 7f4424b0
......@@ -251,24 +251,32 @@ install-all: install install-lib
# Why plugins
##################
PLUGGENERATED =
PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
PLUG_PARSER = genequlin
PLUG_PRINTER = tptpfof
PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_lexer
PLUGINS = genequlin tptpfof
PLUGINS = genequlin tptpfof tptp
TFF1MODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
TFF1CMO = $(addsuffix .cmo, $(TFF1MODULES))
TFF1CMX = $(addsuffix .cmx, $(TFF1MODULES))
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM))
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TFF1MODULES)
PLUGML = $(addsuffix .ml, $(PLUGMODULES))
PLUGMLI = $(addsuffix .mli, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGDIRS = parser printer transform
PLUGDIRS = parser printer transform tptp
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
$(PLUGCMO) $(PLUGCMX): INCLUDES += $(PLUGINCLUDES)
......@@ -300,6 +308,14 @@ lib/plugins/%.cmo: plugins/transform/%.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $<
lib/plugins/tptp.cmxs: $(TFF1CMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -shared -o $@ $<
lib/plugins/tptp.cmo: $(TFF1CMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -pack -o $@ $<
include .depend.plugins
.depend.plugins: $(PLUGGENERATED)
......
......@@ -17,91 +17,73 @@
(* *)
(**************************************************************************)
type loc = Loc.position
type loc = Why3.Loc.position
type atomic_word = string
type variable = string
type distinct = string
(** TFF type *)
type defined_type =
| DTtype | DTprop | DTuniv
| DTint | DTrat | DTreal
| DTunknown of string
| DTtype | DTprop | DTuniv | DTint
| DTrat | DTreal | DTdummy (* placeholder *)
type tff_type_node =
| TVar of variable
| TConstr of atomic_word * tff_type list
| TDef of defined_type
type defined_func =
| DFumin | DFsum | DFdiff | DFprod
| DFquot | DFquot_e | DFquot_t | DFquot_f
| DFrem_e | DFrem_t | DFrem_f
| DFfloor | DFceil | DFtrunc | DFround
| DFtoint | DFtorat | DFtoreal
and tff_type = { ty_node : tff_type_node ; ty_loc : loc }
type defined_pred =
| DPtrue | DPfalse | DPdistinct
| DPless | DPlesseq | DPgreater | DPgreatereq
| DPisint | DPisrat | DPequal | DPnoneq
type top_type = variable list * tff_type list * tff_type
type defined_word =
| DT of defined_type
| DF of defined_func
| DP of defined_pred
(** Formula *)
type binop = BOequ | BOimp | BOpmi | BOand | BOor | BOnand | BOnor
type binop =
| BOequ | BOnequ | BOimp | BOpmi
| BOand | BOor | BOnand | BOnor
type quant = Qforall | Qexists
type tyvar = variable * tff_type
type defined_pred =
| DPtrue | DPfalse | DPdistinct
| DPless | DPlesseq | DPgreater | DPgreatereq
| DPisint | DPisrat | DPequal | DPnoneq
| DPunknown of string
type defined_func =
| DFumin | DFsum | DFdiff
| DFprod | DFquot
| DFquot_e | DFquot_t | DFquot_f
| DFrem_e | DFrem_t | DFrem_f
| DFfloor | DFceil
| DFtrunc | DFround
| DFtoint | DFtorat | DFtoreal
| DFunknown of string
type num_integer = string
type num_rational = string * string
type num_real = string * string option * string option
type number =
| Nint of num_integer
| Nrat of num_rational
| Nint of num_integer
| Nrat of num_rational
| Nreal of num_real
type formula_node =
| LFqnt of quant * tyvar list * formula
| LFbin of binop * formula * formula
| LFnot of formula
| LFite of formula * formula * formula
| LFapp of atomic_word * term list
| LFdef of defined_pred * term list
| LFvar of variable
and term_node =
| LTite of formula * term * term
| LTapp of atomic_word * term list
| LTdef of defined_func * term list
| LTvar of variable
| LTdob of distinct
| LTnum of number
and binding_node =
| LBform of variable * formula
| LBterm of variable * term
| LBtype of variable * tff_type
and formula = { f_node : formula_node ; f_loc : loc }
and term = { t_node : term_node ; t_loc : loc }
and binding = { b_node : binding_node ; b_loc : loc }
type expr = { e_node : expr_node ; e_loc : loc }
and expr_node =
| Elet of expr * expr
| Eite of expr * expr * expr
| Eqnt of quant * tyvar list * expr
| Ebin of binop * expr * expr
| Enot of expr
| Eequ of expr * expr
| Eapp of atomic_word * expr list
| Edef of defined_word * expr list
| Evar of variable
| Edob of distinct
| Enum of number
and tyvar = variable * expr
type top_type = tyvar list * (expr list * expr)
type top_formula =
| LogicFormula of formula
| LogicFormula of expr
| TypedAtom of atomic_word * top_type
| Sequent of formula list * formula list
| Sequent of expr list * expr list
(** Top level *)
......@@ -119,5 +101,5 @@ type input =
| Formula of kind * name * role * top_formula * loc
| Include of file * name list * loc
type tptp_file = tptp_input list
type tptp_file = input list
......@@ -17,4 +17,3 @@
(* *)
(**************************************************************************)
val parse_tptp_file : Lexing.lexbuf -> Tptp_ast.tptp_file
......@@ -22,63 +22,70 @@
open Lexing
open Tptp_ast
open Tptp_parser
open Tptp_typing
(* open Tptp_typing *)
open Why3
(* lexical errors *)
exception IllegalCharacter of char
exception UnterminatedComment
exception UnterminatedString
exception UnknownDDW of string
exception UnknownDW of string
let () = Exn_printer.register (fun fmt e -> match e with
| IllegalCharacter c -> fprintf fmt "illegal character %c" c
| UnterminatedComment -> fprintf fmt "unterminated comment"
| UnterminatedString -> fprintf fmt "unterminated string"
| DoubleDollarWord -> fprintf fmt "system-specifics are not supported"
| UnknownDDW s -> fprintf fmt "unknown system_word %s" s
| UnknownDW s -> fprintf fmt "unknown defined_word %s" s
| _ -> raise e)
(*
let defwords = Hashtbl.create 97
let () = List.iter (fun (x,y) -> Hashtbl.add defwords x y) [
"ceiling", CEILING;
"difference", DIFFERENCE;
"distinct", DISTINCT;
"false", FALSE;
"floor", FLOOR;
"greater", GREATER;
"greatereq", GREATEREQ;
"i", ITYPE;
"int", INT;
"is_int", IS_INT;
"is_rat", IS_RAT;
"ite_f", ITEF;
"ite_t", ITET;
"iType", ITYPE;
"less", LESS;
"lesseq", LESSEQ;
"o", OTYPE;
"oType", OTYPE;
"product", PRODUCT;
"quotient", QUOTIENT;
"quotient_e", QUOTIENT_E;
"quotient_t", QUOTIENT_T;
"quotient_f", QUOTIENT_F;
"rat", RAT;
"real", REAL;
"remainder_e", REMAINDER_E;
"remainder_t", REMAINDER_T;
"remainder_f", REMAINDER_F;
"round", ROUND;
"sum", SUM;
"to_int", TO_INT;
"to_rat", TO_RAT;
"to_real", TO_REAL;
"true", TRUE;
"truncate", TRUNCATE;
"tType", TTYPE;
"uminus", UMINUS;
"ceiling", DWORD (DF DFceil);
"difference", DWORD (DF DFdiff);
"distinct", DWORD (DP DPdistinct);
"false", DWORD (DP DPfalse);
"floor", DWORD (DF DFfloor);
"greater", DWORD (DP DPgreater);
"greatereq", DWORD (DP DPgreatereq);
"i", DWORD (DT DTuniv);
"int", DWORD (DT DTint);
"is_int", DWORD (DP DPisint);
"is_rat", DWORD (DP DPisrat);
"ite_f", ITE_F;
"ite_t", ITE_T;
"iType", DWORD (DT DTuniv);
"let_tt", LET_TT;
"let_ft", LET_FT;
"let_tf", LET_TF;
"let_ff", LET_FF;
"less", DWORD (DP DPless);
"lesseq", DWORD (DP DPlesseq);
"o", DWORD (DT DTprop);
"oType", DWORD (DT DTprop);
"product", DWORD (DF DFprod);
"quotient", DWORD (DF DFquot);
"quotient_e", DWORD (DF DFquot_e);
"quotient_t", DWORD (DF DFquot_t);
"quotient_f", DWORD (DF DFquot_f);
"rat", DWORD (DT DTrat);
"real", DWORD (DT DTreal);
"remainder_e", DWORD (DF DFrem_e);
"remainder_t", DWORD (DF DFrem_t);
"remainder_f", DWORD (DF DFrem_f);
"round", DWORD (DF DFround);
"sum", DWORD (DF DFsum);
"to_int", DWORD (DF DFtoint);
"to_rat", DWORD (DF DFtorat);
"to_real", DWORD (DF DFtoreal);
"true", DWORD (DP DPtrue);
"truncate", DWORD (DF DFtrunc);
"tType", DWORD (DT DTtype);
"uminus", DWORD (DF DFumin);
]
*)
let keywords = Hashtbl.create 97
let () = List.iter (fun (x,y) -> Hashtbl.add keywords x y) [
......@@ -138,10 +145,12 @@ rule token = parse
{ SINGLE_QUOTED sq }
| '"' (do_char* as dob) '"'
{ DISTINCT_OBJECT dob }
| "$_"
{ DWORD (DT DTdummy) }
| '$' (lword as id)
{ DWORD id }
| "$$" lword
{ raise DoubleDollarWord }
{ try Hashtbl.find defwords id with Not_found -> raise (UnknownDW id) }
| "$$" (lword as id)
{ raise (UnknownDDW id) }
| '+'? (natural as s)
| '-' natural as s
{ INTNUM s }
......@@ -189,6 +198,10 @@ rule token = parse
{ NBAR }
| "~"
{ TILDE }
| "&"
{ AMP }
| "|"
{ BAR }
| "="
{ EQUAL }
| "!="
......@@ -212,11 +225,11 @@ and comment_block = parse
| "*/"
{ () }
| newline
{ newline lexbuf; comment lexbuf }
{ newline lexbuf; comment_block lexbuf }
| eof
{ raise (Loc.Located (!comment_start_loc, UnterminatedComment)) }
| _
{ comment lexbuf }
{ comment_block lexbuf }
and comment_line = parse
| newline
......@@ -224,7 +237,7 @@ and comment_line = parse
| eof
{ () }
| _
{ comment lexbuf }
{ comment_line lexbuf }
{
let with_location f lb =
......@@ -237,9 +250,10 @@ and comment_line = parse
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let ast = with_location (tptp_file token) lb in
tptp_typing env path ast
(* tptp_typing env path ast *)
Util.Mstr.empty
let () = Env.register_format "why" ["why"] read_channel
let () = Env.register_format "tptp" ["p";"ax"] read_channel
}
(*
......
This diff is collapsed.
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