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

Retour