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

[Johannes Hölzl]

Okay Fabian and I discovered the following problems when one defines a
type class which contains a constant which is not a function:

1.  If there is a type class which contains data depending on the type
    classes variable, i.e. 

      class test_class =
        fixes test :: "'a filter"

    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.

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