Home
Members
Publications
Projects/Collab.
Software
Events
Open Positions
Contact
News
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
module CliMod where import Expr import CubeExpr tmp1 x = freeVars x tmp4 x y = alphaEq x y
module VarMod where alphaEq y x = x == y freeVars x = [x]
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)
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])
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])
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)))
module KindMod where import PreludeExt alphaEq y x = x == y freeVars = emptylist