Thanks a lot.
Andreas
On 12/05/14 20:07, Florian Haftmann wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
