newt/port/Prelude.newt

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

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

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

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

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 _<_
class Ord a where
  _<_ : a → a → Bool

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

-- Monad

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

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

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

-- 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 : {a b} → (a → b) → m a → m b

infixr 4 _<$>_
_<$>_ : {f} {{Functor f}} {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 : {a} → a → f a
  _<*>_ : {a b} -> f (a → b) → f a → f b

infixr 2 _<|>_
class Alternative (m : U → U) where
  _<|>_ : {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

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

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

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

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 arrayToList : {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
}"


pfunc getArgs : List String := "arrayToList(String, process.argv)"

-- 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 : 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]"

-- 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 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 : U} -> 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 a = \ w => MkIORes a w

pfunc putStrLn : String -> IO Unit := "(s) => (w) => {
  console.log(s)
  return MkIORes(Unit,MkUnit,w)
}"

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

infix 6 _<=_
pfunc _<=_ : Int -> Int -> Bool := "(x,y) => (x <= y) ? True : False"


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


ptype Dummy
pfunc fs : Dummy := "require('fs')"
pfunc readFile : (fn : String) -> IO String := "(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)"

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

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

instance Ord Int where
  x < y = ltInt x y

printLn : {a} {{Show a}} → a → IO Unit
printLn a = putStrLn $ show a