Implement standard List operations for SnocLists (#2364)

Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>

libs/base/Data/SnocList.idr

@@ -217,6 +217,12 @@ toListCast (x::xs) = do
   rewrite toListCast xs
   Refl
 
+||| Append an element to the head of a snoc-list.
+||| Note: Traverses the snoc-list, linear time complexity
+public export
+cons : a -> SnocList a -> SnocList a
+cons x sx = [< x] ++ sx
+
 --- Folds ---
 
 export

libs/base/Data/SnocList/Operations.idr

@@ -0,0 +1,139 @@
+||| Operations on `SnocList`s, analogous to the `List` ones.
+||| Depending on your style of programming, these might cause
+||| ambiguities, so import with care
+module Data.SnocList.Operations
+
+import Data.SnocList
+import Data.List
+import Data.Nat
+import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
+
+%default total
+
+||| Take `n` last elements from `sx`, returning the whole list if
+||| `n` >= length `sx`.
+|||
+||| @ n  the number of elements to take
+||| @ sx the snoc-list to take the elements from
+public export
+takeTail : (n : Nat) -> (sx : SnocList a) -> SnocList a
+takeTail (S n) (sx :< x) = takeTail n sx :< x
+takeTail _ _ = [<]
+
+||| Remove `n` last elements from `xs`, returning the empty list if
+||| `n >= length xs`
+|||
+||| @ n  the number of elements to remove
+||| @ xs the list to drop the elements from
+public export
+dropTail : (n : Nat) -> (sx : SnocList a) -> SnocList a
+dropTail  0    sx        = sx
+dropTail (S n) [<]       = [<]
+dropTail (S n) (sx :< x) = dropTail n sx
+
+public export
+concatDropTailTakeTail : (n : Nat) -> (sx : SnocList a) ->
+  dropTail n sx ++ takeTail n sx === sx
+concatDropTailTakeTail 0 (sx :< x) = Refl
+concatDropTailTakeTail (S n) (sx :< x) = cong (:< x) $ concatDropTailTakeTail n sx
+concatDropTailTakeTail 0 [<] = Refl
+concatDropTailTakeTail (S k) [<] = Refl
+
+
+{- We can traverse a list while retaining both sides by decomposing it
+   into a snoc-list and a cons-list
+-}
+
+||| Shift `n` elements from the beginning of `xs` to the end of `sx`,
+||| returning the same lists if `n` >= length `xs`.
+|||
+||| @ n  the number of elements to take
+||| @ sx the snoc-list to append onto
+||| @ xs the list to take the elements from
+public export
+splitOntoLeft : (n : Nat) -> (sx : SnocList a) -> (xs : List a) -> (SnocList a, List a)
+splitOntoLeft (S n) sx (x :: xs) = splitOntoLeft n (sx :< x) xs
+splitOntoLeft _ sx xs = (sx, xs)
+
+||| Shift `n` elements from the end of `sx` to the beginning of `xs`,
+||| returning the same lists if `n` >= length `sx`.
+|||
+||| @ n  the number of elements to take
+||| @ sx the snoc-list to take the elements from
+||| @ xs the list to append onto
+public export
+splitOntoRight : (n : Nat) -> (sx : SnocList a) -> (xs : List a) -> (SnocList a, List a)
+splitOntoRight (S n) (sx :< x) xs = splitOntoRight n sx (x :: xs)
+splitOntoRight _ sx xs = (sx, xs)
+
+export
+splitOntoRightInvariant : (n : Nat) -> (sx : SnocList a) -> (xs : List a) ->
+  fst (splitOntoRight n sx xs) <>< snd (splitOntoRight n sx xs) === sx <>< xs
+splitOntoRightInvariant (S n) (sx :< x) xs = splitOntoRightInvariant n sx (x :: xs)
+splitOntoRightInvariant  0    sx  xs = Refl
+splitOntoRightInvariant (S k) [<] xs = Refl
+
+export
+splitOntoRightSpec : (n : Nat) -> (sx : SnocList a) -> (xs : List a) ->
+  (fst (splitOntoRight n sx xs) === dropTail n sx, snd (splitOntoRight n sx xs) = takeTail n sx <>> xs)
+splitOntoRightSpec (S k) (sx :< x) xs = splitOntoRightSpec k sx (x :: xs)
+splitOntoRightSpec  0    sx        xs = (Refl, Refl)
+splitOntoRightSpec (S k) [<]       xs = (Refl, Refl)
+
+export
+splitOntoLeftSpec : (n : Nat) -> (sx : SnocList a) -> (xs : List a) ->
+  (fst (splitOntoLeft n sx xs) === sx <>< take n xs, snd (splitOntoLeft n sx xs) = drop n xs)
+splitOntoLeftSpec (S k) sx (x :: xs) = splitOntoLeftSpec k (sx :< x) xs
+splitOntoLeftSpec  0    sx        xs = (Refl, Refl)
+splitOntoLeftSpec (S k) sx [] = (Refl, Refl)
+
+export
+lengthHomomorphism : (sx,sy : SnocList a) -> length (sx ++ sy) === length sx + length sy
+lengthHomomorphism sx [<] = sym $ plusZeroRightNeutral _
+lengthHomomorphism sx (sy :< x) = Calc $
+  |~ 1 + (length (sx ++ sy))
+  ~~ 1 + (length sx + length sy) ...(cong (1+) $ lengthHomomorphism _ _)
+  ~~ length sx + (1 + length sy) ...(plusSuccRightSucc _ _)
+
+-- cons-list operations on snoc-lists
+
+||| Take `n` first elements from `sx`, returning the whole list if
+||| `n` >= length `sx`.
+|||
+||| @ n  the number of elements to take
+||| @ sx the snoc-list to take the elements from
+|||
+||| Note: traverses the whole the input list, so linear in `n` and
+||| `length sx`
+public export
+take : (n : Nat) -> (sx : SnocList a) -> SnocList a
+take n sx = dropTail (length sx `minus` n) sx
+
+||| Drop `n` first elements from `sx`, returning an empty list if
+||| `n` >= length `sx`.
+|||
+||| @ n  the number of elements to drop
+||| @ sx the snoc-list to drop the elements from
+|||
+||| Note: traverses the whole the input list, so linear in `n` and
+||| `length sx`
+public export
+drop : (n : Nat) -> (sx : SnocList a) -> SnocList a
+drop n sx = takeTail (length sx `minus` n) sx
+
+public export
+data NonEmpty : SnocList a -> Type where
+  IsSnoc : NonEmpty (sx :< x)
+
+public export
+last : (sx : SnocList a) -> {auto 0 nonEmpty : NonEmpty sx} -> a
+last (sx :< x) {nonEmpty = IsSnoc} = x
+
+public export
+intersectBy : (a -> a -> Bool) -> SnocList a -> SnocList a -> SnocList a
+intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
+
+public export
+intersect : Eq a => SnocList a -> SnocList a -> SnocList a
+intersect = intersectBy (==)

libs/base/Data/SnocList/Quantifiers.idr

@@ -36,7 +36,7 @@ namespace Any
     uninhabited (There y) = uninhabited y
 
   ||| Modify the property given a pointwise function
-  export
+  public export
   mapProperty : (f : {0 x : a} -> p x -> q x) -> Any p l -> Any q l
   mapProperty f (Here p) = Here (f p)
   mapProperty f (There p) = There (mapProperty f p)
@@ -96,7 +96,7 @@ namespace All
     uninhabited @{Right _} (pxs :< px) = uninhabited pxs
 
   ||| Modify the property given a pointwise function
-  export
+  public export
   mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
   mapProperty f [<] = [<]
   mapProperty f (pxs :< px) = mapProperty f pxs :< f px

libs/base/base.ipkg

@@ -55,6 +55,7 @@ modules = Control.App,
           Data.SnocList,
           Data.SnocList.Elem,
           Data.SnocList.Quantifiers,
+          Data.SnocList.Operations,
           Data.List.Elem,
           Data.List.Views,
           Data.List.Quantifiers,