Skip to content

Instantly share code, notes, and snippets.

@gergoerdi
Created August 19, 2020 11:48
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gergoerdi/753cf5af693f50103a61f5d49568ab93 to your computer and use it in GitHub Desktop.
Save gergoerdi/753cf5af693f50103a61f5d49568ab93 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment