Re: [isabelle] Problems with code-datatype



Dear Wenda,

>> Reading the manual on code-generation and "Data Refinement in Isabelle/HOL", I realized that
>> page 109 it is mentioned that for abstract type A and concrete type C one can
>> lift a function f :: C => (C)? => C to a function f whose type should be A => (A)? => A.
>> So does that mean that I won't be able to define my function create_foo as essentially it is
>> of type C => A?
> 
> This is not quite true, as you can define
> 
> lift_definition g:: "test => no_B "
>  is "% t. if t = B then A else t"
>  by auto
> 
> and the code generation works fine. In terms of
> 
> lift_definition get_no_B :: "test => no_B option"
>  is "% t. if t = B then None else Some t"
>  by auto
> 
> I think the problem is with
> 
> get_no_B.rep_eq: map_option Rep_no_B (get_no_B ?x) = (if ?x = B then None else Some ?x)

I fully agree.

> An ideal code abstract equation for type no_B is of the form
> 
> Rep_no_B (f ...) = ...
> 
> so that code equations that preserve invariants of no_B could be derived for f. Lemma get_no_B.rep_eq does not match such format, and I guess that is why code generation fails for get_no_B (although in theory I think we can still derive code equations in such cases).

Again I agree, in principle the test ensures that no bad terms can walk below an Abs_no_B.

> Experts on data refinements should be able to comment more ;-)
> 
> Hope this helps,

Definitely it was helpful, thanks a lot. Based on your definition of get_no_B I now could modify my code as follows to my original setting, which now is code-exportable.

datatype test = A | B | C
typedef no_B = "{ t :: test. t ~= B}" by auto

setup_lifting type_definition_no_B

lift_definition get_test :: "no_B => test" 
  is "% x. x" .

lift_definition get_no_B' :: "test => no_B" 
  is "% t. if t = B then A else t" 
  by auto

definition get_no_B :: "test => no_B option" where
  "get_no_B t = (if t = B then None else Some (get_no_B' t))"

lemma get_no_B: "get_no_B t = Some no_b ==> 
  get_test no_b = t" 
  unfolding get_no_B_def
  by (cases "t = B", simp_all, transfer, auto)

export_code get_test in Haskell 
export_code get_no_B in Haskell 

However, this solution has the small problem, that the test "t = B" is done in both
get_no_B and get_no_B'. In my real application this test "t = B" is a bit more complicated to
compute, so still the solution is not optimal. (The original definition of get_no_B only had 
one test "t = B")

Cheers,
René




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