
   0 | {--
   1 | Copyright (C) 2021  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 | ||| Generic library utilities.
  17 | module Util
  18 | 
  19 | import Control.Monad.Identity
  20 | import public Control.Monad.Reader
  21 | import Data.Contravariant
  22 | import public Data.List
  23 | import public Data.List.Quantifiers
  24 | import public Data.Nat
  25 | import public Data.Vect
  26 | 
  27 | ||| A `Neq x y` proves `x` is not equal to `y`.
  28 | public export 0
  29 | Neq : Nat -> Nat -> Type
  30 | Neq x y = Either (LT x y) (GT x y)
  31 | 
  32 | namespace Vect
  33 |   ||| All numbers from `0` to `n - 1` inclusive, in increasing order.
  34 |   |||
  35 |   ||| @n The (exclusive) limit of the range.
  36 |   export
  37 |   range : (n : Nat) -> Vect n Nat
  38 |   range Z = []
  39 |   range (S n) = snoc (range n) n
  40 | 
  41 |   ||| Enumerate entries in a vector with their indices. For example, `enumerate [5, 7, 9]`
  42 |   ||| is `[(0, 5), (1, 7), (2, 9)]`.
  43 |   export
  44 |   enumerate : Vect n a -> Vect n (Nat, a)
  45 |   enumerate xs =
  46 |     let lengthOK = lengthCorrect xs
  47 |      in rewrite sym lengthOK in zip (range (length xs)) (rewrite lengthOK in xs)
  48 | 
  49 | namespace List
  50 |   ||| All numbers from `0` to `n - 1` inclusive, in increasing order.
  51 |   |||
  52 |   ||| @n The (exclusive) limit of the range.
  53 |   export
  54 |   range : (n : Nat) -> List Nat
  55 |   range n = toList (Vect.range n)
  56 | 
  57 |   ||| Enumerate entries in a list with their indices. For example, `enumerate [5, 7, 9]`
  58 |   ||| is `[(0, 5), (1, 7), (2, 9)]`.
  59 |   export
  60 |   enumerate : List a -> List (Nat, a)
  61 |   enumerate xs = toList (enumerate (fromList xs))
  62 | 
  63 |   ||| `True` if there are no duplicate elements in the list, else `False`.
  64 |   |||
  65 |   ||| This function has time complexity quadratic in the list length.
  66 |   public export
  67 |   unique : Eq a => List a -> Bool
  68 |   unique [] = True
  69 |   unique (x :: xs) = not (elem x xs) && unique xs
  70 | 
  71 |   -- for some reason type inference doesn't work on the numbers in this proof if they're
  72 |   -- put in the test module
  73 |   unique' : HList [
  74 |         unique [1] = True
  75 |       , unique [0, 1] = True
  76 |       , unique [1, 0] = True
  77 |       , unique [0, 0] = False
  78 |       , unique [0, 0, 1] = False
  79 |       , unique [0, 1, 0] = False
  80 |       , unique [1, 0, 0] = False
  81 |       , unique [1, 1, 0] = False
  82 |       , unique [1, 0, 1] = False
  83 |       , unique [0, 1, 1] = False
  84 |       , unique [1, 2, 3] = True
  85 |     ]
  86 |   unique' = %search
  87 | 
  88 |   namespace All
  89 |     ||| Map a constrained function over a list given a list of constraints.
  90 |     public export
  91 |     map : (f : (x : a) -> {0 ok : p x} -> b) -> (xs : List a) -> {auto 0 allOk : All p xs} -> List b
  92 |     map f [] {allOk = []} = []
  93 |     map f (x :: xs) {allOk = ok :: _} = f {ok} x :: map f xs
  94 | 
  95 |   ||| Index multiple values from a list at once. For example,
  96 |   ||| `multiIndex [1, 3] [5, 6, 7, 8]` is `[6, 8]`.
  97 |   |||
  98 |   ||| @idxs The indices at which to index.
  99 |   ||| @xs The list to index.
 100 |   public export
 101 |   multiIndex : (idxs : List Nat) ->
 102 |                (xs : List a) ->
 103 |                {auto 0 inBounds : All (flip InBounds xs) idxs} ->
 104 |                List a
 105 |   multiIndex idxs xs = map f idxs
 106 | 
 107 |     where
 108 | 
 109 |     f : (i : Nat) -> {0 _ : InBounds i xs} -> a
 110 |     f i = index i xs
 111 | 
 112 |   ||| Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]`
 113 |   ||| is `[6, 8]`.
 114 |   |||
 115 |   ||| @idxs The indices of the values to delete.
 116 |   ||| @xs The list to delete values from.
 117 |   public export
 118 |   deleteAt : (idxs : List Nat) ->
 119 |              (xs : List a) ->
 120 |              {auto 0 inBounds : All (flip InBounds xs) idxs} ->
 121 |              List a
 122 |   deleteAt idxs xs = impl 0 xs
 123 |     where
 124 |     impl : Nat -> List a -> List a
 125 |     impl _ [] = []
 126 |     impl i (x :: xs) = if elem i idxs then impl (S i) xs else x :: impl (S i) xs
 127 | 
 128 |   namespace All2
 129 |     ||| A binary version of `All` from the standard library.
 130 |     public export
 131 |     data All2 : (0 p : a -> b -> Type) -> List a -> List b -> Type where
 132 |       Nil : All2 p [] []
 133 |       (::) : forall xs, ys . p x y -> All2 p xs ys -> All2 p (x :: xs) (y :: ys)
 134 | 
 135 |   ||| A `Sorted f xs` proves that for all consecutive elements `x` and `y` in `xs`, `f x y` exists.
 136 |   ||| For example, a `Sorted LT xs` proves that all `Nat`s in `xs` appear in increasing numerical
 137 |   ||| order.
 138 |   public export
 139 |   data Sorted : (a -> a -> Type) -> List a -> Type where
 140 |     ||| An empty list is sorted.
 141 |     SNil : Sorted f []
 142 | 
 143 |     ||| Any single element is sorted.
 144 |     SOne : Sorted f [x]
 145 | 
 146 |     ||| A list is sorted if its tail is sorted and the head is sorted w.r.t. the head of the tail.
 147 |     SCons : (y : a) -> f y x -> Sorted f (x :: xs) -> Sorted f (y :: x :: xs)
 148 | 
 149 |   ||| If an index is in bounds for a list, it's also in bounds for a longer list
 150 |   public export
 151 |   inBoundsCons : (xs : List a) -> InBounds k xs -> InBounds k (x :: xs)
 152 |   inBoundsCons _ InFirst = InFirst
 153 |   inBoundsCons (_ :: ys) (InLater prf) = InLater (inBoundsCons ys prf)
 154 | 
 155 | ||| Apply a function to the environment of a reader.
 156 | export
 157 | (>$<) : (env' -> env) -> ReaderT env m a -> ReaderT env' m a
 158 | f >$< (MkReaderT g) = MkReaderT (g . f)
 159 |