Concerning typerep, an ease could be achieved: as Alex pointed out, "size" (and also "eq" and "itself") are bootstrapped rather early, whereas "typerep" appears after List.thy. One solution is to move "typerep" up in the hierarchy:
a) Move Nibbles and Characters to a distinct theory Char.thy just right after datatype. b) Therein, provide an explicit type isomorphic to char list; this is a duplication which does not harm since it is only used as a technical facility for code generation, not much logical properties are needed. c) Typerep.thy then could immediately follow Char.thy and is incorporated via Code_Eval.thy (stupid name btw.) in Plain.thy. d) In List.thy, the conventional strings are established as types string = char list This would yield a complete setup of "typerep" since Plain.thy, which leaves only a minimal risk of producing "bad" thygraphs. Florian Florian Haftmann schrieb: > Hi Amine, > >> wrt to d) and e) (Users/Developers, HOL is difficult). >> This theory is for now a "using" HOL, but of course I want to develop it >> in a manner that it could become part of HOL. >> The situation you mention in d) and e) has not to be this way and we >> should not take it for granted that HOL is complex to develop etc. The >> social and psychological consequences are not very nice if it becomes a >> rule (my opinion). > > I share your concerns, though I would see the subtleties of HOL rather > technical consequences than a "rule". > >> Isabelle/HOL is remarkably more user friendly than many other system. >> All this effort of the past decades seems to have negative back effects >> in the past years: Many Developers stand before complex situations >> nobody or sometimes only one understands. Don't you think it is time to >> invest in a more developer-friendly Isabelle/HOL ? > > Not sure whether user-friendliness means less developer-friendliness. > Whether the situation became worse in the past years -- in my view it > got even better, but this may be subjective due to my experience. > Perhaps the focus of problems shifted. > >> If typerep is mainly used in connection with code-generation (as I >> understand) isn't it an option to generate all these instances when you >> call any code-generation facility? Or even in prior step e.g. called >> setup-every-thing-that-has-to-do-with-code-generation? > > This is even worse: in the first case, you won't be able to join any > (!) two theories which invoke code generation since you have a lot of > unredeemable duplication. The problem with the latter case is: there is > *never* such a point. > >> Besides, I don't object to the idea of typerep at all, I am just >> confused why the names clash? (Wasn't this the problem). In other words >> is this problem unavoidable, so that one needs a hard >> discussion/decision like typerep or no typerep? > > The problem is: you can instantiate every type class only once to a > particular type. There is no way to get around. > > Cheers > Florian > > > > ------------------------------------------------------------------------ > > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090121/1474aae7/attachment.pgp>