# HG changeset patch
# User sultana
# Date 1334816741 -3600
# Node ID fce9d97a32581238b66c89c519e40654f26988c3
# Parent  98c8b7542b72594521984d1f16e5c22de15097a7
exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;

diff -r 98c8b7542b72 -r fce9d97a3258 src/HOL/TPTP/TPTP_Parser/tptp.yacc
--- 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  ))
diff -r 98c8b7542b72 -r fce9d97a3258 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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',
diff -r 98c8b7542b72 -r fce9d97a3258 src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML
--- 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
diff -r 98c8b7542b72 -r fce9d97a3258 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- 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 =