Commit 0ab81636 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

begin of tptp-to-why translator

mainly parsing/lexing code
parent 851a4ac7
(** this is a tool to convert tptp files (.p files) to .why files *)
(** abstract tree representation *)
type atom = string
type variable = string
type logical_binop = And | Or | Implies | Equiv
type logical_unop = Not
type term_binop = Equal | NotEqual
type quantifier = Forall | Exist
type fmla =
| FBinop of logical_binop * fmla * fmla
| FUnop of logical_unop * fmla
| FQuant of quantifier * variable list * fmla
| FPred of predicate * term list
| FTermBinop of term_binop * term * term
and term =
| TAtom of atom
| TVar of variable
| TFunctor of atom * term list
and predicate = string
type decl = FOF of string * declType * fmla
and declType = Axiom | Conjecture
type tptp = decl list
{
type tok = FOF | CONJECTURE | AXIOM
let keywords = Hashtbl.create 97
let () =
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[
"fof", FOF;
"conjecture", CONJECTURE;
"axiom", AXIOM
]
let newline lexbuf =
let pos = lexbuf.lex_curr_p in
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
}
let newline = '\n'
let space = [' ' '\t' '\r']
let lalpha = ['a'-'z' '_']
let ualpha = ['A'-'Z']
let alpha = lalpha | ualpha
let digit = ['0'-'9']
let lident = lalpha (alpha | digit | '\'')*
let uident = ualpha (alpha | digit | '\'')*
let decimal_literal =
['0'-'9'] ['0'-'9' '_']*
let hex_literal =
'0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']['0'-'9' 'A'-'F' 'a'-'f' '_']*
let oct_literal =
'0' ['o' 'O'] ['0'-'7'] ['0'-'7' '_']*
let bin_literal =
'0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']*
let int_literal =
decimal_literal | hex_literal | oct_literal | bin_literal
let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
rule token = parse
| newline
{ newline lexbuf; token lexbuf }
| space+
{ token lexbuf }
| '_'
{ UNDERSCORE }
| lident as id
{ try Hashtbl.find keywords id with Not_found -> LIDENT id }
| uident as id
{ UIDENT id }
| int_literal as s
{ INTEGER s }
| "%"
{ COMMENT; comment lexbuf }
| "'"
{ QUOTE }
| "\""
{ QUOTE }
| ","
{ COMMA }
| "("
{ LEFTPAR }
| ")"
{ RIGHTPAR }
| ":"
{ COLON }
| "=>"
{ ARROW }
| "<=>"
{ LRARROW }
| "."
{ DOT }
| "|"
{ PIPE }
| "="
{ EQUAL }
| "!="
{ NEQUAL }
| "["
{ LBRACKET }
| "]"
{ RBRACKET }
| eof
{ EOF }
and comment = parse (* read until newline *)
| newline
{ token lexbuf }
| _
{ comment lexbuf }
%{
open TptpTree
open Tptp_lexer
%}
(** set of tokens *)
%token<int> INT
%token LPAREN RPAREN LBRACKET RBRACKET
%token DOT COMMA COLON
%token PIPE AND ARROW LRARROW EQUAL NEQUAL NOT
%token BANG QUESTION
%token QUOTE
%token FOF AXIOM CONJECTURE UIDENT LIDENT
%token EOL
%start<tptp> tptp
%start<fmla> fmla
%%
tptp:
| e = decl EOL es = decl*
{ e :: es }
decl:
| FOF LPAREN name = lident COMMA ty = decl_type COMMA f = fmla RPAREN DOT
{ FOF (name, ty, f) }
decl_type:
| AXIOM { Axiom }
| CONJECTURE { Conjecture }
fmla:
| quant = quantifier LBRACKET vars = separated_nonempty_list(COMMA, variable) RBRACKET
COLON f = fmla
{ FQuant (quant, vars, f) }
| LPAREN f = fmla RPAREN
{ f }
| f1 = fmla op = logic_binop f2 = fmla
{ FBinop (op, f1, f2) }
| op = logic_unop f = fmla
{ FUnop (op, f) }
| funct = lident LPAREN terms = separated_list(COMMA, term) RPAREN
{ FPred (funct, terms) }
| t1 = term op = term_binop t2 = term
{ FTermBinop (op, t1, t2) }
term:
| atom = lident
{ TAtom atom }
| atom = INT
{ TAtom atom }
| var = uident
{ TVar var }
| funct = lident LPAREN terms = separated_list(COMMA, term) RPAREN
{ TFunctor (funct, terms) }
lident:
| QUOTE i=LIDENT QUOTE { "'" ^ i ^ "'" }
| i = LIDENT { i }
uident:
| i = UIDENT { i }
%inline variable:
| i = uident { i }
%inline quantifier:
| BANG { Forall }
| QUESTION { Exist }
%inline logic_binop:
| PIPE { Or }
| AND { And }
| ARROW { Implies }
| LRARROW { Equiv }
%inline logic_unop:
| NOT { Not }
%inline term_binop:
| EQUAL { Equal }
| NEQUAL { NotEqual }
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