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

Опитвам се да напиша програма на 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

Както казах, не се нуждая от задълбочен отговор, но всяка помощ/намеци/указатели ще бъдат много оценени.


haskell semantics imperative denotational-semantics
person Justin B    schedule 04.12.2013    source източник
comment
Вашите състояния трябва да са частични функции по дефиниция, така че трябва да бъдат Name -> Maybe Int   -  person Daniel Gratzer    schedule 04.12.2013

Отговори (1)


arrow_upward
5
arrow_downward

Ще се отклоня малко от дадения от вас код и ще посоча как бихте могли да започнете да пишете монадичен интерпретатор, който кодира семантиката за оценка за императивен език играчка, много подобен на посочения от вас. Ще ви е необходим интерфейс 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 monad.

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

Надявам се, че това ще ви помогне да започнете.

person Stephen Diehl    schedule 04.12.2013