# HG changeset patch # User wenzelm # Date 1301860773 -7200 # Node ID b3277168c1e748edc07570e74c1c3f6c0e2d5214 # Parent 9c9c97a5040d6e35bc9b7ce683779d7eacae4626 added Position.reports convenience; modernized Syntax.trrule constructors; modernized Sign.add_trrules/del_trrules: internal arguments; modernized Isar_Cmd.translations/no_translations: external arguments; explicit syntax categories class_name/type_name, with reports via type_context; eliminated former class_name/type_name ast translations; tuned signatures; diff -r 9c9c97a5040d -r b3277168c1e7 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sun Apr 03 21:59:33 2011 +0200 @@ -464,13 +464,13 @@ if n = m then arg1 (n, c) else (Constant @{const_syntax bottom}) val case_constant = Constant (syntax (case_const dummyT)) fun case_trans authentic = - (if authentic then ParsePrintRule else ParseRule) + (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")) fun one_abscon_trans authentic (n, c) = - (if authentic then ParsePrintRule else ParseRule) + (if authentic then Parse_Print_Rule else Parse_Rule) (cabs (con1 authentic n c, expvar n), capps (case_constant, map_index (when1 n) spec)) fun abscon_trans authentic = @@ -479,7 +479,7 @@ case_trans false :: case_trans true :: abscon_trans false @ abscon_trans true in - val thy = Sign.add_trrules_i trans_rules thy + val thy = Sign.add_trrules trans_rules thy end (* prove beta reduction rule for case combinator *) diff -r 9c9c97a5040d -r b3277168c1e7 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sun Apr 03 21:59:33 2011 +0200 @@ -24,9 +24,9 @@ fun trans_rules name2 name1 n mx = let val vnames = Name.invents Name.context "a" n - val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1) + val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1) in - [Syntax.ParsePrintRule + [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))] @ @@ -80,7 +80,7 @@ in thy |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) - |> Sign.add_trrules_i (maps #3 transformed_decls) + |> Sign.add_trrules (maps #3 transformed_decls) end in diff -r 9c9c97a5040d -r b3277168c1e7 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Apr 03 18:17:21 2011 +0200 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sun Apr 03 21:59:33 2011 +0200 @@ -516,17 +516,17 @@ val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; in - [ParseRule (app_pat (capps (cname, xs)), + [Parse_Rule (app_pat (capps (cname, xs)), mk_appl pname (map app_pat xs)), - ParseRule (app_var (capps (cname, xs)), + Parse_Rule (app_var (capps (cname, xs)), app_var (args_list xs)), - PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)), + Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)), app "_match" (mk_appl pname ps, args_list vs))] end; val trans_rules : Syntax.ast Syntax.trrule list = maps one_case_trans (pat_consts ~~ spec); in - val thy = Sign.add_trrules_i trans_rules thy; + val thy = Sign.add_trrules trans_rules thy; end; (* prove strictness and reduction rules of pattern combinators *) diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/General/position.ML Sun Apr 03 21:59:33 2011 +0200 @@ -34,6 +34,8 @@ val reported_text: T -> Markup.T -> string -> string val report_text: T -> Markup.T -> string -> unit val report: T -> Markup.T -> unit + type reports = (T * Markup.T) list + val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit val str_of: T -> string type range = T * T val no_range: range @@ -155,6 +157,13 @@ fun report_text pos markup txt = Output.report (reported_text pos markup txt); fun report pos markup = report_text pos markup ""; +type reports = (T * Markup.T) list; + +fun reports _ [] _ _ = () + | reports (r: reports Unsynchronized.ref) ps markup x = + let val ms = markup x + in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end; + (* str_of *) diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sun Apr 03 21:59:33 2011 +0200 @@ -13,6 +13,8 @@ val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory + val translations: (xstring * string) Syntax.trrule list -> theory -> theory + val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory val add_axioms: (Attrib.binding * string) list -> theory -> theory val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory @@ -154,6 +156,22 @@ end; +(* translation rules *) + +fun read_trrules thy raw_rules = + let + val ctxt = ProofContext.init_global thy; + val type_ctxt = ProofContext.type_context ctxt; + val syn = ProofContext.syn_of ctxt; + in + raw_rules |> map (Syntax.map_trrule (fn (r, s) => + Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s))) + end; + +fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; +fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; + + (* oracles *) fun oracle (name, pos) (body_txt, body_pos) = diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sun Apr 03 21:59:33 2011 +0200 @@ -175,9 +175,9 @@ -- Parse.string; fun trans_arrow toks = - ((Parse.$$$ "\\" || Parse.$$$ "=>") >> K Syntax.ParseRule || - (Parse.$$$ "\\" || Parse.$$$ "<=") >> K Syntax.PrintRule || - (Parse.$$$ "\\" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks; + ((Parse.$$$ "\\" || Parse.$$$ "=>") >> K Syntax.Parse_Rule || + (Parse.$$$ "\\" || Parse.$$$ "<=") >> K Syntax.Print_Rule || + (Parse.$$$ "\\" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) @@ -185,11 +185,11 @@ val _ = Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl - (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl - (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); (* axioms and definitions *) diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun Apr 03 21:59:33 2011 +0200 @@ -65,7 +65,9 @@ val allow_dummies: Proof.context -> Proof.context val check_tvar: Proof.context -> indexname * sort -> indexname * sort val check_tfree: Proof.context -> string * sort -> string * sort - val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term + 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 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 @@ -665,12 +667,18 @@ in +fun type_context ctxt : Syntax.type_context = + {get_class = read_class ctxt, + get_type = #1 o dest_Type o read_type_name_proper ctxt false, + markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c], + markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]}; + fun term_context ctxt : Syntax.term_context = {get_sort = get_sort ctxt, get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), get_free = intern_skolem ctxt (Variable.def_type ctxt false), - markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x], + markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c], markup_free = fn x => [if can Name.dest_skolem x then Markup.skolem else Markup.free] @ (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]), @@ -748,14 +756,16 @@ fun parse_sort ctxt text = let val (syms, pos) = Syntax.parse_token ctxt Markup.sort text; - val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos) + val S = + Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos) handle ERROR msg => parse_failed ctxt pos msg "sort"; in Type.minimize_sort (tsig_of ctxt) S end; fun parse_typ ctxt text = let val (syms, pos) = Syntax.parse_token ctxt Markup.typ text; - val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos) + val T = + Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos) handle ERROR msg => parse_failed ctxt pos msg "type"; in T end; @@ -777,8 +787,9 @@ fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE) handle ERROR msg => SOME msg; val t = - Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos) - handle ERROR msg => parse_failed ctxt pos msg kind; + Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt) + root (syms, pos) + handle ERROR msg => parse_failed ctxt pos msg kind; in t end; @@ -1079,13 +1090,6 @@ (* authentic syntax *) -val _ = Context.>> - (Context.map_theory - (Sign.add_advanced_trfuns - (Syntax.type_ast_trs - {read_class = read_class, - read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], []))); - local fun const_ast_tr intern ctxt [Syntax.Variable c] = diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sun Apr 03 21:59:33 2011 +0200 @@ -70,7 +70,7 @@ (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] |> Sign.add_modesyntax_i ("latex", false) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [0, 3], 3))] - |> Sign.add_trrules_i (map Syntax.ParsePrintRule + |> 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") diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Sun Apr 03 21:59:33 2011 +0200 @@ -48,6 +48,7 @@ (string * (term list -> term)) list * (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list + type type_context end; signature SYN_TRANS = @@ -57,8 +58,9 @@ val prop_tr': term -> term val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast - val parsetree_to_ast: Proof.context -> bool -> - (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> 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 val ast_to_term: Proof.context -> (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term end; @@ -549,21 +551,44 @@ (** parsetree_to_ast **) -fun parsetree_to_ast ctxt constrain_pos trf = +type type_context = + {get_class: string -> string, + get_type: string -> string, + markup_class: string -> Markup.T list, + markup_type: string -> Markup.T list}; + +fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree = let + val {get_class, get_type, markup_class, markup_type} = type_context; + + val reports = Unsynchronized.ref ([]: Position.reports); + fun report pos = Position.reports reports [pos]; + fun trans a args = (case trf a of NONE => Ast.mk_appl (Ast.Constant a) args | SOME f => f ctxt args); - fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) = + fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) = + let + val c = get_class (Lexicon.str_of_token tok); + val _ = report (Lexicon.pos_of_token tok) markup_class c; + in Ast.Constant (Lexicon.mark_class c) end + | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) = + let + val c = get_type (Lexicon.str_of_token tok); + val _ = report (Lexicon.pos_of_token tok) markup_type c; + in Ast.Constant (Lexicon.mark_type c) end + | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) = if constrain_pos then Ast.Appl [Ast.Constant "_constrain", ast_of pt, Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))] else ast_of pt | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts) | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); - in ast_of end; + + val ast = ast_of parsetree; + in (! reports, ast) end; diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Apr 03 21:59:33 2011 +0200 @@ -116,17 +116,20 @@ 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) -> term_context -> - Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term - val standard_parse_typ: Proof.context -> syntax -> + val standard_parse_term: (term -> string option) -> + 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 -> syntax -> Symbol_Pos.T list * Position.T -> sort + val standard_parse_sort: Proof.context -> type_context -> syntax -> + Symbol_Pos.T list * Position.T -> sort datatype 'a trrule = - ParseRule of 'a * 'a | - PrintRule of 'a * 'a | - ParsePrintRule of 'a * 'a + 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 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 @@ -149,10 +152,8 @@ 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: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax - val remove_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax - val update_trrules_i: ast trrule list -> syntax -> syntax - val remove_trrules_i: ast trrule list -> syntax -> syntax + val update_trrules: ast trrule list -> syntax -> syntax + val remove_trrules: ast trrule list -> syntax -> syntax end; structure Syntax: SYNTAX = @@ -619,8 +620,8 @@ val basic_nonterms = (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes", Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", - "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", - "index", "struct", "id_position", "longid_position"]); + "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index", + "struct", "id_position", "longid_position", "type_name", "class_name"]); @@ -711,7 +712,7 @@ fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos; -fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) = +fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) = let val {lexicon, gram, parse_ast_trtab, ...} = tabs; val toks = Lexicon.tokenize lexicon raw syms; @@ -725,7 +726,8 @@ val limit = Config.get ctxt ambiguity_limit; fun show_pt pt = - Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt)); + Pretty.string_of + (Ast.pretty_ast (#2 (Syn_Trans.parsetree_to_ast ctxt type_ctxt false (K NONE) pt))); val _ = if len <= Config.get ctxt ambiguity_level then () else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos) @@ -738,17 +740,18 @@ val constrain_pos = not raw andalso Config.get ctxt positions; in - some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts + some_results + (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts end; (* read *) -fun read ctxt (syn as Syntax (tabs, _)) root inp = +fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp = let val {parse_ruletab, parse_trtab, ...} = tabs in - read_asts ctxt syn false root inp - |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)) - |> some_results (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)) + 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))) end; @@ -790,51 +793,60 @@ map (show_term o snd) (take limit results))) end; -fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) = - read ctxt syn root (syms, pos) +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; (* read types *) -fun standard_parse_typ ctxt syn get_sort (syms, pos) = - (case read ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of - [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t +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 sorts *) -fun standard_parse_sort ctxt syn (syms, pos) = - (case read ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of - [t] => Type_Ext.sort_of_term t +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)); (** prepare translation rules **) +(* rules *) + datatype 'a trrule = - ParseRule of 'a * 'a | - PrintRule of 'a * 'a | - ParsePrintRule of 'a * 'a; + Parse_Rule of 'a * 'a | + Print_Rule of 'a * 'a | + Parse_Print_Rule of 'a * 'a; -fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y) - | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y) - | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y); +fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y) + | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y) + | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y); -fun parse_rule (ParseRule pats) = SOME pats - | parse_rule (PrintRule _) = NONE - | parse_rule (ParsePrintRule pats) = SOME pats; +fun parse_rule (Parse_Rule pats) = SOME pats + | parse_rule (Print_Rule _) = NONE + | parse_rule (Parse_Print_Rule pats) = SOME pats; -fun print_rule (ParseRule _) = NONE - | print_rule (PrintRule pats) = SOME (swap pats) - | print_rule (ParsePrintRule pats) = SOME (swap pats); +fun print_rule (Parse_Rule _) = NONE + | print_rule (Print_Rule pats) = SOME (swap pats) + | print_rule (Parse_Print_Rule pats) = SOME (swap pats); fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c; + +(* check_rules *) + local fun check_rule rule = @@ -844,7 +856,18 @@ Pretty.string_of (Ast.pretty_rule rule)) | NONE => rule); -fun read_pattern ctxt syn (root, str) = +in + +fun check_rules rules = + (map check_rule (map_filter parse_rule rules), + map check_rule (map_filter print_rule rules)); + +end; + + +(* read_rule_pattern *) + +fun read_rule_pattern ctxt type_ctxt syn (root, str) = let fun constify (ast as Ast.Constant _) = ast | constify (ast as Ast.Variable x) = @@ -854,25 +877,13 @@ val (syms, pos) = read_token str; in - (case read_asts ctxt syn true root (syms, pos) of - [ast] => constify ast + (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)) end; -fun prep_rules rd_pat raw_rules = - let val rules = map (map_trrule rd_pat) raw_rules in - (map check_rule (map_filter parse_rule rules), - map check_rule (map_filter print_rule rules)) - end - -in - -val cert_rules = prep_rules I; - -fun read_rules ctxt syn = prep_rules (read_pattern ctxt syn); - -end; - (** unparse terms, typs, sorts **) @@ -920,14 +931,8 @@ fun update_const_gram add is_logtype prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls); -fun update_trrules ctxt syn = - ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt syn; - -fun remove_trrules ctxt syn = - remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt syn; - -val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules; -val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules; +val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules; +val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules; (*export parts of internal Syntax structures*) diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/Syntax/type_ext.ML Sun Apr 03 21:59:33 2011 +0200 @@ -13,14 +13,10 @@ val strip_positions: term -> term val strip_positions_ast: Ast.ast -> Ast.ast type term_context - val decode_term: term_context -> term -> (Position.T * Markup.T) list * term + val decode_term: term_context -> Position.reports * term -> Position.reports * term val term_of_typ: bool -> typ -> term val no_brackets: unit -> bool val no_type_brackets: unit -> bool - val type_ast_trs: - {read_class: Proof.context -> string -> string, - read_type: Proof.context -> string -> string} -> - (string * (Proof.context -> Ast.ast list -> Ast.ast)) list end; signature TYPE_EXT = @@ -140,16 +136,13 @@ markup_free: string -> Markup.T list, markup_var: indexname -> Markup.T list}; -fun decode_term (term_context: term_context) tm = +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)); - val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list); - fun report [] _ _ = () - | report ps markup x = - let val ms = markup x - in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end; + 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 @@ -252,30 +245,14 @@ (* parse ast translations *) -val class_ast = Ast.Constant o Lexicon.mark_class; -val type_ast = Ast.Constant o Lexicon.mark_type; - -fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c) - | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts); - -fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] = - Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast] - | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts); +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] + | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); -fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c) - | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts); - -fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] = - Ast.Appl [type_ast (read_type c), ty] - | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts); +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) + | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); -fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] = - Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys) - | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts); - -fun bracket_ast_tr (*"_bracket"*) [dom, cod] = - Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) - | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts); +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod) + | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); (* print ast translations *) @@ -296,32 +273,35 @@ (* type_ext *) -val sortT = Type ("sort", []); -val classesT = Type ("classes", []); -val typesT = Type ("types", []); +fun typ c = Type (c, []); + +val class_nameT = typ "class_name"; +val type_nameT = typ "type_name"; + +val sortT = typ "sort"; +val classesT = typ "classes"; +val typesT = typ "types"; local open Lexicon Syn_Ext in val type_ext = syn_ext' false (K false) [Mfix ("_", tidT --> typeT, "", [], max_pri), Mfix ("_", tvarT --> typeT, "", [], max_pri), - Mfix ("_", idT --> typeT, "_type_name", [], max_pri), - Mfix ("_", longidT --> typeT, "_type_name", [], max_pri), + Mfix ("_", type_nameT --> typeT, "", [], max_pri), + Mfix ("_", idT --> type_nameT, "_type_name", [], max_pri), + Mfix ("_", longidT --> type_nameT, "_type_name", [], max_pri), Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), Mfix ("'_()::_", sortT --> typeT, "_dummy_ofsort", [0], max_pri), - Mfix ("_", idT --> sortT, "_class_name", [], max_pri), - Mfix ("_", longidT --> sortT, "_class_name", [], max_pri), + Mfix ("_", class_nameT --> sortT, "", [], max_pri), + Mfix ("_", idT --> class_nameT, "_class_name", [], max_pri), + Mfix ("_", longidT --> class_nameT, "_class_name", [], max_pri), Mfix ("{}", sortT, "_topsort", [], max_pri), Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), - Mfix ("_", idT --> classesT, "_class_name", [], max_pri), - Mfix ("_", longidT --> classesT, "_class_name", [], max_pri), - Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri), - Mfix ("_,_", [longidT, classesT] ---> classesT, "_classes", [], max_pri), - Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), - Mfix ("_ _", [typeT, longidT] ---> typeT, "_tapp", [max_pri, 0], max_pri), - Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri), - Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri), + Mfix ("_", class_nameT --> classesT, "", [], max_pri), + Mfix ("_,_", [class_nameT, classesT] ---> classesT, "_classes", [], max_pri), + Mfix ("_ _", [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri), + Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri), Mfix ("_", typeT --> typesT, "", [], max_pri), Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "\\<^type>fun", [1, 0], 0), @@ -329,18 +309,12 @@ Mfix ("'(_')", typeT --> typeT, "", [0], max_pri), Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)] ["_type_prop"] - ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')]) + (map Syn_Ext.mk_trfun + [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)], + [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')]) [] ([], []); -fun type_ast_trs {read_class, read_type} = - [("_class_name", class_name_tr o read_class), - ("_classes", classes_tr o read_class), - ("_type_name", type_name_tr o read_type), - ("_tapp", tapp_ast_tr o read_type), - ("_tappl", tappl_ast_tr o read_type), - ("_bracket", K bracket_ast_tr)]; - end; end; diff -r 9c9c97a5040d -r b3277168c1e7 src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Apr 03 18:17:21 2011 +0200 +++ b/src/Pure/sign.ML Sun Apr 03 21:59:33 2011 +0200 @@ -108,10 +108,8 @@ (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: (xstring * string) Syntax.trrule list -> theory -> theory - val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory - val add_trrules_i: ast Syntax.trrule list -> theory -> theory - val del_trrules_i: ast Syntax.trrule list -> theory -> theory + val add_trrules: ast Syntax.trrule list -> theory -> theory + val del_trrules: ast Syntax.trrule list -> theory -> theory val new_group: theory -> theory val reset_group: theory -> theory val add_path: string -> theory -> theory @@ -497,14 +495,8 @@ (* translation rules *) -fun gen_trrules f args thy = thy |> map_syn (fn syn => - let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args - in f (ProofContext.init_global thy) syn rules syn end); - -val add_trrules = gen_trrules Syntax.update_trrules; -val del_trrules = gen_trrules Syntax.remove_trrules; -val add_trrules_i = map_syn o Syntax.update_trrules_i; -val del_trrules_i = map_syn o Syntax.remove_trrules_i; +val add_trrules = map_syn o Syntax.update_trrules; +val del_trrules = map_syn o Syntax.remove_trrules; (* naming *)