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
