Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Greg Bronevetsky <greg@bronevetsky.com>
I'm trying to do use primrec to define a function that is applied to a
nested mutually-recursive datatype. The relevant portion of the datatype
definition is below:
datatype
AppSrcStmt =
skip |
while PvtAddr "AppSrcOp list"
and
AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"
The primrec in question is a measure function on this datatype, defined
as follows:
consts AppSrcStmtSize :: "AppSrcStmt => nat"
AppSrcOpSize :: "AppSrcOp => nat"
AppSrcOpListSize :: "(AppSrcOp list) => nat"
primrec
"AppSrcOpSize (opTriple asOp) = (AppSrcStmtSize (snd (snd asOp)))"
"AppSrcOpListSize [] = 0"
"AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp)"
"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)"
Unfortunately, I get the following error:
*** Constant to be defined occurs on rhs
*** The error(s) above occurred in definition
"AppSrcStmtSize_AppSrcStmt_def":
*** "AppSrcStmtSize ==
*** AppSrcStmt_AppSrcOp_rec_1 (1::nat) (%(pv::nat) aW::AppSrcOp list.
op + (1::nat))
*** (%(asOp::nat * nat * AppSrcStmt) asOpa::unit. AppSrcStmtSize
(snd (snd asOp))) (0::nat)
*** (%(asOp::AppSrcOp) (opList::AppSrcOp list) (asOpa::nat)
opLista::nat. asOpa) arbitrary arbitrary"
*** At command "primrec".
I think I'm following the directions from section 3.4 of the tutorial
but I apparenly I'm missing something. Any thoughts on what the problem
might be?
Email Gateway (Aug 17 2022 at 13:45):From: Stefan Berghofer <berghofe@in.tum.de>
Greg Bronevetsky wrote:
Dear Greg,
the problem is that not only the list datatype, but also the triple type
is unfolded (into two pair types). As a consequence, you need two more
size functions, one on type "FuncMark * TypeMark * AppSrcStmt" and one
on type "FuncMark * TypeMark * AppSrcStmt". The following definition should
work:
consts
AppSrcStmtSize :: "AppSrcStmt => nat"
AppSrcOpSize :: "AppSrcOp => nat"
AppSrcOpListSize :: "(AppSrcOp list) => nat"
AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat"
AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat"
primrec
"AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp"
"AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y"
"AppSrcOpPairSize (x, y) = AppSrcStmtSize y"
"AppSrcOpListSize [] = 0"
"AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp)"
"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize aW)"
See also the theorems AppSrcStmt_AppSrcOp.size provided by the datatype
package, which follow a similar scheme.
Greetings,
Stefan
Email Gateway (Aug 17 2022 at 13:45):From: Greg Bronevetsky <greg@bronevetsky.com>
Thank you. What you suggests works. However, when I apply it to my full
example I'm still getting errors. The problem is that my language has if
statements as well as while statements. Adding them to my type
definition, produces the following:
AppSrcStmt =
skip |
ifStmt PvtAddr "AppSrcOp list" "AppSrcOp list"
while PvtAddr "AppSrcOp list"
and
AppSrcOp = opTriple "FuncMark * TypeMark * AppSrcStmt"
I then use the following definition of the size funciton (directly
derived from your email):
consts
AppSrcStmtSize :: "AppSrcStmt => nat"
AppSrcOpSize :: "AppSrcOp => nat"
AppSrcOpListSize :: "(AppSrcOp list) => nat"
AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat"
AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat"
primrec
"AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp"
"AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y"
"AppSrcOpPairSize (x, y) = AppSrcStmtSize y"
"AppSrcOpListSize [] = 0"
"AppSrcOpListSize (asOp # opList) = (AppSrcOpSize asOp) +
(AppSrcOpListSize opList)"
"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + (AppSrcOpListSize aTrue)
When I do this, I get the following error:
*** Primrec definition error:
*** inconsistent functions for datatype "List.list"
*** in
*** "AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + AppSrcOpListSize aTrue"
*** At command "primrec".
After playing around with it, I see that the problem comes from the fact
that AppSrcOpListSize appears on the right hand side of AppSrcStmtSize
in three spots. If I comment out any two of the references to
AppSrcOpListSize then the definition goes through without a problem.
However, if there is more than one such reference, I get the above
error. Any ideas?
Email Gateway (Aug 17 2022 at 13:45):From: Stefan Berghofer <berghofe@in.tum.de>
Greg Bronevetsky wrote:
The problem is that each occurrence of "AppSrcOp list" is unfolded.
Consequently, you have to give a separate size function for each of
these occurrences, even though they happen to behave in the same way.
The following definition should work:
consts
AppSrcStmtSize :: "AppSrcStmt => nat"
AppSrcOpSize :: "AppSrcOp => nat"
AppSrcOpListSize1 :: "(AppSrcOp list) => nat"
AppSrcOpListSize2 :: "(AppSrcOp list) => nat"
AppSrcOpListSize3 :: "(AppSrcOp list) => nat"
AppSrcOpTripleSize :: "FuncMark * TypeMark * AppSrcStmt => nat"
AppSrcOpPairSize :: "TypeMark * AppSrcStmt => nat"
primrec
"AppSrcOpSize (opTriple asOp) = AppSrcOpTripleSize asOp"
"AppSrcOpTripleSize (x, y) = AppSrcOpPairSize y"
"AppSrcOpPairSize (x, y) = AppSrcStmtSize y"
"AppSrcOpListSize1 [] = 0"
"AppSrcOpListSize1 (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize1 opList)"
"AppSrcOpListSize2 [] = 0"
"AppSrcOpListSize2 (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize2 opList)"
"AppSrcOpListSize3 [] = 0"
"AppSrcOpListSize3 (asOp # opList) = (AppSrcOpSize asOp) + (AppSrcOpListSize3 opList)"
"AppSrcStmtSize skip = 1"
"AppSrcStmtSize (ifStmt pv aTrue aFalse) = 1 + (AppSrcOpListSize1 aTrue) + (AppSrcOpListSize2 aFalse)"
"AppSrcStmtSize (while pv aW) = 1 + (AppSrcOpListSize3 aW)"
Again, a quick look at the theorems AppSrcStmt_AppSrcOp.size reveals
how the scheme works.
Greetings,
Stefan
Email Gateway (Aug 17 2022 at 13:45):From: Greg Bronevetsky <greg@bronevetsky.com>
Ah, that worked! One final question then. You suggested that I look at
the theorem AppSrcStmt_AppSrcOp.size. How do I do that?
Last updated: May 03 2024 at 04:19 UTC