module Language.Pointwise.Syntax where
import Data.Generics hiding (Unit,(:*:),Inl,Inr)
import Data.List
import Data.Maybe
import Generics.Pointless.Combinators
data Term = Var String
| Unit
| Const String
| Term :&: Term
| Fst Term
| Snd Term
| Case Term Term Term
| Match Term [(Term,Term)]
| Inl Term
| Inr Term
| Lam String Term
| Term :@: Term
| In Term
| Out Term
| Fix Term
deriving (Eq,Show,Data,Typeable)
isPair :: Term -> Bool
isPair (_ :&: _) = True
isPair _ = False
pwFst :: Term -> Term
pwFst (l :&: r) = l
pwSnd :: Term -> Term
pwSnd (l :&: r) = r
isInl :: Term -> Bool
isInl (Inl _) = True
isInl _ = False
isInr :: Term -> Bool
isInr (Inr _) = True
isInr _ = False
isInlr :: Term -> Bool
isInlr t = isInl t || isInr t
isIn :: Term -> Bool
isIn (In _) = True
isIn _ = False
free :: Term -> [String]
free (Var v) = [v]
free (Lam v x) = delete v (free x)
free e = nub (concat (gmapQ (mkQ [] free) e))
subst :: [(String, Term)] -> Term -> Term
subst s (Var y) =
case lookup y s
of Nothing -> Var y
Just t -> t
subst s (Lam y e) =
let x = concat (concat (map free (e : map snd s)))
in Lam x (subst ((y, Var x) : s) e)
subst s t =
gmapT (mkT (subst s)) t
step :: Term -> Term
step = everywhere (mkT aux)
where aux ((Lam v t) :@: m) = subst [(v,m)] t
aux t = t
replace :: [(String, Term)] -> Term -> Term
replace defs = everywhere (mkT aux)
where aux (Const x) = fromMaybe (Const x) (lookup x defs)
aux t = t
distr :: Term
distr = Lam "x" (Match (Var "x") [(Var "y" :&: (Inl (Var "z")),Inl (Var "y" :&: Var "z")),(Var "y" :&: (Inr (Var "z")),Inr (Var "y" :&: Var "z"))])
swap :: Term
swap = Lam "x" (Match (Var "x") [(Var "w" :&: Var "y", Var "y" :&: Var "w")])
coswap :: Term
coswap = Lam "x" (Match (Var "x") [(Inl (Var "y"), Inr (Var "y")),(Inr (Var "y"), Inl (Var "y"))])
assocr :: Term
assocr = Lam "w" (Match (Var "w") [((Var "x" :&: Var "y") :&: Var "z", Var "x" :&: (Var "y" :&: Var "z"))])
coassocr :: Term
coassocr = Lam "w" (Match (Var "w") [(Inl (Inl (Var "x")), Inl (Var "x")),(Inl (Inr (Var "x")), Inr (Inl (Var "x"))),(Inr (Var "x"), Inr (Inr (Var "x")))])
test :: Term
test = Lam "x" (Match (Var "x") [(Var "y", Var "y")])