
   0 | {--
   1 | Copyright (C) 2026  Joel Berkeley
   2 | 
   3 | This program is free software: you can redistribute it and/or modify
   4 | it under the terms of the GNU Affero General Public License as published
   5 | by the Free Software Foundation, either version 3 of the License, or
   6 | (at your option) any later version.
   7 | 
   8 | This program is distributed in the hope that it will be useful,
   9 | but WITHOUT ANY WARRANTY; without even the implied warranty of
  10 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  11 | GNU Affero General Public License for more details.
  12 | 
  13 | You should have received a copy of the GNU Affero General Public License
  14 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
  15 | --}
  16 | ||| List definitions.
  17 | module Spidr.Data.List
  18 | 
  19 | import public Data.DPair
  20 | import public Data.List
  21 | import public Data.List.Quantifiers
  22 | 
  23 | ||| All numbers from `0` to `n - 1` inclusive, in increasing order.
  24 | |||
  25 | ||| @n The (exclusive) limit of the range.
  26 | export
  27 | range : (n : Nat) -> List Nat
  28 | range Z = []
  29 | range (S n) = snoc (range n) n
  30 | 
  31 | ||| Enumerate entries in a list with their indices. For example, `enumerate [5, 7, 9]`
  32 | ||| is `[(0, 5), (1, 7), (2, 9)]`.
  33 | export
  34 | enumerate : List a -> List (Nat, a)
  35 | enumerate xs = zip (range (length xs)) xs
  36 | 
  37 | ||| `True` if there are no duplicate elements in the list, else `False`.
  38 | |||
  39 | ||| This function has time complexity quadratic in the list length.
  40 | public export
  41 | unique : Eq a => List a -> Bool
  42 | unique [] = True
  43 | unique (x :: xs) = not (elem x xs) && unique xs
  44 | 
  45 | -- for some reason type inference doesn't work on the numbers in this proof if they're
  46 | -- put in the test module
  47 | unique' : HList [
  48 |       unique [1] = True
  49 |     , unique [0, 1] = True
  50 |     , unique [1, 0] = True
  51 |     , unique [0, 0] = False
  52 |     , unique [0, 0, 1] = False
  53 |     , unique [0, 1, 0] = False
  54 |     , unique [1, 0, 0] = False
  55 |     , unique [1, 1, 0] = False
  56 |     , unique [1, 0, 1] = False
  57 |     , unique [0, 1, 1] = False
  58 |     , unique [1, 2, 3] = True
  59 |   ]
  60 | unique' = %search
  61 | 
  62 | ||| Index multiple values from a list at once. For example,
  63 | ||| `multiIndex [1, 3] [5, 6, 7, 8]` is `[6, 8]`.
  64 | |||
  65 | ||| @idxs The indices at which to index.
  66 | ||| @xs The list to index.
  67 | public export
  68 | multiIndex :
  69 |   (idxs : List Nat) ->
  70 |   (xs : List a) ->
  71 |   {auto 0 inBounds : All (flip InBounds xs) idxs} ->
  72 |   List a
  73 | multiIndex idxs xs = map (\(Element i ib) => index i xs) $ pushIn idxs inBounds
  74 | 
  75 | ||| Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]`
  76 | ||| is `[6, 8]`.
  77 | |||
  78 | ||| @idxs The indices of the values to delete.
  79 | ||| @xs The list to delete values from.
  80 | public export
  81 | deleteAt :
  82 |   (idxs : List Nat) ->
  83 |   (xs : List a) ->
  84 |   {auto 0 inBounds : All (flip InBounds xs) idxs} ->
  85 |   List a
  86 | deleteAt idxs xs = impl 0 xs
  87 |   where
  88 |   impl : Nat -> List a -> List a
  89 |   impl _ [] = []
  90 |   impl i (x :: xs) = if elem i idxs then impl (S i) xs else x :: impl (S i) xs
  91 | 
  92 | public export
  93 | functorIdentity : forall a . (xs : List a) -> map Prelude.id xs = xs
  94 | functorIdentity [] = Refl
  95 | functorIdentity (x :: xs) = cong2 (::) Refl (functorIdentity xs)
  96 | 
  97 | ||| A binary version of `All` from the standard library.
  98 | public export
  99 | data All2 : (0 p : a -> b -> Type) -> List a -> List b -> Type where
 100 |   Nil : All2 p [] []
 101 |   (::) : forall xs, ys . p x y -> All2 p xs ys -> All2 p (x :: xs) (y :: ys)
 102 | 
 103 | ||| The length of an `All2`.
 104 | public export
 105 | length : All2 f xs ys -> Nat
 106 | length [] = 0
 107 | length (_ :: xs) = S (length xs)
 108 | 
 109 | ||| Map a function over the property of an `All2`.
 110 | export
 111 | mapProperty : (forall x, y . f x y -> g x y) -> All2 f xs ys -> All2 g xs ys
 112 | mapProperty f [] = []
 113 | mapProperty f (x :: xs) = f x :: mapProperty f xs
 114 | 
 115 | ||| Run an effectful function over each property of an `All2`, sequencing the effects.
 116 | export
 117 | forProperty :
 118 |   Applicative m => All2 f xs ys -> (forall x, y . f x y -> m (g x y)) -> m (All2 g xs ys)
 119 | forProperty [] _ = pure []
 120 | forProperty (z :: zs) f = [| f z :: forProperty zs f |]
 121 | 
 122 | ||| A `Sorted f xs` proves that for all consecutive elements `x` and `y` in `xs`, `f x y` exists.
 123 | ||| For example, a `Sorted LT xs` proves that all `Nat`s in `xs` appear in increasing numerical
 124 | ||| order.
 125 | public export
 126 | data Sorted : (a -> a -> Type) -> List a -> Type where
 127 |   ||| An empty list is sorted.
 128 |   SNil : Sorted f []
 129 | 
 130 |   ||| Any single element is sorted.
 131 |   SOne : Sorted f [x]
 132 | 
 133 |   ||| A list is sorted if its tail is sorted and the head is sorted w.r.t. the head of the tail.
 134 |   SCons : (y : a) -> f y x -> Sorted f (x :: xs) -> Sorted f (y :: x :: xs)
 135 | 
 136 | ||| If an index is in bounds for a list, it's also in bounds for a longer list
 137 | public export
 138 | inBoundsCons : (xs : List a) -> InBounds k xs -> InBounds k (x :: xs)
 139 | inBoundsCons _ InFirst = InFirst
 140 | inBoundsCons (_ :: ys) (InLater prf) = InLater (inBoundsCons ys prf)
 141 |