Commit 1ec6a28e authored by Simon Cruanes's avatar Simon Cruanes

small changes before refactoring to use why as a library

parent b1928abf
......@@ -64,7 +64,7 @@ let rec print_term drv fmt t = match t.t_node with
| Tlet (_,_) -> unsupportedTerm t
"tptp : you must eliminate let"
| Tif (f1,t1,t2) ->
fprintf fmt "@[itef(%a@, %a@, %a)@]"
fprintf fmt "@[itef(%a,@ %a,@ %a)@]"
(print_fmla drv) f1 (print_term drv) t1 (print_term drv) t2
| Tcase _ -> unsupportedTerm t
"tptp : you must eliminate match"
......@@ -76,7 +76,7 @@ and print_fmla drv fmt f = match f.f_node with
print_symbol fmt id
| Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
| Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
| None -> fprintf fmt "%a(%a)"
| None -> fprintf fmt "@[%a(%a)@]"
print_symbol ls.ls_name (print_list comma (print_term drv)) tl
end
| Fquant (q, fq) ->
......@@ -86,25 +86,25 @@ and print_fmla drv fmt f = match f.f_node with
let rec forall fmt = function
| [] -> print_fmla drv fmt f
| v::l ->
fprintf fmt "@[(%s [%a]@ : (%a))@]" q print_var v forall l
fprintf fmt "%s [%a] :@ %a" q print_var v forall l
in
forall fmt vl;
List.iter forget_var vl
| Fbinop (Fand, f1, f2) ->
fprintf fmt "@[(%a &@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
fprintf fmt "@[(%a@ & %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (For, f1, f2) ->
fprintf fmt "@[(%a |@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
fprintf fmt "@[(%a@ | %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (Fimplies, f1, f2) ->
fprintf fmt "@[(%a =>@ %a)@]"
fprintf fmt "@[(%a@ => %a)@]"
(print_fmla drv) f1 (print_fmla drv) f2
| Fbinop (Fiff, f1, f2) ->
fprintf fmt "@[(%a <=> %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
fprintf fmt "@[(%a@ <=> %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
| Fnot f ->
fprintf fmt "@[(~@ %a)@]" (print_fmla drv) f
| Ftrue ->
fprintf fmt "true"
fprintf fmt "$true"
| Ffalse ->
fprintf fmt "false"
fprintf fmt "$false"
| Fif (_,_,_) -> unsupportedFmla f "Fif not supported"
(* fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f3 *)
......
......@@ -128,11 +128,11 @@ end = struct
let rec printFmla fmter = function
| FBinop (op, f1, f2) ->
fprintf fmter "(@[%a@ %s@ %a@])" printFmla f1 (show_fbinop op) printFmla 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:t.@] %a" (show_quantifier quant)
fprintf fmter "%s@ %a : t.@ %a" (show_quantifier quant)
(print_list printVar) vars printFmla f
| FPred (pred, terms) ->
fprintf fmter "%s(@[%a@])" pred (print_list printTerm) terms
......@@ -178,9 +178,9 @@ end = struct
let fromInclude = function | Include x -> x | _ -> assert false
(** for a given file, returns the list of declarations
for this file and all the files it includes, recursively *)
let rec getAllDecls include_dir filename =
let rec getAllDecls ?first:(first=false) include_dir filename =
try
let filename = include_dir^"/"^filename in
let filename = if first then filename else include_dir^"/"^filename in
let input = open_in filename in
let decls = Tptp_parser.tptp Tptp_lexer.token (Lexing.from_channel input) in
let isInclude = function | Include _ -> true | _ -> false in
......@@ -196,7 +196,7 @@ end = struct
(** process a single file and all includes inside *)
let printFile fmter include_dir theoryName filename =
let decls = getAllDecls include_dir filename in
let decls = getAllDecls ~first:true include_dir filename in
printTheory fmter theoryName decls
end
......@@ -224,7 +224,7 @@ module Init = struct
("-I", String include_updater, "search for included files in this dir")
]
let usage = "tptp2why file1 [file2...] [-o file]
let usage = "tptp2why file1 [file2...] [-o file] [-I dir]
It parses tptp files (fof format) and prints a why file
with one theory per input file."
......
......@@ -12,6 +12,8 @@
"fof", FOF;
"conjecture", CONJECTURE;
"axiom", AXIOM;
"definition", AXIOM; (* TODO : what's the difference ? *)
"hypothesis", AXIOM;
"include", INCLUDE
]
......@@ -86,6 +88,8 @@ rule token = parse
{ RBRACKET }
| "!"
{ BANG }
| "$"
{ DOLLAR }
| "?"
{ QUESTION }
| "&"
......
......@@ -3,6 +3,17 @@
open TptpTree
let translateSpecial t = let module M =
Map.Make(struct type t=string let compare=String.compare end) in
let known = List.fold_left (fun acc (x, y) -> M.add x y acc) M.empty [
("true", "true");
("false", "false")
] in
try
M.find t known
with _ -> t
%}
......@@ -12,7 +23,7 @@
%token LPAREN RPAREN LBRACKET RBRACKET
%token DOT COMMA COLON
%token PIPE AND ARROW LRARROW EQUAL NEQUAL NOT
%token BANG QUESTION
%token BANG QUESTION DOLLAR
%token QUOTE
%token<string> UIDENT
......@@ -29,8 +40,8 @@
%%
tptp:
| e = decl es = decl* EOF
{ e :: es }
| e = decl* EOF
{ e }
| error
{ Printf.printf "error at lexing pos %i\n" $endpos.Lexing.pos_lnum; assert false }
......@@ -62,6 +73,8 @@ fmla:
term:
| DOLLAR atom = lident
{ TAtom (translateSpecial atom) }
| atom = lident
{ TAtom atom }
| c = INT
......
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