some updates to while language

parent a08271b7
......@@ -9,5 +9,5 @@ import Prelude hiding (lookup,id)
import Control.Arrow
class Arrow c => ArrowStore var val c | c -> var, c -> val where
lookup :: c var val
store :: c (var,val) ()
read :: c var val
write :: c (var,val) ()
......@@ -53,7 +53,7 @@ instance (Show var, Identifiable var, Identifiable addr, Complete val, ArrowChoi
lookup = Environment $ Reader $ proc ((env,store),x) -> do
case do {addr <- E.lookup x env; S.lookup addr store} of
Success v -> returnA -< v
Fail _ -> failA -< printf "variable %s not found" (show x)
Fail _ -> failA -< printf "Variable %s not bound" (show x)
Bot -> bottom -< ()
getEnv = Environment askA
extendEnv = proc (x,y,(env,store)) -> do
......
......@@ -37,7 +37,7 @@ instance (Show var, Identifiable var, ArrowChoice c, ArrowFail String c, LowerBo
lookup = Environment $ Reader $ proc (env,x) -> do
case E.lookup x env of
Success y -> returnA -< y
Fail _ -> failA -< printf "variable %s not found" (show x)
Fail _ -> failA -< printf "Variable %s not bound" (show x)
Bot -> bottom -< ()
getEnv = Environment askA
extendEnv = arr $ \(x,y,env) -> E.insert x y env
......
......@@ -9,11 +9,13 @@ module Control.Arrow.Transformer.Abstract.Store where
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Lift
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Store
import Control.Arrow.Transformer.State
import Control.Arrow.Utils
import Control.Category
import Data.Abstract.Error
......@@ -26,14 +28,23 @@ import Text.Printf
newtype StoreArrow var val c x y = StoreArrow (State (Store var val) c x y)
runStore :: StoreArrow var val c x y -> c (Store var val, x) (Store var val, y)
runStore (StoreArrow (State f)) = f
evalStore :: Arrow c => StoreArrow var val c x y -> c (Store var val, x) y
evalStore f = runStore f >>> pi2
execStore :: Arrow c => StoreArrow var val c x y -> c (Store var val, x) (Store var val)
execStore f = runStore f >>> pi1
instance (Show var, Identifiable var, ArrowFail String c, ArrowChoice c, Complete (c ((Store var val,val),var) (Store var val,val)), LowerBounded (c () (Store var val,val))) =>
ArrowStore var val (StoreArrow var val c) where
lookup =
read =
StoreArrow $ State $ proc (s,var) -> case S.lookup var s of
Success v -> joined returnA (proc var -> failA -< printf "could not find variable" (show var)) -< ((s,v),var)
Fail _ -> failA -< printf "could not find variable" (show var)
Bot -> bottom -< ()
store = StoreArrow (State (arr (\(s,(x,v)) -> (S.insert x v s,()))))
write = StoreArrow (State (arr (\(s,(x,v)) -> (S.insert x v s,()))))
instance ArrowState s c => ArrowState s (StoreArrow var val c) where
getA = lift getA
......@@ -45,6 +56,7 @@ deriving instance ArrowChoice c => ArrowChoice (StoreArrow var val c)
deriving instance ArrowLift (StoreArrow var val)
deriving instance ArrowReader r c => ArrowReader r (StoreArrow var val c)
deriving instance ArrowFail e c => ArrowFail e (StoreArrow var val c)
deriving instance ArrowFix (Store var val, x) (Store var val, y) c => ArrowFix x y (StoreArrow var val c)
deriving instance PreOrd (c (Store var val,x) (Store var val,y)) => PreOrd (StoreArrow var val c x y)
deriving instance Complete (c (Store var val,x) (Store var val,y)) => Complete (StoreArrow var val c x y)
deriving instance CoComplete (c (Store var val,x) (Store var val,y)) => CoComplete (StoreArrow var val c x y)
......
......@@ -38,7 +38,7 @@ instance (Show var, Identifiable var, ArrowChoice c, ArrowFail String c) => Arro
env <- getEnv -< ()
case E.lookup x env of
Success y -> returnA -< y
Fail _ -> failA -< printf "variable %s not found" (show x)
Fail _ -> failA -< printf "Variable %s not bound" (show x)
getEnv = Environment askA
extendEnv = arr $ \(x,y,env) -> E.insert x y env
localEnv (Environment f) = Environment (localA f)
......
......@@ -7,35 +7,47 @@
{-# LANGUAGE Arrows #-}
module Control.Arrow.Transformer.Concrete.Store where
import Control.Category
import Prelude hiding ((.))
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Lift
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Fail
import Control.Arrow.Store
import Control.Arrow.Lift
import Control.Arrow.Transformer.State
import Control.Arrow.Utils
import Control.Category
import Data.Concrete.Error
import Data.Concrete.Store (Store)
import qualified Data.Concrete.Store as S
import Data.Order
import Data.Identifiable
import Text.Printf
newtype StoreArrow var val c x y = StoreArrow (State (Store var val) c x y)
runStore :: StoreArrow var val c x y -> c (Store var val, x) (Store var val, y)
runStore (StoreArrow (State f)) = f
evalStore :: Arrow c => StoreArrow var val c x y -> c (Store var val, x) y
evalStore f = runStore f >>> pi2
execStore :: Arrow c => StoreArrow var val c x y -> c (Store var val, x) (Store var val)
execStore f = runStore f >>> pi1
instance ArrowLift (StoreArrow var val) where
lift f = StoreArrow (lift f)
instance (Show var, Identifiable var, ArrowFail String c, ArrowChoice c, Complete (c ((Store var val,val),var) (Store var val,val))) =>
instance (Show var, Identifiable var, ArrowFail String c, ArrowChoice c) =>
ArrowStore var val (StoreArrow var val c) where
lookup =
read =
StoreArrow $ State $ proc (s,var) -> case S.lookup var s of
Success v -> joined returnA (proc var -> failA -< printf "could not find variable" (show var)) -< ((s,v),var)
Success v -> returnA -< (s,v)
Fail _ -> failA -< printf "could not find variable" (show var)
store = StoreArrow (State (arr (\(s,(x,v)) -> (S.insert x v s,()))))
write = StoreArrow (State (arr (\(s,(x,v)) -> (S.insert x v s,()))))
instance ArrowState s c => ArrowState s (StoreArrow var val c) where
getA = lift getA
......@@ -46,3 +58,4 @@ deriving instance Arrow c => Arrow (StoreArrow var val c)
deriving instance ArrowChoice c => ArrowChoice (StoreArrow var val c)
deriving instance ArrowReader r c => ArrowReader r (StoreArrow var val c)
deriving instance ArrowFail e c => ArrowFail e (StoreArrow var val c)
deriving instance ArrowFix (Store var val, x) (Store var val, y) c => ArrowFix x y (StoreArrow var val c)
......@@ -5,7 +5,7 @@
{-# LANGUAGE StandaloneDeriving #-}
module Control.Arrow.Transformer.State(State(..),evalState,execState) where
import Prelude hiding (id,(.),lookup)
import Prelude hiding (id,(.),lookup,read)
import Control.Arrow
import Control.Arrow.Deduplicate
......@@ -15,6 +15,7 @@ import Control.Arrow.Fix
import Control.Arrow.Lift
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Store
import Control.Arrow.Try
import Control.Arrow.Utils
import Control.Category
......@@ -66,6 +67,10 @@ instance ArrowEnv x y env c => ArrowEnv x y env (State r c) where
extendEnv = lift extendEnv
localEnv (State f) = State ((\(r,(env,a)) -> (env,(r,a))) ^>> localEnv f)
instance ArrowStore var val c => ArrowStore var val (State r c) where
read = lift read
write = lift write
instance ArrowFix (s,x) (s,y) c => ArrowFix x y (State s c) where
fixA f = State (fixA (runState . f . State))
......
{-# LANGUAGE DeriveGeneric #-}
module Data.Abstract.Boolean where
import Prelude hiding (Bool(..))
import qualified Prelude as P
import Data.Abstract.Widening
import Data.Boolean
import Data.Hashable
import Data.Order
import Data.Abstract.Widening
data Bool = Bot | True | False | Top deriving (Eq)
import GHC.Generics
data Bool = Bot | True | False | Top deriving (Eq,Generic)
instance Show Bool where
show Bot = "⊥"
......@@ -61,3 +65,5 @@ instance UpperBounded Bool where
top = Top
instance Widening Bool where
instance Hashable Bool
......@@ -13,3 +13,7 @@ instance (Show e,Show a) => Show (Error e a) where
instance (Hashable e, Hashable a) => Hashable (Error e a) where
hashWithSalt s (Fail e) = s `hashWithSalt` (1 :: Int) `hashWithSalt` e
hashWithSalt s (Success a) = s `hashWithSalt` (2 :: Int) `hashWithSalt` a
toEither :: Error e x -> Either e x
toEither (Fail e) = Left e
toEither (Success e) = Right e
......@@ -80,11 +80,11 @@ spec = do
localEnv lookup -< (env7,x)
it "env(a) = [1,6]" $ runTests setup "a" `shouldBe` Success (Interval 1 1)
it "env(b) = Nothing" $ runTests setup "b" `shouldBe` Fail "variable \"b\" not found"
it "env(c) = Nothing" $ runTests setup "c" `shouldBe` Fail "variable \"c\" not found"
it "env(b) = Nothing" $ runTests setup "b" `shouldBe` Fail "Variable \"b\" not bound"
it "env(c) = Nothing" $ runTests setup "c" `shouldBe` Fail "Variable \"c\" not bound"
it "env(d) = [4,4]" $ runTests setup "d" `shouldBe` Success (Interval 4 4)
it "env(e) = Nothing" $ runTests setup "e" `shouldBe` Fail "variable \"e\" not found"
it "env(f) = Nothing" $ runTests setup "f" `shouldBe` Fail "variable \"f\" not found"
it "env(e) = Nothing" $ runTests setup "e" `shouldBe` Fail "Variable \"e\" not bound"
it "env(f) = Nothing" $ runTests setup "f" `shouldBe` Fail "Variable \"f\" not bound"
it "env(g) = [2,7]" $ runTests setup "g" `shouldBe` Success (Interval 7 7)
where
......
......@@ -9,7 +9,7 @@ import Prelude
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Transformer.Concrete.Environment
import Control.Arrow.Transformer.Concrete.Error
import Control.Arrow.Transformer.Concrete.Except
import Control.Arrow.Transformer.Concrete.Fix
import Control.Monad.State
......@@ -27,10 +27,10 @@ import Shared
data Closure = Closure Expr (Env Text Val) deriving (Eq,Generic)
data Val = NumVal Int | ClosureVal Closure deriving (Eq,Generic)
type Interp = Environment Text Val (ErrorArrow String Fix)
type Interp = Environment Text Val (Except String Fix)
evalConcrete :: [(Text,Val)] -> State Label Expr -> Error String Val
evalConcrete env e = runFix (runErrorArrow (runEnvironment eval)) (env,generate e)
evalConcrete env e = runFix (runExcept (runEnvironment eval)) (env,generate e)
instance IsVal Val Interp where
succ = proc x -> case x of
......
......@@ -12,12 +12,10 @@ import Prelude hiding (Bounded)
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.Environment
import Control.Arrow.Transformer.Abstract.Contour hiding (toList)
import Control.Arrow.Transformer.Abstract.BoundedEnvironment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Except
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Reader
import Control.Monad.State hiding (lift)
......@@ -58,20 +56,20 @@ instance Show Closure where
type Addr = (Text,Contour)
type Interp =
ReaderArrow IV
Reader IV
(Environment Text Addr Val
(ContourArrow
(ErrorArrow String
(CacheArrow (Env Text Addr,Store Addr Val,(IV,Expr))
(Error String Val)))))
(Except String
(Fix ((Env Text Addr,Store Addr Val),(IV,Expr))
(Error String Val)))))
evalInterval :: Int -> IV -> [(Text,Val)] -> State Label Expr -> Error String Val
evalInterval k bound env e =
runCacheArrow
(runErrorArrow
runFix
(runExcept
(runContourArrow k
(runEnvironment
(runReaderArrow (eval :: Interp Expr Val)))))
(runReader (eval :: Interp Expr Val)))))
(env,(bound,generate e))
instance IsVal Val Interp where
......@@ -132,8 +130,8 @@ instance Widening Val where
NumVal x NumVal y = NumVal (x y)
x y = x y
instance HasLabel (Env Text Addr,Store (Text, Contour) Val,(IV, Expr)) where
label (_,_,(_,e)) = label e
instance HasLabel ((Env Text Addr,Store (Text, Contour) Val),(IV, Expr)) where
label ((_,_),(_,e)) = label e
instance Hashable Closure
instance Hashable Val
......@@ -4,7 +4,7 @@ module ConcreteSpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import Concrete
import Data.Error
import Data.Concrete.Error
import PCF
import Test.Hspec
......@@ -13,7 +13,7 @@ main = hspec spec
spec :: Spec
spec = do
sharedSpec evalConcrete (NumVal . fromIntegral)
sharedSpec (\env e -> toEither (evalConcrete env e)) (NumVal . fromIntegral)
describe "behavior specific to concrete semantics" $
it "should analyse addition correctly" $ do
......
......@@ -4,11 +4,11 @@ module IntervalAnalysisSpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import Data.Bounded
import Data.Error
import qualified Data.Interval as I
import Data.InfiniteNumbers
import IntervalAnalysis
import Data.Abstract.Bounded
import Data.Abstract.Error
import qualified Data.Abstract.Interval as I
import Data.Abstract.InfiniteNumbers
import IntervalAnalysis hiding (Bot)
import PCF
import Test.Hspec
......@@ -19,7 +19,7 @@ spec :: Spec
spec = do
let lim = I.Interval (-100) 100
bounded = Bounded lim
in sharedSpec (evalInterval 3 lim) (NumVal . bounded . fromIntegral)
in sharedSpec (\env e -> toEither $ evalInterval 3 lim env e) (NumVal . bounded . fromIntegral)
describe "behavior specific to interval analysis" $ do
it "should execute both branches on IfZero on interval containing zero" $
......@@ -65,3 +65,8 @@ spec = do
one = succ zero
two = succ one
toEither :: Error String a -> Either String a
toEither (Fail e) = Left e
toEither (Success x) = Right x
toEither Bot = Left "bottom"
......@@ -5,43 +5,42 @@ import Prelude hiding (succ,pred)
import Control.Monad.State
import Data.Error
import Data.Text (Text)
import Data.Label
import PCF
import Test.Hspec
sharedSpec :: (Show v, Eq v) => ([(Text,v)] -> State Label Expr -> Error String v) -> (Int -> v)-> Spec
sharedSpec :: (Show v, Eq v) => ([(Text,v)] -> State Label Expr -> Either String v) -> (Int -> v)-> Spec
sharedSpec eval fromInt = describe "shared language behavior" $ do
it "should look up a bound variable" $
eval [("x",fromInt 5)] "x" `shouldBe` Success (fromInt 5)
eval [("x",fromInt 5)] "x" `shouldBe` Right (fromInt 5)
it "should fail when looking up an unbound variable" $
eval [] "x" `shouldBe` Error "Variable \"x\" not bound"
eval [] "x" `shouldBe` Left "Variable \"x\" not bound"
it "should apply a function" $
eval [] (app (lam "x" (succ "x")) zero) `shouldBe` Success (fromInt 1)
eval [] (app (lam "x" (succ "x")) zero) `shouldBe` Right (fromInt 1)
it "should fail when applying something other than a function" $
eval [] (app zero zero) `shouldBe` Error "Expected a closure"
eval [] (app zero zero) `shouldBe` Left "Expected a closure"
it "should compute 0 + 1 + 1 = 2" $
eval [] (succ (succ zero)) `shouldBe` Success (fromInt 2)
eval [] (succ (succ zero)) `shouldBe` Right (fromInt 2)
it "should fail when using succ on something other than a number" $
eval [] (succ (lam "x" zero)) `shouldBe` Error "Expected a number as argument for 'succ'"
eval [] (succ (lam "x" zero)) `shouldBe` Left "Expected a number as argument for 'succ'"
it "should fail when using pred on something other than a number" $
eval [] (pred (lam "x" zero)) `shouldBe` Error "Expected a number as argument for 'pred'"
eval [] (pred (lam "x" zero)) `shouldBe` Left "Expected a number as argument for 'pred'"
it "should execute the then branch on IfZero on zero" $
eval [] (ifZero zero (succ zero) zero)
`shouldBe` Success (fromInt 1)
`shouldBe` Right (fromInt 1)
it "should execute the else branch on IfZero on completely non-zero" $
eval [] (ifZero (succ zero) (succ zero) zero)
`shouldBe` Success (fromInt 0)
`shouldBe` Right (fromInt 0)
it "should fail when using a non-number condition for IfZero" $
eval [] (ifZero (lam "x" zero) zero zero) `shouldBe` Error "Expected a number as condition for 'ifZero'"
eval [] (ifZero (lam "x" zero) zero zero) `shouldBe` Left "Expected a number as condition for 'ifZero'"
......@@ -2,7 +2,7 @@
let
hsEnv = pkgs.haskellPackages.ghcWithPackages(p: with p; [
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion fgl arrows
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion fgl
(p.callPackage ../lib/default.nix { })
]);
......
{-# LANGUAGE DeriveGeneric #-}
module Expressions where
import Data.Label
import Data.Text (Text)
import Data.Hashable
import Data.Order
import GHC.Generics
data Expr
= Var Text Label
| BoolLit Bool Label
| And Expr Expr Label
| Or Expr Expr Label
| Not Expr Label
| NumLit Double Label
| RandomNum Label
| Add Expr Expr Label
| Sub Expr Expr Label
| Mul Expr Expr Label
| Div Expr Expr Label
| Eq Expr Expr Label
deriving (Show,Ord,Eq,Generic)
instance HasLabel Expr where
label e = case e of
Var _ l -> l
BoolLit _ l -> l
And _ _ l -> l
Or _ _ l -> l
Not _ l -> l
NumLit _ l -> l
RandomNum l -> l
Add _ _ l -> l
Sub _ _ l -> l
Mul _ _ l -> l
Div _ _ l -> l
Eq _ _ l -> l
instance Hashable Expr where
instance PreOrd Expr where
() = (==)
() = (==)
data Statement
= While Expr [Statement] Label
| If Expr [Statement] [Statement] Label
| Assign Text Expr Label
deriving (Show,Ord,Eq,Generic)
instance HasLabel Statement where
label s = case s of
While _ _ l -> l
If _ _ _ l -> l
Assign _ _ l -> l
instance Hashable Statement where
type Prog = [Statement]
......@@ -2,10 +2,9 @@
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DeriveGeneric #-}
module WhileLanguage where
module Shared where
import Prelude hiding (lookup, and, or, not, div)
import Prelude hiding (lookup, and, or, not, div, read)
import Data.Label
......@@ -13,134 +12,80 @@ import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Utils
import Control.Arrow.Store
import Control.Arrow.Fail
import Data.Text (Text)
import Data.Hashable
import Data.Order
import GHC.Generics
import System.Random
data Expr
= Var Text Label
| BoolLit Bool Label
| And Expr Expr Label
| Or Expr Expr Label
| Not Expr Label
| NumLit Double Label
| RandomNum Label
| Add Expr Expr Label
| Sub Expr Expr Label
| Mul Expr Expr Label
| Div Expr Expr Label
| Eq Expr Expr Label
deriving (Show,Ord,Eq,Generic)
instance HasLabel Expr where
label e = case e of
Var _ l -> l
BoolLit _ l -> l
And _ _ l -> l
Or _ _ l -> l
Not _ l -> l
NumLit _ l -> l
RandomNum l -> l
Add _ _ l -> l
Sub _ _ l -> l
Mul _ _ l -> l
Div _ _ l -> l
Eq _ _ l -> l
instance Hashable Expr where
instance PreOrd Expr where
() = (==)
() = (==)
data Statement = While Expr [Statement] Label
| If Expr [Statement] [Statement] Label
| Assign Text Expr Label
deriving (Show,Ord,Eq)
instance HasLabel Statement where
label s = case s of
While _ _ l -> l
If _ _ _ l -> l
Assign _ _ l -> l
import Expressions
type Prog = [Statement]
class HasRandomGen c where
nextRandom :: Random a => c () a
class Arrow c => Eval v c | c -> v where
boolLit :: c (Bool,Label) v
and :: c (v,v,Label) v
or :: c (v,v,Label) v
not :: c (v,Label) v
numLit :: c (Double,Label) v
randomNum :: c Label v
add :: c (v,v,Label) v
sub :: c (v,v,Label) v
mul :: c (v,v,Label) v
div :: c (v,v,Label) v
eq :: c (v,v,Label) v
class FixEval v c | c -> v where
fixEval :: (c Expr v -> c Expr v) -> c Expr v
eval :: (ArrowFail String c, ArrowStore (Text,Label) v c, ArrowChoice c, FixEval v c, Eval v c) => c Expr v
eval = fixEval $ \ev -> proc e -> case e of
Var x l -> lookup' -< (x,l)
eval :: (ArrowChoice c, HasStore v c, IsVal v c) => c Expr v
eval = proc e -> case e of
Var x l -> lookup -< (x,l)
BoolLit b l -> boolLit -< (b,l)
And e1 e2 l -> do
v1 <- ev -< e1
v2 <- ev -< e2
v1 <- eval -< e1
v2 <- eval -< e2
and -< (v1,v2,l)
Or e1 e2 l -> do
v1 <- ev -< e1
v2 <- ev -< e2
v1 <- eval -< e1
v2 <- eval -< e2
or -< (v1,v2,l)
Not e1 l -> do
v1 <- ev -< e1
v1 <- eval -< e1
not -< (v1,l)
NumLit n l -> numLit -< (n,l)
RandomNum l -> randomNum -< l
Add e1 e2 l -> do
v1 <- ev -< e1
v2 <- ev -< e2
v1 <- eval -< e1
v2 <- eval -< e2
add -< (v1,v2,l)
Sub e1 e2 l -> do
v1 <- ev -< e1
v2 <- ev -< e2
v1 <- eval -< e1