module CC.Thinning import Data.Singleton -- Definition ------------------------------------------------------------------ export data Thins : (src, tgt : SnocList a) -> Type where IsDone : [<] `Thins` [<] IsDrop : src `Thins` tgt -> src `Thins` tgt :< x IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x %name Thins thin -- Operations ------------------------------------------------------------------ export done : [<] `Thins` [<] done = IsDone export drop : src `Thins` tgt -> src `Thins` tgt :< x drop thin = IsDrop thin export 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 = [<]} = 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 Done : View CC.Thinning.done Drop : (thin : src `Thins` tgt) -> View (drop thin) Keep : (thin : src `Thins` tgt) -> View (keep thin) %name View view public export view : (thin : src `Thins` tgt) -> View thin view IsDone = Done view (IsDrop thin) = Drop thin view (IsKeep thin) = Keep thin