From 4d818304fbd902f8903be3f506bb209e61d7e5c2 Mon Sep 17 00:00:00 2001
From: Rob Rix <rob.rix@me.com>
Date: Mon, 11 Sep 2017 09:36:00 -0400
Subject: [PATCH] Compute the max bound metavariable in an ABT.

---
 src/Data/Functor/Binding.hs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Data/Functor/Binding.hs b/src/Data/Functor/Binding.hs
index c45be3251..213406a7a 100644
--- a/src/Data/Functor/Binding.hs
+++ b/src/Data/Functor/Binding.hs
@@ -5,6 +5,7 @@ module Data.Functor.Binding
 , BindingF(..)
 , bindings
 , freeMetavariables
+, maxBoundMetavariable
 -- Environments
 , Env(..)
 , envExtend
@@ -37,6 +38,14 @@ freeMetavariables = cata $ \ diff -> case diff of
   Let bindings body -> foldMap snd bindings <> foldr Set.delete (fold body) (fst <$> bindings)
   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)] }
   deriving (Eq, Foldable, Functor, Monoid, Ord, Show, Traversable)