
   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 |   public export
  50 |   functorIdentity : forall a . (xs : Vect n a) -> map Prelude.id xs = xs
  51 |   functorIdentity [] = Refl
  52 |   functorIdentity (x :: xs) = cong2 (::) Refl (functorIdentity xs)
  53 | 
  54 | namespace List
  55 |   ||| All numbers from `0` to `n - 1` inclusive, in increasing order.
  56 |   |||
  57 |   ||| @n The (exclusive) limit of the range.
  58 |   export
  59 |   range : (n : Nat) -> List Nat
  60 |   range n = toList (Vect.range n)
  61 | 
  62 |   ||| Enumerate entries in a list with their indices. For example, `enumerate [5, 7, 9]`
  63 |   ||| is `[(0, 5), (1, 7), (2, 9)]`.
  64 |   export
  65 |   enumerate : List a -> List (Nat, a)
  66 |   enumerate xs = toList (enumerate (fromList xs))
  67 | 
  68 |   ||| `True` if there are no duplicate elements in the list, else `False`.
  69 |   |||
  70 |   ||| This function has time complexity quadratic in the list length.
  71 |   public export
  72 |   unique : Eq a => List a -> Bool
  73 |   unique [] = True
  74 |   unique (x :: xs) = not (elem x xs) && unique xs
  75 | 
  76 |   -- for some reason type inference doesn't work on the numbers in this proof if they're
  77 |   -- put in the test module
  78 |   unique' : HList [
  79 |         unique [1] = True
  80 |       , unique [0, 1] = True
  81 |       , unique [1, 0] = True
  82 |       , unique [0, 0] = False
  83 |       , unique [0, 0, 1] = False
  84 |       , unique [0, 1, 0] = False
  85 |       , unique [1, 0, 0] = False
  86 |       , unique [1, 1, 0] = False
  87 |       , unique [1, 0, 1] = False
  88 |       , unique [0, 1, 1] = False
  89 |       , unique [1, 2, 3] = True
  90 |     ]
  91 |   unique' = %search
  92 | 
  93 |   namespace All
  94 |     ||| Map a constrained function over a list given a list of constraints.
  95 |     public export
  96 |     map : (f : (x : a) -> {0 ok : p x} -> b) -> (xs : List a) -> {auto 0 allOk : All p xs} -> List b
  97 |     map f [] {allOk = []} = []
  98 |     map f (x :: xs) {allOk = ok :: _} = f {ok} x :: map f xs
  99 | 
 100 |   ||| Index multiple values from a list at once. For example,
 101 |   ||| `multiIndex [1, 3] [5, 6, 7, 8]` is `[6, 8]`.
 102 |   |||
 103 |   ||| @idxs The indices at which to index.
 104 |   ||| @xs The list to index.
 105 |   public export
 106 |   multiIndex : (idxs : List Nat) ->
 107 |                (xs : List a) ->
 108 |                {auto 0 inBounds : All (flip InBounds xs) idxs} ->
 109 |                List a
 110 |   multiIndex idxs xs = map f idxs
 111 | 
 112 |     where
 113 | 
 114 |     f : (i : Nat) -> {0 _ : InBounds i xs} -> a
 115 |     f i = index i xs
 116 | 
 117 |   ||| Delete values from a list at specified indices. For example `deleteAt [0, 2] [5, 6, 7, 8]`
 118 |   ||| is `[6, 8]`.
 119 |   |||
 120 |   ||| @idxs The indices of the values to delete.
 121 |   ||| @xs The list to delete values from.
 122 |   public export
 123 |   deleteAt : (idxs : List Nat) ->
 124 |              (xs : List a) ->
 125 |              {auto 0 inBounds : All (flip InBounds xs) idxs} ->
 126 |              List a
 127 |   deleteAt idxs xs = impl 0 xs
 128 |     where
 129 |     impl : Nat -> List a -> List a
 130 |     impl _ [] = []
 131 |     impl i (x :: xs) = if elem i idxs then impl (S i) xs else x :: impl (S i) xs
 132 | 
 133 |   public export
 134 |   functorIdentity : forall a . (xs : List a) -> map Prelude.id xs = xs
 135 |   functorIdentity [] = Refl
 136 |   functorIdentity (x :: xs) = cong2 (::) Refl (functorIdentity xs)
 137 | 
 138 |   ||| A binary version of `All` from the standard library.
 139 |   public export
 140 |   data All2 : (0 p : a -> b -> Type) -> List a -> List b -> Type where
 141 |     Nil : All2 p [] []
 142 |     (::) : forall xs, ys . p x y -> All2 p xs ys -> All2 p (x :: xs) (y :: ys)
 143 | 
 144 |   ||| The length of an `All2`.
 145 |   public export
 146 |   length : All2 f xs ys -> Nat
 147 |   length [] = 0
 148 |   length (_ :: xs) = S (length xs)
 149 | 
 150 |   ||| Map a function over the property of an `All2`.
 151 |   export
 152 |   mapProperty : (forall x, y . f x y -> g x y) -> All2 f xs ys -> All2 g xs ys
 153 |   mapProperty f [] = []
 154 |   mapProperty f (x :: xs) = f x :: mapProperty f xs
 155 | 
 156 |   ||| Run an effectful function over each property of an `All2`, sequencing the effects.
 157 |   export
 158 |   forProperty :
 159 |     Applicative m => All2 f xs ys -> (forall x, y . f x y -> m (g x y)) -> m (All2 g xs ys)
 160 |   forProperty [] _ = pure []
 161 |   forProperty (z :: zs) f = [| f z :: forProperty zs f |]
 162 | 
 163 |   ||| A `Sorted f xs` proves that for all consecutive elements `x` and `y` in `xs`, `f x y` exists.
 164 |   ||| For example, a `Sorted LT xs` proves that all `Nat`s in `xs` appear in increasing numerical
 165 |   ||| order.
 166 |   public export
 167 |   data Sorted : (a -> a -> Type) -> List a -> Type where
 168 |     ||| An empty list is sorted.
 169 |     SNil : Sorted f []
 170 | 
 171 |     ||| Any single element is sorted.
 172 |     SOne : Sorted f [x]
 173 | 
 174 |     ||| A list is sorted if its tail is sorted and the head is sorted w.r.t. the head of the tail.
 175 |     SCons : (y : a) -> f y x -> Sorted f (x :: xs) -> Sorted f (y :: x :: xs)
 176 | 
 177 |   ||| If an index is in bounds for a list, it's also in bounds for a longer list
 178 |   public export
 179 |   inBoundsCons : (xs : List a) -> InBounds k xs -> InBounds k (x :: xs)
 180 |   inBoundsCons _ InFirst = InFirst
 181 |   inBoundsCons (_ :: ys) (InLater prf) = InLater (inBoundsCons ys prf)
 182 | 
 183 | ||| Apply a function to the environment of a reader.
 184 | export
 185 | (>$<) : (env' -> env) -> ReaderT env m a -> ReaderT env' m a
 186 | f >$< (MkReaderT g) = MkReaderT (g . f)
 187 |