[isabelle-dev] Code generation: privacy of exported types in signatures

[Frederic Tuong (Dr)]

Dear all,

The SML generated code of the following snippet is not well typed
anymore since Isabelle 2014:

datatype 'a A = aaa
datatype 'a B = bbb "'a C A"
     and 'a C = ccc "'a B"

This is because when computing types to be marked as not private (during
the generation of the signature of A, B and C), A has not been assigned
as an "Opaque" type, where the constructor Opaque is defined in
~~/src/Tools/Code/code_namespace.ML .

One solution is to replace the function deps_of defined in line 94 of
http://isabelle.in.tum.de/repos/isabelle/file/7dd1971b39c1/src/Tools/Code/code_namespace.ML
by this function:

    fun deps_of sym =
      let
        val succs1 = Code_Symbol.Graph.Keys.dest o
Code_Symbol.Graph.imm_succs gr;
        fun succs2 x = Code_Symbol.Graph.all_succs gr [x];
        val deps1 = succs1 sym;
        val deps2 = [] |> fold (union (op =)) (map succs2 deps1) |>
subtract (op =) deps1
      in (deps1, deps2) end;

In particular, if sym = ccc, instead of having deps1 = [C] and deps2 =
[B], we now have deps1 = [C] and deps2 = [A, B].


As remark, this problem does not happen when types are by default set to
be publicly exported in signatures. For instance:
- The semantics of @{code ...} has slightly changed since the support of
@{computation}, so the generation works now correctly in recent versions
of Isabelle.
- Whereas code generated by export_code may fail, we can still add the
option "open" for it to skip privacy in signatures.

Best,
Frédéric

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 801 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170409/6706b8bc/attachment.asc>