Re: [isabelle-dev] Code generation: privacy of exported types in signatures
Dear Frédéric, > 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) ok, now I can follow your observations. > [...] 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}) It has not been an intentional semantical change, but a clarification of the implementation as side benefit of the whole @{computation} story. You might try in the next Isabelle release (not scheduled yet) whether your issues still persist, or maybe check against a recent ongoing development revision. Hope this helps, Florian > > 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 >>> > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Code generation: privacy of exported types in signatures
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
Re: [isabelle-dev] Code generation: privacy of exported types in signatures
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