--- 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;