Commit 32fed9f3 authored by Sven Keidel's avatar Sven Keidel

rename arrow transformers

parent f5e18682
......@@ -5,3 +5,5 @@
/.idea
.DS_Store
cabal.config
cabal.project.local
.ghc.environment.*
Copyright (c) 2017-2018, the Sturdy contributors
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.
{ pkgs ? import <nixpkgs> {} }:
let
hsEnv = pkgs.haskellPackages.ghcWithPackages(p: with p; [
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion fgl arrows
(p.callPackage ../lib/default.nix { })
(p.callPackage ../rtg/default.nix { })
]);
in pkgs.stdenv.mkDerivation {
name = "sturdy-lambda-adt";
version = "0.0.1";
src = ./.;
buildInputs = [
hsEnv
];
}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeSynonymInstances#-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Abstract where
import TreeAutomata (Grammar)
import qualified TreeAutomata as G
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Try
import Control.Arrow.Utils
import Control.Monad.Reader
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Text (Text)
import Data.Error
import Data.Order
import Text.Printf
import GHC.Generics (Generic)
import Shared
data Closure = Closure Text Expr Env deriving (Eq,Show)
data Val = Bot | ClsV [Closure] | ConV Grammar | Top deriving (Eq,Show)
type Env = HashMap Text Val
type Interp = Kleisli (ReaderT Env (Error String))
evalAbs :: Env -> Expr -> Error String Val
evalAbs env e = runReaderT (runKleisli eval e) env
instance ArrowFix Expr Val Interp where
fixA f = f (fixA f)
instance IsVal Val Interp where
lookup = proc x -> do
env <- askA -< ()
case M.lookup x env of
Just v -> returnA -< v
Nothing -> failA -< printf "Variable %s not bound." x
con = _
match ev = _
instance IsClosure Expr Val Interp where
closure = proc (x,body) -> do
env <- askA -< ()
returnA -< ClsV (return (Closure x body env))
applyClosure f = proc (fun, arg) -> case fun of
ClsV cls -> lubA (proc (Closure x body env) -> localA f -< (M.insert x arg env, body)) -<< cls
_ -> failA -< "Expected a closure"
instance PreOrd Closure where
Closure g1 Closure g2 = _
instance PreOrd Val where
Bot _ = True
_ Top = True
ClsV c1 ClsV c2 = all (\c -> any (c ) c1) c1
ConV g1 ConV g2 = _
instance Complete Val where
() = _
instance LowerBounded Val where
bottom = Bot
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Arrows #-}
module Concrete where
import Prelude
import Shared
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Try
import Control.Arrow.Utils
import Control.Monad.Reader
import Data.Map (Map)
import qualified Data.Map as M
import Data.Text (Text,unpack)
import Text.Printf
data Val = ClsV Text Expr Env | ConV Constructor [Val] deriving (Eq)
type Env = Map Text Val
type Interp = Kleisli (ReaderT Env (Either String))
evalConcrete :: Env -> Expr -> Either String Val
evalConcrete env e = runReaderT (runKleisli eval e) env
instance ArrowFix Expr Val Interp where
fixA f = f (fixA f)
instance IsVal Val Interp where
lookup = proc x -> do
env <- askA -< ()
case M.lookup x env of
Just v -> returnA -< v
Nothing -> failA -< printf "Variable %s not bound." x
con = arr (uncurry ConV)
match ev =
arr (\(v,ps) -> [(v,p,e) | (p,e) <- ps]) >>>
tryFirst (proc (v,p,e) -> do
env <- askA -< ()
(env',()) <- runStateArrow go -< (env,(v,p))
localA ev -< (env',e))
(proc () -> failA -< "no pattern matched")
where
go :: StateArrow Env Interp (Val,Pat) ()
go = proc (v,p) -> case (v,p) of
(ClsV {},_) -> failA -< "Cannot match against a closures"
(ConV x vs, ConP y ps)
| x == y -> voidA $ zipWithA go -< (vs,ps)
| otherwise -> failA -< "Pattern does not match"
(_, VarP x) -> modifyA insertVar -< (x,v)
insertVar :: Arrow c => c ((Text,Val),Env) Env
insertVar = arr $ uncurry $ uncurry M.insert
instance IsClosure Expr Val Interp where
closure = proc (x,body) ->do
env <- askA -< ()
returnA -< ClsV x body env
applyClosure ev = proc (cls,arg) -> case cls of
ClsV x body env -> localA ev -< (M.insert x arg env,body)
_ -> failA -< printf "Expected a closure, but got %s" (show cls)
instance Show Val where
show (ClsV x e _) = "λ" ++ unpack x ++ ". " ++ show e
show (ConV c ts) = show c ++ show ts
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DeriveGeneric #-}
module Shared where
import Prelude hiding (lookup)
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.Utils
import Data.String
import Data.Hashable
import Data.Text (Text,unpack)
import GHC.Generics (Generic)
newtype Constructor = Constructor Text
deriving (Ord, Eq, IsString, Generic, Hashable)
data Expr
= Var Text
| Lam Text Expr
| App Expr Expr
| Con Constructor [Expr]
| Case Expr [(Pat,Expr)]
deriving (Eq, Generic)
data Pat
= ConP Constructor [Pat]
| VarP Text
deriving (Eq, Generic)
eval :: (ArrowReader env c, ArrowChoice c, ArrowFix Expr v c, IsVal v c, IsClosure Expr v c) => c Expr v
eval = fixA $ \ev -> proc e0 -> case e0 of
Var x -> lookup -< x
Lam x body -> closure -< (x,body)
App e1 e2 -> do
fun <- ev -< e1
arg <- ev -< e2
applyClosure ev -< (fun, arg)
Con c es -> do
vs <- mapA ev -< es
con -< (c,vs)
Case e cases -> do
v <- ev -< e
match ev -< (v,cases)
class Arrow c => IsVal v c | c -> v where
lookup :: c Text v
con :: c (Constructor,[v]) v
match :: c Expr v -> c (v,[(Pat,Expr)]) v
class Arrow c => IsClosure exp v c where
closure :: c (Text,exp) v
applyClosure :: c exp v -> c (v, v) v
instance IsString Expr where
fromString = Var . fromString
instance Show Expr where
showsPrec d e0 = case e0 of
Var x -> showString $ unpack x
Lam x e -> showParen (d > appPrec) $ showString ("λ" ++ unpack x ++ ". ") . shows e
App e1 e2 -> showParen (d > appPrec) $ showsPrec (appPrec + 1) e1 . showString " " . showsPrec (appPrec + 1) e2
Con x t -> showParen (d > appPrec) $ shows x . showString " " . showsPrec d t
Case e cases -> showString "case " . shows e . showString " of " . showList cases
where appPrec = 10
instance Show Pat where
showsPrec d e0 = case e0 of
VarP x -> showString $ unpack x
ConP x t -> showParen (d > appPrec) $ shows x . showString " " . showsPrec d t
where appPrec = 10
instance IsString Pat where
fromString = VarP . fromString
instance Show Constructor where
show (Constructor c) = unpack c
instance Hashable Expr
instance Hashable Pat
name: sturdy-lambda-adt
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
ghc-options: -Wall
exposed-modules: Shared,
Concrete
build-depends: base,
containers,
hashable,
mtl,
sturdy-lib,
text
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,
sturdy-lambda-adt
default-language: Haskell2010
{-# LANGUAGE OverloadedStrings #-}
module ConcreteSpec where
import Prelude hiding (map,succ)
import qualified Data.Map as M
import Shared
import Concrete
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec = describe "evalConcrete" $ do
let map = (fix (Lam "map" (Lam "f" (Lam "l" (Case (Var "l")
[(ConP "Nil" [], list []),
(ConP "Cons" ["x","xs"], Con "Cons" [App "f" "x", App (App "map" "f") "xs"])])))))
it "'map (+1)' should increase the number of each element of a list" $
evalConcrete M.empty (App (App map plusOne) (list [one,three,two]))
`shouldBe` Right (litV (list [two,four,three]))
where
-- Call-by-value fixpoint combinator
fix = App (Lam "f" (App (Lam "x" (App "f" (Lam "v" (App (App "x" "x") "v")))) (Lam "x" (App "f" (Lam "v" (App (App "x" "x") "v"))))))
zero = Con "Z" []
succ x = Con "S" [x]
one = succ zero
two = succ one
three = succ two
four = succ three
plusOne = Lam "x" (Con "S" ["x"])
list [] = Con "Nil" []
list (x:xs) = Con "Cons" [x,list xs]
litV (Con c ts) = ConV c (fmap litV ts)
litV _ = error "can only convert literals"
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Conditional where
import Control.Arrow
import GHC.Exts(Constraint)
-- | Arrow based interface to implement conditionals.
class Arrow c => ArrowCond v x y z c where
class Arrow c => ArrowCond v c | c -> v where
type family Join (c :: * -> * -> *) x y :: Constraint
-- | Performs a case distinction on the given value 'v'. In one case
-- the first continuation is called and in the other case the second
-- continuation. An abstract instance might join on the result type 'z'.
if_ :: c x z -> c y z -> c (v, (x, y)) z
if_ :: Join c (x,y) z => c x z -> c y z -> c (v, (x, y)) z
......@@ -3,6 +3,8 @@
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Control.Arrow.Environment where
import Prelude hiding (lookup,fail)
......@@ -11,15 +13,21 @@ import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Utils
import Text.Printf
import Data.String
import Text.Printf
import GHC.Exts (Constraint)
-- | Arrow-based interface for interacting with environments.
class Arrow c => ArrowEnv var val env c | c -> var, c -> val, c -> env where
type family Join (c :: * -> * -> *) x y :: Constraint
-- | Lookup a variable in the current environment. The first
-- continuation is called if the variable is in the enviroment, the
-- second if it is not.
lookup :: c (val,x) y -> c x y -> c (var,x) y
lookup :: (Join c ((val,x),x) y) => c (val,x) y -> c x y -> c (var,x) y
-- | Retrieve the current environment.
getEnv :: c () env
-- | Extend an environment with a binding.
......@@ -28,7 +36,7 @@ class Arrow c => ArrowEnv var val env c | c -> var, c -> val, c -> env where
localEnv :: c x y -> c (env,x) y
-- | Simpler version of environment lookup.
lookup' :: (Show var, IsString e, ArrowFail e c, ArrowEnv var val env c) => c var val
lookup' :: (Join c ((val,var),var) val, Show var, IsString e, ArrowFail e c, ArrowEnv var val env c) => c var val
lookup' = proc var ->
lookup
(proc (val,_) -> returnA -< val)
......
......@@ -3,42 +3,49 @@
{-# LANGUAGE Arrows #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
module Control.Arrow.Except where
import Prelude hiding (id,(.))
import Control.Category
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Utils
import GHC.Exts(Constraint)
-- | Arrow-based interface for exception handling.
class ArrowFail e c => ArrowExcept x y e c | c -> e where
class Arrow c => ArrowExcept e c | c -> e where
type family Join (c :: * -> * -> *) x y :: Constraint
throw :: c e a
-- | Executes the first computation. If it fails, the exception is
-- handled with the second computation.
tryCatch :: c x y -> c (x,e) y -> c x y
catch :: Join c (x,(x,e)) y => c x y -> c (x,e) y -> c x y
-- | Executes the second computation, no matter if the first
-- computation fails or not.
finally :: c x y -> c x u -> c x y
tryCatch' :: ArrowExcept x y e c => c x y -> c e y -> c x y
tryCatch' f g = tryCatch f (pi2 >>> g)
catch' :: (Join c (x,(x,e)) y, ArrowExcept e c) => c x y -> c e y -> c x y
catch' f g = catch f (pi2 >>> g)
-- | 'tryA f g h' Executes 'f', if it succeeds the result is passed to
-- | 'try f g h' Executes 'f', if it succeeds the result is passed to
-- 'g', if it fails the original input is passed to 'h'.
tryA :: ArrowExcept x z e c => c x y -> c y z -> c x z -> c x z
tryA f g h = tryCatch (f >>> g) (pi1 >>> h)
try :: (Join c (x,(x,e)) z, ArrowExcept e c) => c x y -> c y z -> c x z -> c x z
try f g h = catch (f >>> g) (pi1 >>> h)
-- | Picks the first successful computation.
(<+>) :: ArrowExcept x y e c => c x y -> c x y -> c x y
f <+> g = tryCatch f (pi1 >>> g)
(<+>) :: (Join c (x,(x,e)) y, ArrowExcept e c) => c x y -> c x y -> c x y
f <+> g = catch f (pi1 >>> g)
tryFirst :: (ArrowChoice c, ArrowExcept (x, [x]) y e c) => c x y -> c () y -> c [x] y
tryFirst :: (Join c ((x,[x]),((x,[x]),e)) y, ArrowChoice c, ArrowExcept e c) => c x y -> c () y -> c [x] y
tryFirst f g = proc l -> case l of
[] -> g -< ()
a:as -> tryA (f . pi1) id (tryFirst f g . pi2) -< (a,as)
a:as -> try (f . pi1) id (tryFirst f g . pi2) -< (a,as)
-- | A computation that always succeeds
success :: ArrowExcept a a e c => c a a
success :: ArrowExcept e c => c a a
success = id
......@@ -2,6 +2,7 @@
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Arrows #-}
module Control.Arrow.Store where
......@@ -11,25 +12,23 @@ import Control.Arrow
import Control.Arrow.Fail
import Text.Printf
import Data.String
import GHC.Exts(Constraint)
-- | Arrow-based interface to describe computations that read from a store.
-- The parameter `y` needs to be exposed, because abstract instances
-- may need to join on `y`.
class Arrow c => ArrowRead var val x y c where
class Arrow c => ArrowStore var val c | c -> var, c -> val where
type family Join (c :: * -> * -> *) x y :: Constraint
-- | Reads a value from the store. Fails if the binding is not in the current store.
read :: c (val,x) y -> c x y -> c (var,x) y
read :: Join c ((val,x),x) y => c (val,x) y -> c x y -> c (var,x) y
-- | Writes a value to the store.
write :: c (var,val) ()
-- | Simpler version of 'read'
read' :: (Show var, IsString e, ArrowFail e c, ArrowRead var val var val c) => c var val
read' :: (Show var, Join c ((val,var),var) val, IsString e, ArrowFail e c, ArrowStore var val c) => c var val
read' = proc var ->
read (proc (val,_) -> returnA -< val)
(proc var -> fail -< fromString $ printf "variable %s not bound" (show var))
-< (var,var)
-- | Arrow-based interface to describe computations that modify a store.
class Arrow c => ArrowWrite var val c where
-- | Writes a value to the store.
write :: c (var,val) ()
-- | Arrow-based interface to describe computations manipulate a store.
type ArrowStore var val c = (ArrowRead var val var val c, ArrowWrite var val c)
......@@ -8,7 +8,9 @@
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ImplicitParams #-}
module Control.Arrow.Transformer.Abstract.BoundedEnvironment(Environment,runEnvironment) where
module Control.Arrow.Transformer.Abstract.BoundedEnvironment(EnvT,runEnvT) where
import Prelude hiding ((.),id,Maybe(..))
import Control.Arrow
import Control.Arrow.Environment
......@@ -22,12 +24,12 @@ import Control.Arrow.Transformer.Const
import Control.Arrow.Transformer.Static
import Control.Arrow.Transformer.Reader
import Control.Category
import Prelude hiding ((.),id)
import Data.Order
import Data.Identifiable
import Data.Abstract.FiniteMap (Map)
import qualified Data.Abstract.FiniteMap as M
import Data.Abstract.Maybe(Maybe(..))
-- | Abstract domain for environments in which concrete environments
-- are approximated by a mapping from variables to addresses and a
......@@ -37,51 +39,53 @@ import qualified Data.Abstract.FiniteMap as M
-- Furthermore, closures and environments are defined mutually
-- recursively. By only allowing a finite number of addresses, the
-- abstract domain of closures and environments becomes finite.
newtype Environment var addr val c x y =
Environment ( Const (c (var,val,Map var addr val) addr) (Reader (Map var addr val) c) x y )
newtype EnvT var addr val c x y =
EnvT ( ConstT (c (var,val,Map var addr val) addr) (ReaderT (Map var addr val) c) x y )
runEnvironment :: (Show var, Identifiable var, Identifiable addr, Complete val, ArrowChoice c)
=> c (var,val,Map var addr val) addr -> Environment var addr val c x y -> c ([(var,val)],x) y
runEnvironment alloc f =
let Environment f' = proc (bs,x) -> do
runEnvT :: (Show var, Identifiable var, Identifiable addr, Complete val, ArrowChoice c)
=> c (var,val,Map var addr val) addr -> EnvT var addr val c x y -> c ([(var,val)],x) y
runEnvT alloc f =
let EnvT f' = proc (bs,x) -> do
env <- getEnv -< ()
env' <- bindings -< (bs,env)
localEnv f -< (env',x)
in (const (M.empty) &&& id) ^>> runReader (runConst alloc f')
in (const (M.empty) &&& id) ^>> runReaderT (runConstT alloc f')
instance ArrowLift (Environment var addr val) where
lift f = Environment (lift (lift f))
instance ArrowLift (EnvT var addr val) where
lift f = EnvT (lift (lift f))
instance (Identifiable var, Identifiable addr, Complete val, ArrowChoice c) =>
ArrowEnv var val (Map var addr val) (Environment var addr val c) where
lookup (Environment f) (Environment g) = Environment $ proc (var,x) -> do
ArrowEnv var val (Map var addr val) (EnvT var addr val c) where
type Join (EnvT var addr val c) x y = Complete (c (Map var addr val,x) y)
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- ask -< ()
case do M.lookup var env of
Just val -> f -< (val,x)
Nothing -> g -< x
getEnv = Environment ask
extendEnv = Environment $ Const $ Static $ \alloc -> lift $ M.insertBy alloc
localEnv (Environment f) = Environment $ local f
Just val -> f -< (val,x)
JustNothing val -> joined f g -< ((val,x),x)
Nothing -> g -< x
getEnv = EnvT ask
extendEnv = EnvT $ ConstT $ StaticT $ \alloc -> lift $ M.insertBy alloc
localEnv (EnvT f) = EnvT $ local f
instance ArrowReader r c => ArrowReader r (Environment var addr val c) where
instance ArrowReader r c => ArrowReader r (EnvT var addr val c) where
ask = lift ask
local (Environment (Const (Static f))) =
Environment $ Const $ Static $ \alloc -> Reader $ (\(env,(r,x)) -> (r,(env,x))) ^>> local (runReader (f alloc))
local (EnvT (ConstT (StaticT f))) =
EnvT $ ConstT $ StaticT $ \alloc -> ReaderT $ (\(env,(r,x)) -> (r,(env,x))) ^>> local (runReaderT (f alloc))
instance ArrowApply c => ArrowApply (Environment var addr val c) where
app = Environment $ (\(Environment f,x) -> (f,x)) ^>> app
instance ArrowApply c => ArrowApply (EnvT var addr val c) where
app = EnvT $ (\(EnvT f,x) -> (f,x)) ^>> app