Am Freitag, den 08.01.2016, 15:48 +0100 schrieb Andreas Lochbihler:
> Hi 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.
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-...@in.tum.de
> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> > > abel
> > > le-dev
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-...@in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> >
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
