Re: [isabelle-dev] Problem with code generation for non-executable types
Hi Johannes, hi Andreas, the core of the problem is that dictionaries are always generated for type class instances, even if the operations therein are never referred to. Is this the first time that we have such a situation, or are there more examples (e.g. in the AFP)? If yes, the code generator could be equipped to treat particular constants *not* as class parameters. Cheers, Florian Am 11.01.2016 um 12:00 schrieb Johannes Hölzl: > > > Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann: >> 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. > > Well filters are mostly non-computable. Actually I would prefer to tell > the code-generator to not generate code for topologies and uniform > spaces at all, as these type classes are carry only non-computable > data. > > But of course your implementation looks cleaner, so I changed in > Isabelle df65f5c27c15. > > - Johannes > > >> 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
Re: [isabelle-dev] Problem with code generation for non-executable types
AFAIK, it is the first time we have such a situation. We have two cases I'm aware of: "open" in topological_space and "uniformity" in uniform_space. Up to now we could just remove all code equations from open as it is a predicate and doesn't produce any problem with the dictionary construction. Your suggestion would be great, to completely disable code generation for "open" and "uniformity". It would avoid a lot of [code del] annotations at class instantiations, and some strange constructions for filter ;-) - Johannes Am Donnerstag, den 14.01.2016, 11:47 +0100 schrieb Florian Haftmann: > Hi Johannes, hi Andreas, > > the core of the problem is that dictionaries are always generated for > type class instances, even if the operations therein are never > referred > to. Is this the first time that we have such a situation, or are > there > more examples (e.g. in the AFP)? If yes, the code generator could be > equipped to treat particular constants *not* as class parameters. > > Cheers, > Florian > > Am 11.01.2016 um 12:00 schrieb Johannes Hölzl: > > > > > > Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann: > > > 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. > > > > Well filters are mostly non-computable. Actually I would prefer to > > tell > > the code-generator to not generate code for topologies and uniform > > spaces at all, as these type classes are carry only non-computable > > data. > > > > But of course your implementation looks cleaner, so I changed in > > Isabelle df65f5c27c15. > > > > - Johannes > > > > > > > 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
Re: [isabelle-dev] Problem with code generation for non-executable types
Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann: > 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. Well filters are mostly non-computable. Actually I would prefer to tell the code-generator to not generate code for topologies and uniform spaces at all, as these type classes are carry only non-computable data. But of course your implementation looks cleaner, so I changed in Isabelle df65f5c27c15. - Johannes > 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 =
Re: [isabelle-dev] Problem with code generation for non-executable types
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
[isabelle-dev] Problem with code generation for non-executable types
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 uniform_space.hgbundle Description: Binary data ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem with code generation for non-executable types
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-...@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
Re: [isabelle-dev] Problem with code generation for non-executable types
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-...@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