Define Names.

1 files changed, 92 insertions, 0 deletions

diff --git a/src/Core/Name.idr b/src/Core/Name.idr
new file mode 100644
index 0000000..ae669b8
--- /dev/null
+++ b/src/Core/Name.idr
@@ -0,0 +1,92 @@
+module Core.Name
+
+import public Control.Relation
+
+import Data.List
+import Data.Singleton
+import Data.Stream
+
+import Decidable.Equality
+
+import public Text.Bounded
+import Text.PrettyPrint.Prettyprinter
+
+infix 4 ~~
+
+-- Definitions -----------------------------------------------------------------
+
+||| Names of variables.
+export
+Name : Type
+Name = WithBounds String
+
+%name Name n, m
+
+||| Equivalence relation on names.
+export
+(~~) : Rel Name
+m ~~ n = m.val = n.val
+
+%name (~~) prf
+
+-- Interfaces ------------------------------------------------------------------
+
+export
+Interpolation Name where
+  interpolate n = n.val
+
+export
+Pretty Name where
+  pretty n = pretty n.val
+
+export
+Reflexive Name (~~) where
+  reflexive = Refl
+
+export
+Symmetric Name (~~) where
+  symmetric prf = sym prf
+
+export
+Transitive Name (~~) where
+  transitive prf1 prf2 = trans prf1 prf2
+
+export Equivalence Name (~~) where
+
+-- Operations ------------------------------------------------------------------
+
+||| Constructs a new name from a bounded String.
+export
+MkName : WithBounds String -> Name
+MkName = id
+
+||| Decides if two names are equivalent
+export
+decEquiv : (m, n : Name) -> Dec (m ~~ n)
+decEquiv m n = decEq m.val n.val
+
+||| Returns the bounds of `name`, if any.
+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