|
|
=== Program Data View ===
|
|
|
|
|
|
|
|
|
<code haskell>
|
|
|
module CubeExpr where
|
|
|
|
|
|
import Char(isAlphaNum, isAlpha)
|
|
|
import List(union, (\\))
|
|
|
import Expr
|
|
|
import Sub
|
|
|
import PreludeExt
|
|
|
import VarMod (freeVars,alphaEq)
|
|
|
import AppMod (freeVars,alphaEq)
|
|
|
import LamMod (freeVars,alphaEq)
|
|
|
import PiMod (freeVars,alphaEq)
|
|
|
import KindMod (freeVars,alphaEq)
|
|
|
import LetMod (alphaEq)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
alphaEq x y
|
|
|
=
|
|
|
alphafold KindMod.alphaEq LetMod.alphaEq PiMod.alphaEq
|
|
|
LamMod.alphaEq
|
|
|
AppMod.alphaEq
|
|
|
VarMod.alphaEq
|
|
|
x
|
|
|
y
|
|
|
|
|
|
freeVars x
|
|
|
=
|
|
|
freefold KindMod.freeVars PiMod.freeVars LamMod.freeVars
|
|
|
AppMod.freeVars
|
|
|
VarMod.freeVars
|
|
|
x
|
|
|
|
|
|
{- freeVars :: Expr -> [Sym] -}
|
|
|
freefold fun_kind fun_pi fun_lam fun_app fun_var (Var s) = fun_var s
|
|
|
|
|
|
freefold fun_kind fun_pi fun_lam fun_app fun_var (App f a) = fun_app ((((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) a) ((((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) f)
|
|
|
|
|
|
freefold fun_kind fun_pi fun_lam fun_app fun_var (Lam i t e) = fun_lam ((((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) e) ((((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) t) i
|
|
|
|
|
|
freefold fun_kind fun_pi fun_lam fun_app fun_var (Pi i k t) = fun_pi ((((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) t) ((((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) k) i
|
|
|
|
|
|
freefold fun_kind fun_pi fun_lam fun_app fun_var (Let i t e b) = (((((freefold fun_kind) fun_pi) fun_lam) fun_app) fun_var) (expandLet i t e b)
|
|
|
freefold fun_kind fun_pi fun_lam fun_app fun_var (Kind _) = fun_kind
|
|
|
|
|
|
|
|
|
{- alphaEq :: Expr -> Expr -> Bool -}
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var (App f a) (App f' a') = alp_app
|
|
|
((((((alphafold alp_kind) alp_let) alp_pi) alp_lam) alp_app) alp_var) a' f' a f
|
|
|
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var (Lam s t e) (Lam s' t' e') = alp_lam
|
|
|
((((((alphafold alp_kind) alp_let) alp_pi) alp_lam) alp_app) alp_var) e' t' s' e t s
|
|
|
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var (Pi s k t) (Pi s' k' t') = alp_pi
|
|
|
((((((alphafold alp_kind) alp_let) alp_pi) alp_lam) alp_app) alp_var) t' k' s' t k s
|
|
|
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var (Let s t e b) (Let s' t' e' b') = alp_let
|
|
|
((((((alphafold alp_kind) alp_let) alp_pi) alp_lam) alp_app) alp_var) b' e' t' s' b e t s
|
|
|
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var (Var s) (Var s') = alp_var s' s
|
|
|
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var (Kind k) (Kind k') = alp_kind k' k
|
|
|
|
|
|
alphafold alp_kind alp_let alp_pi alp_lam alp_app alp_var _ _ = 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
|
|
|
|
|
|
alphaEq y x = x == y
|
|
|
|
|
|
freeVars x = [x]
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module AppMod where
|
|
|
|
|
|
import List(union, (\\))
|
|
|
import Expr
|
|
|
|
|
|
|
|
|
|
|
|
alphaEq comp z w y x = (comp x w) && (comp y z)
|
|
|
|
|
|
freeVars arg2 arg1 = (arg1) `union` (arg2)
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module LamMod where
|
|
|
|
|
|
import List(union, (\\))
|
|
|
import Sub
|
|
|
import Expr
|
|
|
|
|
|
alphaEq comp w v u z y x
|
|
|
= (comp y v) && (comp z (substVar u x w))
|
|
|
|
|
|
freeVars arg2 arg1 x
|
|
|
= (arg1) `union` ((arg2) \\ [x])
|
|
|
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module PiMod where
|
|
|
|
|
|
import List(union, (\\))
|
|
|
import Expr
|
|
|
import Sub
|
|
|
|
|
|
|
|
|
alphaEq comp w v u z y x
|
|
|
= (comp y v) && (comp z (substVar u x w))
|
|
|
|
|
|
freeVars arg2 arg1 x = (arg1) `union` ((arg2) \\ [x])
|
|
|
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module LetMod where
|
|
|
import Expr
|
|
|
import Sub
|
|
|
|
|
|
alphaEq comp ww w v u zz z y x
|
|
|
=
|
|
|
(comp y v) &&
|
|
|
((comp z w) && (comp zz (substVar u x ww)))
|
|
|
|
|
|
</code>
|
|
|
<code haskell>
|
|
|
module KindMod where
|
|
|
import PreludeExt
|
|
|
|
|
|
alphaEq y x = x == y
|
|
|
|
|
|
freeVars = emptylist
|
|
|
|
|
|
|
|
|
</code>
|
|
|
|
|
|
[[internet:view_switcher:examples:lambda_cube|Retour]] |
|
|
\ No newline at end of file |