module Prelude


data Bool : U where
  True False : Bool

not : Bool → Bool
not True = False
not False = True

-- In Idris, this is lazy in the second arg, we're not doing
-- magic laziness for now, it's messy
infixr 4 _||_
_||_ : Bool → Bool → Bool
True || _ = True
False || b = b

data Nat : U where
  Z : Nat
  S : Nat -> Nat

data Maybe : U -> U where
  Just : {a : U} -> a -> Maybe a
  Nothing : {a : U} -> Maybe a

fromMaybe : {a} → a → Maybe a → a
fromMaybe a Nothing = a
fromMaybe _ (Just a) = a

data Either : U -> U -> U where
  Left : {a b : U} -> a -> Either a b
  Right : {a b : U} -> b -> Either a b

infixr 7 _::_
data List : U -> U where
  Nil : {A} → List A
  _::_ : {A} → A → List A → List A


infixl 7 _:<_
data SnocList : U → U where
  Lin : {A} → SnocList A
  _:<_ : {A} → SnocList A → A → SnocList A

-- 'chips'
infixr 6 _<>>_
_<>>_ : {a} → SnocList a → List a → List a
Lin <>> ys = ys
(xs :< x) <>> ys = xs <>> x :: ys

-- TODO this is special cased in some languages, maybe for easier
-- inference? Figure out why.
-- Currently very noisy in generated code (if nothing else, optimize it out?)
infixr 0 _$_
_$_ : {a b : U} -> (a -> b) -> a -> b
f $ a = f a

infixr 8 _×_
infixr 2 _,_
data _×_ : U → U → U where
  _,_ : {A B} → A → B → A × B


infixl 6 _<_
data Ord : U → U where
  MkOrd : {A} → (A → A → Bool) → Ord A

_<_ : {A} {{Ord A}} → A → A → Bool
_<_ {{MkOrd cmp}} a b = cmp a b

cmpNat : Nat → Nat → Bool
cmpNat Z Z = True
cmpNat Z m = False
cmpNat n Z = True
cmpNat (S n) (S m) = True

OrdNat : Ord Nat
OrdNat = MkOrd cmpNat

-- Monad

-- TODO sugar for if then else (mixfix is too eager)

-- TODO stack with Applicative, etc?

data Monad : (U -> U) -> U where
  MkMonad : { M : U -> U } ->
            (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
            (pure : {A : U} -> A -> M A) ->
            Monad M

infixl 1 _>>=_ _>>_
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb

_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
ma >> mb = mb

pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
pure {_} {_} {{MkMonad _ pure'}} a = pure' a

-- Equality

infixl 1 _≡_
data _≡_ : {A : U} -> A -> A -> U where
  Refl :  {A : U} -> {a : A} -> a ≡ a

replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
replace p Refl x = x

cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b

sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
sym Refl = Refl

-- Functor
data Functor : (U → U) → U where
  MkFunctor : {m : U → U} → ({a b : U} → (a → b) → m a → m b) → Functor m

map : {m} {{Functor m}} → {a b} → (a → b) → m a → m b
map {{MkFunctor f}} ma = f ma

infixr 4 _<$>_
_<$>_ : {f : U → U} {{Functor f}} {a b} → (a → b) → f a → f b
f <$> ma = map f ma


mapMaybe : {a b} → (a → b) → Maybe a → Maybe b
mapMaybe f Nothing = Nothing
mapMaybe f (Just a) = Just (f a)

FunctorMaybe : Functor Maybe
FunctorMaybe = MkFunctor mapMaybe



-- Idris is lazy in second arg, we don't have that.
data Alternative : (U → U) → U where
  MkAlt : {m : U → U} →
          ({a} → m a → m a → m a) →
          Alternative m

infixr 2 _<|>_
_<|>_ : {m : U → U} {{Alternative m}} → {a} → m a → m a → m a
_<|>_ {m} {{MkAlt f}} {a} x y = f x y

altMaybe : {a} → Maybe a → Maybe a → Maybe a
altMaybe Nothing x = x
altMaybe (Just x) _ = Just x

AltMaybe : Alternative Maybe
AltMaybe = MkAlt altMaybe

-- Semigroup

infixl 8 _<+>_
data Semigroup : U → U where
  MkSemi : {a} → (a → a → a) → Semigroup a

_<+>_ : {a} {{Semigroup a}} → a → a → a
_<+>_ {{MkSemi op}} x y = op x y


infixl 7 _+_
data Add : U → U where
  MkAdd : {A} → (A → A → A) → Add A

_+_ : {A} {{Add A}} → A → A → A
_+_ {{MkAdd add}} x y  = add x y

infixl 8 _*_
data Mul : U → U where
  MkMul : {A} →
          (A → A → A) →
          Mul A

_*_ : {A} {{Mul A}} → A → A → A
_*_ {{MkMul mul}} x y  = mul x y


-- TODO codata/copatterns might be nice here?
-- AddNat : AddNat
-- AddNat .add Z m = m
-- AddNat .add (S n) m = S (self .add n m)

addNat : Nat → Nat → Nat
addNat Z m = m
addNat (S n) m = S (addNat n m)

AddNat : Add Nat
AddNat = MkAdd addNat

mulNat : Nat → Nat → Nat
mulNat Z _ = Z
mulNat (S n) m = m + mulNat n m

MulNat : Mul Nat
MulNat = MkMul mulNat


-- TODO Sub
infixl 7 _-_
_-_ : Nat -> Nat -> Nat
Z - m = Z
n - Z = n
S n - S m = n - m


ptype String
ptype Int
ptype Char

-- probably want to switch to Int or implement magic Nat
pfunc length : String → Nat := "(s) => {
  let rval = Z
  for (let i = 0; i < s.length; s++) rval = S(rval)
  return rval
}"

data Unit : U where
  MkUnit : Unit

ptype Array : U → U
pfunc listToArray : {a : U} -> List a -> Array a := "
(a, l) => {
  let rval = []
  while (l.tag !== 'Nil') {
    rval.push(l.h1)
    l = l.h2
  }
  return rval
}
"
pfunc alen : {a : U} -> Array a -> Int := "(a,arr) => arr.length"
pfunc aget : {a : U} -> Array a -> Int -> a := "(a, arr, ix) => arr[ix]"
pfunc aempty : {a : U} -> Unit -> Array a := "() => []"


pfunc fastConcat : List String → String := "(xs) => listToArray(undefined, xs).join('')"
pfunc replicate : Nat -> Char → String := "() => abort('FIXME replicate')"



ptype World

data IORes : U -> U where
  MkIORes : {a : U} -> a -> World -> IORes a

IO : U -> U
IO a = World -> IORes a

-- TODO - if I move w to the left, I get "extra pattern variable"
-- because I'm not looking instide the IO b type, probably should force it.
iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
iobind ma mab = \ w => case ma w of
  (MkIORes a w) => mab a w

iopure : {a : U} -> a -> IO a
iopure a = \ w => MkIORes a w

IOMonad : Monad IO
IOMonad = MkMonad iobind iopure

pfunc putStrLn : String -> IO Unit := "(s) => (w) => console.log(s)"