--- a/NEWS Thu Jan 02 08:37:52 2025 +0100
+++ b/NEWS Thu Jan 02 08:37:55 2025 +0100
@@ -222,6 +222,9 @@
*** HOL ***
+* Code generator: `code_reserved` now uses brackets for target languages,
+similar to `code_printing.
+
* Sledgehammer:
- Added instantiations of facts using the "of" attribute
(e.g. "assms(1)[of x]"), which can be activated using the
--- a/src/Doc/Codegen/Adaptation.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Thu Jan 02 08:37:55 2025 +0100
@@ -295,7 +295,7 @@
@{command_def "code_reserved"} command:
\<close>
-code_reserved %quote "\<SMLdummy>" bool true false andalso
+code_reserved %quotett ("\<SMLdummy>") bool true false andalso
text \<open>
\noindent Next, we try to map HOL pairs to SML pairs, using the
@@ -388,7 +388,7 @@
errno i = error ("Error number: " ++ show i)\<close>
-code_reserved %quotett Haskell Errno
+code_reserved %quotett (Haskell) Errno
text \<open>
\noindent Such named modules are then prepended to every
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Jan 02 08:37:55 2025 +0100
@@ -2314,7 +2314,7 @@
;
@@{command (HOL) code_deps} (const_expr+)
;
- @@{command (HOL) code_reserved} target (@{syntax string}+)
+ @@{command (HOL) code_reserved} ('(' target ')' (@{syntax string}+) + @'and')
;
symbol_const: @'constant' const
;
--- a/src/HOL/Code_Evaluation.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Evaluation.thy Thu Jan 02 08:37:55 2025 +0100
@@ -88,7 +88,8 @@
ML_file \<open>Tools/code_evaluation.ML\<close>
-code_reserved Eval Code_Evaluation
+code_reserved
+ (Eval) Code_Evaluation
ML_file \<open>~~/src/HOL/Tools/value_command.ML\<close>
@@ -128,7 +129,8 @@
(term_of (- i)))"
by (rule term_of_anything [THEN meta_eq_to_obj_eq])
-code_reserved Eval HOLogic
+code_reserved
+ (Eval) HOLogic
subsection \<open>Generic reification\<close>
--- a/src/HOL/Code_Numeral.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Jan 02 08:37:55 2025 +0100
@@ -780,7 +780,8 @@
subsection \<open>Serializer setup for target language integers\<close>
-code_reserved Eval int Integer abs
+code_reserved
+ (Eval) int Integer abs
code_printing
type_constructor integer \<rightharpoonup>
--- a/src/HOL/Codegenerator_Test/Candidates.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Thu Jan 02 08:37:55 2025 +0100
@@ -42,7 +42,7 @@
text \<open>Avoid popular infix.\<close>
-code_reserved SML upto
+code_reserved (SML) upto
text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close>
--- a/src/HOL/HOL.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/HOL.thy Thu Jan 02 08:37:55 2025 +0100
@@ -2074,14 +2074,10 @@
| constant False \<rightharpoonup>
(SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
-code_reserved SML
- bool true false
-
-code_reserved OCaml
- bool
-
-code_reserved Scala
- Boolean
+code_reserved
+ (SML) bool true false
+ and (OCaml) bool
+ and (Scala) Boolean
code_printing
constant Not \<rightharpoonup>
@@ -2101,11 +2097,9 @@
and (Haskell) "!(if (_)/ then (_)/ else (_))"
and (Scala) "!((_) match {/ case true => (_)/ case false => (_)/ })"
-code_reserved SML
- not
-
-code_reserved OCaml
- not
+code_reserved
+ (SML) not
+ and (OCaml) not
code_identifier
code_module Pure \<rightharpoonup>
--- a/src/HOL/Imperative_HOL/Array.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/Array.thy Thu Jan 02 08:37:55 2025 +0100
@@ -451,7 +451,7 @@
code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ IntInf.toInt _,/ (_)))"
code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
-code_reserved SML Array
+code_reserved (SML) Array
text \<open>OCaml\<close>
@@ -467,7 +467,7 @@
code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Z.to'_int/ _)/ _)"
code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
-code_reserved OCaml Array
+code_reserved (OCaml) Array
text \<open>Haskell\<close>
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jan 02 08:37:55 2025 +0100
@@ -565,7 +565,7 @@
writeArray :: STArray s a -> Integer -> a -> ST s ()
writeArray = Data.Array.ST.writeArray\<close>
-code_reserved Haskell Heap
+code_reserved (Haskell) Heap
text \<open>Monad\<close>
@@ -620,7 +620,7 @@
\<close>
-code_reserved Scala Heap Ref Array
+code_reserved (Scala) Heap Ref Array
code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
--- a/src/HOL/Imperative_HOL/Ref.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Thu Jan 02 08:37:55 2025 +0100
@@ -284,7 +284,7 @@
code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
-code_reserved Eval Unsynchronized
+code_reserved (Eval) Unsynchronized
text \<open>OCaml\<close>
@@ -296,7 +296,7 @@
code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
-code_reserved OCaml ref
+code_reserved (OCaml) ref
text \<open>Haskell\<close>
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jan 02 08:37:55 2025 +0100
@@ -655,7 +655,7 @@
return a
}"
-code_reserved SML upto
+code_reserved (SML) upto
definition "example = do {
a \<leftarrow> Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jan 02 08:37:55 2025 +0100
@@ -956,7 +956,7 @@
return zs
})"
-code_reserved SML upto
+code_reserved (SML) upto
ML_val \<open>@{code test_1} ()\<close>
ML_val \<open>@{code test_2} ()\<close>
--- a/src/HOL/Library/Code_Lazy.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Code_Lazy.thy Thu Jan 02 08:37:55 2025 +0100
@@ -116,7 +116,7 @@
| constant force \<rightharpoonup> (SML) "Lazy.force"
| constant termify_lazy \<rightharpoonup> (SML) "Lazy.termify'_lazy"
-code_reserved SML Lazy
+code_reserved (SML) Lazy
code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe
implementation of lazy from \<^file>\<open>~~/src/Pure/Concurrent/lazy.ML\<close>\<close>
@@ -137,7 +137,7 @@
end;\<close> for constant termify_lazy
| constant termify_lazy \<rightharpoonup> (Eval) "Termify'_Lazy.termify'_lazy"
-code_reserved Eval Termify_Lazy
+code_reserved (Eval) Termify_Lazy
code_printing
type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
@@ -161,7 +161,7 @@
end;;\<close> for constant termify_lazy
| constant termify_lazy \<rightharpoonup> (OCaml) "Termify'_Lazy.termify'_lazy"
-code_reserved OCaml Lazy Termify_Lazy
+code_reserved (OCaml) Lazy Termify_Lazy
code_printing
@@ -175,7 +175,7 @@
| constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
| constant force \<rightharpoonup> (Haskell) "Lazy.force"
-code_reserved Haskell Lazy
+code_reserved (Haskell) Lazy
code_printing
code_module Lazy \<rightharpoonup> (Scala)
@@ -220,7 +220,7 @@
| constant force \<rightharpoonup> (Scala) "Lazy.force"
| constant termify_lazy \<rightharpoonup> (Scala) "Lazy.termify'_lazy"
-code_reserved Scala Lazy
+code_reserved (Scala) Lazy
text \<open>Make evaluation with the simplifier respect \<^term>\<open>delay\<close>s.\<close>
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Jan 02 08:37:55 2025 +0100
@@ -82,7 +82,7 @@
arccos
arctan]]
-code_reserved SML Real
+code_reserved (SML) Real
code_printing
type_constructor real \<rightharpoonup>
--- a/src/HOL/Library/Debug.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Debug.thy Thu Jan 02 08:37:55 2025 +0100
@@ -39,7 +39,6 @@
| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close>
| constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
-code_reserved Eval Output Timing
+code_reserved (Eval) Output Timing
end
-
--- a/src/HOL/Library/IArray.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/IArray.thy Thu Jan 02 08:37:55 2025 +0100
@@ -177,7 +177,7 @@
lists first. Arrays could be converted back into lists for printing if they
were wrapped up in an additional constructor.\<close>
-code_reserved SML Vector
+code_reserved (SML) Vector
code_printing
type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
@@ -222,7 +222,7 @@
}\<close> for type_constructor iarray constant IArray IArray.tabulate IArray.sub' IArray.length'
-code_reserved Haskell IArray_Impl
+code_reserved (Haskell) IArray_Impl
code_printing
type_constructor iarray \<rightharpoonup> (Haskell) "IArray.IArray _"
--- a/src/HOL/Library/Parallel.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Library/Parallel.thy Thu Jan 02 08:37:55 2025 +0100
@@ -23,7 +23,7 @@
| constant fork \<rightharpoonup> (Eval) "Future.fork"
| constant join \<rightharpoonup> (Eval) "Future.join"
-code_reserved Eval Future future
+code_reserved (Eval) Future future
subsection \<open>Parallel lists\<close>
@@ -50,7 +50,7 @@
| constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
| constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
-code_reserved Eval Par_List
+code_reserved (Eval) Par_List
hide_const (open) fork join map exists forall
--- a/src/HOL/Limited_Sequence.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Limited_Sequence.thy Thu Jan 02 08:37:55 2025 +0100
@@ -200,8 +200,8 @@
end;
\<close>
-code_reserved Eval Limited_Sequence
-
+code_reserved
+ (Eval) Limited_Sequence
hide_const (open) yield empty single eval map_seq bind union if_seq not_seq map
pos_empty pos_single pos_bind pos_decr_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
@@ -213,4 +213,3 @@
neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
end
-
--- a/src/HOL/List.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/List.thy Thu Jan 02 08:37:55 2025 +0100
@@ -8089,11 +8089,9 @@
setup \<open>fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]\<close>
-code_reserved SML
- list
-
-code_reserved OCaml
- list
+code_reserved
+ (SML) list
+ and (OCaml) list
subsubsection \<open>Use convenient predefined operations\<close>
--- a/src/HOL/Option.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Option.thy Thu Jan 02 08:37:55 2025 +0100
@@ -373,13 +373,9 @@
| constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
(Haskell) infix 4 "=="
-code_reserved SML
- option NONE SOME
-
-code_reserved OCaml
- option None Some
-
-code_reserved Scala
- Option None Some
+code_reserved
+ (SML) option NONE SOME
+ and (OCaml) option None Some
+ and (Scala) Option None Some
end
--- a/src/HOL/Product_Type.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Product_Type.thy Thu Jan 02 08:37:55 2025 +0100
@@ -195,14 +195,10 @@
| constant "HOL.equal :: unit \<Rightarrow> unit \<Rightarrow> bool" \<rightharpoonup>
(Haskell) infix 4 "=="
-code_reserved SML
- unit
-
-code_reserved OCaml
- unit
-
-code_reserved Scala
- Unit
+code_reserved
+ (SML) unit
+ and (OCaml) unit
+ and (Scala) Unit
subsection \<open>The product type\<close>
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jan 02 08:37:55 2025 +0100
@@ -22,7 +22,8 @@
| type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
-code_reserved Haskell_Quickcheck Typerep
+code_reserved
+ (Haskell_Quickcheck) Typerep
code_printing
type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
--- a/src/HOL/Quickcheck_Random.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Quickcheck_Random.thy Thu Jan 02 08:37:55 2025 +0100
@@ -17,7 +17,8 @@
code_printing
constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
-code_reserved Quickcheck Match
+code_reserved
+ (Quickcheck) Match
subsection \<open>The \<open>random\<close> class\<close>
@@ -271,7 +272,8 @@
for this reason we use a distinguished target \<open>Quickcheck\<close>
not spoiling the regular trusted code generation\<close>
-code_reserved Quickcheck Random_Generators
+code_reserved
+ (Quickcheck) Random_Generators
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
--- a/src/HOL/String.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/String.thy Thu Jan 02 08:37:55 2025 +0100
@@ -721,10 +721,11 @@
end
-code_reserved SML string String Char Str_Literal
-code_reserved OCaml string String Char Str_Literal
-code_reserved Haskell Prelude
-code_reserved Scala string
+code_reserved
+ (SML) string String Char Str_Literal
+ and (OCaml) string String Char Str_Literal
+ and (Haskell) Prelude
+ and (Scala) string
code_identifier
code_module String \<rightharpoonup>
--- a/src/HOL/Typerep.thy Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Typerep.thy Thu Jan 02 08:37:55 2025 +0100
@@ -90,7 +90,8 @@
type_constructor typerep \<rightharpoonup> (Eval) "Term.typ"
| constant Typerep \<rightharpoonup> (Eval) "Term.Type/ (_, _)"
-code_reserved Eval Term
+code_reserved
+ (Eval) Term
hide_const (open) typerep Typerep
--- a/src/Tools/Code/code_target.ML Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Tools/Code/code_target.ML Thu Jan 02 08:37:55 2025 +0100
@@ -739,10 +739,9 @@
in
val _ =
- Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close>
- "declare words as reserved for target language"
- (Parse.name -- Scan.repeat1 Parse.name
- >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
+ Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close> "declare words as reserved for target language"
+ (Parse.and_list1 (\<^keyword>\<open>(\<close> |-- (Parse.name --| \<^keyword>\<open>)\<close> -- Scan.repeat1 Parse.name))
+ >> (Toplevel.theory o fold (fn (target, reserveds) => fold (add_reserved target) reserveds)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>code_identifier\<close> "declare mandatory names for code symbols"