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
by this function:

    fun deps_of sym =
        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.


Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to