Dear Frédéric, I cannot follow reproduce observation; using the attached theory in Isabelle2016-1, I get
> structure Foo : sig > type 'a b > type 'a c > val foo : 'a b -> 'a b > end = struct > > datatype 'a a = A; > > datatype 'a b = B of 'a c a > and 'a c = C of 'a b; > > fun foo x = x; > > end; (*struct Foo*) which is almost perfectly fine, apart from the superfluous 'a c export. How does your theory and export_code statement exactly look like? Two points to note anyway: * This question would belong to the user (published release) rather than the development (ongoing changes to a central code repository) mailing list. * The implementation of code exports is an over-approximation. This is a known issue but not very likely to be addressed in the near future. Cheers, Florian Am 09.04.2017 um 08:04 schrieb 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 > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Foo.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev