newt/newt/Prelude.newt

module Prelude

id : ∀ a. a → a
id x = x

the : (a : U) → a → a
the _ a = a

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

infixr 5 _&&_
_&&_ : Bool → Bool → Bool
False && b = False
True && b = b

infixl 6 _==_
class Eq a where
  _==_ : a → a → Bool

infixl 6 _/=_
_/=_ : ∀ a. {{Eq a}} → a → a → Bool
a /= b = not (a == b)

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

pred : Nat → Nat
pred Z = Z
pred (S k) = k

instance Eq Nat where
  Z == Z = True
  S n == S m = n == m
  x == y = False

data Maybe : U -> U where
  Just : ∀ a. a -> Maybe a
  Nothing : ∀ a. Maybe a

fromMaybe : ∀ a. a → Maybe a → a
fromMaybe a Nothing = a
fromMaybe _ (Just a) = a

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

infixr 7 _::_
data List : U -> U where
  Nil : ∀ A. List A
  _::_ : ∀ A. A → List A → List A

length : ∀ a. List a → Nat
length Nil = Z
length (x :: xs) = S (length xs)


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

-- This is now handled by the parser, and LHS becomes `f a`.
-- infixr 0 _$_
-- _$_ : ∀ a b. (a -> b) -> a -> b
-- f $ a = f a

infixr 8 _×_
infixr 2 _,_
data _×_ : U → U → U where
  _,_ : ∀ A B. A → B → A × B

fst : ∀ a b. a × b → a
fst (a,b) = a

snd : ∀ a b. a × b → b
snd (a,b) = b
-- Monad

class Monad (m : U → U) where
  bind : {0 a b} → m a → (a → m b) → m b
  pure : {0 a} → a → m a

infixl 1 _>>=_ _>>_
_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
ma >>= amb = bind ma amb

_>>_ :  ∀ m a b. {{Monad m}} -> m a -> m b -> m b
ma >> mb = ma >>= (\ _ => mb)

join : ∀ m a. {{Monad m}} → m (m a) → m a
join mma = mma >>= id

-- 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

class Functor (m : U → U) where
  map : {0 a b} → (a → b) → m a → m b

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

instance Functor Maybe where
  map f Nothing = Nothing
  map f (Just a) = Just (f a)

instance Functor List where
  map f Nil = Nil
  map f (x :: xs) = f x :: map f xs

instance Functor SnocList where
  map f Lin = Lin
  map f (xs :< x) = map f xs :< f x

-- TODO this probably should depend on / entail Functor
infixl 3 _<*>_
class Applicative (f : U → U) where
  -- appIsFunctor : Functor f
  return : {0 a} → a → f a
  _<*>_ : {0 a b} -> f (a → b) → f a → f b

class Traversable (t : U → U) where
  traverse : ∀ f a b. {{Applicative f}} → (a → f b) → t a → f (t b)

instance Traversable List where
  traverse f Nil = return Nil
  traverse f (x :: xs) = return _::_ <*> f x <*> traverse f xs

for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b)
for stuff fun = traverse fun stuff

instance Applicative Maybe where
  return a = Just a
  Nothing <*> _ = Nothing
  Just f <*> fa = f <$> fa

infixr 2 _<|>_
class Alternative (m : U → U) where
  _<|>_ : {0 a} → m a → m a → m a

instance Alternative Maybe where
  Nothing <|> x = x
  Just x <|> _ = Just x

-- Semigroup

infixl 8 _<+>_
class Semigroup a where
  _<+>_ : a → a → a

infixl 7 _+_
class Add a where
  _+_ : a → a → a

infixl 8 _*_ _/_
class Mul a where
  _*_ : a → a → a

class Div a where
  _/_ : a → a → a

instance Add Nat where
  Z + m = m
  S n + m = S (n + m)

instance Mul Nat where
  Z * _ = Z
  S n * m = m + n * m

infixl 7 _-_
class Sub a where
  _-_ : a → a → a

instance Sub Nat where
  Z - m = Z
  n - Z = n
  S n - S m = n - m

infixr 7 _++_
class Concat a where
  _++_ : a → a → a

ptype String
ptype Int
ptype Char

pfunc sconcat : String → String → String := `(x,y) => x + y`
instance Concat String where
  _++_ = sconcat


pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False`
pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? True : False`

instance Eq Int where
  a == b = jsEq a b

instance Eq String where
  a == b = jsEq a b

instance Eq Char where
  a == b = jsEq a b

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 : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length`
pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []`

pfunc arrayToList uses (Nil _::_) : {0 a} → Array a → List a := `(a,arr) => {
  let rval = Nil(a)
  for (let i = arr.length - 1;i >= 0; i--) {
    rval = _$3A$3A_(a, arr[i], rval)
  }
  return rval
}`



-- for now I'll run this in JS
pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))`

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 uses (Nil _::_) : String -> String -> List String := `(s, by) => {
  let parts = s.split(by)
  let rval = Nil(String)
  parts.reverse()
  parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
  return rval
}`

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

-- TODO represent Nat as number at runtime
pfunc natToInt : Nat -> Int := `(n) => {
  let rval = 0
  while (n.tag === 'S') {
    n = n.h0
    rval++
  }
  return rval
}`

pfunc intToNat uses (Z S) : Int -> Nat := `(n) => {
  let rval = Z
  for (;n>0;n--) rval = S(rval);
  return rval;
}`



pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')`
pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))`

-- I don't want to use an empty type because it would be a proof of void
ptype World

data IORes : U -> U where
  MkIORes : ∀ a. a -> World -> IORes a

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

instance Monad IO where
  bind ma mab = \ w => case ma w of
    MkIORes a w => mab a w
  pure x = \ w => MkIORes x w

bindList : ∀ a b. List a → (a → List b) → List b

instance ∀ a. Concat (List a) where
  Nil ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

instance Monad List where
  pure a = a :: Nil
  bind Nil amb = Nil
  bind (x :: xs) amb = amb x ++ bind xs amb



-- This is traverse, but we haven't defined Traversable yet
mapA : ∀ m. {{Applicative m}} {0 a b} → (a → m b) → List a → m (List b)
mapA f Nil = return Nil
mapA f (x :: xs) = return _::_ <*> f x <*> mapA f xs


mapM : ∀ m. {{Monad m}} {0 a b} → (a → m b) → List a → m (List b)
mapM f Nil = pure Nil
mapM f (x :: xs) = do
  b <- f x
  bs <- mapM f xs
  pure (b :: bs)

class HasIO (m : U -> U) where
  liftIO : ∀ a. IO a → m a

instance HasIO IO where
  liftIO a = a

pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
  console.log(s)
  return MkIORes(undefined,MkUnit,w)
}`

putStrLn : ∀ io. {{HasIO io}} -> String -> io Unit
putStrLn s = liftIO (primPutStrLn s)

pfunc showInt : Int -> String := `(i) => String(i)`

class Show a where
  show : a → String

instance Show String where
  show a = a

instance Show Int where
  show = showInt

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

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

pfunc pack : List Char → String := `(cs) => {
  let rval = ''
  while (cs.tag === '_::_') {
    rval += cs.h1
    cs = cs.h2
  }
  return rval
}
`

pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
  const go = (obj) => {
    if (obj === undefined) return "_"
    if (obj.tag === '_,_') {
      let rval = '('
      while (obj?.tag === '_,_') {
        rval += go(obj.h2) + ', '
        obj = obj.h3
      }
      return rval + go(obj) + ')'
    }
    if (obj?.tag === '_::_' || obj?.tag === 'Nil') {
      let stuff = listToArray(undefined,obj)
      return '['+(stuff.map(go).join(', '))+']'
    }
    if (obj instanceof Array) {
      return 'io['+(obj.map(go).join(', '))+']'
    }
    if (obj?.tag === 'S' || obj?.tag === 'Z') {
      return ''+natToInt(obj)
    } else if (obj?.tag) {
      let rval = '('+obj.tag
      for(let i=0;;i++) {
        let key = 'h'+i
        if (!(key in obj)) break
        rval += ' ' + go(obj[key])
      }
      return rval+')'
    } else {
      return JSON.stringify(obj)
    }
  }
  return go(obj)
}`

debugLog : ∀ a. a → IO Unit
debugLog a = putStrLn (debugStr a)

pfunc stringToInt : String → Int := `(s) => {
  let rval = Number(s)
  if (isNaN(rval)) throw new Error(s + " is NaN")
  return rval
}`

foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
foldl f acc Nil = acc
foldl f acc (x :: xs) = foldl f (f acc x) xs

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


pfunc addInt : Int → Int → Int := `(x,y) => x + y`
pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
pfunc subInt : Int → Int → Int := `(x,y) => x - y`
pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False`

