lambda_cube_data_view

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