# HG changeset patch # User wenzelm # Date 1302009333 -7200 # Node ID e48baf91aeabfe1afe8ff93fa19b0695b2bd3450 # Parent d53dccb38dd1cb93e511e8567a81d8fabd5aaefe# Parent cb650789f2f0f6bcc98d43ecd37b74e63cc9c2c9 merged diff -r d53dccb38dd1 -r e48baf91aeab NEWS --- a/NEWS Tue Apr 05 11:44:34 2011 +0200 +++ b/NEWS Tue Apr 05 15:15:33 2011 +0200 @@ -93,6 +93,10 @@ be disabled via the configuration option Syntax.positions, which is called "syntax_positions" in Isar attribute syntax. +* Discontinued special treatment of structure Ast: no pervasive +content, no inclusion in structure Syntax. INCOMPATIBILITY, refer to +qualified names like Ast.Constant etc. + New in Isabelle2011 (January 2011) diff -r d53dccb38dd1 -r e48baf91aeab doc-src/Classes/Thy/Setup.thy --- a/doc-src/Classes/Thy/Setup.thy Tue Apr 05 11:44:34 2011 +0200 +++ b/doc-src/Classes/Thy/Setup.thy Tue Apr 05 15:15:33 2011 +0200 @@ -15,16 +15,16 @@ parse_ast_translation {* let - fun alpha_ast_tr [] = Syntax.Variable "'a" - | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); + fun alpha_ast_tr [] = Ast.Variable "'a" + | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts); fun alpha_ofsort_ast_tr [ast] = - Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast] - | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); - fun beta_ast_tr [] = Syntax.Variable "'b" - | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); + Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast] + | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts); + fun beta_ast_tr [] = Ast.Variable "'b" + | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts); fun beta_ofsort_ast_tr [ast] = - Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast] - | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); + Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast] + | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts); in [(@{syntax_const "_alpha"}, alpha_ast_tr), (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr), diff -r d53dccb38dd1 -r e48baf91aeab src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Tue Apr 05 11:44:34 2011 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Tue Apr 05 15:15:33 2011 +0200 @@ -56,9 +56,9 @@ (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *) let fun Lambda_ast_tr [pats, body] = - Syntax.fold_ast_p @{syntax_const "_cabs"} - (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body) - | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts); + Ast.fold_ast_p @{syntax_const "_cabs"} + (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body) + | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts); in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end; *} @@ -67,12 +67,12 @@ (* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *) let fun cabs_ast_tr' asts = - (case Syntax.unfold_ast_p @{syntax_const "_cabs"} - (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of - ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts) - | (xs, body) => Syntax.Appl - [Syntax.Constant @{syntax_const "_Lambda"}, - Syntax.fold_ast @{syntax_const "_cargs"} xs, body]); + (case Ast.unfold_ast_p @{syntax_const "_cabs"} + (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of + ([], _) => raise Ast.AST ("cabs_ast_tr'", asts) + | (xs, body) => Ast.Appl + [Ast.Constant @{syntax_const "_Lambda"}, + Ast.fold_ast @{syntax_const "_cargs"} xs, body]); in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end *} diff -r d53dccb38dd1 -r e48baf91aeab src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Apr 05 15:15:33 2011 +0200 @@ -442,16 +442,14 @@ (* define syntax for case combinator *) (* TODO: re-implement case syntax using a parse translation *) local - open Syntax fun syntax c = Syntax.mark_const (fst (dest_Const c)) fun xconst c = Long_Name.base_name (fst (dest_Const c)) - fun c_ast authentic con = - Constant (if authentic then syntax con else xconst con) + fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con) fun showint n = string_of_int (n+1) - fun expvar n = Variable ("e" ^ showint n) - fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m) + fun expvar n = Ast.Variable ("e" ^ showint n) + fun argvar n (m, _) = Ast.Variable ("a" ^ showint n ^ "_" ^ showint m) fun argvars n args = map_index (argvar n) args - fun app s (l, r) = mk_appl (Constant s) [l, r] + fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r] val cabs = app "_cabs" val capp = app @{const_syntax Rep_cfun} val capps = Library.foldl capp @@ -460,22 +458,21 @@ fun case1 authentic (n, c) = app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n) fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args) - fun when1 n (m, c) = - if n = m then arg1 (n, c) else (Constant @{const_syntax bottom}) - val case_constant = Constant (syntax (case_const dummyT)) + fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom} + val case_constant = Ast.Constant (syntax (case_const dummyT)) fun case_trans authentic = - (if authentic then Parse_Print_Rule else Parse_Rule) - (app "_case_syntax" - (Variable "x", - foldr1 (app "_case2") (map_index (case1 authentic) spec)), - capp (capps (case_constant, map_index arg1 spec), Variable "x")) + (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule) + (app "_case_syntax" + (Ast.Variable "x", + foldr1 (app "_case2") (map_index (case1 authentic) spec)), + capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x")) fun one_abscon_trans authentic (n, c) = - (if authentic then Parse_Print_Rule else Parse_Rule) - (cabs (con1 authentic n c, expvar n), - capps (case_constant, map_index (when1 n) spec)) + (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule) + (cabs (con1 authentic n c, expvar n), + capps (case_constant, map_index (when1 n) spec)) fun abscon_trans authentic = map_index (one_abscon_trans authentic) spec - val trans_rules : ast Syntax.trrule list = + val trans_rules : Ast.ast Syntax.trrule list = case_trans false :: case_trans true :: abscon_trans false @ abscon_trans true in diff -r d53dccb38dd1 -r e48baf91aeab src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Apr 05 15:15:33 2011 +0200 @@ -24,12 +24,13 @@ fun trans_rules name2 name1 n mx = let val vnames = Name.invents Name.context "a" n - val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1) + val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1) in [Syntax.Parse_Print_Rule - (Syntax.mk_appl (Constant name2) (map Variable vnames), - fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a]) - vnames (Constant name1))] @ + (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames), + fold (fn a => fn t => + Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a]) + vnames (Ast.Constant name1))] @ (case mx of Infix _ => [extra_parse_rule] | Infixl _ => [extra_parse_rule] diff -r d53dccb38dd1 -r e48baf91aeab src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Apr 05 11:44:34 2011 +0200 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Apr 05 15:15:33 2011 +0200 @@ -497,33 +497,32 @@ (* syntax translations for pattern combinators *) local - open Syntax fun syntax c = Syntax.mark_const (fst (dest_Const c)); - fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r]; + fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]; val capp = app @{const_syntax Rep_cfun}; val capps = Library.foldl capp - fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"]; - fun app_pat x = Syntax.mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" + fun app_var x = Ast.mk_appl (Ast.Constant "_variable") [x, Ast.Variable "rhs"]; + fun app_pat x = Ast.mk_appl (Ast.Constant "_pat") [x]; + fun args_list [] = Ast.Constant "_noargs" | args_list xs = foldr1 (app "_args") xs; fun one_case_trans (pat, (con, args)) = let - val cname = Constant (syntax con); - val pname = Constant (syntax pat); + val cname = Ast.Constant (syntax con); + val pname = Ast.Constant (syntax pat); val ns = 1 upto length args; - val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; - val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + val xs = map (fn n => Ast.Variable ("x"^(string_of_int n))) ns; + val ps = map (fn n => Ast.Variable ("p"^(string_of_int n))) ns; + val vs = map (fn n => Ast.Variable ("v"^(string_of_int n))) ns; in - [Parse_Rule (app_pat (capps (cname, xs)), - mk_appl pname (map app_pat xs)), - Parse_Rule (app_var (capps (cname, xs)), - app_var (args_list xs)), - Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] + [Syntax.Parse_Rule (app_pat (capps (cname, xs)), + Ast.mk_appl pname (map app_pat xs)), + Syntax.Parse_Rule (app_var (capps (cname, xs)), + app_var (args_list xs)), + Syntax.Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (Ast.mk_appl pname ps, args_list vs))] end; - val trans_rules : Syntax.ast Syntax.trrule list = + val trans_rules : Ast.ast Syntax.trrule list = maps one_case_trans (pat_consts ~~ spec); in val thy = Sign.add_trrules trans_rules thy; diff -r d53dccb38dd1 -r e48baf91aeab src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/HOL/Import/hol4rews.ML Tue Apr 05 15:15:33 2011 +0200 @@ -610,10 +610,10 @@ end local - fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x - | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x - | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x - | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x] + fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x + | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x + | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x + | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x] | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument" in val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)] diff -r d53dccb38dd1 -r e48baf91aeab src/HOL/Tools/string_syntax.ML --- a/src/HOL/Tools/string_syntax.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/HOL/Tools/string_syntax.ML Tue Apr 05 15:15:33 2011 +0200 @@ -16,10 +16,10 @@ (* nibble *) val mk_nib = - Syntax.Constant o Syntax.mark_const o + Ast.Constant o Syntax.mark_const o fst o Term.dest_Const o HOLogic.mk_nibble; -fun dest_nib (Syntax.Constant s) = +fun dest_nib (Ast.Constant s) = (case try Syntax.unmark_const s of NONE => raise Match | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match)); @@ -29,7 +29,7 @@ fun mk_char s = if Symbol.is_ascii s then - Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)] + Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)] else error ("Non-ASCII symbol: " ^ quote s); val specials = raw_explode "\\\"`'"; @@ -40,44 +40,42 @@ then c else raise Match end; -fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2 +fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2 | dest_char _ = raise Match; fun syntax_string cs = - Syntax.Appl - [Syntax.Constant @{syntax_const "_inner_string"}, - Syntax.Variable (Syntax.implode_xstr cs)]; + Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)]; -fun char_ast_tr [Syntax.Variable xstr] = - (case Syntax.explode_xstr xstr of - [c] => mk_char c - | _ => error ("Single character expected: " ^ xstr)) - | char_ast_tr asts = raise AST ("char_ast_tr", asts); +fun char_ast_tr [Ast.Variable xstr] = + (case Syntax.explode_xstr xstr of + [c] => mk_char c + | _ => error ("Single character expected: " ^ xstr)) + | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts); fun char_ast_tr' [c1, c2] = - Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]] + Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]] | char_ast_tr' _ = raise Match; (* string *) -fun mk_string [] = Syntax.Constant @{const_syntax Nil} +fun mk_string [] = Ast.Constant @{const_syntax Nil} | mk_string (c :: cs) = - Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs]; + Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs]; -fun string_ast_tr [Syntax.Variable xstr] = - (case Syntax.explode_xstr xstr of - [] => - Syntax.Appl - [Syntax.Constant Syntax.constrainC, - Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}] - | cs => mk_string cs) - | string_ast_tr asts = raise AST ("string_tr", asts); +fun string_ast_tr [Ast.Variable xstr] = + (case Syntax.explode_xstr xstr of + [] => + Ast.Appl + [Ast.Constant Syntax.constrainC, + Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}] + | cs => mk_string cs) + | string_ast_tr asts = raise Ast.AST ("string_tr", asts); fun list_ast_tr' [args] = - Syntax.Appl [Syntax.Constant @{syntax_const "_String"}, - syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))] + Ast.Appl [Ast.Constant @{syntax_const "_String"}, + syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))] | list_ast_tr' ts = raise Match; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/General/exn.ML Tue Apr 05 15:15:33 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 d53dccb38dd1 -r e48baf91aeab src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Apr 05 15:15:33 2011 +0200 @@ -398,8 +398,8 @@ (* theory setup *) val _ = Context.>> (Context.map_theory - (register_config Syntax.ast_trace_raw #> - register_config Syntax.ast_stat_raw #> + (register_config Ast.ast_trace_raw #> + register_config Ast.ast_stat_raw #> register_config Syntax.positions_raw #> register_config Syntax.show_brackets_raw #> register_config Syntax.show_sorts_raw #> diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Apr 05 15:15:33 2011 +0200 @@ -117,7 +117,7 @@ ML_Lex.read pos txt |> ML_Context.expression pos ("val parse_ast_translation: (string * (" ^ advancedT a ^ - "Syntax.ast list -> Syntax.ast)) list") + "Ast.ast list -> Ast.ast)) list") ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))") |> Context.theory_map; @@ -141,7 +141,7 @@ ML_Lex.read pos txt |> ML_Context.expression pos ("val print_ast_translation: (string * (" ^ advancedT a ^ - "Syntax.ast list -> Syntax.ast)) list") + "Ast.ast list -> Ast.ast)) list") ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))") |> Context.theory_map; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 05 15:15:33 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) @@ -1092,12 +1093,12 @@ local -fun const_ast_tr intern ctxt [Syntax.Variable c] = +fun const_ast_tr intern ctxt [Ast.Variable c] = let val Const (c', _) = read_const_proper ctxt false c; val d = if intern then Syntax.mark_const c' else c; - in Syntax.Constant d end - | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts); + in Ast.Constant d end + | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts); val typ = Simple_Syntax.read_typ; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Isar/runtime.ML Tue Apr 05 15:15:33 2011 +0200 @@ -72,9 +72,9 @@ | Fail msg => [raised exn "Fail" [msg]] | THEORY (msg, thys) => [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))] - | Syntax.AST (msg, asts) => + | Ast.AST (msg, asts) => [raised exn "AST" (msg :: - (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))] + (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))] | TYPE (msg, Ts, ts) => [raised exn "TYPE" (msg :: (if detailed then diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Apr 05 15:15:33 2011 +0200 @@ -71,17 +71,20 @@ |> Sign.add_modesyntax_i ("latex", false) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] |> Sign.add_trrules (map Syntax.Parse_Print_Rule - [(Syntax.mk_appl (Constant "_Lam") - [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"], - Syntax.mk_appl (Constant "_Lam") - [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]), - (Syntax.mk_appl (Constant "_Lam") - [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"], - Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A", - (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]), - (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"], - Syntax.mk_appl (Constant (Syntax.mark_const "Abst")) - [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]); + [(Ast.mk_appl (Ast.Constant "_Lam") + [Ast.mk_appl (Ast.Constant "_Lam0") + [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], + Ast.mk_appl (Ast.Constant "_Lam") + [Ast.Variable "l", + Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]), + (Ast.mk_appl (Ast.Constant "_Lam") + [Ast.mk_appl (Ast.Constant "_Lam1") + [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"], + Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A", + (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]), + (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"], + Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst")) + [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]); (**** translation between proof terms and pure terms ****) diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Syntax/ast.ML Tue Apr 05 15:15:33 2011 +0200 @@ -4,21 +4,18 @@ Abstract syntax trees, translation rules, matching and normalization of asts. *) -signature AST0 = +signature AST = sig datatype ast = Constant of string | Variable of string | Appl of ast list + val mk_appl: ast -> ast list -> ast exception AST of string * ast list -end; - -signature AST1 = -sig - include AST0 - val mk_appl: ast -> ast list -> ast val pretty_ast: ast -> Pretty.T val pretty_rule: ast * ast -> Pretty.T + val head_of_rule: ast * ast -> string + val rule_error: ast * ast -> string option val fold_ast: string -> ast list -> ast val fold_ast_p: string -> ast list * ast -> ast val unfold_ast: string -> ast -> ast list @@ -27,17 +24,10 @@ val ast_trace: bool Config.T val ast_stat_raw: Config.raw val ast_stat: bool Config.T -end; - -signature AST = -sig - include AST1 - val head_of_rule: ast * ast -> string - val rule_error: ast * ast -> string option val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast end; -structure Ast : AST = +structure Ast: AST = struct (** abstract syntax trees **) @@ -53,16 +43,12 @@ Variable of string | (*x, ?x, 'a, ?'a*) Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*) - (*the list of subasts of an Appl node has to contain at least 2 elements, i.e. there are no empty asts or nullary applications; use mk_appl for convenience*) - fun mk_appl f [] = f | mk_appl f args = Appl (f :: args); - (*exception for system errors involving asts*) - exception AST of string * ast list; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Syntax/parser.ML Tue Apr 05 15:15:33 2011 +0200 @@ -9,7 +9,6 @@ type gram val empty_gram: gram val extend_gram: Syn_Ext.xprod list -> gram -> gram - val make_gram: Syn_Ext.xprod list -> gram val merge_gram: gram * gram -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = @@ -54,6 +53,8 @@ lambda productions are stored as normal productions and also as an entry in "lambdas"*) +val union_token = union Lexicon.matching_tokens; +val subtract_token = subtract Lexicon.matching_tokens; (*productions for which no starting token is known yet are associated with this token*) @@ -119,14 +120,14 @@ if forall (fn Nonterminal (id, _) => member (op =) lambdas' id | Terminal _ => false) rhs - then (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs])) + then (true, union (op =) (connected_with chains' [lhs] [lhs]) lambdas') else (false, lambdas'); (*list optional terminal and all nonterminals on which the lookahead of a production depends*) fun lookahead_dependency _ [] nts = (NONE, nts) - | lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts) - | lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts = + | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts) + | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts = if member (op =) lambdas nt then lookahead_dependency lambdas symbs (nt :: nts) else (NONE, nt :: nts); @@ -134,13 +135,11 @@ (*get all known starting tokens for a nonterminal*) fun starts_for_nt nt = snd (fst (Array.sub (prods, nt))); - val token_union = uncurry (union Lexicon.matching_tokens); - (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = let (*propagate added lambda NT*) - fun propagate_lambda [] added_starts lambdas= (added_starts, lambdas) + fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas) | propagate_lambda (l :: ls) added_starts lambdas = let (*get lookahead for lambda NT*) @@ -156,11 +155,12 @@ let val new_lambda = is_none tk andalso subset (op =) (nts, lambdas); - val new_tks = subtract (op =) l_starts - ((if is_some tk then [the tk] else []) @ - Library.foldl token_union ([], map starts_for_nt nts)); + val new_tks = + (if is_some tk then [the tk] else []) + |> fold (union_token o starts_for_nt) nts + |> subtract (op =) l_starts; - val added_tks' = token_union (new_tks, added_tks); + val added_tks' = union_token added_tks new_tks; val nt_dependencies' = union (op =) nts nt_dependencies; @@ -244,9 +244,8 @@ val (start_tk, start_nts) = lookahead_dependency lambdas' rhs []; val start_tks = - Library.foldl token_union - (if is_some start_tk then [the start_tk] else [], - map starts_for_nt start_nts); + (if is_some start_tk then [the start_tk] else []) + |> fold (union_token o starts_for_nt) start_nts; val opt_starts = (if new_lambda then [NONE] @@ -256,10 +255,10 @@ (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts [] = () | add_nts (nt :: nts) = - let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in - if member (op =) old_nts lhs then () - else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps)) - end; + let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in + if member (op =) old_nts lhs then () + else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps)) + end; (*add new start tokens to chained NTs' lookahead list; also store new production for lhs NT*) @@ -268,7 +267,7 @@ let val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); - val new_tks = subtract Lexicon.matching_tokens old_tks start_tks; + val new_tks = subtract_token old_tks start_tks; (*store new production*) fun store [] prods is_new = @@ -288,8 +287,10 @@ else (new_prod :: tk_prods, true) else (new_prod :: tk_prods, true); - val prods' = prods - |> is_new' ? AList.update (op =) (tk: Lexicon.token option, tk_prods'); + val prods' = + if is_new' then + AList.update (op =) (tk: Lexicon.token option, tk_prods') prods + else prods; in store tks prods' (is_new orelse is_new') end; val (nt_prods', prod_count', changed) = @@ -375,17 +376,18 @@ (*associate productions with new lookahead tokens*) val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods); - val nt_prods' = - nt_prods' - |> (key = SOME unknown_start) ? AList.update (op =) (key, tk_prods'); + val nt_prods'' = + if key = SOME unknown_start then + AList.update (op =) (key, tk_prods') nt_prods' + else nt_prods'; - val added_tks = subtract Lexicon.matching_tokens old_tks new_tks; + val added_tks = subtract_token old_tks new_tks; in if null added_tks then - (Array.update (prods, nt, (lookahead, nt_prods')); + (Array.update (prods, nt, (lookahead, nt_prods'')); process_nts nts added) else - (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods')); + (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods'')); process_nts nts ((nt, added_tks) :: added)) end; @@ -422,13 +424,14 @@ fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); val nt_prods = - Library.foldl (uncurry (union (op =))) ([], map snd (snd (Vector.sub (prods, tag)))) @ - map prod_of_chain (these (AList.lookup (op =) chains tag)); + fold (union (op =) o snd) (snd (Vector.sub (prods, tag))) [] @ + map prod_of_chain (these (AList.lookup (op =) chains tag)); in map (pretty_prod name) nt_prods end; in maps pretty_nt (sort_wrt fst (Symtab.dest tags)) end; + (** Operations on gramars **) val empty_gram = @@ -465,10 +468,10 @@ delimiters and predefined terms are stored as terminals, nonterminals are converted to integer tags*) fun symb_of [] nt_count tags result = (nt_count, tags, rev result) - | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result = + | symb_of (Syn_Ext.Delim s :: ss) nt_count tags result = symb_of ss nt_count tags (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result) - | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result = + | symb_of (Syn_Ext.Argument (s, p) :: ss) nt_count tags result = let val (nt_count', tags', new_symb) = (case Lexicon.predef_term s of @@ -482,7 +485,7 @@ (*Convert list of productions by invoking symb_of for each of them*) fun prod_of [] nt_count prod_count tags result = (nt_count, prod_count, tags, result) - | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps) + | prod_of (Syn_Ext.XProd (lhs, xsymbs, const, pri) :: ps) nt_count prod_count tags result = let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; @@ -522,8 +525,6 @@ prods = Array.vector prods'} end; -fun make_gram xprods = extend_gram xprods empty_gram; - (*Merge two grammars*) fun merge_gram (gram_a, gram_b) = @@ -551,15 +552,14 @@ val ((nt_count1', tags1'), tag_table) = let - val tag_list = Symtab.dest tags2; - val table = Array.array (nt_count2, ~1); + fun the_nt tag = + the (Symtab.get_first (fn (n, t) => if t = tag then SOME n else NONE) tags2); fun store_tag nt_count tags ~1 = (nt_count, tags) | store_tag nt_count tags tag = let - val (nt_count', tags', tag') = - get_tag nt_count tags (fst (the (find_first (fn (n, t) => t = tag) tag_list))); + val (nt_count', tags', tag') = get_tag nt_count tags (the_nt tag); val _ = Array.update (table, tag, tag'); in store_tag nt_count' tags' (tag - 1) end; in (store_tag nt_count1 tags1 (nt_count2 - 1), table) end; @@ -584,8 +584,7 @@ fun process_nt ~1 result = result | process_nt nt result = let - val nt_prods = Library.foldl (uncurry (union (op =))) - ([], map snd (snd (Vector.sub (prods2, nt)))); + val nt_prods = fold (union (op =) o snd) (snd (Vector.sub (prods2, nt))) []; val lhs_tag = convert_tag nt; (*convert tags in rhs*) @@ -627,6 +626,7 @@ end; + (** Parser **) datatype parsetree = @@ -647,11 +647,11 @@ (*Get all rhss with precedence >= min_prec*) -fun get_RHS min_prec = filter (fn (_, _, prec:int) => prec >= min_prec); +fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec); (*Get all rhss with precedence >= min_prec and < max_prec*) fun get_RHS' min_prec max_prec = - filter (fn (_, _, prec:int) => prec >= min_prec andalso prec < max_prec); + filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec); (*Make states using a list of rhss*) fun mk_states i min_prec lhs_ID rhss = @@ -660,7 +660,7 @@ (*Add parse tree to list and eliminate duplicates saving the maximum precedence*) -fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)]) +fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)]) | conc (t, prec) ((t', prec') :: ts) = if t = t' then (SOME prec', @@ -671,33 +671,25 @@ in (n, (t', prec') :: ts') end; (*Update entry in used*) -fun update_trees ((B: nt_tag, (i, ts)) :: used) (A, t) = - if A = B then - let val (n, ts') = conc t ts - in ((A, (i, ts')) :: used, n) end - else - let val (used', n) = update_trees used (A, t) - in ((B, (i, ts)) :: used', n) end; +fun update_trees (A, t) used = + let + val (i, ts) = the (Inttab.lookup used A); + val (n, ts') = conc t ts; + in (n, Inttab.update (A, (i, ts')) used) end; (*Replace entry in used*) -fun update_prec (A: nt_tag, prec) used = - let - fun update ((hd as (B, (_, ts))) :: used, used') = - if A = B - then used' @ ((A, (prec, ts)) :: used) - else update (used, hd :: used') - in update (used, []) end; +fun update_prec (A, prec) = + Inttab.map_entry A (fn (_, ts) => (prec, ts)); -fun getS A max_prec Si = - filter - (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec - | _ => false) Si; - -fun getS' A max_prec min_prec Si = - filter - (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) - => A = B andalso prec > min_prec andalso prec <= max_prec - | _ => false) Si; +fun getS A max_prec NONE Si = + filter + (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec + | _ => false) Si + | getS A max_prec (SOME min_prec) Si = + filter + (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => + A = B andalso prec > min_prec andalso prec <= max_prec + | _ => false) Si; fun get_states Estate i ii A max_prec = filter @@ -706,19 +698,17 @@ (Array.sub (Estate, ii)); -fun movedot_term (A, j, ts, Terminal a :: sa, id, i) c = - if Lexicon.valued_token c then (A, j, ts @ [Tip c], sa, id, i) +fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = + if Lexicon.valued_token c then (A, j, Tip c :: ts, sa, id, i) else (A, j, ts, sa, id, i); -fun movedot_nonterm ts (A, j, tss, Nonterminal _ :: sa, id, i) = - (A, j, tss @ ts, sa, id, i); +fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) = + (A, j, List.revAppend (tt, ts), sa, id, i); -fun movedot_lambda _ [] = [] - | movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ((t, ki) :: ts) = - if k <= ki then - (B, j, tss @ t, sa, id, i) :: - movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts - else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts; +fun movedot_lambda [] _ = [] + | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) = + if k <= ki then (B, j, List.revAppend (t, tss), sa, id, i) :: movedot_lambda ts state + else movedot_lambda ts state; (*trigger value for warnings*) @@ -741,7 +731,7 @@ fun get_prods [] result = result | get_prods (nt :: nts) result = let val nt_prods = snd (Vector.sub (prods, nt)); - in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end; + in get_prods nts (token_assoc (nt_prods, tk) @ result) end; in get_prods (connected_with chains nts nts) [] end; @@ -755,30 +745,26 @@ (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) => let (*predictor operation*) val (used', new_states) = - (case AList.lookup (op =) used nt of + (case Inttab.lookup used nt of SOME (used_prec, l) => (*nonterminal has been processed*) if used_prec <= min_prec then (*wanted precedence has been processed*) - (used, movedot_lambda S l) + (used, movedot_lambda l S) else (*wanted precedence hasn't been parsed yet*) let val tk_prods = all_prods_for nt; - - val States' = mk_states i min_prec nt - (get_RHS' min_prec used_prec tk_prods); - in (update_prec (nt, min_prec) used, - movedot_lambda S l @ States') - end - + val States' = + mk_states i min_prec nt (get_RHS' min_prec used_prec tk_prods); + in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end | NONE => (*nonterminal is parsed for the first time*) let val tk_prods = all_prods_for nt; val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods); - in ((nt, (min_prec, [])) :: used, States') end); + in (Inttab.update (nt, (min_prec, [])) used, States') end); - val dummy = + val _ = if not (! warned) andalso - length (new_states @ States) > Config.get ctxt branching_level then + length new_states + length States > Config.get ctxt branching_level then (Context_Position.if_visible ctxt warning "Currently parsed expression could be extremely ambiguous"; warned := true) @@ -789,32 +775,20 @@ | (_, _, _, Terminal a :: _, _, _) => (*scanner operation*) processS used States (S :: Si, - if Lexicon.matching_tokens (a, c) then movedot_term S c :: Sii else Sii) + if Lexicon.matching_tokens (a, c) then movedot_term c S :: Sii else Sii) | (A, prec, ts, [], id, j) => (*completer operation*) - let val tt = if id = "" then ts else [Node (id, ts)] in + let val tt = if id = "" then ts else [Node (id, rev ts)] in if j = i then (*lambda production?*) let - val (used', O) = update_trees used (A, (tt, prec)); - in - (case O of - NONE => - let - val Slist = getS A prec Si; - val States' = map (movedot_nonterm tt) Slist; - in processS used' (States' @ States) (S :: Si, Sii) end - | SOME n => - if n >= prec then processS used' States (S :: Si, Sii) - else - let - val Slist = getS' A prec n Si; - val States' = map (movedot_nonterm tt) Slist; - in processS used' (States' @ States) (S :: Si, Sii) end) - end + val (prec', used') = update_trees (A, (tt, prec)) used; + val Slist = getS A prec prec' Si; + val States' = map (movedot_nonterm tt) Slist; + in processS used' (States' @ States) (S :: Si, Sii) end else let val Slist = get_states Estate i j A prec in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end end) - in processS [] states ([], []) end; + in processS Inttab.empty states ([], []) end; fun produce ctxt warned prods tags chains stateset i indata prev_token = @@ -832,16 +806,16 @@ end | s => (case indata of - [] => Array.sub (stateset, i) - | c :: cs => - let val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s; - in Array.update (stateset, i, si); - Array.update (stateset, i + 1, sii); - produce ctxt warned prods tags chains stateset (i + 1) cs c - end)); + [] => s + | c :: cs => + let + val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s; + val _ = Array.update (stateset, i, si); + val _ = Array.update (stateset, i + 1, sii); + in produce ctxt warned prods tags chains stateset (i + 1) cs c end)); -fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l; +fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states; fun earley ctxt prods tags chains startsymbol indata = let diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Tue Apr 05 15:15:33 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 d53dccb38dd1 -r e48baf91aeab src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Apr 05 15:15:33 2011 +0200 @@ -7,7 +7,6 @@ signature BASIC_SYNTAX = sig - include AST0 include SYN_TRANS0 include MIXFIX0 include PRINTER0 @@ -15,7 +14,6 @@ signature SYNTAX = sig - include AST1 include LEXICON0 include SYN_EXT0 include TYPE_EXT0 @@ -116,44 +114,44 @@ 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 | Parse_Print_Rule of 'a * 'a 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 read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> Ast.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 * ((Ast.ast list -> Ast.ast) * stamp)) list * (string * ((term list -> term) * stamp)) list * (string * ((bool -> typ -> term list -> term) * stamp)) list * - (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax + (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax val update_advanced_trfuns: - (string * ((Proof.context -> ast list -> ast) * stamp)) list * + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list * - (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax + (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> syntax -> syntax val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_const_gram: bool -> (string -> bool) -> mode -> (string * typ * mixfix) list -> syntax -> syntax - val update_trrules: ast trrule list -> syntax -> syntax - val remove_trrules: ast trrule list -> syntax -> syntax + val update_trrules: Ast.ast trrule list -> syntax -> syntax + val remove_trrules: Ast.ast trrule list -> syntax -> syntax end; structure Syntax: SYNTAX = @@ -562,7 +560,7 @@ Syntax ({input = input', lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon, - gram = if changed then Parser.make_gram input' else gram, + gram = if changed then Parser.extend_gram input' Parser.empty_gram else gram, consts = consts, prmodes = prmodes, parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab, @@ -686,17 +684,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 +702,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 +743,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 +884,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 +907,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; @@ -933,16 +941,14 @@ (*export parts of internal Syntax structures*) -open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer; +open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer; end; structure Basic_Syntax: BASIC_SYNTAX = Syntax; open Basic_Syntax; -forget_structure "Ast"; forget_structure "Syn_Ext"; -forget_structure "Parser"; forget_structure "Type_Ext"; forget_structure "Syn_Trans"; forget_structure "Mixfix"; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/Syntax/type_ext.ML Tue Apr 05 15:15:33 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; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/pure_setup.ML Tue Apr 05 15:15:33 2011 +0200 @@ -30,7 +30,7 @@ toplevel_pp ["Context", "theory"] "Context.pretty_thy"; toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; -toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast"; +toplevel_pp ["Syntax", "ast"] "Ast.pretty_ast"; toplevel_pp ["Path", "T"] "Pretty.str o Path.print"; toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"\")"; diff -r d53dccb38dd1 -r e48baf91aeab src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Apr 05 11:44:34 2011 +0200 +++ b/src/Pure/sign.ML Tue Apr 05 15:15:33 2011 +0200 @@ -91,25 +91,25 @@ val primitive_classrel: class * class -> theory -> theory val primitive_arity: arity -> theory -> theory val add_trfuns: - (string * (ast list -> ast)) list * + (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list * (string * (term list -> term)) list * - (string * (ast list -> ast)) list -> theory -> theory + (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory val add_trfunsT: (string * (bool -> typ -> term list -> term)) list -> theory -> theory val add_advanced_trfuns: - (string * (Proof.context -> ast list -> ast)) list * + (string * (Proof.context -> Ast.ast list -> Ast.ast)) list * (string * (Proof.context -> term list -> term)) list * (string * (Proof.context -> term list -> term)) list * - (string * (Proof.context -> ast list -> ast)) list -> theory -> theory + (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory val add_advanced_trfunsT: (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory val add_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory - val add_trrules: ast Syntax.trrule list -> theory -> theory - val del_trrules: ast Syntax.trrule list -> theory -> theory + val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory + val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory val new_group: theory -> theory val reset_group: theory -> theory val add_path: string -> theory -> theory