# HG changeset patch # User wenzelm # Date 1302001660 -7200 # Node ID 098c86e53153ab84b2fb6ba538b0d23e9befbc39 # Parent ff50c436b199c3ba455b74e1f6fc7353e72e1a6c more precise propagation of reports/results through some inner syntax layers; misc reorganization; diff -r ff50c436b199 -r 098c86e53153 src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Mon Apr 04 23:52:56 2011 +0200 +++ b/src/Pure/General/exn.ML Tue Apr 05 13:07:40 2011 +0200 @@ -11,7 +11,9 @@ val get_exn: 'a result -> exn option val capture: ('a -> 'b) -> 'a -> 'b result val release: 'a result -> 'a + val flat_result: 'a result result -> 'a result val map_result: ('a -> 'b) -> 'a result -> 'b result + val maps_result: ('a -> 'b result) -> 'a result -> 'b result exception Interrupt val interrupt: unit -> 'a val is_interrupt: exn -> bool @@ -45,8 +47,13 @@ fun release (Result y) = y | release (Exn e) = reraise e; +fun flat_result (Result x) = x + | flat_result (Exn e) = Exn e; + fun map_result f (Result x) = Result (f x) - | map_result f (Exn e) = (Exn e); + | map_result f (Exn e) = Exn e; + +fun maps_result f = flat_result o map_result f; (* interrupts *) diff -r ff50c436b199 -r 098c86e53153 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Apr 04 23:52:56 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 05 13:07:40 2011 +0200 @@ -67,7 +67,8 @@ val check_tfree: Proof.context -> string * sort -> string * sort val type_context: Proof.context -> Syntax.type_context val term_context: Proof.context -> Syntax.term_context - val decode_term: Proof.context -> Position.reports * term -> Position.reports * term + val decode_term: Proof.context -> + Position.reports * term Exn.result -> Position.reports * term Exn.result val standard_infer_types: Proof.context -> term list -> term list val read_term_pattern: Proof.context -> string -> term val read_term_schematic: Proof.context -> string -> term @@ -784,8 +785,8 @@ then default_root else c | _ => default_root); - fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE) - handle ERROR msg => SOME msg; + fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t) + handle exn as ERROR _ => Exn.Exn exn; val t = Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt) root (syms, pos) diff -r ff50c436b199 -r 098c86e53153 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Mon Apr 04 23:52:56 2011 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Tue Apr 05 13:07:40 2011 +0200 @@ -60,7 +60,7 @@ val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val parsetree_to_ast: Proof.context -> type_context -> bool -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> - Parser.parsetree -> Position.reports * Ast.ast + Parser.parsetree -> Position.reports * Ast.ast Exn.result val ast_to_term: Proof.context -> (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term end; @@ -587,7 +587,7 @@ | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts) | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); - val ast = ast_of parsetree; + val ast = Exn.interruptible_capture ast_of parsetree; in (! reports, ast) end; diff -r ff50c436b199 -r 098c86e53153 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Apr 04 23:52:56 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 05 13:07:40 2011 +0200 @@ -116,13 +116,13 @@ val ambiguity_level_raw: Config.raw val ambiguity_level: int Config.T val ambiguity_limit: int Config.T - val standard_parse_term: (term -> string option) -> + val standard_parse_sort: Proof.context -> type_context -> syntax -> + Symbol_Pos.T list * Position.T -> sort + val standard_parse_typ: Proof.context -> type_context -> syntax -> + ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ + val standard_parse_term: (term -> term Exn.result) -> Proof.context -> type_context -> term_context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term - val standard_parse_typ: Proof.context -> type_context -> syntax -> - ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ - val standard_parse_sort: Proof.context -> type_context -> syntax -> - Symbol_Pos.T list * Position.T -> sort datatype 'a trrule = Parse_Rule of 'a * 'a | Print_Rule of 'a * 'a | @@ -130,13 +130,13 @@ val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule val is_const: syntax -> string -> bool val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast + val standard_unparse_sort: {extern_class: string -> xstring} -> + Proof.context -> syntax -> sort -> Pretty.T + val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} -> + Proof.context -> syntax -> typ -> Pretty.T val standard_unparse_term: {structs: string list, fixes: string list} -> {extern_class: string -> xstring, extern_type: string -> xstring, extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T - val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} -> - Proof.context -> syntax -> typ -> Pretty.T - val standard_unparse_sort: {extern_class: string -> xstring} -> - Proof.context -> syntax -> sort -> Pretty.T val update_trfuns: (string * ((ast list -> ast) * stamp)) list * (string * ((term list -> term) * stamp)) list * @@ -686,17 +686,9 @@ -(** read **) +(** read **) (* FIXME rename!? *) -fun some_results f xs = - let - val exn_results = map (Exn.interruptible_capture f) xs; - val exns = map_filter Exn.get_exn exn_results; - val results = map_filter Exn.get_result exn_results; - in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end; - - -(* read_ast *) +(* configuration options *) val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true); val positions = Config.bool positions_raw; @@ -712,6 +704,23 @@ fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos; + +(* results *) + +fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results; +fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results; + +fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m); + +fun report_result ctxt pos results = + (case (proper_results results, failed_results results) of + ([], (reports, exn) :: _) => (report ctxt reports; reraise exn) + | ([(reports, x)], _) => (report ctxt reports; x) + | _ => error (ambiguity_msg pos)); + + +(* read_asts *) + fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) = let val {lexicon, gram, parse_ast_trtab, ...} = tabs; @@ -736,84 +745,87 @@ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts)))); val constrain_pos = not raw andalso Config.get ctxt positions; - in - some_results - (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts - end; + val parsetree_to_ast = + Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab); + in map parsetree_to_ast pts end; -(* read *) +(* read_raw *) -fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp = - let val {parse_ruletab, parse_trtab, ...} = tabs in - read_asts ctxt type_ctxt syn false root inp - |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab))) - |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab))) +fun read_raw ctxt type_ctxt (syn as Syntax (tabs, _)) root input = + let + val {parse_ruletab, parse_trtab, ...} = tabs; + val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab); + val ast_to_term = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab); + in + read_asts ctxt type_ctxt syn false root input + |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term) end; -(* read terms *) - -fun report_result ctxt (reports, res) = - (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res); - -(*brute-force disambiguation via type-inference*) -fun disambig ctxt _ [arg] = report_result ctxt arg - | disambig ctxt check args = - let - val level = Config.get ctxt ambiguity_level; - val limit = Config.get ctxt ambiguity_limit; - - val ambiguity = length args; - fun ambig_msg () = - if ambiguity > 1 andalso ambiguity <= level then - "Got more than one parse tree.\n\ - \Retry with smaller syntax_ambiguity_level for more information." - else ""; +(* read sorts *) - val errs = Par_List.map_name "Syntax.disambig" (check o snd) args; - val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs); - val len = length results; - - val show_term = string_of_term (Config.put Printer.show_brackets true ctxt); - in - if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs)) - else if len = 1 then - (if ambiguity > level then - Context_Position.if_visible ctxt warning - "Fortunately, only one parse tree is type correct.\n\ - \You may still want to disambiguate your grammar or your input." - else (); report_result ctxt (hd results)) - else cat_error (ambig_msg ()) (cat_lines - (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^ - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: - map (show_term o snd) (take limit results))) - end; - -fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) = - read ctxt type_ctxt syn root (syms, pos) - |> map (Type_Ext.decode_term term_ctxt) - |> disambig ctxt check; +fun standard_parse_sort ctxt type_ctxt syn (syms, pos) = + read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) + |> report_result ctxt pos + |> Type_Ext.sort_of_term; (* read types *) fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) = - (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of - [res] => - let val t = report_result ctxt res - in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end - | _ => error (ambiguity_msg pos)); + read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) + |> report_result ctxt pos + |> (fn t => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t); -(* read sorts *) +(* read terms -- brute-force disambiguation via type-inference *) + +fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) = + let + val results = + read_raw ctxt type_ctxt syn root (syms, pos) + |> map (Type_Ext.decode_term term_ctxt); + + val level = Config.get ctxt ambiguity_level; + val limit = Config.get ctxt ambiguity_limit; + + val ambiguity = length (proper_results results); + + fun ambig_msg () = + if ambiguity > 1 andalso ambiguity <= level then + "Got more than one parse tree.\n\ + \Retry with smaller syntax_ambiguity_level for more information." + else ""; -fun standard_parse_sort ctxt type_ctxt syn (syms, pos) = - (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of - [res] => - let val t = report_result ctxt res - in Type_Ext.sort_of_term t end - | _ => error (ambiguity_msg pos)); + val results' = + if ambiguity > 1 then + (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results + else results; + val reports' = fst (hd results'); + + val errs = map snd (failed_results results'); + val checked = map snd (proper_results results'); + val len = length checked; + + val show_term = string_of_term (Config.put Printer.show_brackets true ctxt); + in + if len = 0 then + report_result ctxt pos + [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))] + else if len = 1 then + (if ambiguity > level then + Context_Position.if_visible ctxt warning + "Fortunately, only one parse tree is type correct.\n\ + \You may still want to disambiguate your grammar or your input." + else (); report_result ctxt pos results') + else + report_result ctxt pos + [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () :: + (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^ + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: + map show_term (take limit checked))))))] + end; @@ -874,11 +886,9 @@ val (syms, pos) = read_token str; in - (case read_asts ctxt type_ctxt syn true root (syms, pos) of - [res] => - let val ast = report_result ctxt res - in constify ast end - | _ => error (ambiguity_msg pos)) + read_asts ctxt type_ctxt syn true root (syms, pos) + |> report_result ctxt pos + |> constify end; @@ -899,16 +909,16 @@ in -fun standard_unparse_term idents extern = - unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term; +fun standard_unparse_sort {extern_class} ctxt syn = + unparse_t (K Printer.sort_to_ast) + (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I}) + Markup.sort ctxt syn false; fun standard_unparse_typ extern ctxt syn = unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false; -fun standard_unparse_sort {extern_class} ctxt syn = - unparse_t (K Printer.sort_to_ast) - (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I}) - Markup.sort ctxt syn false; +fun standard_unparse_term idents extern = + unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term; end; diff -r ff50c436b199 -r 098c86e53153 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Mon Apr 04 23:52:56 2011 +0200 +++ b/src/Pure/Syntax/type_ext.ML Tue Apr 05 13:07:40 2011 +0200 @@ -13,7 +13,8 @@ val strip_positions: term -> term val strip_positions_ast: Ast.ast -> Ast.ast type term_context - val decode_term: term_context -> Position.reports * term -> Position.reports * term + val decode_term: term_context -> + Position.reports * term Exn.result -> Position.reports * term Exn.result val term_of_typ: bool -> typ -> term val no_brackets: unit -> bool val no_type_brackets: unit -> bool @@ -136,55 +137,56 @@ markup_free: string -> Markup.T list, markup_var: indexname -> Markup.T list}; -fun decode_term (term_context: term_context) (reports0: Position.reports, tm) = - let - val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context; - val decodeT = typ_of_term (get_sort (term_sorts tm)); +fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result + | decode_term (term_context: term_context) (reports0, Exn.Result tm) = + let + val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context; + val decodeT = typ_of_term (get_sort (term_sorts tm)); - val reports = Unsynchronized.ref reports0; - fun report ps = Position.reports reports ps; + val reports = Unsynchronized.ref reports0; + fun report ps = Position.reports reports ps; - fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = - (case decode_position typ of - SOME p => decode (p :: ps) qs bs t - | NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) - | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = - (case decode_position typ of - SOME q => decode ps (q :: qs) bs t - | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) - | decode _ qs bs (Abs (x, T, t)) = - let - val id = serial_string (); - val _ = report qs (markup_bound true) id; - in Abs (x, T, decode [] [] (id :: bs) t) end - | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u - | decode ps _ _ (Const (a, T)) = - (case try Lexicon.unmark_fixed a of - SOME x => (report ps markup_free x; Free (x, T)) - | NONE => + fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = + (case decode_position typ of + SOME p => decode (p :: ps) qs bs t + | NONE => Type.constraint (decodeT typ) (decode ps qs bs t)) + | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = + (case decode_position typ of + SOME q => decode ps (q :: qs) bs t + | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t)) + | decode _ qs bs (Abs (x, T, t)) = let - val c = - (case try Lexicon.unmark_const a of - SOME c => c - | NONE => snd (get_const a)); - val _ = report ps markup_const c; - in Const (c, T) end) - | decode ps _ _ (Free (a, T)) = - (case (get_free a, get_const a) of - (SOME x, _) => (report ps markup_free x; Free (x, T)) - | (_, (true, c)) => (report ps markup_const c; Const (c, T)) - | (_, (false, c)) => - if Long_Name.is_qualified c - then (report ps markup_const c; Const (c, T)) - else (report ps markup_free c; Free (c, T))) - | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) - | decode ps _ bs (t as Bound i) = - (case try (nth bs) i of - SOME id => (report ps (markup_bound false) id; t) - | NONE => t); + val id = serial_string (); + val _ = report qs (markup_bound true) id; + in Abs (x, T, decode [] [] (id :: bs) t) end + | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u + | decode ps _ _ (Const (a, T)) = + (case try Lexicon.unmark_fixed a of + SOME x => (report ps markup_free x; Free (x, T)) + | NONE => + let + val c = + (case try Lexicon.unmark_const a of + SOME c => c + | NONE => snd (get_const a)); + val _ = report ps markup_const c; + in Const (c, T) end) + | decode ps _ _ (Free (a, T)) = + (case (get_free a, get_const a) of + (SOME x, _) => (report ps markup_free x; Free (x, T)) + | (_, (true, c)) => (report ps markup_const c; Const (c, T)) + | (_, (false, c)) => + if Long_Name.is_qualified c + then (report ps markup_const c; Const (c, T)) + else (report ps markup_free c; Free (c, T))) + | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) + | decode ps _ bs (t as Bound i) = + (case try (nth bs) i of + SOME id => (report ps (markup_bound false) id; t) + | NONE => t); - val tm' = decode [] [] [] tm; - in (! reports, tm') end; + val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) (); + in (! reports, tm') end;