Commit fd472796 authored by MARCHE Claude's avatar MARCHE Claude

TPTP parser: suppress the quotes around the names of included files

parent de7a7a6e
......@@ -273,8 +273,7 @@ let load file =
match d with
| Formula _ -> d::acc
| Include(file,_,_) ->
let fn = String.sub file 1 (String.length file - 2) in
let ast = aux fn in
let ast = aux file in
List.rev_append ast acc)
[] ast
in List.rev ast
......
......@@ -14,6 +14,8 @@ open Tptp_ast
let mk_expr n s e = { e_node = n; e_loc = Why3.Loc.extract (s,e) }
let remove_quotes s = String.sub s 1 (String.length s - 2)
exception UnsupportedRole of string
let () = Why3.Exn_printer.register (fun fmt exn -> match exn with
......@@ -61,7 +63,7 @@ input:
| kind LEFTPAR name COMMA role COMMA top_formula annotation RIGHTPAR DOT
{ Formula ($1, $3, $5, $7, Why3.Loc.extract ($startpos, $endpos)) }
| INCLUDE LEFTPAR SINGLE_QUOTED formula_selection RIGHTPAR DOT
{ Include ($3, $4, Why3.Loc.extract ($startpos, $endpos)) }
{ Include (remove_quotes $3, $4, Why3.Loc.extract ($startpos, $endpos)) }
kind:
| TFFK { TFF }
......
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