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