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 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/lis > > > > > > > tinf > > > > > > > o/is > > > > > > > abel > > > > > > > le-dev > > > > > > _______________________________________________ > > > > > > isabelle-dev mailing list > > > > > > isabelle-...@in.tum.de > > > > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listi > > > > > > nfo/ > > > > > > isab > > > > > > elle-dev > > > > > > > > > > _______________________________________________ > > > > isabelle-dev mailing list > > > > isabelle-...@in.tum.de > > > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/ > > > > isab > > > > elle-dev > > > > > > > > > _______________________________________________ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isab > > elle-dev > > > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev