TraverseTerm.idr

traverseTerm : (Applicative f) => (Var vars1 -> f (Term vars2)) -> (Term vars1 -> f (Term vars2))
traverseTerm go (Local idx p) = go (MkVar p)
traverseTerm go (Ref nt x) = pure $ Ref nt x
traverseTerm go (Meta x ts) = Meta x <$> traverse (traverseTerm go) ts
traverseTerm go (Bind x b scope) = Bind x <$> traverse (traverseTerm go) b <*> traverseTerm go' scope
  where
    go' : Var (x :: vars1) -> f (Term (x :: vars2))
    go' (MkVar First) = pure $ Local _ First
    go' (MkVar (Later p)) = weaken <$> go (MkVar p)
traverseTerm go (App f e) = App <$> traverseTerm go f <*> traverseTerm go e
traverseTerm go TType = pure TType
traverseTerm go Erased = pure Erased

contractVar : {inner : List Name} -> Var (inner ++ [x] ++ outer) -> Maybe (Var (inner ++ outer))
contractVar {inner = []} (MkVar First) = Nothing
contractVar {inner = []} (MkVar (Later p)) = pure $ MkVar p
contractVar {inner = (x::xs)} (MkVar First) = pure $ MkVar First
contractVar {inner = (x::xs)} (MkVar (Later p)) = do
    MkVar p' <- contractVar {inner = xs} (MkVar p)
    pure $ MkVar (Later p')

export
contract : Term (x :: vars) -> Maybe (Term vars)
contract = traverseTerm $ \v => do
  MkVar p <- contractVar {inner = []} v
  pure $ Local _ p