> 1. Violation of well-sortedness constraints: type ... not an instance of > ... > > declare [[show_sorts]] > code_thms <constant to be exported> > > Then, I use educated guessing and Emacs' incremental search to navigate > the code equations that have been output until I find the fault -- > usually, it's just a missing [code] or [code del] declaration for some > constant that has introduced a quantifier or set comprehension.
> I would really appreciate support for navigating code equations in the > output (e.g., Ctrl-click on a constant on the RHS of an equation takes > me to the code equation of that constant (in the output of code_thms). > > For this particular case, it would also be useful to get the chain of > propagation for the sort constraint like in GHC (arising from the use of > ...), but since Isabelle's code generator strengthens sort constraints > for intermediate functions, this would be a list (tree/graph) of > functions that trace the propagation. I will have to think about something like that seriously. > Here, I have two suggestions for improvements: > > a) Provide an entry to the code preprocessor such that I can trace the > transformation of the code equations for a given (set of) constants. > Currently, I only know how to trace the preprocessing of *all* code > equations, but I am not interested in most of this trace. I will consider this. > b) [code_abbrev] is the worst code generator attribute that I know of, > because there's no reverse [code_abbrev del]. Each time I have to get > rid of a code abbreviation, I have to figure out once again how > [code_abbrev] transforms the theorem before it calls [code_unfold] and > [code_post]. Please add the [code_abbrev del] attribute. See now http://isabelle.in.tum.de/repos/isabelle/rev/40213e24c8c4 > And while I am at it, here is another point that makes my life > unnecessarily hard, but it's not related to jEdit vs. PG: > > 3. Problems with Code_Evaluation.term_of and friends > > The term reconstruction functions are not displayed in code_thms because > of the section "obfuscation" in Code_Evaluation. I do not understand why > this has to be obfuscated. I always have to go via export_code and read > the generated code to figure out what the code equation for one of these > overloaded constants is. And it's bad luck if export_code raises an > error because some of the code equations are invalid. See now http://isabelle.in.tum.de/repos/isabelle/rev/1e50fddbe1f5 Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
