Commit 528a879d authored by Jente Hidskes's avatar Jente Hidskes

Initial commit of PCF

This is not yet working due to not being able to define the least upper
bound of two Interp arrows. For this reason the tests of the sign and
interval semantics have also not been run on this new version where the
shared interpreter abstracts over value types.

As you can see in pcf/src/Shared.hs, we can also remove the definition
of ArrowFail with the one from lib/src/Data/Fail.hs, perhaps extract
ArrowFix into its own file in lib/src/Data as well and perhaps remove a
functional dependency in IsEnv.
parent 0b33b23f
Copyright (c) 2017, Sven Keidel
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.
* Neither the name of Sven Keidel nor the names of other
contributors may be used to endorse or promote products derived
from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
import Distribution.Simple
main = defaultMain
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Concrete where
import Prelude
import Control.Arrow
import Control.Monad.Trans.Reader
import qualified Data.Map as M
import Data.Text (Text)
import PCF (Expr (Lam))
import Shared hiding (Env)
import Utils
data Val = Num Int | Closure Expr Env deriving (Eq, Show)
type Env = M.Map Text Val
-- ReaderT (Env Maybe a) = Env -> Maybe a
type Interp = Kleisli (ReaderT Env Maybe)
evalConcrete :: Env -> Expr -> Maybe Val
evalConcrete env e = runReaderT (runKleisli eval e) env
instance ArrowFix Interp where
fixA f = f (fixA f)
instance ArrowFail Interp where
failA = Kleisli $ const (fail "")
instance IsEnv Env Val Interp where
getEnv = Kleisli $ const ask
lookup = proc x -> do
env <- getEnv -< ()
case M.lookup x env of
Just v -> returnA -< v
Nothing -> failA -< "Variable '" ++ show x ++ "' not bound"
instance IsVal Val Interp where
succ = proc x -> case x of
Num n -> returnA -< Num (n + 1)
_ -> failA -< "Expected a number as argument for 'succ'"
pred = proc x -> case x of
Num n -> returnA -< Num (n - 1)
_ -> failA -< "Expected a number as argument for 'pred'"
zero = arr $ const (Num 0)
ifZero f g = proc (v1, (x, y)) -> case v1 of
Num 0 -> f -< x
Num _ -> g -< y
_ -> failA -< "Expected a number as condition for 'ifZero'"
closure = arr $ \(e,env) -> Closure e env
applyClosure f = proc (fun, arg) -> case (fun, arg) of
(Closure (Lam x _ body) env, Num _) -> localA f -< (M.insert x arg env, body)
_ -> failA -< "Expected a closure and a number argument"
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Interval where
import Prelude
import Control.Arrow
import Control.Monad.Trans.Reader
import Data.InfiniteNumbers
import Data.Interval
import qualified Data.Map as M
import Data.Order
import Data.Text (Text)
import PCF (Expr (Lam))
import Shared hiding (Env)
import Utils
data Val = Num (Interval (InfiniteNumber Int)) | Closure Expr Env deriving (Eq, Show)
type Env = M.Map Text Val
type Interp = Kleisli (ReaderT Env Maybe)
evalInterval :: Env -> Expr -> Maybe Val
evalInterval env e = runReaderT (runKleisli eval e) env
instance ArrowFix Interp where
fixA f = f (fixA f)
instance ArrowFail Interp where
failA = Kleisli $ const (fail "")
instance IsEnv Env Val Interp where
getEnv = Kleisli $ const ask
lookup = proc x -> do
env <- getEnv -< ()
case M.lookup x env of
Just v -> returnA -< v
Nothing -> failA -< "Variable '" ++ show x ++ "' not bound"
instance IsVal Val Interp where
succ = proc x -> case x of
Num n -> returnA -< Num $ withBounds1 (\x -> x + 1) n
_ -> failA -< "Expected a number as argument for 'succ'"
pred = proc x -> case x of
Num n -> returnA -< Num $ withBounds1 (\x -> x - 1) n
_ -> failA -< "Expected a number as argument for 'pred'"
zero = arr $ const (Num (constant 0))
ifZero f g = proc (Num (IV (i1, i2)), (x, y)) ->
if (i1, i2) == (0, 0)
then f -< x
else if i1 > 0 || i2 < 0
then g -< y
else (f -< x) (g -< y)
closure = arr $ \(e, env) -> Closure e env
applyClosure f = proc (fun, arg) -> case (fun, arg) of
(Closure (Lam x _ body) env, Num _) -> localA f -< (M.insert x arg env, body)
_ -> failA -< "Expected a closure and an interval argument"
-- TODO: instance Complete (Interp a b) where ...
module PCF where
import Data.Text(Text)
data Expr = Var Text
| Lam Text Type Expr
| App Expr Expr
| Zero
| Succ Expr
| Pred Expr
| IfZero Expr Expr Expr
| Y Expr deriving (Eq, Show)
data Type = NumT
| FunT Type Type deriving (Eq, Show)
{-# LANGUAGE Arrows #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
module Shared where
import Prelude hiding (succ, pred, lookup)
import PCF (Expr)
import qualified PCF as E
import Control.Arrow
import Data.Map (Map)
import Data.Text (Text)
type Env v = Map Text v
eval :: (ArrowChoice c, ArrowFix c, ArrowFail c, IsEnv (Env v) v c, IsVal v c) => c Expr v
eval = fixA $ \ev -> proc e0 -> case e0 of
E.Var x -> lookup -< x
E.Lam {} -> do
env <- getEnv -< ()
closure -< (e0, env)
E.App e1 e2 -> do
fun <- ev -< e1
arg <- ev -< e2
applyClosure ev -< (fun, arg)
E.Y e -> ev -< E.App e (E.Y e)
E.Zero -> zero -< ()
E.Succ e -> do
v <- ev -< e
succ -< v
E.Pred e -> do
v <- ev -< e
pred -< v
E.IfZero e1 e2 e3 -> do
v1 <- ev -< e1
ifZero ev ev -< (v1, (e2, e3))
-- TODO: extract into separate file?
class Arrow c => ArrowFix c where
fixA :: (c x y -> c x y) -> c x y
-- TODO: replace with Control.Arrow.Fail
class Arrow c => ArrowFail c where
failA :: c x y
-- TODO: v -> env should go now that the shared interpreter does not define Val anymore?
class Arrow c => IsEnv env v c | v -> env, env -> v where
getEnv :: c () env
lookup :: c Text v
class Arrow c => IsVal v c | c -> v where
succ :: c v v
pred :: c v v
zero :: c () v
ifZero :: c x v -> c y v -> c (v, (x, y)) v
closure :: c (Expr, Env v) v
applyClosure :: c Expr v -> c (v, v) v
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Sign where
import Prelude
import Control.Arrow
import Control.Monad.Trans.Reader
import qualified Data.Map as M
import Data.Order
import Data.Sign
import Data.Text (Text)
import PCF (Expr (Lam))
import Shared hiding (Env)
import Utils
data Val = Num Sign | Closure Expr Env deriving (Show)
type Env = M.Map Text Val
type Interp = Kleisli (ReaderT Env Maybe)
evalSign :: Env -> Expr -> Maybe Val
evalSign env e = runReaderT (runKleisli eval e) env
instance ArrowFix Interp where
fixA f = f (fixA f)
instance ArrowFail Interp where
failA = Kleisli $ const (fail "")
instance IsEnv Env Val Interp where
getEnv = Kleisli $ const ask
lookup = proc x -> do
env <- getEnv -< ()
case M.lookup x env of
Just v -> returnA -< v
Nothing -> failA -< "Variable '" ++ show x ++ "' not bound"
instance IsVal Val Interp where
succ = proc s -> case s of
Num Positive -> returnA -< Num Positive
Num Zero -> returnA -< Num Positive
Num Negative -> returnA -< Num Top
Num Top -> returnA -< Num Top
_ -> failA -< "Expected a number as argument for 'succ'"
pred = proc s -> case s of
Num Positive -> returnA -< Num Top
Num Zero -> returnA -< Num Negative
Num Negative -> returnA -< Num Negative
Num Top -> returnA -< Num Top
_ -> failA -< "Expected a number as argument for 'pred'"
zero = arr $ const (Num Zero)
ifZero f g = proc (v1, (x, y)) -> case v1 of
Num Zero -> f -< x
Num Top -> (f -< x) (g -< y)
Num _ -> g -< y
_ -> failA -< "Expected a number as condition for 'ifZero'"
closure = arr $ \(e, env) -> Closure e env
applyClosure f = proc (fun, arg) -> case (fun, arg) of
(Closure (Lam x _ body) env, Num _) -> localA f -< (M.insert x arg env, body)
_ -> failA -< "Expected a closure and a number argument"
-- TODO: instance Complete (Interp a b) where ...
module Utils where
import Control.Arrow
import Control.Monad.Trans.Reader
newtype MaybeArrow c x y = MaybeArrow { runMaybeArrow :: c x (Maybe y) }
--localA :: Interp a b -> Interp (Env, a) b
localA :: Kleisli (ReaderT env m) a b -> Kleisli (ReaderT env m) (env, a) b
localA (Kleisli inner) = Kleisli (\(env, a) -> local (const env) $ inner a)
name: sturdy-pcf
version: 0.1.0.0
license: BSD3
license-file: LICENSE
author: Sven Keidel
maintainer: s.keidel@tudelft.nl
category: Language
build-type: Simple
extra-source-files:
cabal-version: >=1.10
library
exposed-modules: Concrete,
Interval,
PCF,
Shared,
Sign,
Utils
build-depends: base,
containers,
mtl,
sturdy-lib,
text,
transformers
hs-source-dirs: src
default-language: Haskell2010
test-suite specs
type: exitcode-stdio-1.0
ghc-options: -Wall
hs-source-dirs: test
main-is: Spec.hs
build-depends: base,
containers,
hspec,
mtl,
pretty,
sturdy-lib,
sturdy-pcf,
text
default-language: Haskell2010
module ConcreteSpec where
import qualified Data.Map as M
import qualified Data.Text as T
import qualified PCF as E
import Concrete
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec = describe "evalConcrete" $ do
it "should look up a bound variable" $
let x = T.singleton 'x' in
evalConcrete (M.insert x (Num 3) M.empty) (E.Var x) `shouldBe` Just (Num 3)
it "should fail when looking up an unbound variable" $
let x = T.singleton 'x' in
evalConcrete M.empty (E.Var x) `shouldBe` Nothing
it "should create a closure of a FunT" $
let x = T.singleton 'x'
cls = E.Lam x (E.FunT E.NumT E.NumT) (E.Succ (E.Var x)) in
evalConcrete M.empty cls
`shouldBe` Just (Closure cls M.empty)
it "should create a closure of a NumT" $
let x = T.singleton 'x'
cls = E.Lam x E.NumT (E.Var x) in
evalConcrete M.empty cls
`shouldBe` Just (Closure cls M.empty)
it "should apply a function" $
let x = T.singleton 'x'
cls = E.Lam x (E.FunT E.NumT E.NumT) (E.Succ (E.Var x)) in
evalConcrete M.empty (E.App cls E.Zero)
`shouldBe` Just (Num 1)
it "should fail when applying something other than a function" $
evalConcrete M.empty (E.App E.Zero E.Zero) `shouldBe` Nothing
--it "will recurse infinitely when using Y" $
-- evalConcrete M.empty (E.Y (E.Succ E.Zero)) `shouldBe` Just (Num 1)
it "should give zero" $
evalConcrete M.empty E.Zero `shouldBe` Just (Num 0)
it "should give succ of zero" $
evalConcrete M.empty (E.Succ E.Zero) `shouldBe` Just (Num 1)
it "should give succ of succ of zero" $
evalConcrete M.empty (E.Succ (E.Succ E.Zero)) `shouldBe` Just (Num 2)
it "should give pred of zero" $
evalConcrete M.empty (E.Pred E.Zero) `shouldBe` Just (Num (-1))
it "should give pred of pred of zero" $
evalConcrete M.empty (E.Pred (E.Pred E.Zero)) `shouldBe` Just (Num (-2))
it "should give pred of succ of 0" $
evalConcrete M.empty (E.Pred (E.Succ E.Zero)) `shouldBe` Just (Num 0)
it "should give succ of pred of 0" $
evalConcrete M.empty (E.Succ (E.Pred E.Zero)) `shouldBe` Just (Num 0)
it "should execute the then branch on IfZero on zero" $
evalConcrete M.empty (E.IfZero E.Zero (E.Succ E.Zero) E.Zero)
`shouldBe` Just (Num 1)
it "should execute the else branch on IfZero on non-zero" $
evalConcrete M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
`shouldBe` Just (Num 0)
-- TODO: fibonacci
module IntervalSpec where
import qualified Data.Map as M
import qualified Data.Text as T
import qualified PCF as E
import Interval
import Shared
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec = describe "evalInterval" $ do
it "should look up a bound variable" $
let x = T.singleton 'x' in
evalInterval (M.insert x (Num (IV (2, 5))) M.empty) (E.Var x) `shouldBe` Just (Num (IV (2, 5)))
it "should fail when looking up an unbound variable" $
let x = T.singleton 'x' in
evalInterval M.empty (E.Var x) `shouldBe` Nothing
it "should create a closure of a FunT" $
let x = T.singleton 'x'
cls = E.Lam x (E.FunT E.NumT E.NumT) (E.Succ (E.Var x)) in
evalInterval M.empty cls
`shouldBe` Just (Closure cls M.empty)
it "should create a closure of a NumT" $
let x = T.singleton 'x'
cls = E.Lam x E.NumT (E.Var x) in
evalInterval M.empty cls
`shouldBe` Just (Closure cls M.empty)
it "should apply a function" $
let x = T.singleton 'x'
cls = E.Lam x (E.FunT E.NumT E.NumT) (E.Succ (E.Var x)) in
evalInterval M.empty (E.App cls E.Zero)
`shouldBe` Just (Num (IV (1, 1)))
it "should fail when applying something other than a function" $
evalInterval M.empty (E.App E.Zero E.Zero) `shouldBe` Nothing
--it "will recurse infinitely when using Y" $
-- evalInterval M.empty (E.Y (E.Succ E.Zero)) `shouldBe` Just (Num (IV (1, 1)))
it "should correctly give the interval of zero" $
evalInterval M.empty E.Zero `shouldBe` Just (Num (IV (0, 0)))
it "should correctly give the interval of succ of 0" $
evalInterval M.empty (E.Succ E.Zero)
`shouldBe`
Just (Num (IV (1, 1)))
it "should correctly give the interval of succ of succ of 0" $
evalInterval M.empty (E.Succ (E.Succ E.Zero))
`shouldBe`
Just (Num (IV (2, 2)))
it "should correctly give the interval of pred of 0" $
evalInterval M.empty (E.Pred E.Zero)
`shouldBe`
Just (Num (IV ((-1), (-1))))
it "should correctly give the interval of pred of pred of 0" $
evalInterval M.empty (E.Pred (E.Pred E.Zero))
`shouldBe`
Just (Num (IV ((-2), (-2))))
it "should correctly give the interval of pred of succ of 0" $
evalInterval M.empty (E.Pred (E.Succ E.Zero))
`shouldBe`
Just (Num (IV (0, 0)))
it "should correctly give the interval of succ of pred of 0" $
evalInterval M.empty (E.Succ (E.Pred E.Zero))
`shouldBe`
Just (Num (IV (0, 0)))
it "should execute the then branch on IfZero on zero" $
evalInterval M.empty (E.IfZero E.Zero (E.Succ E.Zero) E.Zero)
`shouldBe` Just (Num (IV (1, 1)))
it "should execute the else branch on IfZero on completely non-zero" $
evalInterval M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
`shouldBe` Just (Num (IV (0, 0)))
-- TODO: it seems that the current implementation cannot ever get here.
it "should execute both branches on IfZero on interval containing zero" $
--evalInterval M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
-- `shouldBe` Just (Num (IV (0, 0)))
pendingWith "it seems that the current implementation cannot ever get here"
-- TOOD: fibonacci
module SignSpec where
import qualified Data.Map as M
import qualified Data.Text as T
import qualified PCF as E
import Sign
import Shared
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec = describe "evalSign" $ do
it "should look up a bound variable" $
let x = T.singleton 'x' in
evalSign (M.insert x (Num Positive) M.empty) (E.Var x) `shouldBe` Just (Num Positive)
it "should fail when looking up an unbound variable" $
let x = T.singleton 'x' in
evalSign M.empty (E.Var x) `shouldBe` Nothing
it "should create a closure of a FunT" $
let x = T.singleton 'x'
cls = E.Lam x (E.FunT E.NumT E.NumT) (E.Succ (E.Var x)) in
evalSign M.empty cls
`shouldBe` Just (Closure cls M.empty)
it "should create a closure of a NumT" $
let x = T.singleton 'x'
cls = E.Lam x E.NumT (E.Var x) in
evalSign M.empty cls
`shouldBe` Just (Closure cls M.empty)
it "should apply a function" $
let x = T.singleton 'x'
cls = E.Lam x (E.FunT E.NumT E.NumT) (E.Succ (E.Var x)) in
evalSign M.empty (E.App cls E.Zero)
`shouldBe` Just (Num Positive)
it "should fail when applying something other than a function" $
evalSign M.empty (E.App E.Zero E.Zero) `shouldBe` Nothing
--it "will recurse infinitely when using Y" $
-- evalSign M.empty (E.Y (E.Succ E.Zero)) `shouldBe` Just (Num 1)
it "should correctly give the sign of zero" $
evalSign M.empty E.Zero `shouldBe` Just (Num Zero)
it "should correctly give the sign of succ of 0" $
evalSign M.empty (E.Succ E.Zero)
`shouldBe`
Just (Num Positive)
it "should correctly give the sign of succ of succ of 0" $
evalSign M.empty (E.Succ (E.Succ E.Zero))
`shouldBe`
Just (Num Positive)
it "should correctly give the sign of pred of 0" $
evalSign M.empty (E.Pred E.Zero)
`shouldBe`
Just (Num Negative)
it "should correctly give the sign of pred of pred of 0" $
evalSign M.empty (E.Pred (E.Pred E.Zero))
`shouldBe`
Just (Num Negative)
it "should correctly overapproximate the sign of pred of succ of 0" $
evalSign M.empty (E.Pred (E.Succ E.Zero))
`shouldBe`
Just (Num Top)
it "should correctly overapproximate the sign of succ of pred of 0" $
evalSign M.empty (E.Succ (E.Pred E.Zero))
`shouldBe`
Just (Num Top)
it "should execute the then branch on IfZero on zero" $
evalSign M.empty (E.IfZero E.Zero (E.Succ E.Zero) E.Zero)
`shouldBe` Just (Num Positive)
it "should execute the else branch on IfZero on non-zero" $
evalSign M.empty (E.IfZero (E.Succ E.Zero) (E.Succ E.Zero) E.Zero)
`shouldBe` Just (Num Zero)
-- TODO: fibonacci
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
......@@ -2,6 +2,7 @@ flags: {}
extra-package-dbs: []
packages:
- 'lib'
- 'pcf'
- 'while'
#- 'stratego'
extra-deps:
......
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