[isabelle-dev] Problem with code generation for non-executable types
Johannes Hölzl
hoelzl at in.tum.de
Fri Jan 8 09:56:27 CET 2016
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: uniform_space.hgbundle
Type: application/octet-stream
Size: 9670 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160108/4d92ffac/attachment.obj>
More information about the isabelle-dev
mailing list