...
 
Commits (2)
name: sturdy-jimple
version: 0.1.0.0
license: BSD3
license-file: LICENSE
author: Wouter Raateland
maintainer: Sven Keidel <svenkeidel@gmail.com>
category: Language
dependencies:
- base
- containers
- unordered-containers
- hashable
- logfloat
- mtl
- random
- sturdy-lib
- text
- vector
- vector-instances
library:
source-dirs:
- src
ghc-options: -Wall
tests:
spec:
main: Spec.hs
source-dirs:
- test
ghc-options: -Wall
dependencies:
- sturdy-pcf
- hspec
{ pkgs ? import <nixpkgs> {} }:
let
haskellPackagesWithProfiling = pkgs.haskellPackages.override {
overrides = self: super: {
mkDerivation = args: super.mkDerivation (args // {
enableLibraryProfiling = false;
});
};
};
hsEnv = haskellPackagesWithProfiling.ghcWithPackages(p: with p; [
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion fgl
(p.callPackage ../lib/default.nix { })
]);
in pkgs.stdenv.mkDerivation {
name = "sturdy-jimple";
version = "0.0.1";
src = ./.;
buildInputs = [
hsEnv
];
}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module GenericInterpreter where
import Prelude hiding (rem,mod,div,id,or,and,fail,return,map)
import Data.Text (Text)
import Data.Vector (Vector,(!?))
import qualified Data.Vector as Vec
import Data.Int
import Data.IntMap (IntMap)
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as Map
import Control.Category
import Control.Arrow
import Control.Arrow.Environment as Env
import Control.Arrow.Frame as Frame
import Control.Arrow.Except as Except
import Control.Arrow.Fail
import Control.Arrow.Fix (ArrowFix(..))
import Control.Arrow.Utils (map)
import GHC.Exts
import Syntax
data Frame val =
Frame
{ this :: val
, params :: Vector val
, locals :: HashMap Text val
, stmts :: Vector Statement
, handlers :: HashMap ClassId CatchClause
, caughtException :: Maybe val
}
type PC = Int
type StmtInterpreter c = c PC ()
type ArrowInterp val e c =
( IsString e, IsVal val c
, ArrowChoice c, ArrowReturn val c
, ArrowFrame (Frame val) c, ArrowEnv Variable val c
, ArrowExcept val c, ArrowFail e c
, ArrowFix (StmtInterpreter c)
, JoinVal () c, JoinVal val c, Env.Join val c, Except.Join () c
)
eval :: ArrowInterp val e c => StmtInterpreter c -> c Expr val
eval run' = proc expr -> case expr of
New typ -> new -< typ
NewArray typ e -> do
len <- evalImmediate -< e
newArray -< (typ,[len])
NewMultiArray typ es -> do
lens <- map evalImmediate -< es
newArray -< (typ,lens)
Cast typ e -> do
val <- evalImmediate -< e
cast -< (typ,val)
InstanceOf e typ -> do
val <- evalImmediate -< e
instanceOf -< (val,typ)
InvokeExpr method ->
evalInvoke run' -< method
Ref ref -> lookup' -< ReferenceVar ref
Binop e1 op e2 -> do
v1 <- evalImmediate -< e1
v2 <- evalImmediate -< e2
case op of
And -> and -< (v1,v2)
Or -> or -< (v1,v2)
Xor -> xor -< (v1,v2)
Rem -> rem -< (v1,v2)
Mod -> mod -< (v1,v2)
Cmp -> cmp -< (v1,v2)
Cmpl -> cmpl -< (v1,v2)
Cmpg -> cmpg -< (v1,v2)
Shl -> shl -< (v1,v2)
Shr -> shr -< (v1,v2)
Ushr -> ushr -< (v1,v2)
Plus -> plus -< (v1,v2)
Minus -> minus -< (v1,v2)
Mult -> mult -< (v1,v2)
Div -> div -< (v1,v2)
Unop op e -> do
v <- evalImmediate -< e
case op of
Lengthof -> lengthOf -< v
Neg -> neg -< v
Immediate e -> evalImmediate -< e
MethodHandle {} -> fail -< "Unsupported operation: MethodHandle"
{-# INLINE eval #-}
evalImmediate :: ArrowInterp val e c => c Immediate val
evalImmediate = proc i -> case i of
Local name -> lookup' -< LocalVar name
DoubleConstant f -> doubleConstant -< f
FloatConstant f -> floatConstant -< f
IntConstant n -> intConstant -< n
LongConstant f -> longConstant -< f
NullConstant -> nullConstant -< ()
StringConstant s -> stringConstant -< s
ClassConstant c -> classConstant -< c
{-# INLINE evalImmediate #-}
evalInvoke :: ArrowInterp val e c => StmtInterpreter c -> c Invoke val
evalInvoke run' = proc e -> case e of
InvokeVirtual obj klass methodSig args -> do
receiver <- lookup' -< obj
invoke -< (receiver,klass,methodSig,args)
InvokeSpecial obj klass methodSig args -> do
receiver <- lookup' -< obj
invoke -< (receiver,klass,methodSig,args)
InvokeInterface obj klass methodSig args -> do
receiver <- lookup' -< obj
invoke -< (receiver,klass,methodSig,args)
InvokeStatic klass methodSig args -> do
receiver <- lookup' -< StaticInstance klass
invoke -< (receiver,klass,methodSig,args)
-- InvokeDynamic {} -> fail -< "We currently do not support dynamic method lookup"
where
invoke = proc (receiver,klass,methodSig,args) -> do
argVals <- map evalImmediate -< args
lookupMethod (proc (receiver,body,argVals) -> do
let frame = Frame { this = receiver
, params = Vec.fromList argVals
, locals = Map.empty
, stmts = statements body
, handlers = catchClauses body
, caughtException = Nothing
}
newFrame (handleReturn run') -< (frame,0)
) -< (receiver,klass,methodSig,argVals)
{-# INLINE invoke #-}
{-# INLINE evalInvoke #-}
run :: ArrowInterp val e c => StmtInterpreter c
run = fix $ \run' -> handleExceptions $ proc pc -> do
let nextStmt = pc + 1
frame <- askFrame -< ()
case stmts frame !? pc of
Nothing -> returnA -< ()
Just stmt -> case stmt of
Goto lab -> run' -< lab
Label {} -> run' -< nextStmt
If e lab -> do
condition <- eval run' -< e
if_ run' run' -< (condition,(lab,nextStmt))
TableSwitch key offset cases def -> do
val <- evalImmediate -< key
tableswitch run' -< (val,offset,cases,def)
LookupSwitch key cases def -> do
val <- evalImmediate -< key
lookupswitch run' -< (val,cases,def)
Identity var ident _maybeTyp -> do
val <- lookup' -< ident
extend run' -< (LocalVar var,val,nextStmt)
Assign var e -> do
val <- eval run' -< e
extend run' -< (var,val,nextStmt)
InvokeStmt invoke -> do
evalInvoke run' -< invoke
run' -< nextStmt
Return Nothing -> returnA -< ()
Return (Just e) -> return <<< evalImmediate -< e
Throw e -> throw <<< evalImmediate -< e
Nop -> run' -< nextStmt
Breakpoint {} -> run' -< nextStmt
-- Unsupported Operations
Ret {} -> fail -< "JVM subroutines are not supported"
EnterMonitor {} -> fail -< "JVM monitor statements are not supported"
ExitMonitor {} -> fail -< "JVM monitor statements are not supported"
{-# INLINE run #-}
handleExceptions :: ArrowInterp val e c => StmtInterpreter c -> StmtInterpreter c
handleExceptions run' = catch run' $ proc (pc,exc) -> do
frame <- askFrame -< ()
matchException (proc (exc,handler) -> Env.extend run' -< (CaughtException,exc,withLabel handler)) -< (exc,pc,handlers frame)
{-# INLINE handleExceptions #-}
class ArrowReturn v c where
return :: c v x
handleReturn :: c x y -> c x v
-- | Interface for value operations.
class IsVal v c | c -> v where
-- | In case of the abstract interpreter allows to join the result
-- of an @if@ statement.
type family JoinVal x (c :: * -> * -> *) :: Constraint
if_ :: JoinVal z c => c x z -> c y z -> c (v, (x, y)) z
tableswitch :: JoinVal y c => c x y -> c (v, Int, Vector Label, Label) y
lookupswitch :: JoinVal y c => c x y -> c (v, IntMap Label, Label) y
lookupMethod :: JoinVal y c => c (v,MethodBody,x) y -> c (v,ClassId,MethodSignature,x) y
matchException :: JoinVal y c => c (v,CatchClause) y -> c (v,PC,HashMap ClassId CatchClause) y
new :: c Type v
newArray :: c (Type,[v]) v
doubleConstant :: c Double v
floatConstant :: c Float v
intConstant :: c Int32 v
longConstant :: c Int64 v
nullConstant :: c () v
stringConstant :: c Text v
classConstant :: c Text v
and :: c (v,v) v
or :: c (v,v) v
xor :: c (v,v) v
rem :: c (v,v) v
mod :: c (v,v) v
cmp :: c (v,v) v
cmpg :: c (v,v) v
cmpl :: c (v,v) v
shl :: c (v,v) v
shr :: c (v,v) v
ushr :: c (v,v) v
plus :: c (v,v) v
minus :: c (v,v) v
mult :: c (v,v) v
lengthOf :: c v v
div :: c (v,v) v
neg :: c v v
cast :: c (Type,v) v
instanceOf :: c (v,Type) v
This diff is collapsed.
This diff is collapsed.
name: sturdy-jimple
version: 0.1.0.0
license: BSD3
license-file: LICENSE
author: Wouter Raateland
maintainer: wouterraateland@gmail.com
category: Language
build-type: Simple
extra-source-files:
cabal-version: >=1.10
cabal-version: 1.12
-- This file has been generated from package.yaml by hpack version 0.33.0.
--
-- see: https://github.com/sol/hpack
--
-- hash: 683be31214f2b83403a0b2eddd3a28777bcd124ce83864dfbda0e2595288614d
name: sturdy-jimple
version: 0.1.0.0
category: Language
author: Wouter Raateland
maintainer: Sven Keidel <svenkeidel@gmail.com>
license: BSD3
license-file: LICENSE
build-type: Simple
library
exposed-modules: ConcreteSemantics,
-- IntervalSemantics,
NullnessSemantics,
SharedSemantics,
Syntax,
Data.Concrete.Exception
Data.Abstract.Exception
ghc-options: -Wall
build-depends: base,
containers,
hashable,
mtl,
random,
logfloat,
sturdy-lib,
text,
QuickCheck
hs-source-dirs: src
default-language: Haskell2010
exposed-modules:
ConcreteSemantics
Data.Abstract.Exception
Data.Concrete.Exception
GenericInterpreter
IntervalSemantics
NullnessSemantics
Syntax
other-modules:
Paths_sturdy_jimple
hs-source-dirs:
src
ghc-options: -Wall
build-depends:
base
, containers
, hashable
, logfloat
, mtl
, random
, sturdy-lib
, text
, unordered-containers
, vector
, vector-instances
default-language: Haskell2010
test-suite specs
type: exitcode-stdio-1.0
ghc-options: -Wall
hs-source-dirs: test
main-is: Spec.hs
other-modules: ConcreteSpec,
-- IntervalSpec,
NullnessSpec,
JimpleSoundness,
Soundness,
Utils,
Java.Lang.ArithmeticException,
Java.Lang.ArrayIndexOutOfBoundsException,
Java.Lang.ClassCastException,
Java.Lang.IllegalArgumentException,
Java.Lang.NullPointerException,
Java.Lang.Object,
Java.Lang.Throwable,
Classes.FactorialExample,
Classes.ArrayFieldExample,
Classes.SingleMethodExample,
Classes.PersonExample,
Classes.TryCatchExample
build-depends: base,
containers,
hashable,
logfloat,
hspec,
hspec-core,
sturdy-lib,
sturdy-jimple,
text,
QuickCheck
default-language: Haskell2010
test-suite spec
type: exitcode-stdio-1.0
main-is: Spec.hs
other-modules:
Classes.ArrayFieldExample
Classes.FactorialExample
Classes.PersonExample
Classes.SingleMethodExample
Classes.TryCatchExample
ConcreteSpec
IntervalSpec
Java.Lang.ArithmeticException
Java.Lang.ArrayIndexOutOfBoundsException
Java.Lang.ClassCastException
Java.Lang.IllegalArgumentException
Java.Lang.NullPointerException
Java.Lang.Object
Java.Lang.Throwable
JimpleSoundness
NullnessSpec
Soundness
Utils
Paths_sturdy_jimple
hs-source-dirs:
test
ghc-options: -Wall
build-depends:
base
, containers
, hashable
, hspec
, logfloat
, mtl
, random
, sturdy-lib
, sturdy-pcf
, text
, unordered-containers
, vector
, vector-instances
default-language: Haskell2010
......@@ -11,16 +11,16 @@ import Data.Profunctor
import GHC.Exts
class (Arrow c, Profunctor c) => ArrowClosure expr cls c | cls -> expr where
type Join y c :: Constraint
type Join y cls c :: Constraint
-- | creates a non-recursive closure from expression.
closure :: c expr cls
-- | Apply a closure in its closed environment.
apply :: Join y c => c (expr,x) y -> c (cls, x) y
apply :: Join y cls c => c (expr,x) y -> c (cls, x) y
-- default lifting
default closure :: (c ~ (t c'), ArrowLift t, ArrowClosure expr cls c') => c expr cls
default closure :: (c ~ t c', ArrowLift t, ArrowClosure expr cls c') => c expr cls
closure = lift' closure
{-# INLINE closure #-}
......
{-# LANGUAGE FunctionalDependencies #-}
module Control.Arrow.Frame where
import Control.Arrow
import Data.Profunctor
class (Arrow c, Profunctor c) => ArrowFrame frame c | c -> frame where
newFrame :: c x y -> c (frame,x) y
askFrame :: c () frame
......@@ -25,10 +25,10 @@ class (Arrow c, Profunctor c) => ArrowStore var val c | c -> var, c -> val where
-- | Writes a value to the store.
write :: c (var,val) ()
-- | Simpler version of 'read'
read' :: (Show var, Join val c, 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)
{-# INLINE read' #-}
......@@ -43,20 +43,20 @@ import Data.Coerce
import GHC.Exts
newtype EnvT (env :: k1 -> k2 -> *) var val c x y = EnvT (ReaderT (env var val) c x y)
newtype EnvT env c x y = EnvT (ReaderT env c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,ArrowLowerBounded, ArrowComplete z,
ArrowState s, ArrowFail e, ArrowExcept e, ArrowStore var' val', ArrowConst k, ArrowRun, ArrowCont)
runEnvT :: EnvT env var val c x y -> c (env var val,x) y
runEnvT :: EnvT env c x y -> c (env,x) y
runEnvT = coerce
{-# INLINE runEnvT #-}
runEnvT' :: (IsList (env var val), Item (env var val) ~ (var,val), Profunctor c) => EnvT env var val c x y -> c ([(var,val)],x) y
runEnvT' :: (IsList env, Item env ~ (var,val), Profunctor c) => EnvT env c x y -> c ([(var,val)],x) y
runEnvT' f = lmap (first fromList) (runEnvT f)
{-# INLINE runEnvT' #-}
instance (Identifiable var, UpperBounded val, ArrowChoice c, Profunctor c) => ArrowEnv var val (EnvT SM.Map var val c) where
type Join y (EnvT SM.Map var val c) = ArrowComplete y c
instance (Identifiable var, UpperBounded val, ArrowChoice c, Profunctor c) => ArrowEnv var val (EnvT (SM.Map var val) c) where
type Join y (EnvT (SM.Map var val) c) = ArrowComplete y c
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- Reader.ask -< ()
case SM.lookup' var env of
......@@ -69,8 +69,8 @@ instance (Identifiable var, UpperBounded val, ArrowChoice c, Profunctor c) => Ar
{-# INLINE lookup #-}
{-# INLINE extend #-}
instance (Identifiable var, Traversable val, Complete (val (Set var)), ArrowChoice c, Profunctor c) => ArrowEnv var (val (FM.Env var val)) (EnvT FM.Env var val c) where
type Join y (EnvT FM.Env var val c) = ArrowComplete y c
instance (Identifiable var, Traversable val, Complete (val (Set var)), ArrowChoice c, Profunctor c) => ArrowEnv var (val (FM.Env var val)) (EnvT (FM.Env var val) c) where
type Join y (EnvT (FM.Env var val) c) = ArrowComplete y c
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- Reader.ask -< ()
case FM.lookup var env of
......@@ -83,14 +83,14 @@ instance (Identifiable var, Traversable val, Complete (val (Set var)), ArrowChoi
{-# INLINE lookup #-}
{-# INLINE extend #-}
instance (Identifiable var, Traversable val, Complete (val (Set var)), ArrowChoice c, Profunctor c) => ArrowLetRec var (val (FM.Env var val)) (EnvT FM.Env var val c) where
instance (Identifiable var, Traversable val, Complete (val (Set var)), ArrowChoice c, Profunctor c) => ArrowLetRec var (val (FM.Env var val)) (EnvT (FM.Env var val) c) where
letRec (EnvT f) = EnvT $ proc (ls,x) -> do
env <- Reader.ask -< ()
Reader.local f -< (FM.insertRec ls env,x)
{-# INLINE letRec #-}
instance (Identifiable expr, ArrowLowerBounded c, ArrowChoice c, Profunctor c) => ArrowClosure expr (Closure expr (env var val)) (EnvT env var val c) where
type Join y (EnvT env var val c) = ArrowComplete y c
instance (Identifiable expr, ArrowLowerBounded c, ArrowChoice c, Profunctor c) => ArrowClosure expr (Closure expr env) (EnvT env c) where
type Join y (Closure expr env) (EnvT env c) = ArrowComplete y c
closure = EnvT $ proc expr -> do
env <- Reader.ask -< ()
returnA -< Abs.closure expr env
......@@ -99,15 +99,15 @@ instance (Identifiable expr, ArrowLowerBounded c, ArrowChoice c, Profunctor c) =
{-# INLINE closure #-}
{-# INLINE apply #-}
instance (ArrowApply c, Profunctor c) => ArrowApply (EnvT env var val c) where
instance (ArrowApply c, Profunctor c) => ArrowApply (EnvT env c) where
app = EnvT (app .# first coerce)
{-# INLINE app #-}
instance ArrowReader r c => ArrowReader r (EnvT env var val c) where
instance ArrowReader r c => ArrowReader r (EnvT env c) where
ask = lift' Reader.ask
local f = lift $ lmap (\(env,(r,x)) -> (r,(env,x))) (Reader.local (unlift f))
{-# INLINE ask #-}
{-# INLINE local #-}
type instance Fix (EnvT env var val c) x y = EnvT env var val (Fix c (env var val,x) y)
deriving instance ArrowFix (Underlying (EnvT env var val c) x y) => ArrowFix (EnvT env var val c x y)
type instance Fix (EnvT env c) x y = EnvT env (Fix c (env,x) y)
deriving instance ArrowFix (Underlying (EnvT env c) x y) => ArrowFix (EnvT env c x y)
......@@ -78,7 +78,7 @@ instance (Identifiable var, Identifiable addr, Complete val, ArrowEffectCommutat
instance (Identifiable var, Identifiable addr, Identifiable expr, ArrowEffectCommutative c, ArrowChoice c, Profunctor c) =>
ArrowClosure expr (Closure expr (HashSet (HashMap var addr))) (EnvT var addr val c) where
type Join y (EnvT var addr val c) = Complete y
type Join y (Closure expr (HashSet (HashMap var addr))) (EnvT var addr val c) = Complete y
closure = EnvT $ proc expr -> do
env <- Reader.ask -< ()
returnA -< Cls.closure expr (Set.singleton env)
......@@ -98,7 +98,6 @@ instance (Identifiable var, Identifiable addr, Complete val, IsClosure val (Hash
Reader.local f -< (env',x)
{-# INLINE letRec #-}
instance (ArrowApply c, Profunctor c) => ArrowApply (EnvT var addr val c) where
app = EnvT (app .# first coerce)
{-# INLINE app #-}
......
......@@ -36,25 +36,25 @@ import Data.Profunctor
import Data.Profunctor.Unsafe((.#))
import Data.Coerce
newtype StoreT store var val c x y = StoreT (StateT (store var val) c x y)
newtype StoreT store c x y = StoreT (StateT store c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,
ArrowCont, ArrowConst r, ArrowReader r,
ArrowEnv var' val', ArrowClosure expr cls,
ArrowFail e, ArrowExcept e, ArrowState (store var val),
ArrowFail e, ArrowExcept e, ArrowState store,
ArrowLowerBounded, ArrowRun, ArrowJoin)
runStoreT :: StoreT store var val c x y -> c (store var val, x) (store var val, y)
runStoreT :: StoreT store c x y -> c (store, x) (store, y)
runStoreT = coerce
{-# INLINE runStoreT #-}
evalStoreT :: Profunctor c => StoreT store var val c x y -> c (store var val, x) y
evalStoreT :: Profunctor c => StoreT store c x y -> c (store, x) y
evalStoreT f = rmap pi2 (runStoreT f)
execStoreT :: Profunctor c => StoreT store var val c x y -> c (store var val, x) (store var val)
execStoreT :: Profunctor c => StoreT store c x y -> c (store, x) store
execStoreT f = rmap pi1 (runStoreT f)
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (StoreT Map var val c) where
type Join y (StoreT Map var val c) = ArrowComplete (Map var val,y) c
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (StoreT (Map var val) c) where
type Join y (StoreT (Map var val) c) = ArrowComplete (Map var val,y) c
read (StoreT f) (StoreT g) = StoreT $ proc (var,x) -> do
s <- get -< ()
case M.lookup var s of
......@@ -65,10 +65,10 @@ instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (
{-# INLINE read #-}
{-# INLINE write #-}
deriving instance (ArrowComplete (store var val,y) c) => ArrowComplete y (StoreT store var val c)
instance (ArrowApply c, Profunctor c) => ArrowApply (StoreT store var val c) where
deriving instance (ArrowComplete (store,y) c) => ArrowComplete y (StoreT store c)
instance (ArrowApply c, Profunctor c) => ArrowApply (StoreT store c) where
app = StoreT (app .# first coerce)
{-# INLINE app #-}
type instance Fix (StoreT store var val c) x y = StoreT store var val (Fix c (store var val,x) (store var val,y))
deriving instance ArrowFix (Underlying (StoreT store var val c) x y) => ArrowFix (StoreT store var val c x y)
type instance Fix (StoreT store c) x y = StoreT store (Fix c (store,x) (store,y))
deriving instance ArrowFix (Underlying (StoreT store c) x y) => ArrowFix (StoreT store c x y)
......@@ -99,7 +99,7 @@ instance (ArrowComonad f c, ArrowEnv x y c) => ArrowEnv x y (CokleisliT f c) whe
{-# INLINE extend #-}
instance (ArrowComonad f c, ArrowClosure expr cls c) => ArrowClosure expr cls (CokleisliT f c) where
type Join y (CokleisliT f c) = Cls.Join y c
type Join y cls (CokleisliT f c) = Cls.Join y cls c
apply f = lift (lmap costrength2 (Cls.apply (lmap strength2 (unlift f))))
{-# INLINE apply #-}
......
......@@ -35,20 +35,13 @@ import Data.Profunctor.Unsafe
import Data.Coerce
-- | Arrow transformer that adds an environment to a computation.
newtype EnvT var val c x y = EnvT (ReaderT (HashMap var val) c x y)
newtype EnvT env c x y = EnvT (ReaderT env c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowLift,ArrowTrans,
ArrowFail e,ArrowExcept e,ArrowState s,ArrowConst r,
ArrowStore var' val', ArrowRun)
runEnvT :: EnvT var val c x y -> c (HashMap var val,x) y
runEnvT = coerce
{-# INLINE runEnvT #-}
runEnvT' :: (Profunctor c, Identifiable var) => EnvT var val c x y -> c ([(var,val)],x) y
runEnvT' f = lmap (first M.fromList) (runEnvT f)
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowEnv var val (EnvT var val c) where
type Join y (EnvT var val c) = ()
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowEnv var val (EnvT (HashMap var val) c) where
type Join y (EnvT (HashMap var val) c) = ()
lookup (EnvT f) (EnvT g) = EnvT $ proc (var,x) -> do
env <- Reader.ask -< ()
case M.lookup var env of
......@@ -58,8 +51,8 @@ instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowEnv var val (En
env <- Reader.ask -< ()
Reader.local f -< (M.insert var val env, x)
instance (ArrowChoice c, Profunctor c) => ArrowClosure expr (Closure expr (HashMap var val)) (EnvT var val c) where
type Join y (EnvT var val c) = ()
instance (ArrowChoice c, Profunctor c) => ArrowClosure expr (Closure expr env) (EnvT env c) where
type Join y (Closure expr env) (EnvT env c) = ()
closure = EnvT $ proc expr -> do
env <- Reader.ask -< ()
returnA -< Closure expr env
......@@ -67,19 +60,19 @@ instance (ArrowChoice c, Profunctor c) => ArrowClosure expr (Closure expr (HashM
Reader.local f -< (env,(expr,x))
instance (Identifiable var, IsClosure val (HashMap var val), ArrowChoice c, Profunctor c)
=> ArrowLetRec var val (EnvT var val c) where
=> ArrowLetRec var val (EnvT (HashMap var val) c) where
letRec (EnvT f) = EnvT $ proc (bindings,x) -> do
env <- Reader.ask -< ()
let env' = foldr (\(var,val) -> M.insert var (setEnvironment env' val)) env bindings
Reader.local f -< (env',x)
instance (ArrowApply c,Profunctor c) => ArrowApply (EnvT var val c) where
instance (ArrowApply c,Profunctor c) => ArrowApply (EnvT env c) where
app = EnvT $ app .# first coerce
instance ArrowReader r c => ArrowReader r (EnvT var val c) where
instance ArrowReader r c => ArrowReader r (EnvT env c) where
ask = lift' Reader.ask
local (EnvT (ReaderT f)) = EnvT (ReaderT (lmap (\(env,(r,x)) -> (r,(env,x))) (Reader.local f)))
deriving instance ArrowFix (Underlying (EnvT var val c) x y) => ArrowFix (EnvT var val c x y)
deriving instance ArrowFix (Underlying (EnvT env c) x y) => ArrowFix (EnvT env c x y)
type instance Fix (EnvT var val c) x y = EnvT var val (Fix c (HashMap var val,x) y)
type instance Fix (EnvT env c) x y = EnvT env (Fix c (env,x) y)
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
......@@ -23,32 +22,32 @@ import Control.Arrow.Trans
import Control.Arrow.Transformer.State
import Control.Arrow.Utils
import Data.Profunctor
import Data.Profunctor.Unsafe
import Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as S
import Data.Identifiable
import Data.Coerce
-- | Arrow transformer that adds a store to a computation.
newtype StoreT var val c x y = StoreT (StateT (HashMap var val) c x y)
newtype StoreT store c x y = StoreT (StateT store c x y)
deriving (Profunctor,Category,Arrow,ArrowChoice,ArrowTrans,ArrowLift,ArrowRun,
ArrowConst r, ArrowReader r, ArrowFail e, ArrowExcept e, ArrowState (HashMap var val))
ArrowConst r, ArrowReader r, ArrowFail e, ArrowExcept e, ArrowState store)
-- | Execute a computation and only return the result value and store.
runStoreT :: StoreT var val c x y -> c (HashMap var val, x) (HashMap var val, y)
runStoreT :: StoreT store c x y -> c (store, x) (store, y)
runStoreT = coerce
{-# INLINE runStoreT #-}
-- | Execute a computation and only return the result value.
evalStoreT :: (Profunctor c) => StoreT var val c x y -> c (HashMap var val, x) y
evalStoreT :: (Profunctor c) => StoreT store c x y -> c (store, x) y
evalStoreT f = rmap pi2 (runStoreT f)
-- | Execute a computation and only return the result store.
execStoreT :: (Profunctor c) => StoreT var val c x y -> c (HashMap var val, x) (HashMap var val)
execStoreT :: (Profunctor c) => StoreT store c x y -> c (store, x) store
execStoreT f = rmap pi1 (runStoreT f)
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (StoreT var val c) where
type Join y (StoreT var val c) = ()
instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (StoreT (HashMap var val) c) where
type Join y (StoreT (HashMap var val) c) = ()
read (StoreT f) (StoreT g) = StoreT $ proc (var,x) -> do
s <- get -< ()
case S.lookup var s of
......@@ -56,7 +55,9 @@ instance (Identifiable var, ArrowChoice c, Profunctor c) => ArrowStore var val (
Nothing -> g -< x
write = StoreT $ modify $ arr (\((x,v),s) -> ((),S.insert x v s))
instance (ArrowApply c,Profunctor c) => ArrowApply (StoreT var val c) where app = StoreT ((\(StoreT f,x) -> (f,x)) ^>> app)
instance (ArrowApply c,Profunctor c) => ArrowApply (StoreT store c) where
app = StoreT (app .# first coerce)
{-# INLINE app #-}
instance ArrowFix (Underlying (StoreT var val c) x y) => ArrowFix (StoreT var val c x y)
type instance Fix (StoreT var val c) x y = StoreT var val (Fix c (HashMap var val,x) (HashMap var val,y))
instance ArrowFix (Underlying (StoreT store c) x y) => ArrowFix (StoreT store c x y)
type instance Fix (StoreT store c) x y = StoreT store (Fix c (store,x) (store,y))
......@@ -116,7 +116,7 @@ instance (ArrowMonad f c, ArrowLetRec x y c) => ArrowLetRec x y (KleisliT f c) w
{-# INLINE letRec #-}
instance (ArrowMonad f c, ArrowClosure expr cls c) => ArrowClosure expr cls (KleisliT f c) where
type Join y (KleisliT f c) = Cls.Join (f y) c
type Join y cls (KleisliT f c) = Cls.Join (f y) cls c
apply f = lift (Cls.apply (unlift f))
{-# INLINE apply #-}
......
......@@ -121,7 +121,7 @@ instance ArrowLetRec var val c => ArrowLetRec var val (NoInlineT c) where
{-# NOINLINE letRec #-}
instance ArrowClosure expr cls c => ArrowClosure expr cls (NoInlineT c) where
type Join y (NoInlineT c) = Cls.Join y c
type Join y cls (NoInlineT c) = Cls.Join y cls c
closure = lift Cls.closure
apply f = lift $ Cls.apply (unlift f)
{-# NOINLINE closure #-}
......
......@@ -125,7 +125,7 @@ instance ArrowEnv var val c => ArrowEnv var val (ReaderT r c) where
{-# INLINE extend #-}
instance ArrowClosure expr cls c => ArrowClosure expr cls (ReaderT r c) where
type Join y (ReaderT r c) = Cls.Join y c
type Join y cls (ReaderT r c) = Cls.Join y cls c
apply f = lift $ lmap shuffle1 $ Cls.apply (lmap shuffle1 (unlift f))
{-# INLINE apply #-}
......
......@@ -146,7 +146,7 @@ instance (ArrowEnv var val c) => ArrowEnv var val (StateT s c) where
{-# INLINE extend #-}
instance ArrowClosure expr cls c => ArrowClosure expr cls (StateT s c) where
type Join y (StateT s c) = Cls.Join (s,y) c
type Join y cls (StateT s c) = Cls.Join (s,y) cls c
apply f = lift $ lmap shuffle1 (Cls.apply (lmap shuffle1 (unlift f)))
{-# INLINE apply #-}
......
......@@ -138,7 +138,7 @@ instance (Applicative f, ArrowEnv var val c) => ArrowEnv var val (StaticT f c) w
{-# SPECIALIZE instance ArrowEnv var val c => ArrowEnv var val (StaticT ((->) r) c) #-}
instance (Applicative f, ArrowClosure expr cls c) => ArrowClosure expr cls (StaticT f c) where
type Join y (StaticT f c) = Cls.Join y c
type Join y cls (StaticT f c) = Cls.Join y cls c
apply (StaticT f) = StaticT $ Cls.apply <$> f
{-# INLINE apply #-}
{-# SPECIALIZE instance ArrowClosure expr cls c => ArrowClosure expr cls (StaticT ((->) r) c) #-}
......
......@@ -140,7 +140,7 @@ instance (Monoid w, ArrowEnv var val c) => ArrowEnv var val (WriterT w c) where
{-# INLINE extend #-}
instance (Monoid w, ArrowClosure expr cls c) => ArrowClosure expr cls (WriterT w c) where
type Join y (WriterT w c) = Cls.Join (w,y) c
type Join y cls (WriterT w c) = Cls.Join (w,y) cls c
apply f = lift (Cls.apply (unlift f))
{-# INLINE apply #-}
......
......@@ -39,7 +39,7 @@ data Val = NumVal Int | ClosureVal Cls deriving (Eq,Generic)
-- implemented by instantiating the shared semantics with the concrete
-- interpreter arrow `Interp`.
evalConcrete :: [(Text,Val)] -> State Label Expr -> Error String Val
evalConcrete env e = run (eval :: ValueT Val (EnvT Text Val (FailureT String (->))) Expr Val) (M.fromList env,generate e)
evalConcrete env e = run (eval :: ValueT Val (EnvT Env (FailureT String (->))) Expr Val) (M.fromList env,generate e)
-- | Concrete instance of the interface for value operations.
instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c) => IsVal Val (ValueT Val c) where
......@@ -62,7 +62,7 @@ instance (ArrowClosure Expr Cls c, ArrowChoice c, ArrowFail String c) => IsVal V
instance (ArrowChoice c, ArrowFail String c, ArrowClosure Expr Cls c)
=> ArrowClosure Expr Val (ValueT Val c) where
type Join y (ValueT Val c) = Cls.Join y c
type Join y Val (ValueT Val c) = Cls.Join y Cls c
closure = ValueT $ rmap ClosureVal Cls.closure
apply (ValueT f) = ValueT $ proc (v,x) -> case v of
ClosureVal cls -> Cls.apply f -< (cls,x)
......
......@@ -24,7 +24,7 @@ import GHC.Exts (IsString(..),Constraint)
-- | Shared interpreter for PCF.
eval :: (ArrowChoice c, ArrowFix (c Expr v), ArrowEnv Text v c, ArrowFail e c, IsString e,
ArrowClosure Expr v c, ArrowLetRec Text v c, IsVal v c, Env.Join v c, Cls.Join v c, Join v c)
ArrowClosure Expr v c, ArrowLetRec Text v c, IsVal v c, Env.Join v c, Cls.Join v v c, Join v c)
=> c Expr v
eval = fix $ \ev -> proc e0 -> case e0 of
Var x _ -> Env.lookup' -< x
......
......@@ -153,7 +153,7 @@ instance (IsString e, ArrowChoice c, ArrowFail e c) => IsVal Val (ValueT Val c)
instance (IsString e, ArrowChoice c, ArrowFail e c, ArrowClosure Expr Cls c)
=> ArrowClosure Expr Val (ValueT Val c) where
type Join y (ValueT Val c) = Cls.Join y c
type Join y Val (ValueT Val c) = Cls.Join y Cls c
closure = ValueT $ rmap ClosureVal Cls.closure
apply (ValueT f) = ValueT $ proc (v,x) -> case v of
ClosureVal cls -> Cls.apply f -< (cls,x)
......
......@@ -6,7 +6,7 @@ packages:
- 'pcf'
- 'while'
# - 'stratego'
# - 'jimple'
- 'jimple'
# - 'tutorial'
extra-deps:
- dump-core-0.1.3.2
......
......@@ -47,6 +47,8 @@ import GHC.Generics (Generic)
-- | Values of the While language can be booleans or numbers.
data Val = BoolVal Bool | NumVal Int deriving (Eq, Show, Generic)
type Addr = Label
type Env = HashMap Text Addr
type Store = HashMap Addr Val
type Exception = (Text,Val)
-- | The concrete interpreter of the while language instantiates
......@@ -59,8 +61,8 @@ run ss =
(Generic.run ::
ConcreteT
(RandomT
(EnvT Text Addr
(StoreT Addr Val
(EnvT Env
(StoreT Store
(ExceptT Exception
(FailureT String
(->)))))) [Statement] ())
......@@ -78,7 +80,7 @@ instance (ArrowChoice c, Profunctor c) => ArrowAlloc Addr (ConcreteT c) where
instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
type JoinVal y (ConcreteT c) = ()
boolLit = arr (BoolVal)
boolLit = arr BoolVal
and = proc (v1,v2) -> case (v1,v2) of
(BoolVal b1,BoolVal b2) -> returnA -< BoolVal (b1 && b2)
_ -> fail -< "Expected two booleans as arguments for 'and'"
......@@ -88,7 +90,7 @@ instance (ArrowChoice c, ArrowFail String c) => IsVal Val (ConcreteT c) where
not = proc v -> case v of
BoolVal b -> returnA -< BoolVal (Prelude.not b)
_ -> fail -< "Expected a boolean as argument for 'not'"
numLit = arr (\d -> NumVal d)
numLit = arr NumVal
add = proc (v1,v2) -> case (v1,v2) of
(NumVal n1,NumVal n2) -> returnA -< NumVal (n1 + n2)
_ -> fail -< "Expected two numbers as arguments for 'add'"
......
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
-- | Generic interpreter for the While-Language.
module GenericInterpreter where
......
......@@ -88,6 +88,8 @@ import Text.Printf
data Val = BoolVal Bool | NumVal IV | TypeError (Pow String) deriving (Eq,Generic)
type IV = Interval (InfiniteNumber Int)
type Addr = FreeCompletion Label
type Env = SM.Map Text Addr
type Store = Map Addr Val
newtype Exception = Exception (Map Text Val) deriving (PreOrd,Complete,Show,Eq)
-- | The interval analysis instantiates the generic interpreter
......@@ -100,8 +102,8 @@ run k env ss = fmap (fmap (fmap fst)) <$> snd $
(Generic.run ::
Fix'
(ValueT Val
(EnvT SM.Map Text Addr
(StoreT Map Addr Val
(EnvT Env
(StoreT Store
(ExceptT Exception
(ErrorT (Pow String)
(TerminatingT
......
......@@ -55,6 +55,8 @@ import Control.Arrow.Transformer.Abstract.Terminating
-- Value semantics for the while language that does not approximate values at all.
type Addr = FreeCompletion Label
type Env = SM.Map Text Addr
type Store = M.Map Addr Val
type Val = ()
type Exception = ()
......@@ -66,8 +68,8 @@ run env ss =
(Generic.run ::
Fix'
(UnitT
(EnvT SM.Map Text Addr
(StoreT M.Map Addr Val
(EnvT Env
(StoreT Store
(ExceptT Exception
(ErrorT (Pow String)
(TerminatingT
......