Re: [isabelle] Problems with code-datatype



Hi René,

On 30/09/14 15:14, René Thiemann wrote:
1) I do not see why in your solution there is only one test "t = B":
    in get_noB' there definitely is one "t = B" test, and the second one is hidden in
    unpack_no_B_option, where again you make a case analysis which seems similar to a "t = B" test,
    i.e., here you have to choose the reason why the value is in no_B (whether it is the reason A or C)
That's right. I just thought that a case analysis is faster than a complicated predicate test, but at second thought it does not buy you anything.

2) I did not understand why the type-copy no_B_option should help at all: with A_no_B and C_no_B at hand you can
    more easily and directly define

   definition get_no_B :: "test => no_B option" where
      "get_no_B t == if t = B then None else case t of A => Some A_no_B | C => Some C_no_B"

    or even

   definition get_no_B :: "test => no_B option" where
      "get_no_B t == case t of A => Some A_no_B | B => None | C => Some C_no_B"
The idea for the type copy comes from the paper on Data Refinement, as I have answered on stackexchange some time ago:

http://stackoverflow.com/questions/16040064/isabelles-code-generation-abstraction-lemmas-for-containers

However, this does not solve your problem with duplicate testing. In a follow-up thread, Joachim describes a solution to avoid duplicate tests:

http://stackoverflow.com/questions/16273812/working-with-isabelles-code-generator-data-refinement-and-higher-order-functio

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.