Re: [isabelle] Casting records efficiently



Something like the attached?

- René

Am 03.12.2013 22:07, schrieb Florian Haftmann:
> Hi René.
> 
> it might be helpful if you could provide me with a small self-contained
> example.
> 
> Cheers,
> 	Florian
> 
> On 03.12.2013 18:27, René Neumann wrote:
>> Dear all,
>>
>> when given a record hierarchy (let's take 'foo' and 'foo_bar', where
>> 'foo_bar' extends 'foo'), I couldn't find a good way to "cast" a record
>> of type foo into one of type foo_bar, s.t. the construct is executable
>> (the additional fields of 'foo_bar' are going to be initialized with
>> constants).
>>
>> I.e. I need a function "cast :: foo ⇒ foo_bar" or more generally
>> "cast :: 'a foo_scheme ⇒ 'b foo_scheme"
>>
>> First attempt (not executable):
>>
>> cast g = foo.extend g (foo_bar.fields arg1 arg2)
>>
>>
>> Second attempt (wrong type -- g here already needs to be of type foo_bar):
>>
>> cast g = g(| arg1 := arg1, arg2 := arg2 |)
>>
>>
>> Third attempt (parsing error):
>>
>> cast g = g(| … := (| arg1 = arg1, arg2 = arg2 |)|)
>>
>>
>> Fourth attempt (wrong type -- see 2nd):
>>
>> cast g = foo.more_update (λ_. (| arg1 = arg1, arg2 = arg2 |)) g
>>
>>
>> Fifth attempt (working, but very clumsy):
>>
>> function cast where
>>  "cast (| foo_1 = x1, foo_2 = x2, foo_3 = x3 |) = (| foo_1 = x1, foo_2 =
>> x2, foo_3 = x3, arg1 = arg1, arg2 = arg2 |)"
>> by (metis foo.cases) (metis foo.ext_inject)
>> termination by lexicographic_order
>>
>>
>> Is there some better alternative for this? Where I am not forced to
>> spell out all fields of 'foo', and proof trivial obligations?
>>
>> Thanks a lot,
>> René
>>
> 

theory Scratch
imports Main
begin

record foo =
  foo1 :: int
  foo2 :: int
  foo3 :: bool

record foo_bar = foo +
  bar1 :: nat
  bar2 :: "bool set"

text {* Problem: Convert @{typ "'a foo_scheme"} into @{typ "'b foo_scheme"}. A special variant is
@{typ foo} (= @{typ "unit foo_scheme"}) to @{typ foo_bar} (= @{typ "unit foo_bar_ext foo_scheme"})*}

definition cast1 :: "foo \<Rightarrow> foo_bar" where
"cast1 g = foo.extend g (foo_bar.fields 0 {})"

export_code cast1 checking SML -- "fails"

definition cast2 :: "foo \<Rightarrow> foo_bar" where
"cast2 = g(| bar1 := 0, bar2 := {} |)" -- "fails: Type mismatch"

definition cast3 :: "foo \<Rightarrow> foo_bar" where
"cast3 g = g\<lparr> \<dots> := \<lparr> bar1 = 0, bar2 = {}\<rparr>\<rparr>" -- "fails: Syntax error"

definition cast4:: "foo \<Rightarrow> foo_bar" where
"cast4 g = foo.more_update (\<lambda>_. \<lparr> bar1 = 0, bar2 = {} \<rparr>) g" -- "fails: Type mismatch"

text {* The previous definition fails, as @{const foo.more_update} has type 
@{typ "('a \<Rightarrow> 'a) \<Rightarrow> 'a foo_scheme \<Rightarrow> 'a foo_scheme"} and not
@{typ "('a \<Rightarrow> 'b) \<Rightarrow> 'a foo_scheme \<Rightarrow> 'b foo_scheme"} *}

text {* The following works, but is rather clumsy. In particular, it needs to specify
all fields of @{typ foo}.*}

function cast5 where
 "cast5 \<lparr> foo1 = x1, foo2 = x2, foo3 = x3 \<rparr> = \<lparr> foo1 = x1, foo2 =
x2, foo3 = x3, bar1 = 0, bar2 = {}\<rparr>"
by (metis foo.cases) (metis foo.ext_inject)
termination by lexicographic_order

export_code cast5 checking SML -- "works"

end


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