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

[Florian Haftmann]

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-dev at 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170417/97d1c77d/attachment.sig>