Pi calculus

PiCalc.hs

{-# LANGUAGE GADTs, StandaloneDeriving, RankNTypes #-}

type Var = String

data RecT a
data SendT a
data RepT a
data ParT a b
data NilT
data NuT a

data Pi a where
    Send :: Var -> Var -> Pi a -> Pi (SendT a)

    Rec  :: Var -> Var -> Pi a -> Pi (RecT a)

    Par  :: Pi a -> Pi b -> Pi (ParT a b)

    Nu   :: Var -> Pi a -> Pi (NuT a)

    Rep  :: Pi a -> Pi (RepT a)

    PNil :: Pi NilT

deriving instance Show (Pi a)

given :: Bool -> a -> Maybe a
given b x = if b then Just x else Nothing

changeWhen :: Bool -> a -> a -> a 
changeWhen f x y = if f then y else x

sendReduceL :: Pi (ParT (SendT a) (RecT b)) -> Maybe (Pi (ParT a b))
sendReduceL (Par (Send c x p) (Rec c' y q)) = given (c == c') $ Par p (replace y x q)

assocCongL :: Pi (ParT (ParT a b) c) -> Pi (ParT a (ParT b c))
assocCongL (Par (Par p q) r) = Par p (Par q r)

assocCongR :: Pi (ParT a (ParT b c)) -> Pi (ParT (ParT a b) c)
assocCongR (Par p (Par q r)) = Par (Par p q) r

flipCong :: Pi (ParT a b) -> Pi (ParT b a)
flipCong (Par p q) = Par q p

nilParCong :: Pi (ParT a NilT) -> Pi a
nilParCong (Par p PNil) = p

nilNuCong :: Pi (NuT NilT) -> Pi NilT
nilNuCong (Nu x PNil) = PNil

repCong :: Pi (RepT a) -> Pi (ParT a (RepT a))
repCong proc@(Rep p) = Par p proc


replace :: Var -> Var -> Pi a -> Pi a
replace y x PNil = PNil
replace y x (Par p q) = Par (replace y x p) (replace y x q)

replace y x (Send a b p) = Send (changeWhen (a == y) a x) 
                                (changeWhen (b == y) b x)
                                (replace y x p)

replace y x (Rec a b p) = Rec (changeWhen (a == y) a x) 
                              (changeWhen (b == y) b x)
                              (replace y x p)

replace y x (Rep p) = Rep (replace y x p)