From e833322ebe878ac7fef3a25a06aa4d0793c3fdf4 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 23 Dec 2021 15:52:56 +0100
Subject: [PATCH] add separate type for dimension endpoints

---
 src/Quox.idr            |  4 ++--
 src/Quox/Syntax/Dim.idr | 37 +++++++++++++++++++++++++++----------
 2 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/Quox.idr b/src/Quox.idr
index 785cc8a..4e1b620 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -11,11 +11,11 @@ export
 tm : Term 1 2
 tm =
   (Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
-    `DCloT` (DOne ::: id))
+    `DCloT` (K One ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
 
 main : IO Unit
 main = do
   prettyTerm tm
   prettyTerm $ pushSubstsT tm
-  putStrLn ":qtuwu:"
+  putStrLn "\n:qtuwu:"
diff --git a/src/Quox/Syntax/Dim.idr b/src/Quox/Syntax/Dim.idr
index e58e98d..f05f64e 100644
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@@ -7,26 +7,44 @@ import Quox.Pretty
 %default total
 
 
+public export
+data DimConst = Zero | One
+%name DimConst e
+
+private DCRepr : Type
+DCRepr = Nat
+
+private %inline dcrepr : DimConst -> DCRepr
+dcrepr e = case e of Zero => 0; One => 1
+
+export Eq  DimConst where (==) = (==) `on` dcrepr
+export Ord DimConst where compare = compare `on` dcrepr
+
+
 public export
 data Dim : Nat -> Type where
-  DZero, DOne : Dim d
-  DBound : Var d -> Dim d
+  K : DimConst -> Dim d
+  B : Var d -> Dim d
 %name Dim.Dim p, q
 
 private DRepr : Type
 DRepr = Nat
 
 private %inline drepr : Dim n -> DRepr
-drepr d = case d of DZero => 0; DOne => 1; DBound i => 2 + i.nat
+drepr p = case p of K i => dcrepr i; B i => 2 + i.nat
 
 export Eq  (Dim n) where (==) = (==) `on` drepr
 export Ord (Dim n) where compare = compare `on` drepr
 
+export
+PrettyHL DimConst where
+  prettyM Zero = hl Dim <$> ifUnicode "𝟬" "0"
+  prettyM One  = hl Dim <$> ifUnicode "𝟭" "1"
+
 export
 PrettyHL (Dim n) where
-  prettyM DZero      = hl Dim <$> ifUnicode "𝟬" "0"
-  prettyM DOne       = hl Dim <$> ifUnicode "𝟭" "1"
-  prettyM (DBound i) = prettyVar DVar DVarErr (!ask).dnames i
+  prettyM (K e) = prettyM e
+  prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i
 
 
 public export
@@ -41,10 +59,9 @@ prettyDSubst th =
     !(ifUnicode "⟨" "<") !(ifUnicode "⟩" ">") th
 
 
-export FromVar Dim where fromVar = DBound
+export FromVar Dim where fromVar = B
 
 export
 CanSubst Dim Dim where
-  DZero    // _  = DZero
-  DOne     // _  = DOne
-  DBound i // th = th !! i
+  K e // _  = K e
+  B i // th = th !! i