module Lib

-- Prelude
data Unit : U where
  MkUnit : Unit

data Bool : U where
  True : Bool
  False : Bool

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

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 : U} -> List a
  _::_ : {a : U} -> a -> List a -> List a

Cons : {a : U} -> a -> List a -> List a
Cons x xs = x :: xs

-- TODO where clauses
reverse' : {A : U} -> List A -> List A -> List A
reverse' Nil acc = acc
reverse' (x :: xs) acc = reverse' xs (x :: acc)

reverse : {A : U} -> List A -> List A
reverse xs = reverse' xs Nil

length : {a : U} -> List a -> Nat
length Nil = Z
length (x :: xs) = S (length xs)

infixr 0 _,_

data Pair : U -> U -> U where
  _,_ : {a b : U} -> a -> b -> Pair a b

-- Idris says it special cases to deal with unification issues
infixr 0 _$_

_$_ : {a b : U} -> (a -> b) -> a -> b
f $ a = f a

-- JS Bridge

ptype Dummy


ptype World
data IO : U -> U where
  MkIO : {a : U} -> (World -> Pair World a) -> IO a

-- TODO unified Number for now





ptype Array : U -> U

pfunc arrayToList : {a : U} -> Array a -> List a := "
(a, arr) => {
  let rval = Nil(a)
  for (let i = arr.length - 1; i >= 0; i--) {
    rval = Cons(a, arr[i], rval)
  }
  return rval
}
"

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 getArgs : List String := `arrayToList(String, process.argv)`
-- Maybe integrate promises?


pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`

pfunc _<_ : Int -> Int -> Bool := `(x,y) => (x < y) ? True : False`
pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`
pfunc _+_ : Int -> Int -> Int := `(x,y) => x + y`
pfunc _-_ : Int -> Int -> Int := `(x,y) => x - y`
pfunc _*_ : Int -> Int -> Int := `(x,y) => x * y`
pfunc _/_ : Int -> Int -> Int := `(x,y) => x / y`

infix 6 _<_ _<=_
infixl 8 _+_ _-_
infixl 9 _*_ _/_

-- Ideally we'd have newt write the arrows for us to keep things correct
-- We'd still have difficulty with callbacks...
pfunc fs : Dummy := `require('fs')`
pfunc readFile : (fn : String) -> String := `(fn) => fs.readFileSync(fn, 'utf8')`
pfunc log : {a : U} -> a -> Dummy := `(a, obj) => console.log(obj)`

pfunc p_strHead : (s : String) -> Char := `(s) => s[0]`
pfunc p_strTail : (s : String) -> String := `(s) => s[0]`

pfunc trim : String -> String := `s => s.trim()`
pfunc split : String -> String -> List String := "(s, by) => {
  let parts = s.split(by)
  let rval = Nil(String)
  parts.reverse()
  parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) })
  return rval
}"

pfunc slen : String -> Int := `s => s.length`
pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`


infixl 7 _++_
pfunc _++_ : String -> String -> String := `(a,b) => a + b`


pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => {
  console.log(lab,a)
  return a
}"

pfunc unpack : String -> List Char
  := "(s) => {
    let acc = Nil(Char)
    for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
    return acc
}"

foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
foldl f acc Nil = acc
foldl f acc (x :: xs) = foldl f (f acc x) xs

map : {A B : U} -> (A -> B) -> List A -> List B
map f Nil = Nil
map f (x :: xs) = f x :: map f xs


infixl 9 _∘_
_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
(f ∘ g) x = f (g x)
