module LambdaDeBruijn where {- Proving Termination of Parallel Substitutions, see ยง 3.2.2 of Dependent Types and Multi Monadic Effects in F* -} import Language.Haskell.Liquid.Prelude {-@ LIQUID "--totality" @-} type Var = Int {-@ type EVar = {v:Expr| isEVar v} @-} type Subst = [(Var,Expr)] {-@ type RenamingSubst = {su: [(Var,Expr)] | isRenaming su} @-} {- TODO: in the F* paper, substitutions are functions, can we have function representation with LH? -} data Typ data Expr = EVar Var | ELam Typ Expr | EUnit | EApp Expr Expr {-@ data Expr [elen] @-} {-@ type MEVar E SU = {v:Expr | (isEVar E && isRenaming SU) => (isEVar v) } @-} {-@ sub :: su:Subst -> v:Var -> {v:Expr | (isRenaming su) => (isEVar v) } @-} sub [] v = EVar v sub ((vx, x):su) v | v == vx = x | otherwise = sub su v {-@ subst :: e:Expr -> su:Subst -> MEVar e su / [if (isEVar e) then 0 else 1, if (isRenaming su) then 0 else 1, elen e] @-} subst EUnit su = EUnit subst (EVar v) su = sub su v subst (EApp e1 e2) su = EApp (subst e1 su) (subst e2 su) subst (ELam t e) su | isRenaming su = let su' = toRem \$ (0, EVar 0): map (\i -> (i, subst (sub su (i-1)) \$ incrsubst ())) [1..] in ELam t \$ subst e su' subst (ELam t e) su = -- | not \$ isRenaming su let su' = (0, EVar 0): map (\i -> (i, subst (sub su (i-1)) \$ incrsubst ())) [1..] in ELam t \$ subst e su' {-- Helper functions and measure definitions --} {-@ toRem :: [(Var, EVar)] -> RenamingSubst @-} toRem :: Subst -> Subst toRem [] = [] toRem ((x, y):sus) = (x, y):toRem sus {-@ incrsubst :: () -> RenamingSubst @-} incrsubst :: () -> Subst incrsubst _ = toRem \$ map (\i -> (i, EVar \$ i+1)) [0..] {-@ measure isEVar @-} isEVar :: Expr -> Bool isEVar (EVar _) = True isEVar _ = False {-@ measure isRenaming @-} isRenaming :: Subst -> Bool isRenaming (vx:sus) = isEVar (mysnd vx) && isRenaming sus isRenaming [] = True {-@ measure mysnd @-} mysnd (_,y) = y {-@ invariant {v:Expr | elen v >= 0 } @-} {-@ measure elen @-} elen :: Expr -> Int elen EUnit = 0 elen (EVar v) = 0 elen (ELam _ e) = 1 + elen e elen (EApp e1 e2) = 1 + elen e1 + elen e2