diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Thinning.idr | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr new file mode 100644 index 0000000..425d4ad --- /dev/null +++ b/src/Core/Thinning.idr @@ -0,0 +1,49 @@ +module Core.Thinning + +import Core.Context + +-- Definition ------------------------------------------------------------------ + +data Thinner : Context -> Context -> Type where + IsBase : (0 n : Name) -> Thinner sx (sx :< n) + IsDrop : Thinner sx sy -> (0 n : Name) -> Thinner sx (sy :< n) + IsKeep : Thinner sx sy -> (0 n : Name) -> Thinner (sx :< n) (sy :< n) + +export +data Thins : Context -> Context -> Type where + IsId : sx `Thins` sx + IsThinner : Thinner sx sy -> sx `Thins` sy + +%name Thinner thinner +%name Thins thin + +-- Constructors ---------------------------------------------------------------- + +export +id : (0 sx : Context) -> sx `Thins` sx +id sx = IsId + +export +drop : sx `Thins` sy -> (0 n : Name) -> sx `Thins` sy :< n +drop IsId n = IsThinner (IsBase n) +drop (IsThinner thinner) n = IsThinner (IsDrop thinner n) + +export +keep : sx `Thins` sy -> (0 n : Name) -> sx :< n `Thins` sy :< n +keep IsId n = IsId +keep (IsThinner thinner) n = IsThinner (IsKeep thinner n) + +-- Views ----------------------------------------------------------------------- + +public export +data View : sx `Thins` sy -> Type where + Id : (0 sx : Context) -> View (id sx) + Drop : (thin : sx `Thins` sy) -> (0 n : Name) -> View (drop thin n) + Keep : (thin : sx `Thins` sy) -> (0 n : Name) -> View (keep thin n) + +export +view : (thin : sx `Thins` sy) -> View thin +view IsId = Id sx +view (IsThinner (IsBase n)) = Drop IsId n +view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n +view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n |