Re: [isabelle-dev] Problem with code generation for non-executable types
Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
> Ho Johannes.
>
> > > > Then the dictionary construction for type constructors
> > > > does
> > > > not
> > > > work in ML! The type signature would be the following:
> > > >
> > > >val test_prod : ('a * 'b) filter
> > > >
> > > > Which apparently is not allow in ML.
> > > This is the famous value restriction (which I also regularly run
> > > into). The standard
> > > solution is to add a unit closure, because functions may be
> > > polymorphic in ML.
>
> Nothing to add about that.
>
> In the examples there is also the problem that constructing a
> dictionary
> provokes an exception already. Here the general solution is to hide
> the
> problematic terms beneath an abstraction beneath a constructor.
>
> Applying that to your examples, I had a look at the sources and came
> to
> the conclusion that it is a bad idea have Abs_filter and Rep_filter
> in
> generated code at all.
>
> For the simple examples, it is much better to use »principal« as a
> formal constructor, which maps nicely to sets and provides some
> executability for a considerable class of filters.
>
> I did not have an idea in which algebraic framework »uniformity«
> could
> fit. Hence I provided a constructor which is a variant of identity
> and
> used that, which makes also the examples involving uniformity
> compileable (but of course not evaluable).
>
> Maybe you have an idea how this could be improved.
Well filters are mostly non-computable. Actually I would prefer to tell
the code-generator to not generate code for topologies and uniform
spaces at all, as these type classes are carry only non-computable
data.
But of course your implementation looks cleaner, so I changed in
Isabelle df65f5c27c15.
- Johannes
> Cheers,
> Florian
>
> >
> > Ah thanks! This explains it.
> >
> > Unfortunately, in my case the type is fixed in HOL to:
> >
> > uniformity :: ('a * 'a) filter (where 'a :: uniform_space)
> >
> > And I do not want to change the type signature for code generation.
> > So
> > I will stick to Solution 3.
> >
> > - Johannes
> >
> >
> > > > 2. If your type class contains non-computable data, i.e.
> > > >
> > > >instantiation bool :: test_class
> > > >begin
> > > >
> > > >definition "test = if P = NP then top else bot"
> > > >
> > > >instance proof qed
> > > >end
> > > >
> > > > You get a non-terminating program at the time point when
> > > > the
> > > > dictionary for bool :: test_class is constructed. When the
> > > > code equation is hidden with [code del] one gets a
> > > > exception!
> > > >
> > > > 3. Our current solution is to introduce code_datatype
> > > > Abs_filter
> > > > Rep_filter [code del] and define for each uniformity:
> > > >
> > > >uniformity = Abs_filter (%P. Code.abort (STR''FAILED'')
> > > > (Rep_filter test P))
> > > >
> > > > @Florian: is the an alternative solution?
> > > >
> > > >
> > > > - Johannes
> > > >
> > > > PS: Here is a short, concrete example:
> > > >
> > > > theory Scratch
> > > >imports Complex_Main
> > > > begin
> > > >
> > > > class test_class =
> > > >fixes test :: "'a filter"
> > > >
> > > > instantiation prod :: (test_class, test_class) test_class
> > > > begin
> > > >
> > > > definition [code del]: "test = (test ×⇩F test :: ('a × 'b)
> > > > filter)"
> > > >
> > > > instance proof qed
> > > > end
> > > >
> > > > instantiation unit :: test_class
> > > > begin
> > > >
> > > > definition [code del]:
> > > >"(test :: unit filter) = bot"
> > > >
> > > > instance proof qed
> > > > end
> > > >
> > > > definition "test2 (x::'a::test_class) = (Suc 0)"
> > > > definition "test3 = test2 ((), ())"
> > > >
> > > > value [code] "test3"
> > > >
> > > > section ‹Solution›
> > > >
> > > > code_datatype Abs_filter
> > > > declare [[code abort: Rep_filter]]
> > > >
> > > > lemma test_Abort: "test = Abs_filter (λP. Code.abort (STR
> > > > ''test'')
> > > > (λx. Rep_filter test P))"
> > > >unfolding Code.abort_def Rep_filter_inverse ..
> > > >
> > > > declare test_Abort[where 'a="'a::test_class * 'b ::
> > > > test_class",
> > > > code]
> > > > declare test_Abort[where 'a=unit, code]
> > > >
> > > > end
> > > >
> > > >
> > > >
> > > >
> > > >
> > > >
> > > > Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:
> > > > > Hi,
> > > > >
> > > > > I want to introduce uniform spaces in HOL, for this I need to
> > > > > introduce
> > > > > a type class of the form (see the attached bundle):
> > > > >
> > > > >class uniformity =
> > > > > fixes uniformity :: "('a × 'a) filter"
> > > > >
> > > > > Note that uniformity is a filter and not a function.
> > > > >
> > > > > which sits between topological spaces and metric spaces, i.e.
> > > > > every
> > > > > metric type is also in the following type classes:
> > > > >
> > > > >class open_uniformity =
[isabelle-dev] Isabelle2016-RC0: potential changes
Dear all, there are some changes I would like to add for the upcoming release. It would be nice, if someone can integrate them: - improved code equations for binomial coefficients and certain divmod-algorithms. (cf. http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html) - change type in definition and lemmas about pderiv from real to arbitrary fields, or even more general, cf. lines starting with (* TODO: inform Isabelle developers *) in http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html - change type of divides_degree from complex to 'a :: idom, cf beginning of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html Moreover, everything of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_* http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_* can freely be moved from the AFP into the distribution, where I ask the developers to judge which parts belong in the distribution and which are too specific, etc. With best regards, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
I already moved a few small lemmas. I also defined the notion of an algebraic number; as soon as your AFP entry works with the development version of Isabelle again (is that already the case?), I will prove equivalence of my definition in Poly_Deriv.thy to your definition in Algebraic_Numbers and adapt the AFP entry accordingly. (I needed this for Liouville_Numbers) As for the binomial numbers: that looks a bit suboptimal to me. I would have expected something like "listprod [k+1..n] div fact (n - k)" plus an additional check if "2*k >= n", reducing "n choose k" to "n choose (n - k)" if appropriate. (Not sure what code generation makes of "listprod [k+1..n]", a code_unfold rule to compute this efficiently with an accumulator and without constructing the list explicitly might be required. Same for "fact".) Cheers, Manuel On 11/01/16 09:57, Thiemann, Rene wrote: Dear all, there are some changes I would like to add for the upcoming release. It would be nice, if someone can integrate them: - improved code equations for binomial coefficients and certain divmod-algorithms. (cf. http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improved_Code_Equations.html) - change type in definition and lemmas about pderiv from real to arbitrary fields, or even more general, cf. lines starting with (* TODO: inform Isabelle developers *) in http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Square_Free_Factorization.html - change type of divides_degree from complex to 'a :: idom, cf beginning of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_Polynomial.html Moreover, everything of http://afp.sourceforge.net/browser_info/devel/AFP/Jordan_Normal_Form/Missing_* http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Missing_* can freely be moved from the AFP into the distribution, where I ask the developers to judge which parts belong in the distribution and which are too specific, etc. With best regards, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
algebraic number.
Oh, yes, you're right. It's in
https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
.
Its definitely not optimal, and you’re right that one can improve it
by using an inline-version of listprod [k+1..n], but even the version
that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is
by far better than the current setup, since that just uses the
recursive direct definition of binomial. (I noticed this since I got
timeouts in my experiments with algebraic numbers and one of the
culprits was binomial!)
I suggest this:
function fold_atLeastAtMost_nat where
[simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
(if a > b then acc else fold_atLeastAtMost_nat f (a+1)
b (f a acc))"
by pat_completeness auto
termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto
lemma fold_atLeastAtMost_nat:
assumes "comp_fun_commute f"
shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
using assms
proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
case (1 f a b acc)
interpret comp_fun_commute f by fact
show ?case
proof (cases "a > b")
case True
thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
next
case False
with 1 show ?thesis
by (subst fold_atLeastAtMost_nat.simps)
(auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
qed
qed
lemma setprod_atLeastAtMost_code:
"setprod f {a..b} = fold_atLeastAtMost_nat (λa acc. f a * acc) a b 1"
proof -
have "comp_fun_commute (λa. op * (f a))"
by unfold_locales (auto simp: o_def mult_ac)
thus ?thesis
by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
qed
lemma fact_altdef': "fact n = of_nat (∏{1..n})"
by (induction n)
(simp_all add: setprod_nat_ivl_Suc' of_nat_mult [symmetric]
One_nat_def [symmetric]
del: of_nat_Suc of_nat_add of_nat_mult One_nat_def)
lemma fact_code [code]:
"fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a ::
semiring_char_0)"
proof -
have "fact n = (of_nat (∏{1..n}) :: 'a)" by (simp add: fact_altdef')
also have "∏{1..n} = ∏{2..n}"
by (intro setprod.mono_neutral_right) auto
also have "… = fold_atLeastAtMost_nat (op *) 2 n 1"
by (simp add: setprod_atLeastAtMost_code)
finally show ?thesis .
qed
lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
proof -
{
assume "k ≤ n"
hence "{1..n} = {1..n-k} ∪ {n-k+1..n}" by auto
hence "(fact n :: nat) = fact (n-k) * ∏{n-k+1..n}"
by (simp add: setprod.union_disjoint fact_altdef_nat)
}
thus ?thesis by (auto simp: binomial_altdef_nat mult_ac
setprod_atLeastAtMost_code)
qed
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
Hi Manuel, > I already moved a few small lemmas. Thanks. > I also defined the notion of an algebraic number; as soon as your AFP entry > works with the development version of Isabelle again (is that already the > case?), Yes, it should work. (At least, on Friday afternoon, it worked) > I will prove equivalence of my definition in Poly_Deriv.thy to your > definition in Algebraic_Numbers and adapt the AFP entry accordingly. I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of algebraic number. > As for the binomial numbers: that looks a bit suboptimal to me. > I would have expected something like "listprod [k+1..n] div fact (n - k)" > plus an additional check if "2*k >= n", reducing "n choose k" to "n choose (n > - k)" if appropriate. > (Not sure what code generation makes of "listprod [k+1..n]", a code_unfold > rule to compute this efficiently with an accumulator and without constructing > the list explicitly might be required. Same for "fact“.) Its definitely not optimal, and you’re right that one can improve it by using an inline-version of listprod [k+1..n], but even the version that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is by far better than the current setup, since that just uses the recursive direct definition of binomial. (I noticed this since I got timeouts in my experiments with algebraic numbers and one of the culprits was binomial!) Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of >> algebraic number. > Oh, yes, you're right. It's in > https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy > . Ah, I see. Indeed: definitely equivalent. > >> Its definitely not optimal, and you’re right that one can improve it by >> using an inline-version of listprod [k+1..n], but even the version that is >> mentioned in Algebraic_Numbers/Improved_Code_Equations.html is by far better >> than the current setup, since that just uses the recursive direct definition >> of binomial. (I noticed this since I got timeouts in my experiments with >> algebraic numbers and one of the culprits was binomial!) > > I suggest this: > > > function fold_atLeastAtMost_nat where > [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = > (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a > acc))" > by pat_completeness auto > termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto > ... Looks good from my viewpoint. Best, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL-Codegenerator_Test error
I have finally installed my great mass of new material, but when I try to test it, it fails as shown below. I can’t imagine what I could have done to trigger such an error. Nearly all of my changes are confined to Multivariate_Analysis. Does anybody have an idea what could be going on here? Larry Running HOL-Codegenerator_Test ... HOL-Codegenerator_Test FAILED (see also /Users/lp15/isabelle/Repos/heaps/polyml-5.6_x86-darwin/log/HOL-Codegenerator_Test) ^ ROOT.scala:17271: error: ambiguous implicit values: both method semiring_char_0_nat in object Generated_Code of type => Generated_Code.semiring_char_0[Generated_Code.nat] and method semiring_div_nat in object Generated_Code of type => Generated_Code.semiring_div[Generated_Code.nat] match expected type Generated_Code.power[Generated_Code.nat] power[nat](cb, ca) else zero_nata()) ^ 10 errors found ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2016-RC0: potential changes
I added the efficient code equations for fact and binomial, and similar ones for pochhammer and gbinomial. I also adapted everything from Square_Free_Factorization and Missing_Polynomial that seemed to be of general interest to me (especially the generalisation of the type of pderiv). I also noticed the ring_gcd instance for polynomials. Finalising the changes to the GCD class hierarchy and updating the AFP entries that rely on half-finished versions of this change (such as Echelon_Form) is something that I should probably take care of soon, but definitely not before the 2016 release – hopefully before the 2017 one. Manuel ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Codegenerator_Test error
It looks like I'm the one who broke it. It does not work after my commit 3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately before. I have no idea what causes this problem. Maybe one of our resident code generator experts could comment on it? I'll try to find out which code equation exactly causes the problem tomorrow. If all else fails, I'll just comment out changes until it works again and leave this matter to be re-examined after the release. Cheers, Manuel On 11/01/16 18:16, Lawrence Paulson wrote: I have finally installed my great mass of new material, but when I try to test it, it fails as shown below. I can’t imagine what I could have done to trigger such an error. Nearly all of my changes are confined to Multivariate_Analysis. Does anybody have an idea what could be going on here? Larry Running HOL-Codegenerator_Test ... HOL-Codegenerator_Test FAILED (see also /Users/lp15/isabelle/Repos/heaps/polyml-5.6_x86-darwin/log/HOL-Codegenerator_Test) ^ ROOT.scala:17271: error: ambiguous implicit values: both method semiring_char_0_nat in object Generated_Code of type => Generated_Code.semiring_char_0[Generated_Code.nat] and method semiring_div_nat in object Generated_Code of type => Generated_Code.semiring_div[Generated_Code.nat] match expected type Generated_Code.power[Generated_Code.nat] power[nat](cb, ca) else zero_nata()) ^ 10 errors found ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Codegenerator_Test error
On Mon, 11 Jan 2016, Manuel Eberl wrote: It looks like I'm the one who broke it. It does not work after my commit 3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately before. Just a reminder of the normal routine: push to the Isabelle repository always requires a full "isabelle build -a" -- there is no way around it. It would be also nice to have a continously working AFP, as we are approaching the release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
