Email Gateway (Aug 18 2022 at 09:57): Email Gateway (Aug 18 2022 at 09:57):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Is there any chance the following will come to be allowed by the
record definition package?
theory foo imports Main
begin
datatype 'a ptr = Ptr nat
record listnode =
item :: nat
nextnode :: "listnode ptr"
end
It'd be annoying to have to make the nextnode field of "unit ptr", and
end up with an Isabelle model that has less type information than the
original C program.
Michael.
Email Gateway (Aug 18 2022 at 09:57):From: Norbert Schirmer <norbert.schirmer@web.de>
Hi Michael,
On Wednesday 29 November 2006 23:12, Michael Norrish wrote:
Is there any chance the following will come to be allowed by the
record definition package?
Such a change is not planned since recursion and extensibility of records
doesn't seem to fit together too well.
If you really need recursion you can still use a datatype.
theory foo imports Main
begindatatype 'a ptr = Ptr nat
record listnode =
item :: nat
nextnode :: "listnode ptr"end
However, in your example you only want to maintain a kind of type-tag for
"ptr". Maybe one of the following workarounds can still help you:
1)
datatype 'a ptr = Ptr nat
typedecl listnodeT
record listnode =
item :: nat
nextnode :: "listnodeT ptr"
2)
record 'a listnode =
item ::nat
nextnode :: "'a ptr"
term "r::(unit listnode) listnode"
Norbert
Email Gateway (Aug 18 2022 at 09:59):From: Norbert Schirmer <norbert.schirmer@web.de>
Hi Michael,
On Wednesday 29 November 2006 23:12, Michael Norrish wrote:
Is there any chance the following will come to be allowed by the
record definition package?
Such a change is not planned since recursion and extensibility of records
doesn't seem to fit together too well.
If you really need recursion you can still use a datatype.
theory foo imports Main
begindatatype 'a ptr = Ptr nat
record listnode =
item :: nat
nextnode :: "listnode ptr"end
However, in your example you only want to maintain a kind of type-tag for
"ptr". Maybe one of the following workarounds can still help you:
1)
datatype 'a ptr = Ptr nat
typedecl listnodeT
record listnode =
item :: nat
nextnode :: "listnodeT ptr"
2)
record 'a listnode =
item ::nat
nextnode :: "'a ptr"
term "r::(unit listnode) listnode"
Norbert
Last updated: May 03 2024 at 04:19 UTC