On 09/19/2011 01:56 PM, René Thiemann wrote:
Dear all,
There are still some improvements to the Haskell serializer and the code
generator I would like to get into the release.
After some discussions with Florian, the remaining changesets are about ready
and final, so I can probably commit them till this Wednesday.
Afterwards, the code generator is probably best checked against the two largest
executable formalisations (JinjaThreads and CeTA) -- I will try to get the
developers to re-run these with a current repository version or the first
pre-release version.
When reading this post (and since we will port to the new distribution in any
way), I started to adapt our library to the upcoming version where I used the
bundle http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Sep-2011/download.html
After some first adaptations I got stuck when at the first place where we use
partial_function. It seems that the partial_function package is broken if
polymorphic types are used. (which was not the case in Isabelle2011)
partial_function(option) foo :: "nat list \<Rightarrow> unit option" where "foo x =
foo x"
works, but
partial_function(option) foo :: "'a list \<Rightarrow> unit option" where "foo x =
foo x"
yields the following error message.
*** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type conflict
*** ?F :: (?'a2 list \<Rightarrow> unit option) \<Rightarrow> ?'a2 list
\<Rightarrow> unit option
*** \<lambda>foo. foo :: ('a list \<Rightarrow> unit option) \<Rightarrow> 'a
list \<Rightarrow> unit option
*** At command "partial_function" (line 216 of
"/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy")
or if I output sorts
*** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type conflict
*** ?F\<Colon>(?'a2\<Colon>type list \<Rightarrow> unit option) \<Rightarrow> ?'a2\<Colon>type list
\<Rightarrow> unit option :: (?'a2\<Colon>type list \<Rightarrow> unit option) \<Rightarrow> ?'a2\<Colon>type
list \<Rightarrow> unit option
*** \<lambda>foo\<Colon>'a\<Colon>type list \<Rightarrow> unit option. foo :: ('a\<Colon>type list
\<Rightarrow> unit option) \<Rightarrow> 'a\<Colon>type list \<Rightarrow> unit option
*** At command "partial_function" (line 216 of
"/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy")
I think this is a triviality since it looks to me that one just has to replace
?a2 by 'a,
but I do not know where to fix it.
After that, I'm happy to test any further version, also repository snapshots.
Alex seems to have fixed this issue with changeset 8b74cfea913a -- so,
if you can get hold on any version >= 8b74cfea913a, you can report if
there are further unresolved issues.
The mentioned changes of the code generator are also already in the
repository.
Lukas
Cheers,
René
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
