Theory CPSScheme
section "Syntax"
theory CPSScheme
imports Main
begin
text ‹
First, we define the syntax tree of a program in our toy functional language, using continuation passing style, corresponding to section 3.2 in Shivers' dissertation.
›
text ‹
We assume that the program to be investigated is already parsed into a syntax tree. Furthermore, we assume that distinct labels were added to distinguish different code positions and that the program has been alphatised, i.e. that each variable name is only bound once. This binding position is, as a convenience, considered part of the variable name.
›
type_synonym label = nat
type_synonym var = "label × string"
definition "binder" :: "var ⇒ label" where [simp]: "binder v = fst v"
text ‹
The syntax consists now of lambda abstractions, call expressions and values, which can either be lambdas, variable references, constants or primitive operations. A program is a lambda expression.
Shivers' language has as the set of basic values integers plus a special value for \textit{false}. We simplified this to just the set of integers. The conditional ‹If› considers zero as false and any other number as true.
Shivers also restricts the values in a call expression: No constant maybe be used as the called value, and no primitive operation may occur as an argument. This restriction is dropped here and just leads to runtime errors when evaluating the program.
›
datatype prim = Plus label | If label label