# HG changeset patch # User wenzelm # Date 1734216525 -3600 # Node ID 7e1b66416b7fd23cf85afab73795da44ae4534f8 # Parent 4bad9c465eefa181708d9d6ee5f2ebd1bc9b4153 commands 'syntax_types' and 'syntax_consts' now work in a local theory context; diff -r 4bad9c465eef -r 7e1b66416b7f src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Dec 14 23:48:45 2024 +0100 @@ -1121,8 +1121,8 @@ @{command_def "nonterminal"} & : & \theory \ theory\ \\ @{command_def "syntax"} & : & \local_theory \ local_theory\ \\ @{command_def "no_syntax"} & : & \local_theory \ local_theory\ \\ - @{command_def "syntax_types"} & : & \theory \ theory\ \\ - @{command_def "syntax_consts"} & : & \theory \ theory\ \\ + @{command_def "syntax_types"} & : & \local_theory \ local_theory\ \\ + @{command_def "syntax_consts"} & : & \local_theory \ local_theory\ \\ @{command_def "translations"} & : & \local_theory \ local_theory\ \\ @{command_def "no_translations"} & : & \local_theory \ local_theory\ \\ @{attribute_def syntax_ast_trace} & : & \attribute\ & default \false\ \\ diff -r 4bad9c465eef -r 7e1b66416b7f src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Dec 14 23:48:45 2024 +0100 @@ -15,9 +15,9 @@ val print_ast_translation: Input.source -> theory -> theory val translations: bool -> (string * string) Syntax.trrule list -> theory -> theory val syntax_consts: ((string * Position.T) list * (xstring * Position.T) list) list -> - theory -> theory + local_theory -> local_theory val syntax_types: ((string * Position.T) list * (xstring * Position.T) list) list -> - theory -> theory + local_theory -> local_theory val oracle: bstring * Position.range -> Input.source -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition @@ -108,15 +108,13 @@ local -fun syntax_deps_cmd f args thy = +fun syntax_deps_cmd f args lthy = let - val ctxt = Proof_Context.init_global thy; - - val check_lhs = Proof_Context.check_syntax_const ctxt; + val check_lhs = Proof_Context.check_syntax_const lthy; fun check_rhs (b: xstring, pos: Position.T) = let - val (c: string, reports) = f ctxt (b, pos); - val _ = Context_Position.reports ctxt reports; + val (c: string, reports) = f lthy (b, pos); + val _ = Context_Position.reports lthy reports; in c end; fun check (raw_lhs, raw_rhs) = @@ -124,15 +122,15 @@ val lhs = map check_lhs raw_lhs; val rhs = map check_rhs raw_rhs; in map (fn l => (l, rhs)) lhs end; - in Sign.syntax_deps (maps check args) thy end; + in Local_Theory.syntax_deps (maps check args) lthy end; fun check_const ctxt (s, pos) = Proof_Context.check_const {proper = true, strict = false} ctxt (s, [pos]) - |>> (Term.dest_Const_name #> Lexicon.mark_const); + |>> (Term.dest_Const_name #> Lexicon.mark_const #> tap (Sign.check_syntax_dep ctxt)); fun check_type_name ctxt arg = Proof_Context.check_type_name {proper = true, strict = false} ctxt arg - |>> (Term.dest_Type_name #> Lexicon.mark_type); + |>> (Term.dest_Type_name #> Lexicon.mark_type #> tap (Sign.check_syntax_dep ctxt)); in diff -r 4bad9c465eef -r 7e1b66416b7f src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Pure/Isar/local_theory.ML Sat Dec 14 23:48:45 2024 +0100 @@ -67,6 +67,7 @@ local_theory -> local_theory val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> local_theory -> local_theory + val syntax_deps: (string * string list) list -> Proof.context -> local_theory val translations: bool -> Ast.ast Syntax.trrule list -> local_theory -> local_theory val translations_cmd: bool -> (string * string) Syntax.trrule list -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory @@ -335,6 +336,10 @@ val syntax = gen_syntax (K I); val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax; +fun syntax_deps args = + declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} + (fn _ => Proof_Context.generic_syntax_deps args); + (* translations *) diff -r 4bad9c465eef -r 7e1b66416b7f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Dec 14 23:48:45 2024 +0100 @@ -167,6 +167,7 @@ Proof.context -> Proof.context val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Context.generic -> Context.generic + val generic_syntax_deps: (string * string list) list -> Context.generic -> Context.generic val translations: bool -> Ast.ast Syntax.trrule list -> Proof.context -> Proof.context val generic_translations: bool -> Ast.ast Syntax.trrule list -> Context.generic -> Context.generic val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context @@ -1219,6 +1220,10 @@ fun generic_syntax add mode args = Context.mapping (Sign.syntax_global add mode args) (syntax add mode args); +fun generic_syntax_deps args = + Context.mapping (Sign.syntax_deps args) + (fn ctxt => map_syntax (Local_Syntax.syntax_deps ctxt args) ctxt); + (* translations *) diff -r 4bad9c465eef -r 7e1b66416b7f src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Pure/Pure.thy Sat Dec 14 23:48:45 2024 +0100 @@ -408,12 +408,12 @@ Parse.!!! (Scan.repeat1 Parse.name_position)); val _ = - Outer_Syntax.command \<^command_keyword>\syntax_consts\ "declare syntax const dependencies" - (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_consts)); + Outer_Syntax.local_theory \<^command_keyword>\syntax_consts\ "declare syntax const dependencies" + (syntax_consts >> Isar_Cmd.syntax_consts); val _ = - Outer_Syntax.command \<^command_keyword>\syntax_types\ "declare syntax const dependencies (type names)" - (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_types)); + Outer_Syntax.local_theory \<^command_keyword>\syntax_types\ "declare syntax const dependencies (type names)" + (syntax_consts >> Isar_Cmd.syntax_types); val trans_pat = Scan.optional diff -r 4bad9c465eef -r 7e1b66416b7f src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Pure/Syntax/local_syntax.ML Sat Dec 14 23:48:45 2024 +0100 @@ -14,6 +14,7 @@ datatype kind = Type | Const | Fixed val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list -> T -> {structs: string list, fixes: string list} option * T + val syntax_deps: Proof.context -> (string * string list) list -> T -> T val translations: Proof.context -> bool -> Ast.ast Syntax.trrule list -> T -> T val set_mode: Syntax.mode -> T -> T val restore_mode: T -> T -> T @@ -36,14 +37,15 @@ local_syntax: Syntax.syntax, mode: Syntax.mode, mixfixes: local_mixfix list, + consts: (string * string list) list, translations: (bool * Ast.ast Syntax.trrule list) list}; -fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, translations) = +fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, consts, translations) = Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode, - mixfixes = mixfixes, translations = translations}; + mixfixes = mixfixes, consts = consts, translations = translations}; -fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, translations}) = - make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, translations)); +fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, consts, translations}) = + make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, consts, translations)); fun is_consistent ctxt (Syntax {thy_syntax, ...}) = Syntax.eq_syntax (Sign.syntax_of (Proof_Context.theory_of ctxt), thy_syntax); @@ -53,7 +55,7 @@ (* build syntax *) -fun build_syntax ctxt mode mixfixes translations = +fun build_syntax ctxt mode mixfixes consts translations = let val thy = Proof_Context.theory_of ctxt; val thy_syntax = Sign.syntax_of thy; @@ -64,16 +66,17 @@ val local_syntax = thy_syntax |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))) + |> Syntax.update_consts ctxt consts |> fold_rev (uncurry (Syntax.update_trrules ctxt)) translations; - in make_syntax (thy_syntax, local_syntax, mode, mixfixes, translations) end; + in make_syntax (thy_syntax, local_syntax, mode, mixfixes, consts, translations) end; fun init thy = let val thy_syntax = Sign.syntax_of thy - in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, [], []) end; + in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, [], [], []) end; -fun rebuild ctxt (syntax as Syntax {mode, mixfixes, translations, ...}) = +fun rebuild ctxt (syntax as Syntax {mode, mixfixes, consts, translations, ...}) = if is_consistent ctxt syntax then syntax - else build_syntax ctxt mode mixfixes translations; + else build_syntax ctxt mode mixfixes consts translations; (* mixfix declarations *) @@ -97,7 +100,7 @@ in -fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, translations, ...})) = +fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, consts, translations, ...})) = (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of [] => (NONE, syntax) | decls => @@ -113,7 +116,7 @@ else subtract (op =) new_structs (#structs idents), fixes = fold (fn ({name = x, is_fixed = true}, _) => cons x | _ => I) mixfixes' []}; - val syntax' = build_syntax ctxt mode mixfixes' translations; + val syntax' = build_syntax ctxt mode mixfixes' consts translations; in (if idents = idents' then NONE else SOME idents', syntax') end); fun add_syntax ctxt = update_syntax ctxt true; @@ -123,14 +126,18 @@ (* translations *) -fun translations ctxt add args (Syntax {thy_syntax, local_syntax, mode, mixfixes, translations}) = - (Sign.check_translations ctxt args; build_syntax ctxt mode mixfixes ((add, args) :: translations)); +fun syntax_deps ctxt args (Syntax {mode, mixfixes, consts, translations, ...}) = + build_syntax ctxt mode mixfixes (args @ consts) translations; + +fun translations ctxt add args (Syntax {mode, mixfixes, consts, translations, ...}) = + (Sign.check_translations ctxt args; + build_syntax ctxt mode mixfixes consts ((add, args) :: translations)); (* syntax mode *) -fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, translations) => - (thy_syntax, local_syntax, mode, mixfixes, translations)); +fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, consts, translations) => + (thy_syntax, local_syntax, mode, mixfixes, consts, translations)); fun restore_mode (Syntax {mode, ...}) = set_mode mode; diff -r 4bad9c465eef -r 7e1b66416b7f src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Dec 14 22:26:27 2024 +0100 +++ b/src/Pure/sign.ML Sat Dec 14 23:48:45 2024 +0100 @@ -102,6 +102,7 @@ (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory + val check_syntax_dep: Proof.context -> string -> unit val check_translations: Proof.context -> Ast.ast Syntax.trrule list -> unit val translations: Proof.context -> bool -> Ast.ast Syntax.trrule list -> theory -> theory val translations_global: bool -> Ast.ast Syntax.trrule list -> theory -> theory @@ -520,26 +521,27 @@ (* translation rules *) -fun check_translations ctxt = +fun check_syntax_dep ctxt s = let val thy = Proof_Context.theory_of ctxt; - - fun err msg = error ("Malformed syntax translations: " ^ msg); + fun print_type c = uncurry Markup.markup (Name_Space.markup_extern ctxt (type_space thy) c); + fun print_const c = uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c); + in + s |> Lexicon.unmark + {case_class = K (), + case_type = fn c => + if declared_tyname thy c then () else error ("Not a global type: " ^ quote (print_type c)), + case_const = fn c => + if declared_const thy c then () else error ("Not a global const: " ^ quote (print_const c)), + case_fixed = fn x => error ("Bad local variable: " ^ quote x), + case_default = K ()} + end; - fun print_const c = - uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c); - +fun check_translations ctxt = + let fun check_ast (Ast.Appl asts) = List.app check_ast asts | check_ast (Ast.Variable _) = () - | check_ast (Ast.Constant s) = - (case try Lexicon.unmark_fixed s of - NONE => - (case try Lexicon.unmark_const s of - SOME c => - if declared_const thy c then () - else err ("non-global constant " ^ quote (print_const c)) - | NONE => ()) - | SOME x => err ("local variable " ^ Syntax.string_of_term ctxt (Syntax.free x))); + | check_ast (Ast.Constant s) = check_syntax_dep ctxt s; in List.app (ignore o Syntax.map_trrule (tap check_ast)) end; fun translations ctxt add args thy =