Email Gateway (Aug 19 2022 at 13:00): Email Gateway (Aug 19 2022 at 13:00):From: René Neumann <rene.neumann@in.tum.de>
Hi,
for modelling an AST I got lots of datatypes together with their
constructors (about 100). As the types and the constructors have rather
generic names, I only want them to be accessed with a prefix. Normally I
would use hide_const and hide_type for this, but explicitly writing all
of the 100 constructors again seems cumbersome and error-prone.
Is there some generic mechanism for declaring them and NOT putting the
names into the global namespace?
A workaround I found is using datatype_new inside a locale, in the
following manner
locale ast
begin
datatype_new binOp = …
datatype_new expr = …
end
interpretation AST!: ast .
(* register them all again for code-generation *)
datatype_new_compat AST.binOP AST.expr …
But it still feels somewhat wrong for me. Especially throwing two
different datatype packages at it just for hiding names :)
Email Gateway (Aug 19 2022 at 13:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hello,
May a solution can be found somewhere in “implementation.pdf”, from the
documentation pan. I believe it's possible to modify a theory context
using an embedded SML function (embedded in the theory file), without a
need for modifying Isabelle internal (I'm looking at it, will be back if I
feel I've found anything useful in “implementation.pdf”).
Email Gateway (Aug 19 2022 at 13:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
May be looking at page 10 and later, “0.2 SML embedded into
Isabelle/Isar”, then at page 59 and later, “2.1 Types”.
Email Gateway (Aug 19 2022 at 13:01):From: Dmitriy Traytel <traytel@in.tum.de>
Hi René,
I guess this is about Isabelle2013-2.
I think there is nothing wrong about this setup.
The new (co)datatype package (which is still rapidly evolving) is
localized, while the old isn't. The command datatype_new_compat is a
cheap shortcut to backwards compatibility during this evolution period
(assuming your datatype is in the fragment of the old package).
Eventually, when the new package is as integrated as the old one, it
should be possible just to drop this command and its invocations.
Actually, in the development repository (e.g. 010eefa0a4f3), you should
not need datatype_new_compat for code generation (but there are other
useful features that it gives you, notably the size function for
automated termination proofs in "fun").
Hope that helps,
Dmitriy
Email Gateway (Aug 19 2022 at 13:01):From: René Neumann <rene.neumann@in.tum.de>
I came up with the following short snippet:
setup {*
let
fun hide_const (c,_) thy = Sign.hide_const false c thy;
fun hide_type t thy =
let
val t = Sign.intern_type thy t;
val thy = case Datatype.get_constrs thy t of
NONE => thy (* Error would be better *)
| SOME xs => fold hide_const xs thy
in
Sign.hide_type false t thy
end
fun hide_all ts thy =
fold hide_type ts thy
in
hide_all ["binOp", …]
end
*}
Probably specifying the list explicitly at the end can also scripted
away :).
smime.p7s
Email Gateway (Aug 19 2022 at 13:01):From: Makarius <makarius@sketis.net>
The most relevant section is 1.2.4 Name spaces, especially the "chemical
equation" about binding + naming.
Here is a quick example:
context
begin
local_setup {*
Local_Theory.map_naming (Name_Space.mandatory_path "foo.bar")
*}
definition "a = True"
definition "b = False"
end
Thus all name bindings that are applied in the context come out with the
extra prefix.
This avoids the need to "repair" unintended name space access via the
old-fashioned "hide" operations.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC