Commit 160b4fe1 authored by Simon Cruanes's avatar Simon Cruanes

tptp2why compiles (with some small problems caused by menhir)

currently lexing is not operational
parent e008702d
...@@ -387,6 +387,61 @@ clean:: ...@@ -387,6 +387,61 @@ clean::
rm -f $(COQGENERATED) rm -f $(COQGENERATED)
rm -f .depend.coq rm -f .depend.coq
########
# Tptp2why
########
# TODO : autoconf
MENHIR=/usr/bin/menhir
TPTPGENERATED = src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli \
src/tptp2why/tptp_parser.output src/tptp2why/tptp_lexer.ml
TPTP_FILES = tptpTree tptp_parser tptp_lexer tptp2why
TPTP_DIR=src/tptp2why/
TPTPMODULES = $(addprefix $(TPTP_DIR), $(TPTP_FILES))
TPTPML = $(addsuffix .ml, $(TPTPMODULES))
TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
$(TPTPCMO) $(TPTPCMX): INCLUDES = -I $(TPTP_DIR)
# build targets
byte: bin/tptp2why.byte
opt: bin/tptp2why.opt
src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli: src/tptp2why/tptpTree.cmi src/tptp2why/tptp_parser.mly
cd $(TPTP_DIR) && $(MENHIR) --infer tptp_parser.mly
bin/tptp2why.opt: $(TPTPCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $^
$(STRIP) $@
bin/tptp2why.byte: $(TPTPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $^
# depend and clean targets
include .depend.tptp2why
.depend.tptp2why: $(TPTPGENERATED)
$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@
depend: .depend.tptp2why
clean::
rm -f $(TPTPGENERATED)
rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
rm -f src/tptp2why/*.annot src/tptp2why/*~
rm -f bin/tptp2why.byte bin/tptp2why.opt
rm -f .depend.tptp2why
####### #######
# tools # tools
####### #######
......
(** this is a tool to convert tptp files (.p files) to .why files *) (** this is a tool to convert tptp files (.p files) to .why files *)
open TptpTree
(** ugly basic printer for trees *)
module Print : sig
val printDecl : decl -> unit
val printFmla : Format.formatter -> fmla -> unit
val printFile : string -> unit
end = struct
open Format
let show_type ty = match ty with
| Axiom -> "axiom"
| Conjecture -> "conjecture"
let show_fbinop op = match op with
| And -> "and"
| Or -> "or"
| Implies -> "->"
| Equiv -> "<->"
let show_funop = function
| Not -> "not"
let show_tbinop = function
| Equal -> "="
| NotEqual -> "<>"
let show_quantifier = function
| Forall -> "forall"
| Exist -> "exists"
(** prints a list of items with printer *)
let rec print_list printer fmter = function
| x::xs when xs <> [] -> fprintf fmter "%a@, %a" printer x (print_list printer) xs
| x::[] -> fprintf fmter "%a" printer x
| [] -> ()
let rec printTerm fmter = function
| TAtom atom -> pp_print_string fmter atom
| TConst c -> pp_print_string fmter c
| TVar v -> pp_print_string fmter v
| TFunctor (atom, terms) ->
fprintf fmter "%s(@%a)" atom (print_list printTerm) terms
let rec printFmla fmter = function
| FBinop (op, f1, f2) ->
fprintf fmter "%a @%s %a" printFmla f1 (show_fbinop op) printFmla f2
| FUnop (op, f) ->
fprintf fmter "@[(%s %a)@]" (show_funop op) printFmla f
| FQuant (quant, vars, f) ->
fprintf fmter "%s@ %a.@ (%a)" (show_quantifier quant)
(print_list pp_print_string) vars printFmla f
| FPred (pred, terms) ->
fprintf fmter "%s(@%a)" pred (print_list printTerm) terms
| FTermBinop (op, t1, t2) ->
fprintf fmter "@[%a %s %a@]" printTerm t1 (show_tbinop op) printTerm t2
let printDecl = function
| Fof (name, ty, fmla) ->
printf "fof(%s, %s, %a).\n" name (show_type ty) printFmla fmla
let printFile filename =
let input = open_in filename in
let decls = Tptp_parser.tptp Tptp_lexer.token (Lexing.from_channel input) in
close_in input;
List.iter printDecl decls
end
(** main function and arg parsing *)
open Arg
let debug = ref false
let print_in = ref false
let input_files = ref []
let options = [
("-debug", Set debug, "activates debug mode");
("-print-in", Set print_in, "prints parsed input")
]
let usage = "tptp2why [-debug] [-print-in] file1 [file2...]
It parses tptp files (fof format) and prints a why file
with one theory per input file."
let _ =
parse options (fun file -> input_files := file :: (!input_files)) usage;
input_files := List.rev !input_files;
if !print_in
then List.iter Print.printFile !input_files
else failwith "not implemented !"
(** 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
| TConst of string
| 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
(** 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
tptpTree.ml
\ No newline at end of file
{ {
type tok = FOF | CONJECTURE | AXIOM open Lexing
open Tptp_parser
let keywords = Hashtbl.create 97 let keywords = Hashtbl.create 97
let () = let () =
...@@ -45,26 +46,22 @@ rule token = parse ...@@ -45,26 +46,22 @@ rule token = parse
{ newline lexbuf; token lexbuf } { newline lexbuf; token lexbuf }
| space+ | space+
{ token lexbuf } { token lexbuf }
| '_'
{ UNDERSCORE }
| lident as id | lident as id
{ try Hashtbl.find keywords id with Not_found -> LIDENT id } { try Hashtbl.find keywords id with Not_found -> LIDENT id }
| uident as id | uident as id
{ UIDENT id } { UIDENT id }
| int_literal as s | int_literal as s
{ INTEGER s } { INT s }
| "%" | "%"
{ COMMENT; comment lexbuf } { comment lexbuf }
| "'" | "'"
{ QUOTE } { QUOTE }
| "\""
{ QUOTE }
| "," | ","
{ COMMA } { COMMA }
| "(" | "("
{ LEFTPAR } { LPAREN }
| ")" | ")"
{ RIGHTPAR } { RPAREN }
| ":" | ":"
{ COLON } { COLON }
| "=>" | "=>"
......
...@@ -2,39 +2,38 @@ ...@@ -2,39 +2,38 @@
%{ %{
open TptpTree open TptpTree
open Tptp_lexer
%} %}
(** set of tokens *) (** set of tokens *)
%token<string> INT
%token<int> INT
%token LPAREN RPAREN LBRACKET RBRACKET %token LPAREN RPAREN LBRACKET RBRACKET
%token DOT COMMA COLON %token DOT COMMA COLON
%token PIPE AND ARROW LRARROW EQUAL NEQUAL NOT %token PIPE AND ARROW LRARROW EQUAL NEQUAL NOT
%token BANG QUESTION %token BANG QUESTION
%token QUOTE %token QUOTE
%token FOF AXIOM CONJECTURE UIDENT LIDENT %token<string> UIDENT
%token<string> LIDENT
%token EOL %token FOF AXIOM CONJECTURE
%token EOL EOF
%start<tptp> tptp %start<TptpTree.decl list> tptp
%start<fmla> fmla %start<TptpTree.decl> decl
%% %%
tptp: tptp:
| e = decl EOL es = decl* | e = decl EOL es = decl* EOF
{ e :: es } { e :: es }
decl: decl:
| FOF LPAREN name = lident COMMA ty = decl_type COMMA f = fmla RPAREN DOT | FOF LPAREN name = lident COMMA ty = decl_type COMMA f = fmla RPAREN DOT
{ FOF (name, ty, f) } { Fof (name, ty, f) }
decl_type: decl_type:
| AXIOM { Axiom } | AXIOM { Axiom }
...@@ -60,8 +59,8 @@ fmla: ...@@ -60,8 +59,8 @@ fmla:
term: term:
| atom = lident | atom = lident
{ TAtom atom } { TAtom atom }
| atom = INT | c = INT
{ TAtom atom } { TConst c }
| var = uident | var = uident
{ TVar var } { TVar var }
| funct = lident LPAREN terms = separated_list(COMMA, term) RPAREN | funct = lident LPAREN terms = separated_list(COMMA, term) RPAREN
......
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