Re: [isabelle] Hide all constructors of a datatype automatically



Am 14.12.2013 12:50, schrieb René Neumann:
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 :)
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




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