simplified configuration options for syntax ambiguity;
authorwenzelm
Thu Feb 16 22:18:28 2012 +0100 (2012-02-16)
changeset 46506c7faa011bfa7
parent 46505 cefceb54c656
child 46507 1b24c24017dd
simplified configuration options for syntax ambiguity;
NEWS
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
src/HOL/Import/proof_kernel.ML
src/HOL/MicroJava/J/JListExample.thy
src/HOL/Proofs/Lambda/Commutation.thy
src/HOL/Proofs/Lambda/Lambda.thy
src/HOL/Proofs/Lambda/ListOrder.thy
src/Pure/Isar/attrib.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/NEWS	Thu Feb 16 17:09:15 2012 +0100
     1.2 +++ b/NEWS	Thu Feb 16 22:18:28 2012 +0100
     1.3 @@ -36,6 +36,10 @@
     1.4  "num_position" etc. are mainly used instead (which also include
     1.5  position information via constraints).
     1.6  
     1.7 +* Simplified configuration options for syntax ambiguity: see
     1.8 +"syntax_ambiguity" and "syntax_ambiguity_limit" in isar-ref manual.
     1.9 +Minor INCOMPATIBILITY.
    1.10 +
    1.11  
    1.12  *** Pure ***
    1.13  
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Feb 16 17:09:15 2012 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Feb 16 22:18:28 2012 +0100
     2.3 @@ -980,13 +980,10 @@
     2.4  
     2.5  text {*
     2.6    \begin{tabular}{rcll}
     2.7 -    @{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\
     2.8 +    @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
     2.9 +    @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
    2.10    \end{tabular}
    2.11  
    2.12 -  \begin{mldecls}
    2.13 -    @{index_ML Syntax.ambiguity_limit: "int Config.T"} \\  %FIXME attribute
    2.14 -  \end{mldecls}
    2.15 -
    2.16    Depending on the grammar and the given input, parsing may be
    2.17    ambiguous.  Isabelle lets the Earley parser enumerate all possible
    2.18    parse trees, and then tries to make the best out of the situation.
    2.19 @@ -1003,11 +1000,11 @@
    2.20  
    2.21    \begin{description}
    2.22  
    2.23 -  \item @{attribute syntax_ambiguity_level} determines the number of
    2.24 -  parser results that are tolerated without printing a detailed
    2.25 -  message.
    2.26 +  \item @{attribute syntax_ambiguity} determines reaction on multiple
    2.27 +  results of parsing; this string option can be set to @{text
    2.28 +  "ignore"}, @{text "warning"}, or @{text "error"}.
    2.29  
    2.30 -  \item @{ML Syntax.ambiguity_limit} determines the number of
    2.31 +  \item @{attribute syntax_ambiguity_limit} determines the number of
    2.32    resulting parse trees that are shown as part of the printed message
    2.33    in case of an ambiguity.
    2.34  
     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 16 17:09:15 2012 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Feb 16 22:18:28 2012 +0100
     3.3 @@ -1154,13 +1154,10 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{tabular}{rcll}
     3.7 -    \indexdef{}{attribute}{syntax\_ambiguity\_level}\hypertarget{attribute.syntax-ambiguity-level}{\hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}} \\
     3.8 +    \indexdef{}{attribute}{syntax\_ambiguity}\hypertarget{attribute.syntax-ambiguity}{\hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}}} & : & \isa{attribute} & default \isa{warning} \\
     3.9 +    \indexdef{}{attribute}{syntax\_ambiguity\_limit}\hypertarget{attribute.syntax-ambiguity-limit}{\hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
    3.10    \end{tabular}
    3.11  
    3.12 -  \begin{mldecls}
    3.13 -    \indexdef{}{ML}{Syntax.ambiguity\_limit}\verb|Syntax.ambiguity_limit: int Config.T| \\  %FIXME attribute
    3.14 -  \end{mldecls}
    3.15 -
    3.16    Depending on the grammar and the given input, parsing may be
    3.17    ambiguous.  Isabelle lets the Earley parser enumerate all possible
    3.18    parse trees, and then tries to make the best out of the situation.
    3.19 @@ -1177,11 +1174,10 @@
    3.20  
    3.21    \begin{description}
    3.22  
    3.23 -  \item \hyperlink{attribute.syntax-ambiguity-level}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}level}}} determines the number of
    3.24 -  parser results that are tolerated without printing a detailed
    3.25 -  message.
    3.26 +  \item \hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}} determines reaction on multiple
    3.27 +  results of parsing; this string option can be set to \isa{{\isaliteral{22}{\isachardoublequote}}ignore{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}warning{\isaliteral{22}{\isachardoublequote}}}, or \isa{{\isaliteral{22}{\isachardoublequote}}error{\isaliteral{22}{\isachardoublequote}}}.
    3.28  
    3.29 -  \item \verb|Syntax.ambiguity_limit| determines the number of
    3.30 +  \item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of
    3.31    resulting parse trees that are shown as part of the printed message
    3.32    in case of an ambiguity.
    3.33  
     4.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Feb 16 17:09:15 2012 +0100
     4.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Feb 16 22:18:28 2012 +0100
     4.3 @@ -198,7 +198,7 @@
     4.4  fun smart_string_of_cterm ctxt0 ct =
     4.5      let
     4.6          val ctxt = ctxt0
     4.7 -          |> Config.put Syntax.ambiguity_enabled true
     4.8 +          |> Config.put Syntax.ambiguity "warning"  (* FIXME actually "error" (!?) *)
     4.9            |> Config.put show_brackets false
    4.10            |> Config.put show_all_types false
    4.11            |> Config.put show_types false
     5.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Thu Feb 16 17:09:15 2012 +0100
     5.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Feb 16 22:18:28 2012 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  imports Eval
     5.5  begin
     5.6  
     5.7 -declare [[syntax_ambiguity_level = 100000]]
     5.8 +declare [[syntax_ambiguity = ignore]]
     5.9  
    5.10  consts
    5.11    list_nam :: cnam
     6.1 --- a/src/HOL/Proofs/Lambda/Commutation.thy	Thu Feb 16 17:09:15 2012 +0100
     6.2 +++ b/src/HOL/Proofs/Lambda/Commutation.thy	Thu Feb 16 22:18:28 2012 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  
     6.5  theory Commutation imports Main begin
     6.6  
     6.7 -declare [[syntax_ambiguity_level = 100]]
     6.8 +declare [[syntax_ambiguity = ignore]]
     6.9  
    6.10  
    6.11  subsection {* Basic definitions *}
     7.1 --- a/src/HOL/Proofs/Lambda/Lambda.thy	Thu Feb 16 17:09:15 2012 +0100
     7.2 +++ b/src/HOL/Proofs/Lambda/Lambda.thy	Thu Feb 16 22:18:28 2012 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  theory Lambda imports Main begin
     7.6  
     7.7 -declare [[syntax_ambiguity_level = 100]]
     7.8 +declare [[syntax_ambiguity = ignore]]
     7.9  
    7.10  
    7.11  subsection {* Lambda-terms in de Bruijn notation and substitution *}
     8.1 --- a/src/HOL/Proofs/Lambda/ListOrder.thy	Thu Feb 16 17:09:15 2012 +0100
     8.2 +++ b/src/HOL/Proofs/Lambda/ListOrder.thy	Thu Feb 16 22:18:28 2012 +0100
     8.3 @@ -7,7 +7,7 @@
     8.4  
     8.5  theory ListOrder imports Main begin
     8.6  
     8.7 -declare [[syntax_ambiguity_level = 100]]
     8.8 +declare [[syntax_ambiguity = ignore]]
     8.9  
    8.10  
    8.11  text {*
     9.1 --- a/src/Pure/Isar/attrib.ML	Thu Feb 16 17:09:15 2012 +0100
     9.2 +++ b/src/Pure/Isar/attrib.ML	Thu Feb 16 22:18:28 2012 +0100
     9.3 @@ -503,8 +503,8 @@
     9.4    register_config Printer.show_types_raw #>
     9.5    register_config Printer.show_structs_raw #>
     9.6    register_config Printer.show_question_marks_raw #>
     9.7 -  register_config Syntax.ambiguity_level_raw #>
     9.8 -  register_config Syntax.ambiguity_warnings_raw #>
     9.9 +  register_config Syntax.ambiguity_raw #>
    9.10 +  register_config Syntax.ambiguity_limit_raw #>
    9.11    register_config Syntax_Trans.eta_contract_raw #>
    9.12    register_config Name_Space.names_long_raw #>
    9.13    register_config Name_Space.names_short_raw #>
    10.1 --- a/src/Pure/Syntax/syntax.ML	Thu Feb 16 17:09:15 2012 +0100
    10.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Feb 16 22:18:28 2012 +0100
    10.3 @@ -10,12 +10,10 @@
    10.4    type operations
    10.5    val install_operations: operations -> unit
    10.6    val root: string Config.T
    10.7 -  val ambiguity_enabled: bool Config.T
    10.8 -  val ambiguity_level_raw: Config.raw
    10.9 -  val ambiguity_level: int Config.T
   10.10 +  val ambiguity_raw: Config.raw
   10.11 +  val ambiguity: string Config.T
   10.12 +  val ambiguity_limit_raw: Config.raw
   10.13    val ambiguity_limit: int Config.T
   10.14 -  val ambiguity_warnings_raw: Config.raw
   10.15 -  val ambiguity_warnings: bool Config.T
   10.16    val read_token: string -> Symbol_Pos.T list * Position.T
   10.17    val parse_token: Proof.context -> (XML.tree list -> 'a) ->
   10.18      Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
   10.19 @@ -157,19 +155,11 @@
   10.20  
   10.21  val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
   10.22  
   10.23 -val ambiguity_enabled =
   10.24 -  Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
   10.25 -
   10.26 -val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
   10.27 -val ambiguity_level = Config.int ambiguity_level_raw;
   10.28 +val ambiguity_raw = Config.declare "syntax_ambiguity" (fn _ => Config.String "warning");
   10.29 +val ambiguity = Config.string ambiguity_raw;
   10.30  
   10.31 -val ambiguity_limit =
   10.32 -  Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
   10.33 -
   10.34 -val ambiguity_warnings_raw = 
   10.35 -  Config.declare "syntax_ambiguity_warnings" (fn _ => Config.Bool true);
   10.36 -val ambiguity_warnings =
   10.37 -  Config.bool ambiguity_warnings_raw;
   10.38 +val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
   10.39 +val ambiguity_limit = Config.int ambiguity_limit_raw;
   10.40  
   10.41  
   10.42  (* outer syntax token -- with optional YXML content *)
    11.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Feb 16 17:09:15 2012 +0100
    11.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Feb 16 22:18:28 2012 +0100
    11.3 @@ -259,8 +259,6 @@
    11.4  
    11.5  (* results *)
    11.6  
    11.7 -fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
    11.8 -
    11.9  fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
   11.10  fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
   11.11  
   11.12 @@ -268,7 +266,7 @@
   11.13    (case (proper_results results, failed_results results) of
   11.14      ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
   11.15    | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
   11.16 -  | _ => error (ambiguity_msg pos));
   11.17 +  | _ => error ("Parse error: ambiguous syntax" ^ Position.str_of pos));
   11.18  
   11.19  
   11.20  (* parse raw asts *)
   11.21 @@ -288,23 +286,27 @@
   11.22              (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
   11.23      val len = length pts;
   11.24  
   11.25 +    val ambiguity = Config.get ctxt Syntax.ambiguity;
   11.26 +    val _ =
   11.27 +      member (op =) ["ignore", "warning", "error"] ambiguity orelse
   11.28 +        error ("Bad value for syntax_ambiguity: " ^ quote ambiguity);
   11.29 +
   11.30      val limit = Config.get ctxt Syntax.ambiguity_limit;
   11.31 -    val warnings = Config.get ctxt Syntax.ambiguity_warnings;
   11.32 +
   11.33      val _ =
   11.34 -      if len <= Config.get ctxt Syntax.ambiguity_level then ()
   11.35 -      else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
   11.36 -      else if warnings then
   11.37 -        (Context_Position.if_visible ctxt warning (cat_lines
   11.38 -          (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
   11.39 -            "\nproduces " ^ string_of_int len ^ " parse trees" ^
   11.40 -            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   11.41 -            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))))
   11.42 -      else ();
   11.43 +      if len <= 1 orelse ambiguity = "ignore" then ()
   11.44 +      else
   11.45 +        (if ambiguity = "error" then error else Context_Position.if_visible ctxt warning)
   11.46 +          (cat_lines
   11.47 +            (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
   11.48 +              "\nproduces " ^ string_of_int len ^ " parse trees" ^
   11.49 +              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   11.50 +              map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts)));
   11.51    in
   11.52      map (parsetree_to_ast ctxt raw ast_tr) pts
   11.53    end;
   11.54  
   11.55 -fun parse_raw ctxt root input =
   11.56 +fun parse_tree ctxt root input =
   11.57    let
   11.58      val syn = Proof_Context.syn_of ctxt;
   11.59      val tr = Syntax.parse_translation syn;
   11.60 @@ -326,7 +328,7 @@
   11.61  fun parse_sort ctxt =
   11.62    Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
   11.63      (fn (syms, pos) =>
   11.64 -      parse_raw ctxt "sort" (syms, pos)
   11.65 +      parse_tree ctxt "sort" (syms, pos)
   11.66        |> report_result ctxt pos
   11.67        |> decode_sort
   11.68        |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
   11.69 @@ -335,7 +337,7 @@
   11.70  fun parse_typ ctxt =
   11.71    Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
   11.72      (fn (syms, pos) =>
   11.73 -      parse_raw ctxt "type" (syms, pos)
   11.74 +      parse_tree ctxt "type" (syms, pos)
   11.75        |> report_result ctxt pos
   11.76        |> decode_typ
   11.77        handle ERROR msg => parse_failed ctxt pos msg "type");
   11.78 @@ -351,17 +353,16 @@
   11.79      Syntax.parse_token ctxt decode markup
   11.80        (fn (syms, pos) =>
   11.81          let
   11.82 -          val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
   11.83 -          val ambiguity = length (proper_results results);
   11.84 +          val results = parse_tree ctxt root (syms, pos) |> map (decode_term ctxt);
   11.85 +          val parsed_len = length (proper_results results);
   11.86  
   11.87 -          val level = Config.get ctxt Syntax.ambiguity_level;
   11.88 +          val ambiguity = Config.get ctxt Syntax.ambiguity;
   11.89            val limit = Config.get ctxt Syntax.ambiguity_limit;
   11.90 -          val warnings = Config.get ctxt Syntax.ambiguity_warnings;
   11.91  
   11.92            val ambig_msg =
   11.93 -            if ambiguity > 1 andalso ambiguity <= level then
   11.94 +            if parsed_len > 1 andalso ambiguity = "ignore" then
   11.95                ["Got more than one parse tree.\n\
   11.96 -              \Retry with smaller syntax_ambiguity_level for more information."]
   11.97 +              \Retry with syntax_ambiguity = \"warning\" for more information."]
   11.98              else [];
   11.99  
  11.100            (*brute-force disambiguation via type-inference*)
  11.101 @@ -369,7 +370,7 @@
  11.102              handle exn as ERROR _ => Exn.Exn exn;
  11.103  
  11.104            val results' =
  11.105 -            if ambiguity > 1 then
  11.106 +            if parsed_len > 1 then
  11.107                (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
  11.108                  check results
  11.109              else results;
  11.110 @@ -377,15 +378,15 @@
  11.111  
  11.112            val errs = map snd (failed_results results');
  11.113            val checked = map snd (proper_results results');
  11.114 -          val len = length checked;
  11.115 +          val checked_len = length checked;
  11.116  
  11.117            val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
  11.118          in
  11.119 -          if len = 0 then
  11.120 +          if checked_len = 0 then
  11.121              report_result ctxt pos
  11.122                [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
  11.123 -          else if len = 1 then
  11.124 -            (if ambiguity > level andalso warnings then
  11.125 +          else if checked_len = 1 then
  11.126 +            (if parsed_len > 1 andalso ambiguity <> "ignore" then
  11.127                Context_Position.if_visible ctxt warning
  11.128                  ("Fortunately, only one parse tree is type correct" ^
  11.129                  Position.str_of (Position.reset_range pos) ^
  11.130 @@ -394,8 +395,9 @@
  11.131            else
  11.132              report_result ctxt pos
  11.133                [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
  11.134 -                (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
  11.135 -                  (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
  11.136 +                (("Ambiguous input, " ^ string_of_int checked_len ^ " terms are type correct" ^
  11.137 +                  (if checked_len <= limit then ""
  11.138 +                   else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
  11.139                    map show_term (take limit checked))))))]
  11.140          end handle ERROR msg => parse_failed ctxt pos msg kind)
  11.141    end;