module Util where

open import Data.Nat
open import List
open import Data.Product hiding (map)
open import IO.Primitive
open import Function
open import Data.Bool renaming (T to isTrue)
open import Relation.Binary.PropositionalEquality
open import Maybe
open import Data.String hiding (_==_)
open import Eq

postulate Integer : Set
{-# BUILTIN INTEGER Integer #-}
{-# COMPILED_TYPE Integer Integer #-}

primitive primIntegerAbs   : Integer → ℕ
          primNatToInteger : ℕ → Integer

postulate showInteger : Integer → String
{-# COMPILED showInteger (show :: Integer -> String) #-}

showNat : ℕ → String
showNat = showInteger ∘ primNatToInteger

primitive primStringAppend : String → String → String

postulate
  ioError : {A : Set} → String → IO A

{-# COMPILED ioError (\_ -> error) #-}

_<$>_ : {A B : Set} → (A → B) → IO A → IO B
f <$> m = m >>= \x → return (f x)

withMaybe : {A B : Set} → Maybe A → B → (A → B) → B
withMaybe nothing  n j = n
withMaybe (just x) n j = j x

bindMaybe : {A B : Set} → Maybe A → (A → Maybe B) → Maybe B
bindMaybe m f = withMaybe m nothing f

mapMaybe : {A B : Set} → (A → Maybe B) → List A → Maybe (List B)
mapMaybe f [] = just []
mapMaybe f (x ∷ xs) =
  bindMaybe (f x)           \y  →
  bindMaybe (mapMaybe f xs) \ys →
  just (y ∷ ys)

elem : {u : EqType} → El u → List (El u) → Bool
elem x xs = any (_==_ x) xs

nub : {u : EqType} → List (El u) → List (El u)
nub []        = []
nub (x ∷ xs) = x ∷ filter (\y → not (x == y)) (nub xs)

lookup : {u : EqType}{A : Set} → El u → List (El u × A) → Maybe A
lookup x [] = nothing
lookup x ((y , z) ∷ xs) with x == y
... | true  = just z
... | false = lookup x xs

haskey : {u : EqType}{A : Set} → El u → List (El u × A) → Bool
haskey x xs = elem x (map proj₁ xs)

hasKeys : {u : EqType}{A : Set} → List (El u) → List (El u × A) → Bool
hasKeys []        xs = true
hasKeys (k ∷ ks) xs = haskey k xs ∧ hasKeys ks xs

lookup' : {u : EqType}{A : Set}(x : El u)(xs : List (El u × A)) →
          isTrue (elem x (map proj₁ xs)) → A
lookup' x [] ()
lookup' x ((y , z) ∷ xs) p with x == y
... | true  = z
... | false = lookup' x xs p

istrue : ∀ {b} → true ≡ b → isTrue b
istrue refl = _

isfalse : ∀ {b} → false ≡ b → isTrue (not b)
isfalse refl = _