Dear Florian, Your previous example works because it is foo which is given to deps_of as argument, not the constant C. So one way for calling deps_of with C is to replace foo by C: export_code C in SML (or also by writing @{code C} in ML)
On the other hand, without knowing if the exportation of constants generated by datatypes has meanwhile become abandoned since Isabelle 2014, I can nevertheless suggest to catch earlier that situation and say in the error message to first do: definition "foo = C". For example, "export_code C in SML" terminates without detecting that C is a datatype constructor (because constants are all uniquely mapped to "Constant" in ~~/src/Tools/Code/code_symbol.ML), whereas "code_reflect Z functions C" terminates with an error encouraging us to look why in the source code: Error: Type constructor (a) has not been declared datatype 'a b = B of 'a c a and 'a c = C of 'a b At (line 1 of "generated code") Exception- Fail "Static Errors" raised (In my case, the error message is more long because I am originally working with a combination of datatypes written in more than 200 lines.) This is why I still tend to think this is probably just a minor typo or omission in the code generator that can be quickly fixed in the isabelle-dev mailing list, or at least taken as a semantical discussion on the generator. In my previous answer, apart from modifying deps_of there are actually several ways of fixing that, then of course any over-approximations on export_code look good to me, as long as it does not differ too much from code_reflect... (or @{code}, for instance I hope its semantical change was intentional during the introduction of @{computation}) Best, Frédéric Fri, 14 Apr 2017 10:09:38 +0200, Florian Haftmann : > 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 >>
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev