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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Apr 14 10:09:38 CEST 2017


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: Foo.thy
Type: application/x-extension-thy
Size: 233 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170414/6b6d80e4/attachment-0002.bin>
-------------- 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/20170414/6b6d80e4/attachment.sig>


More information about the isabelle-dev mailing list