Initial Program again (Function View)

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