Re: [isabelle] Code Generator: Sealed Data

Hi René,

> First I thought to use the approach given in Library/Dlist.thy: a
> structure annotated with an invariant.

this is how you have to start anyway to deal with invariants.

Unfortunately, the code generator
> exports the constructor as part of signature. Hence, in outside code, I
> simply can write "Dlist [1,2,2,2,2]" -- and any code exported from
> Isabelle is convinced that the underlying list is distinct, while in
> fact it is not.

Currently it is indeed assumed that »client code« knows how to deal with
generated code.

As a workaround, you can do something like (e.g. in SML):

structure Generated_Code =
  <generated code>

signature FOO =
  <what is really needed for client code without abstract constructors>

structure Foo: FOO =
  open Generated_Code

Future Isabelle releases will minimize their exports.  In the more
remote future this could also be used as a vehicle to prevent export of
abstract constructors entirely.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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