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.
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
