bikeshedding

This commit is contained in:
rhiannon morris 2021-12-23 15:55:18 +01:00
parent dbd0a3a451
commit 2a5b8ec815

View file

@ -36,25 +36,25 @@ Context' a = Context (\_ => a)
export
toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
toSnocList : Telescope {tm, _} -> SnocList (Exists tm)
toSnocList [<] = [<]
toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
private
toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
toListAcc : Telescope {tm, _} -> List (Exists tm) -> List (Exists tm)
toListAcc [<] acc = acc
toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
export %inline
toList : Telescope tm _ _ -> List (Exists tm)
toList : Telescope {tm, _} -> List (Exists tm)
toList tel = toListAcc tel []
export %inline
toSnocList' : Telescope' a _ _ -> SnocList a
toSnocList' : Telescope' {a, _} -> SnocList a
toSnocList' = map snd . toSnocList
export %inline
toList' : Telescope' a _ _ -> List a
toList' : Telescope' {a, _} -> List a
toList' = map snd . toList
@ -65,15 +65,15 @@ tel1 . [<] = tel1
tel1 . (tel2 :< s) = (tel1 . tel2) :< s
export
getWith : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
getWith (ctx :< t) VZ th = t // drop1 th
getWith (ctx :< t) (VS i) th = getWith ctx i (drop1 th)
public export
getShift : CanShift tm => Context tm len -> Var len -> Shift len out -> tm out
getShift (ctx :< t) VZ by = t // drop1 by
getShift (ctx :< t) (VS i) by = getShift ctx i (drop1 by)
infixl 8 !!
export %inline
public export %inline
(!!) : CanShift tm => Context tm len -> Var len -> tm len
ctx !! i = getWith ctx i SZ
ctx !! i = getShift ctx i SZ
||| a triangle of bindings. each type binding in a context counts the ues of
@ -173,35 +173,34 @@ zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
export
lengthPrf : Telescope _ from to -> Subset Nat $ \len => len + from = to
lengthPrf [<] = Element 0 Refl
lengthPrf (tel :< _) = let len = lengthPrf tel in
Element (S len.fst) (cong S len.snd)
lengthPrf : Telescope _ from to -> (len : Nat ** len + from = to)
lengthPrf [<] = (0 ** Refl)
lengthPrf (tel :< _) =
let len = lengthPrf tel in (S len.fst ** cong S len.snd)
public export %inline
length : Telescope {} -> Nat
length = fst . lengthPrf
parameters {0 acc : Nat -> Type}
export
foldl : (forall m, n. acc m -> tm n -> acc (S m)) ->
acc 0 -> (tel : Telescope tm from to) -> acc (length tel)
foldl : {0 acc : Nat -> Type} ->
(f : forall n. acc n -> tm (n + from) -> acc (S n)) ->
(z : acc 0) -> (tel : Telescope tm from to) -> acc (length tel)
foldl f z [<] = z
foldl f z (tel :< t) = f (foldl f z tel) t
foldl f z (tel :< t) = f (foldl f z tel) (rewrite (lengthPrf tel).snd in t)
parameters {auto _ : Monoid a}
export %inline
foldMap : (forall n. tm n -> a) -> Telescope tm from to -> a
foldMap : Monoid a => (forall n. tm n -> a) -> Telescope tm from to -> a
foldMap f = foldl (\acc, tm => acc <+> f tm) neutral
export %inline
fold : Telescope' a from to -> a
fold : Monoid a => Telescope' a from to -> a
fold = foldMap id
||| like `fold` but calculate the elements only when actually appending
export %inline
foldLazy : Telescope' (Lazy a) from to -> a
foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
foldLazy = foldMap force