(A subset of) the two-sided linear logic sequent calculus

Sequent.hs

delete :: (Eq a) => a -> [a] -> [a]
delete _ []        = error "delete: element not present"
delete x (y:ys)    = if x == y then ys else y : delete x ys

data Atom
    = Var String
    | Constant String
    deriving (Eq,Ord,Show)

data Exp 
    = Atom Atom
    | Perp Exp
    | Bot
    | Zero
    | Plus Exp Exp
    | Lolli Exp Exp
    | Bang Exp
    | Quest Exp
    deriving (Eq,Ord,Show)

dual :: Exp -> Exp
dual a@(Atom _) = Perp a
dual (Perp a) = a
dual (Bang e) = Quest (dual e)
dual (Quest e) = Bang (dual e)
dual (Lolli x Bot) = x
dual (Lolli x y) = Lolli (dual y) (dual x)
dual x = Perp x

async Bot = True
async (Lolli _ _) = True
async (Quest _) = True
async (Perp a) = not (async a)
async _ = False

data Seq = Seq [Exp] [Exp]
   deriving (Eq,Ord,Show)

par a b = Lolli (Perp a) b
tensor a b = Perp (Lolli a (Perp b))
with a b = Perp (Plus (Perp a) (Perp b))
unit = Perp Bot
top = Perp Zero

data Rule
  = Identity Exp
  | Cut Exp Seq Seq
  | PerpL Exp Seq
  | PerpR Exp Seq
  | PlusL Exp Exp Seq Seq
  | PlusR Exp Exp Seq Seq
  | BotR Seq
  | BotL
  | ZeroL Seq
  | ImplR Exp Exp Seq
  | ImplL Exp Exp Seq Seq
  | WeakenL Exp Seq
  | WeakenR Exp Seq
  | ContractL Exp Seq
  | ContractR Exp Seq
  | BangL Exp Seq
  | QuestR Exp Seq
  | BangR Exp Seq
  | QuestL Exp Seq
    deriving (Eq,Ord,Show)

rule (Identity a) = Seq [a] [a]
rule (Cut a (Seq w x) (Seq y z)) = Seq (w ++ delete a y) (delete a x ++ z)
rule (PerpL a (Seq x y)) = Seq (x ++ [Perp a]) (delete a y)
rule (PerpR a (Seq x y)) = Seq (delete a x) ([Perp a] ++ y)
rule (PlusL a b (Seq w x) (Seq y z))
    | delete a w == delete b y && x == z
    = Seq (delete a w ++ [Plus a b]) z
rule (PlusR a b (Seq w x) (Seq y z))
    | delete a x == delete b z && w == y
    = Seq w (delete a x ++ [Plus a b])
rule (BotR (Seq x y)) = Seq x (y ++ [Bot])
rule BotL = Seq [Bot] []
rule (ZeroL (Seq x y)) = Seq (x ++ [Zero]) y
rule (ImplR a b (Seq x y))
    = Seq (delete a x) (delete b y ++ [Lolli a b])
rule (ImplL a b (Seq w x) (Seq y z))
    = Seq ([Lolli a b] ++ w ++ delete b y) (delete a x ++ z)
rule (WeakenL a (Seq x y)) = Seq (x ++ [Bang a]) y
rule (WeakenR a (Seq x y)) = Seq x (y ++ [Quest a])
rule (ContractL a (Seq x y)) =
    let aa = Bang a
        xx = [aa] ++ delete aa (delete aa x)
        in Seq xx y
rule (ContractR a (Seq x y)) =
    let aa = Quest a
        yy = [aa] ++ delete aa (delete aa y)
        in Seq x yy
rule (BangL a (Seq x y)) = Seq ([Bang a] ++ delete a x) y
rule (QuestR a (Seq x y)) = Seq x ([Quest a] ++ delete a y)
rule (BangR a (Seq x y)) = Seq x ([Bang a] ++ delete a y) -- assert: x is all Bang's, delete a y is all Quest's
rule (QuestL a (Seq x y)) = Seq ([Quest a] ++ delete a x) y  -- assert: delete a x is all Bang's, y is all Quest's