Commit 906983bc authored by Katharina Ritter's avatar Katharina Ritter
Browse files

Finished ConcreteInterpreter and tests for it

parent 56eae7b3
Pipeline #149013 failed with stages
in 37 minutes and 12 seconds
......@@ -62,3 +62,6 @@ instance (ArrowApply c,Profunctor c) => ArrowApply (StoreT store c) where
instance ArrowFix (Underlying (StoreT store c) x y) => ArrowFix (StoreT store c x y) where
type Fix (StoreT store c x y) = Fix (Underlying (StoreT store c) x y)
--instance ArrowState s c => ArrowState s (StoreT (HashMap s val) c) where
{- get = lift' get
put = lift' put-}
......@@ -6,6 +6,10 @@
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
-- | Concrete interpreter of the While language.
module ConcreteInterpreter where
......@@ -45,10 +49,15 @@ import Text.Printf
import Data.String
import Data.Functor.Identity
--import Control.Monad.Trans.State
import Control.Arrow.State
import Control.Arrow.Transformer.State
import Control.Arrow.Store as S
import Control.Arrow.Const
import Control.Arrow.Reader
import Control.Arrow.Except
import Control.Arrow.Reader
import Control.Arrow.Environment
import Control.Arrow.Fix
......@@ -58,62 +67,59 @@ type Addr = Int
type Env = HashMap Text Addr
type Store = HashMap Addr Val
type Exception = (Text,Val)
--type AllocT c x y = StateT Int (State Int) Int
--newtype AllocT c x y = AllocT (StateT Int)
--type AllocT c x y = c x y -> (StateT Int (State Int))
newtype AllocT c x y = AllocT (StateT Addr c x y)
deriving(Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,ArrowRun,
ArrowStore var val, ArrowConst r, ArrowReader r, ArrowFail e, ArrowExcept e, ArrowEnv var val)
instance (ArrowState s c) => ArrowState s (AllocT c) where
put = lift' put
get = lift' get
instance (Arrow c, ArrowFix (Underlying (AllocT c) x y)) => ArrowFix (AllocT c x y) where
type Fix (AllocT c x y) = Fix (Underlying (AllocT c) x y)
-- | The concrete interpreter of the while language instantiates
-- 'Generic.run' with the concrete components for failure ('FailureT'), store ('StoreT'),
-- environments ('EnvT'), random numbers ('RandomT'), and values ('ConcreteT').
run :: [LStatement] -> Error String (Error Exception (HashMap Addr Val)) --TODO: working on this atm
run :: [LStatement] -> Error String (HashMap Addr Val)
run ss =
let ?fixpointAlgorithm = Function.fix in
fst <$>
Trans.run
(Generic.run ::
ValueT Val
(RandomT
(StateT Addr
(EnvT Env
(StoreT Store
(ExceptT Exception
(FailureT String
(->))))))) [Statement] ())
(M.empty,(M.empty,(R.mkStdGen 0, generate <$> ss)))
{-run1 :: [(Text,Addr)] -> [LStatement] -> Error String (Error Exception (HashMap Addr Val))
(AllocT
(EnvT Env
(StoreT Store
(FailureT String
(->))))) [Statement] ())
(M.empty,(M.empty, (0, generate <$> ss)))
run1 :: [(Text,Addr)] -> [LStatement] -> Error String (HashMap Addr Val)
run1 env0 ss =
let ?fixpointAlgorithm = Function.fix in
fmap fst <$>
fst <$>
Trans.run
(Generic.run ::
ValueT Val
(RandomT
(AllocT
(EnvT Env
(StoreT Store
(ExceptT Exception
(FailureT String
(->)))))) [Statement] ())
(M.empty,(M.fromList env0 ,(R.mkStdGen 0, generate <$> ss)))-}
--TODO: working on this atm
--instance (ArrowChoice c, Profunctor c, ArrowFail String c, Fail.Join Addr c) => ArrowAlloc Addr Val (ValueT (AllocT c) c) where
instance (ArrowChoice c, Profunctor c, ArrowFail String c, ArrowState Addr c, Fail.Join Addr c) => ArrowAlloc Addr Val (ValueT Val c) where
(FailureT String
(->))))) [Statement] ())
(M.empty,(M.fromList env0 ,(0, generate <$> ss)))
instance (ArrowChoice c, Profunctor c) => ArrowAlloc Addr (AllocT c) where
--this is the code that should work with StateT included
allocVar = proc _ -> do
allocVar = AllocT $ proc _ -> do
addr <- get -< ()
put -< addr + 1
returnA -< addr
allocValue = proc _ -> do
allocValue = AllocT $ proc _ -> do
addr <- get -< ()
put -< addr + 1
returnA -< addr
{- allocVar = arr $ \(_,_,l) -> labelVal l
allocValue = arr $ \(_,l) -> labelVal l-}
addr2Val = proc addr -> returnA -< (Pointer addr)
val2Addr = proc v1 -> case v1 of
Pointer addr1 -> returnA -< addr1
_ -> Fail.fail -< fromString $ printf "Value %s is not a pointer" (show v1)
instance (ArrowChoice c, ArrowFail String c, Fail.Join Val c) => IsVal Val (ValueT Val c) where
type JoinVal y (ValueT Val c) = (Fail.Join y c)
......@@ -149,7 +155,10 @@ instance (ArrowChoice c, ArrowFail String c, Fail.Join Addr c) => IsAddr Addr Va
store_ = proc v1 -> case v1 of
Pointer addr1 -> returnA -< addr1
_ -> Fail.fail -< fromString $ printf "Value %s is not a pointer" (show v1)
addr2Val = proc addr -> returnA -< (Pointer addr)
val2Addr = proc v1 -> case v1 of
Pointer addr1 -> returnA -< addr1
_ -> Fail.fail -< fromString $ printf "Value %s is not a pointer" (show v1)
instance (Profunctor c, ArrowRand Int c) => ArrowRand Val (ValueT Val c) where
random = ValueT $ proc () -> do
......@@ -161,13 +170,5 @@ instance R.Random Val where
randomR _ = error "random not defined for other values than numerical"
random = first NumVal . R.random
instance ArrowChoice c => IsException Exception Val (ValueT Val c) where
type JoinExc y (ValueT Val c) = ()
namedException = id
matchException f g = proc (name,(name',v),x) ->
if (name == name')
then f -< (v,x)
else g -< x
instance Hashable Val
......@@ -3,6 +3,12 @@
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Generic interpreter for the While-Language.
module GenericInterpreter where
......@@ -26,7 +32,15 @@ import Data.String
import Syntax
import GHC.Exts
import Control.Arrow.State
import Control.Arrow.State
import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Concrete.Environment as E
import Control.Arrow.Transformer.Concrete.Store as S
import Data.HashMap.Lazy(HashMap)
import Control.Arrow.Trans
import Data.Profunctor
type Prog = [Statement]
......@@ -39,9 +53,9 @@ type Prog = [Statement]
-- @ArrowEnv@ and @ArrowStore@ interface to access the environment.
eval :: (Show addr, Show v, ArrowChoice c,
ArrowEnv Text addr c, ArrowStore addr v c,
ArrowAlloc addr v c,
ArrowExcept exc c, ArrowFail e c,
IsVal v c, IsString e,
ArrowAlloc addr c,
ArrowFail e c,
IsVal v c, IsString e, IsAddr addr v c,
Env.Join v c, Env.Join addr c, Store.Join v c, Fail.Join v c, Fail.Join addr c
)
=> c Expr v
......@@ -77,9 +91,9 @@ eval = proc e -> case e of
Address x _ -> do
addr1 <- Env.lookup' -< x
addr2Val -< addr1
Alloc e1 l -> do
Alloc e1 _ -> do
v1 <- eval -< e1
addr1 <- allocValue -< (v1,l)
addr1 <- allocValue -< ()
write -< (addr1, v1)
addr2Val -< addr1
Load e1 _ -> do
......@@ -96,35 +110,21 @@ run :: (Show addr, Show v,
?fixpointAlgorithm :: FixpointAlgorithm (Fix (c [Statement] ())),
ArrowChoice c, ArrowFix (c [Statement] ()),
ArrowEnv Text addr c, ArrowStore addr v c,
ArrowFail err c, ArrowState Int c,
ArrowAlloc addr v c,
ArrowExcept exc c, ArrowRand v c,
ArrowFail err c,
ArrowAlloc addr c,
IsString err, IsVal v c, IsAddr addr v c,
Env.Join v c, Env.Join addr c, Store.Join v c,
Fail.Join v c, JoinVal () c, JoinExc () c, Fail.Join addr c
Fail.Join v c, JoinVal () c, Fail.Join addr c
)
=> c [Statement] ()
run = fix $ \run' -> proc stmts -> case stmts of
Assign x e l:ss -> do
v <- eval -< e
addr <- Env.lookup (proc (addr,_) -> returnA -< addr)
(proc (x,v,l) -> allocVar -< (x,v,l))
(proc (x,v,l) -> allocVar -< ())
-< (x,(x,v,l))
write -< (addr,v)
Env.extend run' -< (x,addr,ss)
{- Alloc _ _ -> do
v <- eval -< e
addr <- Env.lookup (proc (addr,_) -> returnA -< addr)--(proc x -> Fail.fail -< fromString $ printf "Variable %s already bound" (show x))
(proc (x,v,l) -> allocAssign -< (x,v,l))
-< (x,(x,v,l))
Env.extend (proc (a1,x1) -> returnA -< (a1,x1)) -< (x,addr,(x,addr))
write -< (addr,v)
_ -> do
v <- eval -< e
addr <- Env.lookup (proc (addr,_) -> returnA -< addr)
(proc x -> Fail.fail -< fromString $ printf "Variable %s not yet bound" (show x))
-< (x,(x,v,l))
write -< (addr,v)-}
If cond s1 s2 _:ss -> do
b <- eval -< cond
if_ run' run' -< (b,([s1],[s2]))
......@@ -144,7 +144,7 @@ run = fix $ \run' -> proc stmts -> case stmts of
returnA -< ()
-- | Interface for value operations.
class Arrow c => IsVal v c | c -> v where
class Arrow c => IsVal v c where
-- | In case of the abstract interpreter allows to join the result
-- of an @if@ statement.
type family JoinVal x (c :: * -> * -> *) :: Constraint
......@@ -160,21 +160,15 @@ class Arrow c => IsVal v c | c -> v where
null_ :: c Label v
alloc_ :: c (v,Label) v
-- | Interface for value operations.
class Arrow c => IsAddr addr v c | c -> addr where
-- | Interface for address operations.
class Arrow c => IsAddr addr v c where
store_ :: c v addr
--class ArrowAssign addr c where
class ArrowAlloc addr v c | c -> addr where
--allocVar :: c () addr
--allocValue :: c () addr
allocVar :: c (Text,v,Label) addr
allocValue :: c (v,Label) addr
addr2Val :: c addr v
val2Addr :: c v addr
class IsException exc v c | c -> v where
type family JoinExc y (c :: * -> * -> *) :: Constraint
namedException :: c (Text,v) exc
matchException :: JoinExc y c => c (v,x) y -> c x y -> c (Text,exc,x) y
-- | Interface for allocation
class Arrow c => ArrowAlloc addr c where
allocVar :: c () addr
allocValue :: c () addr
deriving instance (ArrowAlloc a c) => ArrowAlloc a (ValueT val2 c)
......@@ -146,8 +146,8 @@ run k env0 ss =
deriving instance ArrowComplete () c => ArrowComplete () (ValueT Val c)
instance (ArrowChoice c, Profunctor c) => ArrowAlloc Addr Val (ValueT Val c) where
allocValue = arr $ \(_,l) -> return l
{-instance (ArrowChoice c, Profunctor c) => ArrowAlloc Addr Val (ValueT Val c) where
allocValue = arr $ \(_,l) -> return l-}
......@@ -183,13 +183,13 @@ instance (IsString e, ArrowChoice c, ArrowFail e c, Fail.Join Val c) => IsVal Va
null_ = proc _ -> returnA -< NullVal
instance ArrowChoice c => IsException Exception Val (ValueT Val c) where
{-instance ArrowChoice c => IsException Exception Val (ValueT Val c) where
type JoinExc y (ValueT Val c) = ArrowComplete y (ValueT Val c)
namedException = proc (name,val) -> returnA -< Exception (M.singleton name val)
matchException f g = proc (name,Exception m,x) -> case M.lookup name m of
AM.Just v -> f -< (v,x)
AM.Nothing -> g -< x
AM.JustNothing v -> (f -< (v,x)) <> (g -< x)
AM.JustNothing v -> (f -< (v,x)) <⊔> (g -< x)-}
instance (ArrowChoice c, Profunctor c) => ArrowRand Val (ValueT Val c) where
random = proc _ -> returnA -< NumVal top
......
......@@ -23,47 +23,59 @@ spec = do
it "x = alloc null;" $ do
run1 [] (["x" =: (alloc' null')])
`shouldBe` res (M.insert 2 (Pointer 1) (M.singleton 1 (NullVal)))
`shouldBe` res (M.insert 1 (Pointer 0) (M.singleton 0 (NullVal)))
it "x = alloc null; p= alloc null; x = p" $ do
it "x = alloc null; (env: x = 0)" $ do
run1 [("x",0)] (["x" =: (alloc' null')])
`shouldBe` res (M.insert 0 (Pointer 1) (M.singleton 1 (NullVal)))
it "x = alloc null; p = alloc null; x = p" $ do
run1 [] (["x" =: (alloc' null'), "p" =: (alloc' null'), "x" =: "p"])
`shouldBe` res (M.insert 2 (Pointer 99) (M.singleton 1 (NullVal)))
`shouldBe` res (M.insert 3 (Pointer 2) (M.insert 2 (NullVal) (M.insert 1 (Pointer 2) (M.singleton 0 (NullVal)))))
it "x = alloc null; *x = x;" $ do
run1 [] (["x" =: (alloc' null'), store "x" "x"])
`shouldBe` res (M.insert 2 (Pointer 1) (M.singleton 1 (Pointer 1)))
`shouldBe` res (M.insert 1 (Pointer 0) (M.singleton 0 (Pointer 0)))
it "x = alloc 13;" $ do
run1 [] (["x" =: (alloc' 13)])
`shouldBe` res (M.insert 2 (Pointer 1) (M.singleton 1 (NumVal 13)))
`shouldBe` res (M.insert 1 (Pointer 0) (M.singleton 0 (NumVal 13)))
it "y = &x;" $ do
run1 [("x",99),("y",100)] ["y" =: (address' "x")]
`shouldBe` res (M.singleton 100 (Pointer 99))
it "y = &x; no env0" $ do
run1 [] ["y" =: (address' "x")]
`shouldBe` Err.Fail "Variable \"x\" not bound"
it "x = alloc null; *x = 42;" $ do
run1 [("x",99)] ["x" =: (alloc' null'), store "x" 42]
`shouldBe` res (M.insert 99 (Pointer 1) (M.singleton 1 (NumVal 42)))
`shouldBe` res (M.insert 99 (Pointer 0) (M.singleton 0 (NumVal 42)))
it "x = alloc null; *x = 42; no env0" $ do
run1 [] ["x" =: (alloc' null'), store "x" 42]
`shouldBe` res (M.insert 2 (Pointer 1) (M.singleton 1 (NumVal 42)))
`shouldBe` res (M.insert 1 (Pointer 0) (M.singleton 0 (NumVal 42)))
it "x = alloc null; y = &x; z = *y;" $ do
run1 [("x",99), ("y",100), ("z",101)] ["x" =: (alloc' null'), "y" =: (address' "x"), "z" =: load' "y"]
`shouldBe` res (M.insert 99 (Pointer 1) (M.insert 100 (Pointer 99) (M.insert 1 (NullVal) (M.singleton 101 (Pointer 1)))))
`shouldBe` res (M.insert 99 (Pointer 0) (M.insert 100 (Pointer 99) (M.insert 0 (NullVal) (M.singleton 101 (Pointer 0)))))
it "x = alloc null; y = &x; z = *y; no env0" $ do
run1 [] ["x" =: (alloc' null'), "y" =: (address' "x"), "z" =: load' "y"]
`shouldBe` res (M.insert 3 (Pointer 0) (M.insert 2 (Pointer 1) (M.insert 1 (Pointer 0) (M.singleton 0 (NullVal)))))
it "x = alloc null; y = &x; z = **y;" $ do
run1 [("x",99), ("y",100), ("z",101)] ["x" =: (alloc' null'), "y" =: (address' "x"), "z" =: load' (load' "y")]
`shouldBe` res (M.insert 99 (Pointer 1) (M.insert 100 (Pointer 99) (M.insert 1 (NullVal) (M.singleton 101 (NullVal)))))
`shouldBe` res (M.insert 99 (Pointer 0) (M.insert 100 (Pointer 99) (M.insert 0 (NullVal) (M.singleton 101 (NullVal)))))
it "x = alloc null; y = &x; *x = 42;" $ do
run1 [("x",99), ("y",100)] ["x" =: (alloc' null'), "y" =: (address' "x"), store "x" 42]
`shouldBe` res (M.insert 100 (Pointer 99) (M.insert 99 (Pointer 1) (M.singleton 1 (NumVal 42))))
`shouldBe` res (M.insert 100 (Pointer 99) (M.insert 99 (Pointer 0) (M.singleton 0 (NumVal 42))))
it "x = alloc null; y = &x; *x = 42; z = **y;" $ do
run1 [("x",99),("y",100),("z",101)] ["x" =: (alloc' null'), "y" =: (address' "x"), store "x" 42, "z" =: (load' (load' "y"))]
`shouldBe` res (M.insert 99 (Pointer 1) (M.insert 100 (Pointer 99) (M.insert 1 (NumVal 42) (M.singleton 101 (NumVal 42)))))
`shouldBe` res (M.insert 99 (Pointer 0) (M.insert 100 (Pointer 99) (M.insert 0 (NumVal 42) (M.singleton 101 (NumVal 42)))))
it "11 < 10 == false" $ do
run1 [("x",99)] ["x" =: 11 < 10]
......@@ -77,13 +89,13 @@ spec = do
run1 [("x",99),("y",100)] ["x" =: 1, "y" =: 2,while ("x" < "y") ["x" =: "y" + 1]]
`shouldBe` res (M.insert 100 (NumVal 2) (M.singleton 99 (NumVal 3)))
it "{x = alloc null; y = alloc null; \n*x = null; *y = y; n = 3; \nwhile (n > 0) { \np = alloc null; q = alloc null; \n*p = x; *q = y; \nx = p; y = q; n = n - 1}" $ do
it "{x = alloc null; y = alloc null; \n\t*x = null; *y = y; n = 3; \n\twhile (n > 0) { \n\tp = alloc null; q = alloc null; \n\t*p = x; *q = y; \n\tx = p; y = q; n = n - 1}" $ do
run1 [("x",99),("y",100),("p",101),("q",102),("n",103)] ["x" =: (alloc' null'), "y" =: (alloc' null'), store "x" null', store "y" "y", "n" =: 3, while (0 < "n") ["p" =: (alloc' null'), "q" =: (alloc' null'), store "p" "x", store "q" "y", "x" =: "p", "y" =: "q", "n" =: "n" - 1]]
`shouldBe` res (M.insert 99 (Pointer 1) (M.insert 100 (Pointer 99) (M.insert 2 (NumVal 42) (M.singleton 99 (Pointer 2)))))
`shouldBe` res (M.insert 7 (Pointer 5) (M.insert 6 (Pointer 4) (M.insert 5 (Pointer 3) (M.insert 4 (Pointer 2) (M.insert 102 (Pointer 7) (M.insert 3 (Pointer 1) (M.insert 101 (Pointer 6) (M.insert 2 (Pointer 0) (M.insert 103 (NumVal 0) (M.insert 100 (Pointer 7) (M.insert 1 (Pointer 1) (M.insert 99 (Pointer 6) (M.singleton 0 (NullVal))))))))))))))
it "{x = alloc null; y = alloc null; \n*x = null; *y = y; n = 3; \nwhile (n > 0) { \np = alloc null; q = alloc null; \n*p = x; *q = y; \nx = p; y = q; n = n - 1} no env0" $ do
it "{x = alloc null; y = alloc null; \n\t*x = null; *y = y; n = 3; \n\twhile (n > 0) { \n\tp = alloc null; q = alloc null; \n\t*p = x; *q = y; \n\tx = p; y = q; n = n - 1} no env0" $ do
run1 [] ["x" =: (alloc' null'), "y" =: (alloc' null'), store "x" null', store "y" "y", "n" =: 3, while (0 < "n") ["p" =: (alloc' null'), "q" =: (alloc' null'), store "p" "x", store "q" "y", "x" =: "p", "y" =: "q", "n" =: "n" - 1]]
`shouldBe` res (M.insert 99 (Pointer 1) (M.insert 100 (Pointer 99) (M.insert 2 (NumVal 42) (M.singleton 99 (Pointer 2)))))
`shouldBe` res (M.insert 16 (Pointer 15) (M.insert 15 (Pointer 11) (M.insert 14 (Pointer 13) (M.insert 13 (Pointer 9) (M.insert 12 (Pointer 11) (M.insert 11 (Pointer 7) (M.insert 10 (Pointer 9) (M.insert 9 (Pointer 5) (M.insert 8 (Pointer 7) (M.insert 7 (Pointer 2) (M.insert 6 (Pointer 5) (M.insert 5 (Pointer 0) (M.insert 4 (NumVal 0) (M.insert 3 (Pointer 15) (M.insert 2 (Pointer 2) (M.insert 1 (Pointer 13) (M.singleton 0 (NullVal))))))))))))))))))
where
res x = (Err.Success (Err.Success x))
res x = (Err.Success x)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment