content: module LambdaDeBruijn where
  
  {-@ LIQUID "--prune-unsorted" @-}
  
  {- Proving Termination of Parallel Substitutions,
     see  § 3.2.2 of Dependent Types and Multi Monadic Effects in F*
   -}
  
  import Language.Haskell.Liquid.Prelude
  
  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 :: (a, b) -> b
  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
  