link prelude copies to same file

TODO.md

@@ -21,7 +21,7 @@
 - [ ] records
 - [ ] rework unify case tree
   - Idris needs help with the case tree to keep code size down, do it in stages, one dcon at a time.
-- [ ] Strategy to avoid three copies of `Prelude.newt` in this source tree
+- [x] Strategy to avoid three copies of `Prelude.newt` in this source tree
 - [ ] `mapM` needs inference help when scrutinee (see Day2.newt)
   - Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one.
 - [ ] Can't skip an auto. We need `{{_}}` to be auto or `%search` syntax.

aoc2023/Prelude.newt

@@ -1,629 +0,0 @@
-module Prelude
-
-id : ∀ a. a → a
-id x = x
-
-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
-
-infixl 6 _<_ _<=_
-class Ord a where
-  _<_ : a → a → Bool
-
-instance Ord Nat where
-  _ < Z = False
-  Z < S _ = True
-  S n < S m = n < m
-
-_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
-a <= b = a == b || a < 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 _>>=_ _>>_
-_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
-ma >>= amb = bind ma amb
-
-_>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
-ma >> mb = ma >>= (\ _ => mb)
-
-join : ∀ m. {{Monad m}} {0 a} → 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`
-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 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
-
-
-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 debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
-  console.log(s)
-  return MkIORes(undefined,MkUnit,w)
-}`
-
-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 : 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
-}`
-
-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?.tag === '_::_' || obj?.tag === 'Nil') {
-      let stuff = listToArray(undefined,obj)
-      return '['+(stuff.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)
-}`
-
-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
-
-instance Ord Int where
-  x < y = ltInt 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 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)
-}`
-
-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

aoc2023/Prelude.newt

@@ -0,0 +1 @@
+../newt/Prelude.newt

aoc2024/Prelude.newt

@@ -1 +1 @@
-../aoc2023/Prelude.newt
+../newt/Prelude.newt

newt/Prelude.newt

@@ -114,7 +114,7 @@ _>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
 ma >>= amb = bind ma amb
 
 _>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
-ma >> mb = mb
+ma >> mb = ma >>= (\ _ => mb)
 
 join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a
 join mma = mma >>= id
@@ -162,7 +162,14 @@ class Applicative (f : U → U) where
   _<*>_ : {0 a b} -> f (a → b) → f a → f b
 
 class Traversable (t : U → U) where
-  traverse : {f : U → U} → {{appf : Applicative f}} → {a : U} → {b : U} → (a → f b) → t a → f (t b)
+  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
@@ -187,10 +194,13 @@ infixl 7 _+_
 class Add a where
   _+_ : a → a → a
 
-infixl 8 _*_
+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)
@@ -305,6 +315,7 @@ instance Monad IO where
     MkIORes a w => mab a w
   pure a = \ w => MkIORes a w
 
+
 bindList : ∀ a b. List a → (a → List b) → List b
 
 instance ∀ a. Concat (List a) where
@@ -383,11 +394,11 @@ pfunc pack : List Char → String := `(cs) => {
 
 pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
   const go = (obj) => {
-    if (obj?.tag === '_::_') {
+    if (obj?.tag === '_::_' || obj?.tag === 'Nil') {
       let stuff = listToArray(undefined,obj)
       return '['+(stuff.map(go).join(', '))+']'
     }
-    if (obj?.tag === 'S') {
+    if (obj?.tag === 'S' || obj?.tag === 'Z') {
       return ''+natToInt(obj)
     } else if (obj?.tag) {
       let rval = '('+obj.tag
@@ -535,3 +546,84 @@ elem v (x :: xs) = if v == x then True else elem v xs
 -- 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 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)
+}`
+
+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

playground/build

@@ -1,4 +1,5 @@
 #!/bin/sh
+mkdir -p public
 echo build monaco worker
 esbuild --bundle node_modules/monaco-editor/esm/vs/editor/editor.worker.js > public/workerMain.js
 echo build newt worker

playground/samples/Prelude.newt

@@ -1,566 +0,0 @@
-module Prelude
-
-id : ∀ a. a → a
-id x = x
-
-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
-
-infixl 6 _<_ _<=_
-class Ord a where
-  _<_ : a → a → Bool
-
-instance Ord Nat where
-  _ < Z = False
-  Z < S _ = True
-  S n < S m = n < m
-
-_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
-a <= b = a == b || a < 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 _>>=_ _>>_
-_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
-ma >>= amb = bind ma amb
-
-_>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
-ma >> mb = mb
-
-join : ∀ m. {{Monad m}} {0 a} → 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 : U → U} → {{appf : Applicative f}} → {a : U} → {b : U} → (a → f b) → t a → f (t b)
-
-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`
-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 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
-
-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 debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
-  console.log(s)
-  return MkIORes(undefined,MkUnit,w)
-}`
-
-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 : 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
-}`
-
-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?.tag === '_::_') {
-      let stuff = listToArray(undefined,obj)
-      return '['+(stuff.map(go).join(', '))+']'
-    }
-    if (obj?.tag === 'S') {
-      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)
-}`
-
-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
-
-instance Ord Int where
-  x < y = ltInt 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

playground/samples/Prelude.newt

@@ -0,0 +1 @@
+../../newt/Prelude.newt

port/Prelude.newt

@@ -1,566 +0,0 @@
-module Prelude
-
-id : ∀ a. a → a
-id x = x
-
-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
-
-infixl 6 _<_ _<=_
-class Ord a where
-  _<_ : a → a → Bool
-
-instance Ord Nat where
-  _ < Z = False
-  Z < S _ = True
-  S n < S m = n < m
-
-_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
-a <= b = a == b || a < 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 _>>=_ _>>_
-_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
-ma >>= amb = bind ma amb
-
-_>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
-ma >> mb = mb
-
-join : ∀ m. {{Monad m}} {0 a} → 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 : U → U} → {{appf : Applicative f}} → {a : U} → {b : U} → (a → f b) → t a → f (t b)
-
-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`
-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 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
-
-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 debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
-  console.log(s)
-  return MkIORes(undefined,MkUnit,w)
-}`
-
-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 : 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
-}`
-
-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?.tag === '_::_') {
-      let stuff = listToArray(undefined,obj)
-      return '['+(stuff.map(go).join(', '))+']'
-    }
-    if (obj?.tag === 'S') {
-      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)
-}`
-
-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
-
-instance Ord Int where
-  x < y = ltInt 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