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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
