I am trying to write a program in Haskell to compute the denotational semantics of an imperative language program with integer variables, 1-dimensional (integer) arrays and functions. The function I am starting with is of the type:
progsem :: Prog -> State -> State
where State is the following:
type State (Name -> Int, Name -> Int -> Int)
The first part is the value of integer variables, while the second part is the value of an array variable at a particular index.
The program will have the following qualities:
progsem will return the resulting state after the program executes
functions have two parameter lists, one for integer variables, and one for array variables.
functions are call by value result
Here is the abstract syntax for the imperative language:
-- names (variables) are just strings.
type Name = String
-- a program is a series (list) of function definitions, followed by a
-- series of statements.
type Prog = ([FunDefn],[Stmt])
-- a statement is either...
data Stmt =
Assign Name Exp -- ...assignment (<name> := <exp>;)
| If BExp [Stmt] [Stmt] -- ...if-then-else (if <bexp> { <stmt>* } else { <stmt>* })
| While BExp [Stmt] -- ...or a while-loop (while <bexp> { <stmt>*> })
| Let Name Exp [Stmt] -- ...let bindings (let <name>=<exp> in { <stmt> *})
| LetArray Name Exp Exp [Stmt] -- ...let-array binding (letarray <name> [ <exp> ] := <exp> in { <stmt>* })
| Case Exp [(Int,[Stmt])] -- ...case statements
| For Name Exp Exp [Stmt] -- ...for statements
| Return Exp -- ...return statement
| ArrayAssign Name Exp Exp -- ...or array assignment (<name> [ <exp> ] := <exp>;)
deriving Show
-- an integer expression is either...
data Exp =
Add Exp Exp -- ...addition (<exp> + <exp>)
| Sub Exp Exp -- ...subtract (<exp> - <exp>)
| Mul Exp Exp -- ...multiplication (<exp> * <exp>)
| Neg Exp -- ...negation (-<exp>)
| Var Name -- ...a variable (<name>)
| LitInt Int -- ...or an integer literal (e.g. 3, 0, 42, 1999)
| FunCall Name [Exp] [Name] -- ...or a function call (<name> (<exp>,...,<exp> [; <name>,...,<name>]))
| VarArray Name Exp -- ...or an array lookup (<name> [ <exp> ])
deriving Show
-- a boolean expression is either...
data BExp =
IsEq Exp Exp -- ...test for equality (<exp> == <exp>)
| IsNEq Exp Exp -- ...test for inequality (<exp> != <exp>)
| IsGT Exp Exp -- ...test for greater-than (<exp> > <exp>)
| IsLT Exp Exp -- ...test for less-than (<exp> < <exp>)
| IsGTE Exp Exp -- ...test for greater-or-equal (<exp> >= <exp>)
| IsLTE Exp Exp -- ...test for less-or-equal (<exp> <= <exp>)
| And BExp BExp -- ...boolean and (<bexp> && <bexp>)
| Or BExp BExp -- ...boolean or (<bexp> || <bexp>)
| Not BExp -- ...boolean negation (!<bexp>)
| LitBool Bool -- ... or a boolean literal (true or false)
deriving Show
type FunDefn = (Name,[Name],[Name],[Stmt])
Now, I do not have a specific question, but I was wondering if someone could point me in the right direction on how to go about writing the semantics.
In the past I have done something similar for an imperative programming language without arrays and functions. It looked something like this:
expsem :: Exp -> State -> Int
expsem (Add e1 e2) s = (expsem e1 s) + (expsem e2 s)
expsem (Sub e1 e2) s = (expsem e1 s) - (expsem e2 s)
expsem (Mul e1 e2) s = (expsem e1 s) * (expsem e2 s)
expsem (Neg e) s = -(expsem e s)
expsem (Var x) s = s x
expsem (LitInt m) _ = m
boolsem :: BExp -> State -> Bool
boolsem (IsEq e1 e2) s = expsem e1 s == expsem e2 s
boolsem (IsNEq e1 e2) s= not(expsem e1 s == expsem e2 s)
boolsem (IsGT e1 e2) s= expsem e1 s > expsem e2 s
boolsem (IsGTE e1 e2) s= expsem e1 s >= expsem e2 s
boolsem (IsLT e1 e2) s= expsem e1 s < expsem e2 s
boolsem (IsLTE e1 e2) s= expsem e1 s <= expsem e2 s
boolsem (And b1 b2) s= boolsem b1 s && boolsem b2 s
boolsem (Or b1 b2) s= boolsem b1 s || boolsem b2 s
boolsem (Not b) s= not (boolsem b s)
boolsem (LitBool x) _= x
stmtsem :: Stmt -> State -> State
stmtsem (Assign x e) s = (\z -> if (z==x) then expsem e s else s z)
stmtsem (If b pt pf) s = if (boolsem b s) then (progsem pt s) else (progsem pf s)
stmtsem (While b p) s = if (boolsem b s) then stmtsem (While b p) (progsem p s) else s
stmtsem (Let x e p) s = s1 where
initvalx = s x
letvalx = expsem e s
snew = progsem p (tweak s x letvalx)
s1 z = if (z == x) then initvalx else snew z
tweak :: State->Name->Int->State
tweak s vr n = \y -> if vr == y then n else s y
progsem :: Prog -> State -> State
progsem smlist s0 = (foldl (\s -> \sm -> (stmtsem sm s)) (s0) ) smlist
s :: State
s "x" = 10
Where states were of the type
type State= Name -> Int
Like I said, I do not need an in depth answer, but any help/hints/pointers would be much appreciated.
I'll deviate a bit from your given code and indicate how you might start to write a monadic interpreter which encodes the evaluation semantics for an toy imperative language, much like the one you specified. You'll need a frontend AST like you have:
We will evaluate via a function
eval
into concreteValue
types.To run the interpreter we need to feed it two values: the binding environment of variables and the values on the heap. This will return a tuple of the resulting value and the memory state which you can then feed back to the function itself if building a REPL-like loop.
Since you're writing an imperative language likely you'll want to add state and references, so you can create new AST nodes working allocating and mutating
Refs
. Left for you to do is to add the logic for allocating anArray
as a sequence ofRef
s and using pointer arithmetic when indexing and assigning into it.With this we'll need some helper functions for dealing with the values on the heap which are just thin wrappers around the State monad functions.
Hope that helps get you started.