[isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
hoelzl at in.tum.de
Thu Jan 14 17:38:23 CET 2016
AFAIK, it is the first time we have such a situation. We have two cases
I'm aware of: "open" in topological_space and "uniformity" in
uniform_space. Up to now we could just remove all code equations from
open as it is a predicate and doesn't produce any problem with the
dictionary construction.
Your suggestion would be great, to completely disable code generation
for "open" and "uniformity". It would avoid a lot of [code del]
annotations at class instantiations, and some strange constructions for
filter ;-)
- Johannes
Am Donnerstag, den 14.01.2016, 11:47 +0100 schrieb Florian Haftmann:
> Hi Johannes, hi Andreas,
>
> the core of the problem is that dictionaries are always generated for
> type class instances, even if the operations therein are never
> referred
> to. Is this the first time that we have such a situation, or are
> there
> more examples (e.g. in the AFP)? If yes, the code generator could be
> equipped to treat particular constants *not* as class parameters.
>
> Cheers,
> Florian
>
> Am 11.01.2016 um 12:00 schrieb Johannes Hölzl:
> >
> >
> > 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 = "open" + uniformity +
> > > > > > > assumes open_uniformity: "⋀U. open U ⟷ (∀x∈U.
> > > > > > > eventually
> > > > > > > (λ(x',
> > > > > > > y). x' = x ⟶ y ∈ U) uniformity)"
> > > > > > >
> > > > > > > class uniformity_dist = dist + uniformity +
> > > > > > > assumes uniformity_dist: "uniformity = (INF e:{0
> > > > > > > <..}.
> > > > > > > principal
> > > > > > > {(x, y). dist x y < e})"
> > > > > > >
> > > > > > > Everything works fine until Affinite_Arithmetic, there in
> > > > > > > Intersection.thy the code generation fails with the
> > > > > > > following
> > > > > > > ML
> > > > > > > error:
> > > > > > >
> > > > > > > Error: Type mismatch in type constraint.
> > > > > > > Value: {uniformity = uniformity_proda} :
> > > > > > > {uniformity:
> > > > > > > 'a}
> > > > > > > Constraint: ('a * 'b) uniformity
> > > > > > > Reason:
> > > > > > > Can't unify 'a to (('a * 'b) * ('a * 'b)) filter
> > > > > > > (Type variable is free in surrounding scope)
> > > > > > > {uniformity = uniformity_proda} : ('a * 'b) uniformity
> > > > > > > At (line 1619 of "generated code")
> > > > > > > Exception- Fail "Static Errors" raised
> > > > > > >
> > > > > > > I assume this is a strange interaction btw code_abort and
> > > > > > > the
> > > > > > > fact
> > > > > > > that
> > > > > > > uniformity is a filter (datatype 'a filter = _EMPTY) and
> > > > > > > not
> > > > > > > a
> > > > > > > function.
> > > > > > >
> > > > > > > Does anybody know how to avoid such kind of errors? Do I
> > > > > > > need
> > > > > > > to
> > > > > > > sprinkle more [code del] or code_abort annotations?
> > > > > > >
> > > > > > > - Johannes
> > > > > > >
> > > > > > > _______________________________________________
> > > > > > > isabelle-dev mailing list
> > > > > > > isabelle-dev at in.tum.de
> > > > > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/lis
> > > > > > > tinf
> > > > > > > o/is
> > > > > > > abel
> > > > > > > le-dev
> > > > > > _______________________________________________
> > > > > > isabelle-dev mailing list
> > > > > > isabelle-dev at in.tum.de
> > > > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listi
> > > > > > nfo/
> > > > > > isab
> > > > > > elle-dev
> > > > > >
> > > > _______________________________________________
> > > > isabelle-dev mailing list
> > > > isabelle-dev at in.tum.de
> > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/
> > > > isab
> > > > elle-dev
> > > >
> > >
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> >
>
More information about the isabelle-dev
mailing list