From 389a38f8b114379b9ee8c37da78a4ab1986883d6 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 31 Mar 2023 17:52:54 +0100 Subject: Define thinning composition. --- src/Core/Thinning.idr | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'src/Core') 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 -- cgit v1.2.3