Initial View of the lambda cube program

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
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

internet/view_switcher/examples/lambda_cube/initial_page.txt · Last modified: 2011/02/07 15:15 by akram