simplified configuration options for syntax ambiguity;
authorwenzelm
Fri Feb 17 15:42:26 2012 +0100 (2012-02-17)
changeset 465124f9f61f9b535
parent 46511 fbb3c68a8d3c
child 46513 2659ee0128c2
child 46526 c4cf9d03c352
simplified configuration options for syntax ambiguity;
NEWS
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
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	Fri Feb 17 11:24:39 2012 +0100
     1.2 +++ b/NEWS	Fri Feb 17 15:42:26 2012 +0100
     1.3 @@ -37,8 +37,8 @@
     1.4  position information via constraints).
     1.5  
     1.6  * Simplified configuration options for syntax ambiguity: see
     1.7 -"syntax_ambiguity" and "syntax_ambiguity_limit" in isar-ref manual.
     1.8 -Minor INCOMPATIBILITY.
     1.9 +"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
    1.10 +manual.  Minor INCOMPATIBILITY.
    1.11  
    1.12  
    1.13  *** Pure ***
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Feb 17 11:24:39 2012 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Feb 17 15:42:26 2012 +0100
     2.3 @@ -980,7 +980,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{tabular}{rcll}
     2.7 -    @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
     2.8 +    @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
     2.9      @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
    2.10    \end{tabular}
    2.11  
    2.12 @@ -1000,9 +1000,8 @@
    2.13  
    2.14    \begin{description}
    2.15  
    2.16 -  \item @{attribute syntax_ambiguity} determines reaction on multiple
    2.17 -  results of parsing; this string option can be set to @{text
    2.18 -  "ignore"}, @{text "warning"}, or @{text "error"}.
    2.19 +  \item @{attribute syntax_ambiguity_warning} controls output of
    2.20 +  explicit warning messages about syntax ambiguity.
    2.21  
    2.22    \item @{attribute syntax_ambiguity_limit} determines the number of
    2.23    resulting parse trees that are shown as part of the printed message
     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Feb 17 11:24:39 2012 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Feb 17 15:42:26 2012 +0100
     3.3 @@ -1154,7 +1154,7 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{tabular}{rcll}
     3.7 -    \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.8 +    \indexdef{}{attribute}{syntax\_ambiguity\_warning}\hypertarget{attribute.syntax-ambiguity-warning}{\hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}}} & : & \isa{attribute} & default \isa{true} \\
     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 @@ -1174,8 +1174,8 @@
    3.13  
    3.14    \begin{description}
    3.15  
    3.16 -  \item \hyperlink{attribute.syntax-ambiguity}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity}}} determines reaction on multiple
    3.17 -  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.18 +  \item \hyperlink{attribute.syntax-ambiguity-warning}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}warning}}} controls output of
    3.19 +  explicit warning messages about syntax ambiguity.
    3.20  
    3.21    \item \hyperlink{attribute.syntax-ambiguity-limit}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}ambiguity{\isaliteral{5F}{\isacharunderscore}}limit}}} determines the number of
    3.22    resulting parse trees that are shown as part of the printed message
     4.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Fri Feb 17 11:24:39 2012 +0100
     4.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Feb 17 15:42:26 2012 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  imports Eval
     4.5  begin
     4.6  
     4.7 -declare [[syntax_ambiguity = ignore]]
     4.8 +declare [[syntax_ambiguity_warning = false]]
     4.9  
    4.10  consts
    4.11    list_nam :: cnam
     5.1 --- a/src/HOL/Proofs/Lambda/Commutation.thy	Fri Feb 17 11:24:39 2012 +0100
     5.2 +++ b/src/HOL/Proofs/Lambda/Commutation.thy	Fri Feb 17 15:42:26 2012 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  theory Commutation imports Main begin
     5.6  
     5.7 -declare [[syntax_ambiguity = ignore]]
     5.8 +declare [[syntax_ambiguity_warning = false]]
     5.9  
    5.10  
    5.11  subsection {* Basic definitions *}
     6.1 --- a/src/HOL/Proofs/Lambda/Lambda.thy	Fri Feb 17 11:24:39 2012 +0100
     6.2 +++ b/src/HOL/Proofs/Lambda/Lambda.thy	Fri Feb 17 15:42:26 2012 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  
     6.5  theory Lambda imports Main begin
     6.6  
     6.7 -declare [[syntax_ambiguity = ignore]]
     6.8 +declare [[syntax_ambiguity_warning = false]]
     6.9  
    6.10  
    6.11  subsection {* Lambda-terms in de Bruijn notation and substitution *}
     7.1 --- a/src/HOL/Proofs/Lambda/ListOrder.thy	Fri Feb 17 11:24:39 2012 +0100
     7.2 +++ b/src/HOL/Proofs/Lambda/ListOrder.thy	Fri Feb 17 15:42:26 2012 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  theory ListOrder imports Main begin
     7.6  
     7.7 -declare [[syntax_ambiguity = ignore]]
     7.8 +declare [[syntax_ambiguity_warning = false]]
     7.9  
    7.10  
    7.11  text {*
     8.1 --- a/src/Pure/Isar/attrib.ML	Fri Feb 17 11:24:39 2012 +0100
     8.2 +++ b/src/Pure/Isar/attrib.ML	Fri Feb 17 15:42:26 2012 +0100
     8.3 @@ -503,7 +503,7 @@
     8.4    register_config Printer.show_types_raw #>
     8.5    register_config Printer.show_structs_raw #>
     8.6    register_config Printer.show_question_marks_raw #>
     8.7 -  register_config Syntax.ambiguity_raw #>
     8.8 +  register_config Syntax.ambiguity_warning_raw #>
     8.9    register_config Syntax.ambiguity_limit_raw #>
    8.10    register_config Syntax_Trans.eta_contract_raw #>
    8.11    register_config Name_Space.names_long_raw #>
     9.1 --- a/src/Pure/Syntax/syntax.ML	Fri Feb 17 11:24:39 2012 +0100
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Feb 17 15:42:26 2012 +0100
     9.3 @@ -10,8 +10,8 @@
     9.4    type operations
     9.5    val install_operations: operations -> unit
     9.6    val root: string Config.T
     9.7 -  val ambiguity_raw: Config.raw
     9.8 -  val ambiguity: string Config.T
     9.9 +  val ambiguity_warning_raw: Config.raw
    9.10 +  val ambiguity_warning: bool Config.T
    9.11    val ambiguity_limit_raw: Config.raw
    9.12    val ambiguity_limit: int Config.T
    9.13    val read_token: string -> Symbol_Pos.T list * Position.T
    9.14 @@ -155,8 +155,8 @@
    9.15  
    9.16  val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
    9.17  
    9.18 -val ambiguity_raw = Config.declare "syntax_ambiguity" (fn _ => Config.String "warning");
    9.19 -val ambiguity = Config.string ambiguity_raw;
    9.20 +val ambiguity_warning_raw = Config.declare "syntax_ambiguity_warning" (fn _ => Config.Bool true);
    9.21 +val ambiguity_warning = Config.bool ambiguity_warning_raw;
    9.22  
    9.23  val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
    9.24  val ambiguity_limit = Config.int ambiguity_limit_raw;
    10.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Feb 17 11:24:39 2012 +0100
    10.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Feb 17 15:42:26 2012 +0100
    10.3 @@ -262,11 +262,14 @@
    10.4  fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
    10.5  fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
    10.6  
    10.7 -fun report_result ctxt pos results =
    10.8 +fun report_result ctxt pos ambig_msgs results =
    10.9    (case (proper_results results, failed_results results) of
   10.10      ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
   10.11    | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
   10.12 -  | _ => error ("Parse error: ambiguous syntax" ^ Position.str_of pos));
   10.13 +  | _ =>
   10.14 +      if null ambig_msgs then
   10.15 +        error ("Parse error: ambiguous syntax" ^ Position.str_of pos)
   10.16 +      else error (cat_lines ambig_msgs));
   10.17  
   10.18  
   10.19  (* parse raw asts *)
   10.20 @@ -286,36 +289,28 @@
   10.21              (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks));
   10.22      val len = length pts;
   10.23  
   10.24 -    val ambiguity = Config.get ctxt Syntax.ambiguity;
   10.25 -    val _ =
   10.26 -      member (op =) ["ignore", "warning", "error"] ambiguity orelse
   10.27 -        error ("Bad value for syntax_ambiguity: " ^ quote ambiguity);
   10.28 -
   10.29      val limit = Config.get ctxt Syntax.ambiguity_limit;
   10.30 -
   10.31 -    val _ =
   10.32 -      if len <= 1 orelse ambiguity = "ignore" then ()
   10.33 +    val ambig_msgs =
   10.34 +      if len <= 1 then []
   10.35        else
   10.36 -        (if ambiguity = "error" then error else Context_Position.if_visible ctxt warning)
   10.37 -          (cat_lines
   10.38 -            (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
   10.39 -              "\nproduces " ^ string_of_int len ^ " parse trees" ^
   10.40 -              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   10.41 -              map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts)));
   10.42 -  in
   10.43 -    map (parsetree_to_ast ctxt raw ast_tr) pts
   10.44 -  end;
   10.45 +        [cat_lines
   10.46 +          (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^
   10.47 +            "\nproduces " ^ string_of_int len ^ " parse trees" ^
   10.48 +            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   10.49 +            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
   10.50 +
   10.51 +  in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end;
   10.52  
   10.53  fun parse_tree ctxt root input =
   10.54    let
   10.55      val syn = Proof_Context.syn_of ctxt;
   10.56      val tr = Syntax.parse_translation syn;
   10.57      val parse_rules = Syntax.parse_rules syn;
   10.58 -  in
   10.59 -    parse_asts ctxt false root input
   10.60 -    |> (map o apsnd o Exn.maps_result)
   10.61 -        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr))
   10.62 -  end;
   10.63 +    val (ambig_msgs, asts) = parse_asts ctxt false root input;
   10.64 +    val results =
   10.65 +      (map o apsnd o Exn.maps_result)
   10.66 +        (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
   10.67 +  in (ambig_msgs, results) end;
   10.68  
   10.69  
   10.70  (* parse logical entities *)
   10.71 @@ -329,7 +324,7 @@
   10.72    Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
   10.73      (fn (syms, pos) =>
   10.74        parse_tree ctxt "sort" (syms, pos)
   10.75 -      |> report_result ctxt pos
   10.76 +      |> uncurry (report_result ctxt pos)
   10.77        |> decode_sort
   10.78        |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
   10.79        handle ERROR msg => parse_failed ctxt pos msg "sort");
   10.80 @@ -338,7 +333,7 @@
   10.81    Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ
   10.82      (fn (syms, pos) =>
   10.83        parse_tree ctxt "type" (syms, pos)
   10.84 -      |> report_result ctxt pos
   10.85 +      |> uncurry (report_result ctxt pos)
   10.86        |> decode_typ
   10.87        handle ERROR msg => parse_failed ctxt pos msg "type");
   10.88  
   10.89 @@ -353,18 +348,12 @@
   10.90      Syntax.parse_token ctxt decode markup
   10.91        (fn (syms, pos) =>
   10.92          let
   10.93 -          val results = parse_tree ctxt root (syms, pos) |> map (decode_term ctxt);
   10.94 +          val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
   10.95            val parsed_len = length (proper_results results);
   10.96  
   10.97 -          val ambiguity = Config.get ctxt Syntax.ambiguity;
   10.98 +          val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
   10.99            val limit = Config.get ctxt Syntax.ambiguity_limit;
  10.100  
  10.101 -          val ambig_msg =
  10.102 -            if parsed_len > 1 andalso ambiguity = "ignore" then
  10.103 -              ["Got more than one parse tree.\n\
  10.104 -              \Retry with syntax_ambiguity = \"warning\" for more information."]
  10.105 -            else [];
  10.106 -
  10.107            (*brute-force disambiguation via type-inference*)
  10.108            fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
  10.109              handle exn as ERROR _ => Exn.Exn exn;
  10.110 @@ -383,19 +372,20 @@
  10.111            val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
  10.112          in
  10.113            if checked_len = 0 then
  10.114 -            report_result ctxt pos
  10.115 -              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
  10.116 +            report_result ctxt pos []
  10.117 +              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
  10.118            else if checked_len = 1 then
  10.119 -            (if parsed_len > 1 andalso ambiguity <> "ignore" then
  10.120 +            (if parsed_len > 1 andalso ambiguity_warning then
  10.121                Context_Position.if_visible ctxt warning
  10.122 -                ("Fortunately, only one parse tree is type correct" ^
  10.123 -                Position.str_of (Position.reset_range pos) ^
  10.124 -                ",\nbut you may still want to disambiguate your grammar or your input.")
  10.125 -            else (); report_result ctxt pos results')
  10.126 +                (cat_lines (ambig_msgs @
  10.127 +                  ["Fortunately, only one parse tree is type correct" ^
  10.128 +                  Position.str_of (Position.reset_range pos) ^
  10.129 +                  ",\nbut you may still want to disambiguate your grammar or your input."]))
  10.130 +             else (); report_result ctxt pos [] results')
  10.131            else
  10.132 -            report_result ctxt pos
  10.133 -              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
  10.134 -                (("Ambiguous input, " ^ string_of_int checked_len ^ " terms are type correct" ^
  10.135 +            report_result ctxt pos []
  10.136 +              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
  10.137 +                (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
  10.138                    (if checked_len <= limit then ""
  10.139                     else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
  10.140                    map show_term (take limit checked))))))]
  10.141 @@ -419,7 +409,7 @@
  10.142      val (syms, pos) = Syntax.read_token str;
  10.143    in
  10.144      parse_asts ctxt true root (syms, pos)
  10.145 -    |> report_result ctxt pos
  10.146 +    |> uncurry (report_result ctxt pos)
  10.147      |> constify
  10.148    end;
  10.149