1
1
mirror of https://github.com/github/semantic.git synced 2025-01-03 04:51:57 +03:00

Compute the max bound metavariable in an ABT.

This commit is contained in:
Rob Rix 2017-09-11 09:36:00 -04:00
parent d064e3f1e5
commit 4d818304fb

View File

@ -5,6 +5,7 @@ module Data.Functor.Binding
, BindingF(..) , BindingF(..)
, bindings , bindings
, freeMetavariables , freeMetavariables
, maxBoundMetavariable
-- Environments -- Environments
, Env(..) , Env(..)
, envExtend , envExtend
@ -37,6 +38,14 @@ freeMetavariables = cata $ \ diff -> case diff of
Let bindings body -> foldMap snd bindings <> foldr Set.delete (fold body) (fst <$> bindings) Let bindings body -> foldMap snd bindings <> foldr Set.delete (fold body) (fst <$> bindings)
Var v -> Set.singleton v Var v -> Set.singleton v
maxBoundMetavariable :: (Foldable syntax, Functor syntax, Recursive t, Base t ~ BindingF syntax) => t -> Maybe Metavar
maxBoundMetavariable = cata $ \ diff -> case diff of
Let bindings _ -> foldMaxMap (Just . fst) bindings
Var _ -> Nothing
foldMaxMap :: (Foldable t, Ord b) => (a -> Maybe b) -> t a -> Maybe b
foldMaxMap f = foldr (max . f) Nothing
newtype Env a = Env { unEnv :: [(Metavar, a)] } newtype Env a = Env { unEnv :: [(Metavar, a)] }
deriving (Eq, Foldable, Functor, Monoid, Ord, Show, Traversable) deriving (Eq, Foldable, Functor, Monoid, Ord, Show, Traversable)