module Util where

open import Data.Nat
open import Data.List
open import Data.Product hiding (map)
open import IO.Primitive
open import Data.Function
open import Data.Bool renaming (T to isTrue)
open import Relation.Binary.PropositionalEquality
open import Data.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 = _