[isabelle-dev] Problem with code generation for non-executable types

[Johannes Hölzl]

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-dev at in.tum.de
> > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> > > abel
> > > le-dev
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab
> > elle-dev
> >