module Development.Contract (
Contract
, ContractFailed(..)
, Partner(..)
, assert
, attach
, (&)
, (|>)
, (>->)
, (>>->)
, true
, false
, Flat(prop)
, p
, pNot
, deriveContracts
, dropContext
, pNil, pCons, (=:), pNotNil, pNotCons, list
, io
, pTuple0, pTuple2, pTuple3, pTuple4
, pNothing, pJust, pNotNothing, pNotJust, maybe
) where
import Prelude hiding (maybe)
import Data.Char(isLetter)
import Data.Either(either)
import Data.List (intercalate)
import Language.Haskell.TH
import Language.Haskell.TH.Syntax (Lift(..))
import Data.Typeable(Typeable)
import Control.Exception(Exception, throw)
data ContractFailed =
ContractFailed {culprit :: Partner, loc :: Loc, explanation :: String}
deriving (Typeable)
instance Show ContractFailed where
show (ContractFailed culprit loc explanation) =
"Contract at " ++ loc_filename loc ++ ":" ++ show line ++ ":" ++ show col ++
" failed at\n" ++ explanation ++ "\n" ++
"The " ++ show culprit ++ " is to blame."
where
(line,col) = loc_start loc
instance Exception ContractFailed
data Partner = Server | Client | Contract
instance Show Partner where
show Server = "server"
show Client = "client"
show Contract = "contract"
type Blame = (Partner, Partner)
getCulprit :: Blame -> Partner
getCulprit = fst
contra :: Blame -> Blame
contra (p1,p2) = (p2,p1)
newClient :: Blame -> Partner -> Blame
newClient (p1,_) p2 = (p1,p2)
newtype Contract a =
C (Blame -> Loc -> ExplanationB -> a -> Either (Partner,String) a)
assert :: Q Exp
assert = do
loc <- location
[|monitor (Server,Client) loc id|]
attach :: Q Exp
attach = do
loc <- location
[|\x c -> monitor (Server,Client) loc id c x|]
instance Lift Loc where
lift (Loc a1 a2 a3 a4 a5) = [|Loc a1 a2 a3 a4 a5|]
monitor :: Blame -> Loc -> ExplanationB -> Contract a -> (a -> a)
monitor b l e (C f) x
= either
(\(cul,con) -> throw (ContractFailed cul l (e ("{" ++ con ++ "}"))))
id
(f b l e x)
cFail :: Blame -> String -> Either (Partner,String) a
cFail (p1,p2) err = Left (p1,err)
infixr 3 &
infixr 2 |>
infixr 1 >->
infixr 1 >>->
(&) :: Contract a -> Contract a -> Contract a
C p1 & C p2 = C (\b l e x -> p1 b l e x >>= p2 b l e)
(|>) :: Contract a -> Contract a -> Contract a
C p1 |> C p2 = C (\b l e x -> case p1 b l e x of
Left _ -> p2 b l e x
Right y -> Right y)
true :: Contract a
true = C (\b l e x -> Right x)
false :: Contract a
false = C (\b l e x -> cFail (contra b) "NOT false")
(>->) :: Contract a -> Contract b -> Contract (a -> b)
c1 >-> c2 =
C (\b l e f -> Right (f `seq`
(monitor b l (e . \s->("(_->"++s++")")) c2 . f .
monitor (contra b) l (e . \s->("("++s++"->_)")) c1)))
(>>->) :: Contract a -> (a -> Contract b) -> Contract (a -> b)
pre >>-> post =
C (\b l e f -> Right (f `seq`
\x -> let b' = contra b
e' = e . \s->("("++s++"->_)")
in monitor b l (e . \s->("(_->"++s++")"))
(post (monitor (newClient b' Contract) l e' pre x))
(f (monitor b' l e' pre x))))
class Show a => Flat a where
prop :: (a -> Bool) -> Contract a
prop p = C (\b l e x -> if p x then Right x else cFail b (show x))
instance Flat Int
instance Flat Integer
instance Flat Float
instance Flat Double
instance Flat Char
instance Flat Bool
dropContext :: Contract a -> Contract a
dropContext (C f) = C (\b l e x -> f b l (\s->(".."++s++"..")) x)
type ExplanationB = String -> String
context :: String -> Arity -> Int -> ExplanationB
context cons a n s = "("++cons++ concatMap arg [1..a]++")"
where
arg :: Int -> String
arg m = if n==m then ' ':s else " _"
contextI :: String -> Arity -> Int -> ExplanationB
contextI cons _ 1 s = "("++s++cons++"_)"
contextI cons _ 2 s = "(_"++cons++s++")"
showParen :: Bool -> String -> String
showParen True s = "("++s++")"
showParen False s = s
contextVar :: Con -> ExpQ
contextVar (InfixC _ _ _) = varE 'contextI
contextVar _ = varE 'context
deriveContracts :: Name -> Q [Dec]
deriveContracts dataTyName = do
(TyConI (DataD _ _ _ constructors _)) <- reify dataTyName
conNameArities <- mapM conNameArity constructors
let conNames = map fst conNameArities
conContracts <- mapM deriveConContract conNames
notContracts <- mapM deriveNotContract conNames
return (concat conContracts ++ concat notContracts)
deriveConContract :: Name -> Q [Dec]
deriveConContract conName = do
(DataConI _ conTy dataTyName _) <- reify conName
(TyConI (DataD cxt _ _ constructors _)) <- reify dataTyName
tyDec <- sigD pname (return (conContractType cxt conTy))
runIO (putStrLn (pprint conTy))
runIO (putStrLn (pprint cxt))
runIO (putStrLn (pprint tyDec))
def <- valD (varP pname) (normalB (p conName)) []
return [tyDec,def]
where
pname = mkName (prefix : name)
name = nameBase conName
prefix = if isLetter (head name) then 'p' else '='
deriveNotContract :: Name -> Q [Dec]
deriveNotContract conName =
if isLetter (head name)
then do
(DataConI _ conTy dataTyName _) <- reify conName
(TyConI (DataD cxt _ tyVars constructors _)) <- reify dataTyName
tyDec <- sigD pname (return (notContractType cxt dataTyName tyVars))
def <- valD (varP pname) (normalB (pNot conName)) []
return [tyDec,def]
else return []
where
name = nameBase conName
pname = mkName ("pNot" ++ name)
notContractType :: Cxt -> Name -> [TyVarBndr] -> Type
notContractType cxt tyName tyVars =
ForallT tyVars cxt
(AppT (ConT ''Contract)
(if null tyVars
then (ConT tyName)
else AppT (ConT tyName) (foldr1 AppT (map mkTVar tyVars))))
where
mkTVar :: TyVarBndr -> Type
mkTVar (PlainTV name) = VarT name
mkTVar (KindedTV name _) = VarT name
conContractType :: Cxt -> Type -> Type
conContractType cxt (ForallT tyvars cxt2 ty) =
ForallT tyvars cxt (conContractType cxt ty)
conContractType cxt (AppT (AppT ArrowT t1) t2) =
AppT (AppT ArrowT (AppT (ConT ''Contract) t1)) (conContractType cxt t2)
conContractType _ t = AppT (ConT ''Contract) t
type Arity = Int
arity :: Name -> [Con] -> Arity
arity conName [] = error "arity: constructor not in list"
arity conName (InfixC _ cName _ : cs) =
if conName == cName then 2 else arity conName cs
arity conName (NormalC cName fields : cs) =
if conName == cName then length fields else arity conName cs
arity conName (RecC cName fields : cs) =
if conName == cName then length fields else arity conName cs
arity conName (ForallC _ _ _ : cs) = arity conName cs
isConName :: Name -> Con -> Bool
isConName conName (InfixC _ cName _) = conName==cName
isConName conName (NormalC cName _) = conName==cName
isConName conName (RecC cName _) = conName==cName
isConName conName (ForallC _ _ _) = False
name2Con :: Name -> [Con] -> Con
name2Con conName cons = head (filter (isConName conName) cons)
p :: Name -> ExpQ
p conName = do
(DataConI _ conTy dataTyName fixity) <- reify conName
(TyConI (DataD _ _ _ constructors _)) <- reify dataTyName
let conArity = arity conName constructors
conArgNames <- mapM (const (newName "c")) [1..conArity]
projName <- newName "proj"
mkPatternContract conName conArity conTy conArgNames projName constructors
pNot :: Name -> ExpQ
pNot conName = do
(DataConI _ conTy dataTyName _) <- reify conName
(TyConI (DataD _ _ _ constructors _)) <- reify dataTyName
let conArity = arity conName constructors
projName <- newName "proj"
let projDef =
funD projName
[clauseCon conName conArity (name2Con conName constructors), clauseO]
letE [projDef] (appE (conE 'C) (varE projName))
clauseCon :: Name -> Arity -> Con -> ClauseQ
clauseCon conName arity con = do
blameName <- newName "b"
locName <- newName "loc"
explName <- newName "expl"
clause [varP blameName, varP locName, varP explName
,conP conName (replicate arity wildP)]
(normalB (appsE [varE 'cFail, varE blameName,
litE (stringL (faultString conName arity con))])) []
clauseO :: ClauseQ
clauseO = do
blameName <- newName "b"
locName <- newName "loc"
explName <- newName "expl"
argName <- newName "x"
clause [varP blameName, varP locName, varP explName, varP argName]
(normalB (appE (conE 'Right) (varE argName))) []
mkPatternContract :: Name -> Int -> Type -> [Name] -> Name -> [Con] -> ExpQ
mkPatternContract conName conArity conTy conArgNames projName constructors =
conExp
where
clauses = map (mkClause conName conArgNames) constructors
projDef = funD projName clauses
contractExp = letE [projDef] (appE (conE 'C) (varE projName))
conExp = if conArity == 0 then contractExp
else lamE (map varP conArgNames) contractExp
faultString :: Name -> Arity -> Con -> String
faultString cName cArity (InfixC _ _ _) = "_" ++ nameBase cName ++ "_"
faultString cName cArity _ = nameBase cName ++ concat (replicate cArity " _")
conNameArity :: Con -> Q (Name,Arity)
conNameArity (InfixC _ cName _) = return (cName,2)
conNameArity (NormalC cName fields) = return (cName, length fields)
conNameArity (RecC cName vFields) = return (cName, length vFields)
conNameArity (ForallC _ _ _) = do
report True "Cannot make contract pattern when constructor has existential type."
return undefined
mkClause :: Name -> [Name] -> Con -> ClauseQ
mkClause conName conArgNames con = do
blameName <- newName "b"
locName <- newName "loc"
explName <- newName "expl"
(cName,cArity) <- conNameArity con
cArgNames <- mapM (const (newName "x")) [1..cArity]
let recExp :: Name -> Name -> Int -> ExpQ
recExp conArgName cArgName i =
appsE [varE 'monitor, varE blameName, varE locName, appsE [varE '(.), varE explName, appsE [contextVar con, litE (stringL (nameBase conName)), litE (integerL (fromIntegral cArity)), litE (integerL (fromIntegral i))]], varE conArgName, varE cArgName]
let body :: ExpQ
body = if cName == conName
then appE (conE 'Right)
(appsE ((conE cName) :
zipWith3 recExp conArgNames cArgNames [1..cArity]))
else appsE [varE 'cFail, varE blameName,
litE (stringL (faultString cName cArity con))]
clause [varP blameName, varP locName, varP explName
,conP cName (map varP cArgNames)]
(normalB body) []
pNil :: Contract [a]
pNil = C (\b l e x -> case x of [] -> Right x; _:_ -> cFail b "_:_")
pCons :: Contract a -> Contract [a] -> Contract [a]
pCons cx cxs =
C (\b l e x -> case x of
(y:ys) -> Right (monitor b l (e . \s->("("++s++":_)")) cx y :
monitor b l (e . \s->("(_:"++s++")")) cxs ys)
[] -> cFail b "[]")
(=:) :: Contract a -> Contract [a] -> Contract [a]
(=:) = pCons
infixr 5 =:
pNotNil :: Contract [a]
pNotNil = C (\b l e x -> case x of [] -> cFail b "[]"; _ -> Right x)
pNotCons :: Contract [a]
pNotCons = C (\b l e x -> case x of _:_ -> cFail b "_:_"; _ -> Right x)
list :: Contract a -> Contract [a]
list c = pNil |> pCons c (dropContext (list c))
io :: Contract a -> Contract (IO a)
io c = C (\b l e m -> Right (m >>= return . monitor b l (e . \s->("IO "++s)) c))
pTuple0 :: Contract ()
pTuple0 = C (\b l e () -> Right ())
pTuple2 :: Contract a -> Contract b -> Contract (a,b)
pTuple2 c1 c2 =
C (\b l e (x1,x2) -> Right (monitor b l (e . \s->("("++s++",_)")) c1 x1
,monitor b l (e . \s->("(_,"++s++")")) c2 x2))
pTuple3 :: Contract a -> Contract b -> Contract c -> Contract (a,b,c)
pTuple3 c1 c2 c3 =
C (\b l e (x1,x2,x3) -> Right (monitor b l (e . \s->("("++s++",_,_)")) c1 x1
,monitor b l (e . \s->("(_,"++s++",_)")) c2 x2
,monitor b l (e . \s->("(_,_,"++s++")")) c3 x3))
pTuple4 ::
Contract a -> Contract b -> Contract c -> Contract d -> Contract (a,b,c,d)
pTuple4 c1 c2 c3 c4 =
C (\b l e (x1,x2,x3,x4) -> Right
(monitor b l (e . \s->("("++s++",_,_,_)")) c1 x1
,monitor b l (e . \s->("(_,"++s++",_,_)")) c2 x2
,monitor b l (e . \s->("(_,_,"++s++",_)")) c3 x3
,monitor b l (e . \s->("(_,_,_,"++s++")")) c4 x4))
pJust :: Contract a -> Contract (Maybe a)
pJust cy = C proj
where
proj b l e (Just y) = Right (Just (monitor b l (e . context "Just" 1 1) cy y))
proj b l e Nothing = cFail b "Nothing"
pNothing :: Contract (Maybe a)
pNothing = C proj
where
proj b l e Nothing = Right Nothing
proj b l e (Just _) = cFail b "Just _"
pNotNothing :: Contract (Maybe a)
pNotNothing =
C (\b l e x -> case x of Nothing -> cFail b "Nothing"; _ -> Right x)
pNotJust :: Contract (Maybe a)
pNotJust =
C (\b l e x -> case x of Just _ -> cFail b "Just _"; _ -> Right x)
maybe :: Contract a -> Contract (Maybe a)
maybe c = pNothing |> pJust c