module CubeExpr  where
 
import Char(isAlphaNum, isAlpha)
import List(union, (\\))
import Expr
import Sub
import PreludeExt
 
freeVars :: Expr -> [Sym]
freeVars (Var s) = [s]
freeVars (App f a) = freeVars f `union` freeVars a
freeVars (Lam i t e) = freeVars t `union` (freeVars e \\ [i])
freeVars (Pi i k t) = freeVars k `union` (freeVars t \\ [i])
freeVars (Let i t e b) = freeVars (expandLet i t e b)
freeVars (Kind _) = emptylist
 
 
alphaEq :: Expr -> Expr -> Bool
alphaEq (App f a)   (App f' a')    = alphaEq f f' && alphaEq a a'
alphaEq (Lam s t e) (Lam s' t' e') = alphaEq t t' && alphaEq e (substVar s' s e')
alphaEq (Pi s k t)  (Pi s' k' t')  = alphaEq k k' && alphaEq t (substVar s' s t')
alphaEq (Let s t e b) (Let s' t' e' b') = alphaEq t t' && alphaEq e e' && alphaEq b (substVar s' s b')
alphaEq (Var s)     (Var s')       = s == s'
alphaEq (Kind k)    (Kind k')      = k == k'
alphaEq _ _ = False

module CliMod where
 import Expr
 import CubeExpr
 
 tmp1 x = freeVars x
 
 
 tmp4 x y = alphaEq x y

module VarMod where