<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body smarttemplateinserted="true" bgcolor="#FFFFFF" text="#000000">
<div id="smartTemplate4-template">Dear Florian,<br>
<br>
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:<br>
export_code C in SML<br>
(or also by writing @{code C} in ML)<br>
<br>
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:<br>
<br>
Error: Type constructor (a) has not been declared<br>
datatype 'a b = B of 'a c a and 'a c = C of 'a b<br>
At (line 1 of "generated code")<br>
Exception- Fail "Static Errors" raised<br>
<br>
(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.)<br>
<br>
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})<br>
<br>
Best,<br>
Frédéric<br>
<br>
<br>
<p>Fri, 14 Apr 2017 10:09:38 +0200, Florian Haftmann : </p>
</div>
<br>
<blockquote
cite="mid:4094dc92-eb83-16fa-c056-2f68eef2a2f2@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">Dear Frédéric,
I cannot follow reproduce observation; using the attached theory in
Isabelle2016-1, I get
</pre>
<blockquote type="cite">
<pre wrap="">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*)
</pre>
</blockquote>
<pre wrap="">
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):
</pre>
<blockquote type="cite">
<pre wrap="">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
<a class="moz-txt-link-freetext" href="http://isabelle.in.tum.de/repos/isabelle/file/7dd1971b39c1/src/Tools/Code/code_namespace.ML">http://isabelle.in.tum.de/repos/isabelle/file/7dd1971b39c1/src/Tools/Code/code_namespace.ML</a>
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
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<pre wrap="">
</pre>
</blockquote>
<br>
</body>
</html>