From 3649c9965e787c9cb0dc1cedc4400cdec4c5b8a2 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sun, 26 Mar 2023 03:50:28 +0100 Subject: Add type checking. Currently, there is Set in Set. Next step is to add universe levels. --- src/CC/Name.idr | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'src/CC/Name.idr') 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 -- cgit v1.2.3