# HG changeset patch # User wenzelm # Date 1734209240 -3600 # Node ID d570d215e38009c00ee99d32f1567d8d6ec0e7a8 # Parent e656c5edc35223214cdf3540a14726e761c983b4 syntax translations now work in a local theory context; diff -r e656c5edc352 -r d570d215e380 NEWS --- a/NEWS Sat Dec 14 17:35:53 2024 +0100 +++ b/NEWS Sat Dec 14 21:47:20 2024 +0100 @@ -25,6 +25,9 @@ printing, concerning declaration scopes and highlighting of undeclared variables. +* Syntax translations now work in a local theory context, notably within +"bundle begin ... end". + * Syntax translations now support formal dependencies via commands 'syntax_types' or 'syntax_consts'. This is essentially an abstract specification of the effect of 'translations' (or translation functions diff -r e656c5edc352 -r d570d215e380 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat Dec 14 21:47:20 2024 +0100 @@ -1123,8 +1123,8 @@ @{command_def "no_syntax"} & : & \local_theory \ local_theory\ \\ @{command_def "syntax_types"} & : & \theory \ theory\ \\ @{command_def "syntax_consts"} & : & \theory \ theory\ \\ - @{command_def "translations"} & : & \theory \ theory\ \\ - @{command_def "no_translations"} & : & \theory \ theory\ \\ + @{command_def "translations"} & : & \local_theory \ local_theory\ \\ + @{command_def "no_translations"} & : & \local_theory \ local_theory\ \\ @{attribute_def syntax_ast_trace} & : & \attribute\ & default \false\ \\ @{attribute_def syntax_ast_stats} & : & \attribute\ & default \false\ \\ \end{tabular} diff -r e656c5edc352 -r d570d215e380 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Dec 14 21:47:20 2024 +0100 @@ -293,6 +293,7 @@ the polarity of certain declaration commands should be inverted, notably: \<^item> @{command syntax} versus @{command no_syntax} + \<^item> @{command translations} versus @{command no_translations} \<^item> @{command notation} versus @{command no_notation} \<^item> @{command type_notation} versus @{command no_type_notation} diff -r e656c5edc352 -r d570d215e380 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Pure/Isar/local_theory.ML Sat Dec 14 21:47:20 2024 +0100 @@ -67,6 +67,8 @@ local_theory -> local_theory val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> local_theory -> 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 val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory @@ -334,6 +336,21 @@ val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax; +(* translations *) + +fun gen_translations prep_trrule add raw_args lthy = + let + val args = map (prep_trrule lthy) raw_args; + val _ = Sign.check_translations lthy args; + in + declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} + (fn _ => Proof_Context.generic_translations add args) lthy + end; + +val translations = gen_translations (K I); +val translations_cmd = gen_translations Syntax.parse_trrule; + + (* notation *) local diff -r e656c5edc352 -r d570d215e380 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Dec 14 21:47:20 2024 +0100 @@ -167,6 +167,8 @@ Proof.context -> Proof.context val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) 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 val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism -> @@ -1218,6 +1220,18 @@ Context.mapping (Sign.syntax_global add mode args) (syntax add mode args); +(* translations *) + +fun translations add args ctxt = + let + val add' = Syntax.effective_polarity ctxt add; + val _ = Sign.check_translations ctxt args; + in ctxt |> map_syntax (Local_Syntax.translations ctxt add' args) end; + +fun generic_translations add args = + Context.mapping (Sign.translations_global add args) (translations add args); + + (* notation *) local diff -r e656c5edc352 -r d570d215e380 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Pure/Pure.thy Sat Dec 14 21:47:20 2024 +0100 @@ -430,12 +430,12 @@ >> (fn (left, (arr, right)) => arr (left, right)); val _ = - Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" - (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations true)); + Outer_Syntax.local_theory \<^command_keyword>\translations\ "add syntax translation rules" + (Scan.repeat1 trans_line >> Local_Theory.translations_cmd true); val _ = - Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" - (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations false)); + Outer_Syntax.local_theory \<^command_keyword>\no_translations\ "delete syntax translation rules" + (Scan.repeat1 trans_line >> Local_Theory.translations_cmd false); in end\ diff -r e656c5edc352 -r d570d215e380 src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Pure/Syntax/local_syntax.ML Sat Dec 14 21:47:20 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 translations: Proof.context -> bool -> Ast.ast Syntax.trrule list -> T -> T val set_mode: Syntax.mode -> T -> T val restore_mode: T -> T -> T val update_modesyntax: Proof.context -> bool -> Syntax.mode -> @@ -34,13 +35,15 @@ {thy_syntax: Syntax.syntax, local_syntax: Syntax.syntax, mode: Syntax.mode, - mixfixes: local_mixfix list}; + mixfixes: local_mixfix list, + translations: (bool * Ast.ast Syntax.trrule list) list}; -fun make_syntax (thy_syntax, local_syntax, mode, mixfixes) = - Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode, mixfixes = mixfixes}; +fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, translations) = + Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, mode = mode, + mixfixes = mixfixes, translations = translations}; -fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes}) = - make_syntax (f (thy_syntax, local_syntax, mode, mixfixes)); +fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, translations}) = + make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, translations)); fun is_consistent ctxt (Syntax {thy_syntax, ...}) = Syntax.eq_syntax (Sign.syntax_of (Proof_Context.theory_of ctxt), thy_syntax); @@ -50,7 +53,7 @@ (* build syntax *) -fun build_syntax ctxt mode mixfixes = +fun build_syntax ctxt mode mixfixes translations = let val thy = Proof_Context.theory_of ctxt; val thy_syntax = Sign.syntax_of thy; @@ -60,16 +63,17 @@ Syntax.update_const_gram ctxt add (Sign.logical_types thy) mode decls; val local_syntax = thy_syntax - |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); - in make_syntax (thy_syntax, local_syntax, mode, mixfixes) end; + |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))) + |> fold_rev (uncurry (Syntax.update_trrules ctxt)) translations; + in make_syntax (thy_syntax, local_syntax, mode, mixfixes, 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, ...}) = +fun rebuild ctxt (syntax as Syntax {mode, mixfixes, translations, ...}) = if is_consistent ctxt syntax then syntax - else build_syntax ctxt mode mixfixes; + else build_syntax ctxt mode mixfixes translations; (* mixfix declarations *) @@ -93,7 +97,7 @@ in -fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) = +fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, translations, ...})) = (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of [] => (NONE, syntax) | decls => @@ -109,7 +113,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'; + val syntax' = build_syntax ctxt mode mixfixes' translations; in (if idents = idents' then NONE else SOME idents', syntax') end); fun add_syntax ctxt = update_syntax ctxt true; @@ -117,10 +121,16 @@ end; +(* 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)); + + (* syntax mode *) -fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes) => - (thy_syntax, local_syntax, mode, mixfixes)); +fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, translations) => + (thy_syntax, local_syntax, mode, mixfixes, translations)); fun restore_mode (Syntax {mode, ...}) = set_mode mode; diff -r e656c5edc352 -r d570d215e380 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Pure/sign.ML Sat Dec 14 21:47:20 2024 +0100 @@ -102,6 +102,8 @@ (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_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 val get_scope: theory -> Binding.scope option val new_scope: theory -> Binding.scope * theory @@ -518,7 +520,36 @@ (* translation rules *) -fun translations_global add = update_syn_global (fn ctxt => Syntax.update_trrules ctxt add); +fun check_translations ctxt = + let + val thy = Proof_Context.theory_of ctxt; + + fun err msg = error ("Malformed syntax translations: " ^ msg); + + fun print_const c = + uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c); + + 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))); + in List.app (ignore o Syntax.map_trrule (tap check_ast)) end; + +fun translations ctxt add args thy = + (check_translations ctxt args; map_syn (Syntax.update_trrules ctxt add args) thy); + +fun translations_global add args thy = + let + val thy_ctxt = Proof_Context.init_global thy; + val add' = Syntax.effective_polarity thy_ctxt add; + in translations thy_ctxt add' args thy end; (* naming *)