|
|
=== Initial View of the lambda cube program ===
|
|
|
|<code haskell>
|
|
|
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
|
|
|
|
|
|
</code>|<code haskell>
|
|
|
module CliMod where
|
|
|
import Expr
|
|
|
import CubeExpr
|
|
|
|
|
|
tmp1 x = freeVars x
|
|
|
|
|
|
|
|
|
tmp4 x y = alphaEq x y
|
|
|
|
|
|
</code>|<code haskell>
|
|
|
module VarMod where
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
</code>|<code haskell>
|
|
|
module AppMod where
|
|
|
|
|
|
import List(union, (\\))
|
|
|
import Expr
|
|
|
|
|
|
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module LamMod where
|
|
|
|
|
|
import List(union, (\\))
|
|
|
import Sub
|
|
|
import Expr
|
|
|
|
|
|
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module PiMod where
|
|
|
|
|
|
import List(union, (\\))
|
|
|
import Expr
|
|
|
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module LetMod where
|
|
|
import Expr
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module KindMod where
|
|
|
import PreludeExt
|
|
|
|
|
|
</code>
|
|
|
|
|
|
|
|
|
[[internet:view_switcher:examples:lambda_cube|Retour]] |