diff options
Diffstat (limited to 'src/Core')
| -rw-r--r-- | src/Core/Thinning.idr | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index de0d5dc..1c8f41f 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -57,3 +57,18 @@ 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 ItIsThinner + +-- Operations ------------------------------------------------------------------ + +comp : Thinner sy sz -> Thinner sx sy -> sx `Thins` sz +comp (IsBase n) thinner1 = drop (IsThinner thinner1) n +comp (IsDrop thinner2 n) thinner1 = drop (comp thinner2 thinner1) n +comp (IsKeep thinner2 n) (IsBase n) = drop (IsThinner thinner2) n +comp (IsKeep thinner2 n) (IsDrop thinner1 n) = drop (comp thinner2 thinner1) n +comp (IsKeep thinner2 n) (IsKeep thinner1 n) = keep (comp thinner2 thinner1) n + +export +(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz +IsId . thin1 = thin1 +(IsThinner thinner2) . IsId = IsThinner thinner2 +(IsThinner thinner2) . (IsThinner thinner1) = comp thinner2 thinner1 |