instance Mul Int where
  x * y = mulInt x y

instance Add Int where
  x + y = addInt x y

instance Sub Int where
  x - y = subInt x y

printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
printLn a = putStrLn (show a)

-- opaque JSObject
ptype JSObject

reverse : ∀ a. List a → List a
reverse {a} = go Nil
  where
    go : List a → List a → List a
    go acc Nil = acc
    go acc (x :: xs) = go (x :: acc) xs

-- Like Idris1, but not idris2, we need {a} to put a in scope.
span : ∀ a. (a -> Bool) -> List a -> List a × List a
span {a} f xs = go xs Nil
  where
    go : List a -> List a -> List a × List a
    go Nil left = (reverse left, Nil)
    go (x :: xs) left = if f x
      then go xs (x :: left)
      else (reverse left, x :: xs)

instance Show Nat where
  show n = show (natToInt n)

enumerate : ∀ a. List a → List (Nat × a)
enumerate {a} xs = go Z xs
  where
    go : Nat → List a → List (Nat × a)
    go k Nil = Nil
    go k (x :: xs) = (k,x) :: go (S k) xs

filter : ∀ a. (a → Bool) → List a → List a
filter pred Nil = Nil
filter pred (x :: xs) = if pred x then x :: filter pred xs else filter pred xs

drop : ∀ a. Nat -> List a -> List a
drop _ Nil = Nil
drop Z xs = xs
drop (S k) (x :: xs) = drop k xs

take : ∀ a. Nat -> List a -> List a
take Z xs = Nil
take _ Nil = Nil
take (S k) (x :: xs) = x :: take k xs

getAt : ∀ a. Nat → List a → Maybe a
getAt _ Nil = Nothing
getAt Z (x :: xs) = Just x
getAt (S k) (x :: xs) = getAt k xs

splitOn : ∀ a. {{Eq a}} → a → List a → List (List a)
splitOn {a} v xs = go Nil xs
  where
    go : List a → List a → List (List a)
    go acc Nil = reverse acc :: Nil
    go acc (x :: xs) = if x == v
      then reverse acc :: go Nil xs
      else go (x :: acc) xs


class Inhabited a where
  default : a

instance ∀ a. Inhabited (List a) where
  default = Nil

getAt! : ∀ a. {{Inhabited a}} → Nat → List a → a
getAt! _ Nil = default
getAt! Z (x :: xs) = x
getAt! (S k) (x :: xs) = getAt! k xs


instance ∀ a. Applicative (Either a) where
  return b = Right b
  Right x <*> Right y = Right (x y)
  Left x <*> _ = Left x
  Right x <*> Left y = Left y

instance ∀ a. Monad (Either a) where
  pure x = Right x
  bind (Right x) mab = mab x
  bind (Left x) mab = Left x

instance Monad Maybe where
  pure x = Just x
  bind Nothing mab = Nothing
  bind (Just x) mab = mab x


elem : ∀ a. {{Eq a}} → a → List a → Bool
elem v Nil = False
elem v (x :: xs) = if v == x then True else elem v xs

-- TODO no empty value on my `Add`, I need a group..
-- sum : ∀ a. {{Add a}} → List a → a
-- sum xs = foldl _+_
pfunc trace uses (debugStr) : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }`

mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
mapMaybe f Nil = Nil
mapMaybe f (x :: xs) = case f x of
  Just y => y :: mapMaybe f xs
  Nothing => mapMaybe f xs

zip : ∀ a b. List a → List b → List (a × b)
zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
zip _ _ = Nil

-- TODO add double literals
ptype Double
pfunc intToDouble : Int → Double := `(x) => x`
pfunc doubleToInt : Double → Int := `(x) => x`
pfunc addDouble : Double → Double → Double := `(x,y) => x + y`
pfunc subDouble : Double → Double → Double := `(x,y) => x - y`
pfunc mulDouble : Double → Double → Double := `(x,y) => x * y`
pfunc divDouble : Double → Double → Double := `(x,y) => x / y`
pfunc sqrtDouble : Double → Double := `(x) => Math.sqrt(x)`
pfunc ceilDouble : Double → Double := `(x) => Math.ceil(x)`

instance Add Double where x + y = addDouble x y
instance Sub Double where x - y = subDouble x y
instance Mul Double where x * y = mulDouble x y
instance Div Double where x / y = divDouble x y

ptype IOArray : U → U

pfunc newArray uses (MkIORes) : ∀ a. Int → a → IO (IOArray a) :=
  `(_, n, v) => (w) => MkIORes(undefined,Array(n).fill(v),w)`
pfunc arrayGet : ∀ a. IOArray a → Int → IO a := `(_, arr, ix) => w => MkIORes(undefined, arr[ix], w)`
pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_, arr, ix, v) => w => {
  arr[ix] = v
  return MkIORes(undefined, MkUnit, w)
}`
pfunc arraySize uses (MkIORes) : ∀ a. IOArray a → IO Int := `(_, arr) => w => MkIORes(undefined, arr.length, w)`

pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a) := `(a,arr) => w => {
  let rval = Nil(a)
  for (let i = arr.length - 1;i >= 0; i--) {
    rval = _$3A$3A_(a, arr[i], rval)
  }
  return MkIORes(undefined, rval, w)
}`

pfunc listToIOArray uses (MkIORes) : {0 a} → List a → IO (Array a) := `(a,list) => w => {
  let rval = []
  while (list.tag === '_::_') {
    rval.push(list.h1)
    list = list.h2
  }
  return MkIORes(undefined,rval,w)
}`

class Cast a b where
  cast : a → b

instance Cast Nat Int where
  cast = natToInt

instance Cast Int Double where
  cast = intToDouble

instance Applicative IO where
  return a = \ w => MkIORes a w
  f <*> a = \ w =>
    let (MkIORes f w) = trace "fw" $ f w in
    let (MkIORes a w) = trace "aw" $ a w in
    MkIORes (f a) w

class Bifunctor (f : U → U → U) where
  bimap : ∀ a b c d. (a → c) → (b → d) → f a b → f c d

mapFst : ∀ a b c f. {{Bifunctor f}} → (a → c) → f a b → f c b
mapFst f ab = bimap f id ab

mapSnd : ∀ a b c f. {{Bifunctor f}} → (b → c) → f a b → f a c
mapSnd f ab = bimap id f ab

isNothing : ∀ a. Maybe a → Bool
isNothing Nothing = True
isNothing _ = False

instance Bifunctor _×_ where
  bimap f g (a,b) = (f a, g b)

instance Functor IO where
  map f a = bind a $ \ a => pure (f a)

uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c
uncurry f (a,b) = f a b

-- TODO Idris has a tail recursive version of this
instance Applicative List where
  return a = a :: Nil
  Nil <*> _ = Nil
  fs <*> ys = join $ map (\ f => map f ys) fs

tail : ∀ a. List a → List a
tail Nil = Nil
tail (x :: xs) = xs

--

infixl 6 _<_ _<=_
class Ord a where
  -- isEq : Eq a
  _<_ : a → a → Bool

_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
a <= b = a == b || a < b


search : ∀ cl. {{cl}} -> cl
search {{x}} = x

instance Ord Nat where
  -- isEq = search
  _ < Z = False
  Z < S _ = True
  S n < S m = n < m


instance Ord Int where
  -- isEq = ?
  x < y = ltInt x y

instance Ord Char where
  x < y = jsLT x y

-- foo : ∀ a. {{Ord a}} -> a -> Bool
-- foo a = a == a


flip : ∀ a b c. (a → b → c) → (b → a → c)
flip f b a = f a b

partition : ∀ a. (a → Bool) → List a → List a × List a
partition {a} pred xs = go xs Nil Nil
  where
    go : List a → List a → List a → List a × List a
    go Nil as bs = (as, bs)
    go (x :: xs) as bs = if pred x
      then go xs (x :: as) bs
      else go xs as (x :: bs)

-- probably not super efficient, but it works
qsort : ∀ a. (a → a → Bool) → List a → List a
qsort lt Nil = Nil
qsort lt (x :: xs) = qsort lt (filter (λ y => not $ lt x y) xs) ++ x :: qsort lt (filter (lt x) xs)

ordNub : ∀ a. {{Eq a}} {{Ord a}} -> List a -> List a
ordNub {a} {{ordA}} xs = go $ qsort _<_ xs
  where
    go : List a → List a
    go (a :: b :: xs) = if a == b then go (a :: xs) else a :: go (b :: xs)
    go t = t

ite : ∀ a. Bool → a → a → a
ite c t e = if c then t else e

instance Ord String where
  a < b = jsLT a b

instance Cast Int Nat where
  cast n = intToNat n