Написание программы на языке haskell для вычисления денотационной семантики императивного языка программирования

Question

Написание программы на языке haskell для вычисления денотационной семантики императивного языка программирования

Я пытаюсь написать программу на Хаскеле для вычисления денотационной семантики императивной языковой программы с целочисленными переменными, одномерными (целочисленными) массивами и функциями. Функция, с которой я начинаю, имеет тип:

    progsem :: Prog -> State -> State

где состояние следующее:

    type State (Name -> Int, Name -> Int -> Int)

Первая часть - это значение целочисленных переменных, а вторая часть - это значение переменной массива по определенному индексу.

Программа будет обладать следующими качествами:

progsem вернет полученное состояние после выполнения программы
функции имеют два списка параметров, один для целочисленных переменных и один для переменных массива.
функции вызываются по значению результата

Вот абстрактный синтаксис для императивного языка:

     -- 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])

Теперь у меня нет конкретного вопроса, но мне было интересно, если кто-то может указать мне правильное направление о том, как писать семантику.

В прошлом я делал нечто подобное для императивного языка программирования без массивов и функций. Это выглядело примерно так:

   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

Где государства были типа

  type State=  Name -> Int

Как я уже сказал, мне не нужен подробный ответ, но любая помощь / подсказки / указатели будут высоко оценены.

4

haskell semantics imperative denotational-semantics

Источник

user1555678 04 дек '13 в 19:10

1 ответ

Решение

Другие вопросы по тегам haskell semantics imperative denotational-semantics

user190744 04 дек '13 в 19:53 2013-12-04 19:53 · Accepted Answer · 2013-12-04 19:53

Я немного отклонюсь от вашего кода и укажу, как вы можете начать писать монадический интерпретатор, который кодирует семантику оценки для игрушечного императивного языка, очень похожего на тот, который вы указали. Вам понадобится интерфейс AST, как у вас есть:

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)

Мы будем оценивать через функцию eval в бетон Value типы.

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.

программы вернут результирующее состояние после выполнения программы

Чтобы запустить интерпретатор, нам нужно передать ему два значения: окружение привязки переменных и значения в куче. Это вернет кортеж полученного значения и состояние памяти, которое вы можете затем передать обратно самой функции при построении цикла, подобного REPL.

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

initMem = []
initTermEnv = Map.empty

Поскольку вы пишете императивный язык, вероятно, вы захотите добавить состояние и ссылки, поэтому вы можете создавать новые узлы AST, работающие с выделением и изменением Refs, Оставлено для вас, чтобы добавить логику для распределения Array как последовательность Refs и использование арифметики указателя при индексации и присвоении ему.

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

Для этого нам понадобятся некоторые вспомогательные функции для работы со значениями в куче, которые являются просто тонкими обертками для функций монады State.

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

Надеюсь, это поможет вам начать.