Add type checking.HEADmaster

Currently, there is Set in Set. Next step is to add universe levels.

1 files changed, 25 insertions, 0 deletions

diff --git a/src/CC/Name.idr b/src/CC/Name.idr
index 4c25f5c..d1df253 100644
--- a/src/CC/Name.idr
+++ b/src/CC/Name.idr
@@ -2,6 +2,10 @@ module CC.Name
 
 import public Control.Relation
 
+import Data.List
+import Data.Singleton
+import Data.Stream
+
 import Decidable.Equality
 
 import Text.Bounded
@@ -65,3 +69,24 @@ decEquiv m n = decEq m.val n.val
 export
 bounds : (name : Name) -> Maybe Bounds
 bounds name = if name.isIrrelevant then Nothing else Just name.bounds
+
+||| Returns a new name not in the set.
+export
+fresh : Foldable f => f Name -> Name
+fresh xs =
+  irrelevantBounds $
+  select (unfoldr (\n => ("_\{show n}", S n)) 0) $
+  sort $
+  foldMap (singleton . val) xs
+  where
+  select : Ord a => Stream a -> List a -> a
+  select (x :: xs) [] = x
+  select (x :: xs) (y :: ys) =
+    case compare x y of
+      LT => x
+      EQ => select xs ys
+      GT => select (x :: xs) ys
+
+export
+fresh' : Foldable f => Singleton {a = f Name} xs -> Name
+fresh' (Val xs) = fresh xs