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 -- Is this really necessary? 
          | 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 variables
-- only works correctly when there are no Match constructors in Term

free :: Term -> [String]
free (Var v)   = [v]
free (Lam v x) = delete v (free x)
free e         = nub (concat (gmapQ (mkQ [] free) e))

-- Substitution
-- only works correctly when there are no Match constructors in Term

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

-- single traversal (bottom-up) beta reduction

step :: Term -> Term
step = everywhere (mkT aux)
    where aux ((Lam v t) :@: m) = subst [(v,m)] t
	  aux t = t

-- Replacing constant by definition

replace :: [(String, Term)] -> Term -> Term
replace defs = everywhere (mkT aux)
    where aux (Const x) = fromMaybe (Const x) (lookup x defs)
	  aux t = t

-- Examples

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")])