walk :: Var -> Subst -> Var | |
walk var subst = go var subst | |
where go :: Var -> List Var -> Maybe Var -> Var | |
go (Unbound k) stack acc = | |
case (subst k, acc) of | |
(Nothing, Nothing) -> Unbound k | |
(Nothing, Just u) -> Cons u v | |
(Just v, _) -> go v stack acc | |
go (Cons h t) stack acc = go h (t :: stack) acc | |
go v [] Nothing = v | |
go v [] (Just u) = Cons u v | |
go v (x :: xs) Nothing = go x xs (Just v) | |
go v (x :: xs) (Some u) = go x xs v (Just (Cons u v)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment