Add type checking.HEADmaster

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

1 files changed, 23 insertions, 6 deletions

diff --git a/src/CC/Thinning.idr b/src/CC/Thinning.idr
index 284a230..d1e7745 100644
--- a/src/CC/Thinning.idr
+++ b/src/CC/Thinning.idr
@@ -1,10 +1,12 @@
 module CC.Thinning
 
+import Data.Singleton
+
 -- Definition ------------------------------------------------------------------
 
 export
 data Thins : (src, tgt : SnocList a) -> Type where
-  IsEmpty : [<] `Thins` [<]
+  IsDone : [<] `Thins` [<]
   IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
   IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x
 
@@ -13,8 +15,8 @@ data Thins : (src, tgt : SnocList a) -> Type where
 -- Operations ------------------------------------------------------------------
 
 export
-empty : [<] `Thins` [<]
-empty = IsEmpty
+done : [<] `Thins` [<]
+done = IsDone
 
 export
 drop : src `Thins` tgt -> src `Thins` tgt :< x
@@ -25,15 +27,30 @@ keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
 keep thin = IsKeep thin
 
 export
+empty : {ctx : SnocList a} -> [<] `Thins` ctx
+empty {ctx = [<]} = done
+empty {ctx = _ :< _} = drop empty
+
+export
 id : {ctx : SnocList a} -> ctx `Thins` ctx
-id {ctx = [<]} = empty
+id {ctx = [<]} = done
 id {ctx = _ :< _} = keep id
 
+export
+id' : Singleton ctx -> ctx `Thins` ctx
+id' (Val ctx) = id
+
+export
+(++) : src1 `Thins` tgt1 -> src2 `Thins` tgt2 -> src1 ++ src2 `Thins` tgt1 ++ tgt2
+thin ++ IsDone = thin
+thin ++ IsDrop thin' = IsDrop (thin ++ thin')
+thin ++ IsKeep thin' = IsKeep (thin ++ thin')
+
 -- Views -----------------------------------------------------------------------
 
 public export
 data View : src `Thins` tgt -> Type where
-  Empty : View CC.Thinning.empty
+  Done : View CC.Thinning.done
   Drop : (thin : src `Thins` tgt) -> View (drop thin)
   Keep : (thin : src `Thins` tgt) -> View (keep thin)
 
@@ -41,6 +58,6 @@ data View : src `Thins` tgt -> Type where
 
 public export
 view : (thin : src `Thins` tgt) -> View thin
-view IsEmpty = Empty
+view IsDone = Done
 view (IsDrop thin) = Drop thin
 view (IsKeep thin) = Keep thin