Re: [isabelle] Casting records efficiently



Hi René,

the short answer: put something like

  declare foo.defs [code]

for every record specificaton »foo«, and code generation succeeds
without further ado.

My only explanation why this straight-forward equations have never been
used so far for generating code is that due to a historic
misunderstanding how code should be generated for record types these
have never been considered as candidates.

Thanks for reporting this.
	Florian

On 03.12.2013 22:34, René Neumann wrote:
> 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é
>>>
>>
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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