Writing a haskell program for computing denotational semantics of an imperative programming language

Question

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.

Your states should are partial functions by definition, so they should be `Name -> Maybe Int` — daniel gratzer, Dec 04 '13 at 19:31

Stephen Diehl · Accepted Answer · 2013-12-04T20:10:13.490

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:

import Control.Monad.State 
import qualified Data.Map as Map

data Expr = Var Var
          | App Expr Expr
          | Fun Var Expr
          | Lit Ground
          | If Expr Expr Expr
          -- Fill in the rest
          deriving (Show, Eq, Ord)

data Ground = LInt Integer
            | LBool Bool
            deriving (Show, Eq, Ord)

We will evaluate via a function eval into concrete Value types.

data Value = VInt Integer
           | VBool Bool
           | VUnit
           | VAddress Int
           | VClosure String Expr TermEnv

type TermEnv = Map.Map String Value
type Memory = [Value]
type Interpreter t = State Memory t

eval :: TermEnv -> Expr -> State Memory Value
eval _ (Lit (LInt k)) = return $ VInt k
eval _ (Lit (LBool k)) = return $ VBool k
eval env (Fun x body) = return (VClosure x body env)
eval env (App fun arg) = do
  VClosure x body clo <- eval env fun
  res <- eval env fun
  args <- eval env arg
  let nenv = Map.insert x args clo
  eval nenv body
eval env (Var x) = case (Map.lookup x env) of
  Just v -> return v
  Nothing -> error "prevent this statically!"
eval env (If cond tr fl) = do
  VBool br <- eval env cond
  if br == True
  then eval env tr
  else eval env fl

-- Finish with the rest of your syntax.

programs will return the resulting state after the program executes

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.

runInterpreter :: TermEnv -> Memory -> Expr -> (Value, [Value])
runInterpreter env mem x = runState (eval env x) mem

initMem = []
initTermEnv = Map.empty

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 an Array as a sequence of Refs and using pointer arithmetic when indexing and assigning into it.

data Expr = -- Same as above
          | Ref Expr
          | Access Expr
          | Assign Expr Expr

eval :: TermEnv -> Expr -> State Memory Value
...
eval env (Ref e) = do
  ev <- eval env e
  alloc ev
eval env (Access a) = do
  VAddress i <- eval env a
  readAddr i
eval env (Assign a e) = do
  VAddress i <- eval env a
  ev <- eval env e
  updateAddr ev i

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.

access :: Int -> Memory -> Value
access i mem = mem !! i

update :: Int -> Value -> Memory -> Memory
update addr val mem = a ++ [val] ++ b
  where
    (a, _:b) = splitAt addr mem

alloc :: Value -> Interpreter Value
alloc val = do
  mem <- get
  put $ mem ++ [val]
  return $ VAddress (length mem)

readAddr :: Int -> Interpreter Value
readAddr i = do
  mem <- get
  return $ access i mem

updateAddr ::  Value -> Int -> Interpreter Value
updateAddr val i = do
  mem <- get
  put $ update i val mem
  return VUnit

Hope that helps get you started.

Writing a haskell program for computing denotational semantics of an imperative programming language

1 Answers1