module CubeExpr  where
 
import Char(isAlphaNum, isAlpha)
import List(union, (\\))
import Error
import HughesPJ(Doc, renderStyle, style, text, (<>), (<+>), parens, ($$),
       				 vcat, punctuate, sep, fsep, nest)
import ReadP (ReadP, (+++), char, munch1, many1, string, pfail, sepBy,
                                optional, many, skipSpaces, readP_to_S, look)
import Expr
import Sub
import PreludeExt
import VarMod ()
import AppMod ()
import LamMod ()
import PiMod ()
import KindMod ()
import LetMod ()
 
 
 
 
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
 
 
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

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

module VarMod where

module AppMod where
 
 import List(union, (\\))
 import Expr

module LamMod where
 
 import List(union, (\\))
 import Sub
 import Expr

module PiMod where 
 
 import List(union, (\\))
 import Expr

module LetMod where
 import Expr

module KindMod where
 import PreludeExt

Retour