florian.haftmann at informatik.tu-muenchen.de
Wed Jan 21 10:58:23 CET 2009
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
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 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
> 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.
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev