[isabelle] Hide all constructors of a datatype automatically



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 :)

- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.