[isabelle-dev] Code generation: privacy of exported types in signatures

[Frederic Tuong (Dr)]

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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170415/4cb92ed9/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 801 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170415/4cb92ed9/attachment.sig>