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 =
struct
  <generated code>
end

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

structure Foo: FOO =
struct
  open Generated_Code
end

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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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