Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Casting records efficiently

Email Gateway (Aug 19 2022 at 13:11):

From: René Neumann <rene.neumann@in.tum.de>
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é
smime.p7s

Email Gateway (Aug 19 2022 at 13:11):

From: René Neumann <rene.neumann@in.tum.de>
Just noticed: The same problem exists for the other direction:
foo.truncate is also not executable.

• René
  smime.p7s

Email Gateway (Aug 19 2022 at 13:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René.

it might be helpful if you could provide me with a small self-contained
example.

Cheers,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 13:11):

From: René Neumann <rene.neumann@in.tum.de>
Something like the attached?

• René
  Scratch.thy

Email Gateway (Aug 19 2022 at 13:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Last updated: Apr 30 2024 at 12:28 UTC