--- 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
--- 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"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "syntax_types"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "syntax_consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
+ @{command_def "translations"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "no_translations"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def syntax_ast_stats} & : & \<open>attribute\<close> & default \<open>false\<close> \\
\end{tabular}
--- 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}
--- 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
--- 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
--- 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>\<open>translations\<close> "add syntax translation rules"
- (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations true));
+ Outer_Syntax.local_theory \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
+ (Scan.repeat1 trans_line >> Local_Theory.translations_cmd true);
val _ =
- Outer_Syntax.command \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
- (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations false));
+ Outer_Syntax.local_theory \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
+ (Scan.repeat1 trans_line >> Local_Theory.translations_cmd false);
in end\<close>
--- 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;
--- 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 *)