exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
--- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc Wed Apr 18 17:44:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc Thu Apr 19 07:25:41 2012 +0100
@@ -197,7 +197,7 @@
%pos int
%eop EOF
%noshift EOF
-%arg (file_name) : string
+%arg (this_file_name) : string
%nonassoc LET
%nonassoc RPAREN
@@ -247,22 +247,22 @@
| cnf_annotated (( cnf_annotated ))
thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
- Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
+ Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
THF, name, formula_role, thf_formula, annotations)
))
tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
- Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
+ Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
TFF, name, formula_role, tff_formula, annotations)
))
fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
- Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
+ Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
FOF, name, formula_role, fof_formula, annotations)
))
cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
- Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
+ Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
CNF, name, formula_role, cnf_formula, annotations)
))
@@ -791,7 +791,8 @@
useful_info : general_list (( general_list ))
include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
- Include (file_name, formula_selection)
+ Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
+ file_name, formula_selection)
))
formula_selection : COMMA LBRKT name_list RBRKT (( name_list ))
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 17:44:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Apr 19 07:25:41 2012 +0100
@@ -97,6 +97,8 @@
val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
theory -> tptp_general_meaning * theory
+ type position = string * int * int
+ exception MISINTERPRET of position list * exn
exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula
exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol
exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
@@ -119,6 +121,8 @@
struct
open TPTP_Syntax
+type position = string * int * int
+exception MISINTERPRET of position list * exn
exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula
exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol
exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
@@ -672,7 +676,7 @@
fun interpret_line config inc_list type_map const_map path_prefix line thy =
case line of
- Include (quoted_path, inc_list) =>
+ Include (_, quoted_path, inc_list) =>
interpret_file'
config
inc_list
@@ -685,7 +689,7 @@
type_map
const_map
thy
- | Annotated_Formula (pos, lang, label, role, tptp_formula, annotation_opt) =>
+ | Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) =>
(*interpret a line only if "label" is in "inc_list", or if "inc_list" is
empty (in which case interpret all lines)*)
(*FIXME could work better if inc_list were sorted*)
@@ -779,6 +783,7 @@
end
else (*do nothing if we're not to includ this AF*)
((type_map, const_map, []), thy)
+
and interpret_problem config inc_list path_prefix lines type_map const_map thy =
let
val thy_name = Context.theory_name thy
@@ -789,6 +794,16 @@
(*process the line, ignoring the type-context for variables*)
val ((type_map', const_map', l'), thy') =
interpret_line config inc_list type_map const_map path_prefix line thy
+ handle
+ (*package all exceptions to include position information,
+ even relating to multiple levels of "include"ed files*)
+ (*FIXME "exn" contents may appear garbled due to markup
+ FIXME this appears as ML source position *)
+ MISINTERPRET (pos_list, exn) =>
+ raise MISINTERPRET
+ (TPTP_Syntax.pos_of_line line :: pos_list, exn)
+ | exn => raise MISINTERPRET
+ ([TPTP_Syntax.pos_of_line line], exn)
in
((type_map',
const_map',
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Wed Apr 18 17:44:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML Thu Apr 19 07:25:41 2012 +0100
@@ -3717,7 +3717,7 @@
local open Header in
val actions =
fn (i392,defaultPos,stack,
- (file_name):arg) =>
+ (this_file_name):arg) =>
case (i392,stack)
of ( 0, ( ( _, ( MlyValue.tptp_file tptp_file, tptp_file1left,
tptp_file1right)) :: rest671)) => let val result = MlyValue.tptp (
@@ -3784,7 +3784,7 @@
MlyValue.name name, _, _)) :: _ :: ( _, ( _, (THFleft as THF1left),
THFright)) :: rest671)) => let val result = MlyValue.thf_annotated (
(
- Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
+ Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
THF, name, formula_role, thf_formula, annotations)
)
)
@@ -3797,7 +3797,7 @@
MlyValue.name name, _, _)) :: _ :: ( _, ( _, (TFFleft as TFF1left),
TFFright)) :: rest671)) => let val result = MlyValue.tff_annotated (
(
- Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
+ Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
TFF, name, formula_role, tff_formula, annotations)
)
)
@@ -3810,7 +3810,7 @@
MlyValue.name name, _, _)) :: _ :: ( _, ( _, (FOFleft as FOF1left),
FOFright)) :: rest671)) => let val result = MlyValue.fof_annotated (
(
- Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
+ Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
FOF, name, formula_role, fof_formula, annotations)
)
)
@@ -3823,7 +3823,7 @@
MlyValue.name name, _, _)) :: _ :: ( _, ( _, (CNFleft as CNF1left),
CNFright)) :: rest671)) => let val result = MlyValue.cnf_annotated (
(
- Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
+ Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
CNF, name, formula_role, cnf_formula, annotations)
)
)
@@ -5519,11 +5519,14 @@
end
| ( 249, ( ( _, ( _, _, PERIOD1right)) :: _ :: ( _, (
MlyValue.formula_selection formula_selection, _, _)) :: ( _, (
-MlyValue.file_name file_name, _, _)) :: _ :: ( _, ( _, INCLUDE1left, _
-)) :: rest671)) => let val result = MlyValue.include_ (
+MlyValue.file_name file_name, _, _)) :: _ :: ( _, ( _, (INCLUDEleft
+ as INCLUDE1left), INCLUDEright)) :: rest671)) => let val result =
+MlyValue.include_ (
(
- Include (file_name, formula_selection)
-))
+ Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
+ file_name, formula_selection)
+)
+)
in ( LrTable.NT 132, ( result, INCLUDE1left, PERIOD1right), rest671)
end
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Apr 18 17:44:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Thu Apr 19 07:25:41 2012 +0100
@@ -131,7 +131,7 @@
datatype tptp_line =
Annotated_Formula of position * language * string * role *
tptp_formula * annotation option
- | Include of string * string list
+ | Include of position * string * string list
type tptp_problem = tptp_line list
@@ -143,6 +143,8 @@
val nameof_tff_atom_type : tptp_type -> string
+ val pos_of_line : tptp_line -> position
+
(*Returns the list of all files included in a directory and its
subdirectories. This is only used for testing the parser/interpreter against
all THF problems.*)
@@ -275,7 +277,7 @@
datatype tptp_line =
Annotated_Formula of position * language * string * role * tptp_formula * annotation option
- | Include of string * string list
+ | Include of position * string * string list
type tptp_problem = tptp_line list
@@ -284,6 +286,11 @@
fun nameof_tff_atom_type (Atom_type str) = str
| nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
+fun pos_of_line tptp_line =
+ case tptp_line of
+ Annotated_Formula (position, _, _, _, _, _) => position
+ | Include (position, _, _) => position
+
(*Used for debugging. Returns all files contained within a directory or its
subdirectories. Follows symbolic links, filters away directories.*)
fun get_file_list path =