[isabelle-dev] Problem with code generation for non-executable types
Andreas Lochbihler
andreas.lochbihler at inf.ethz.ch
Fri Jan 8 15:48:06 CET 2016
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.
Andreas
> 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/isabel
>> le-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
More information about the isabelle-dev
mailing list