Hi Johannes,
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.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.
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel le-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
