add samples to playground

playground/samples/Day1.newt

@@ -0,0 +1,75 @@
+module Day1
+
+-- Need to visit Lib.newt for this to work in playground
+import Lib
+
+digits1 : List Char -> List Int
+digits1 Nil = Nil
+digits1 (c :: cs) = let x = ord c in
+  case x < 58 of
+    True => case 48 < x of
+      True => x - 48 :: digits1 cs
+      False => digits1 cs
+    False => digits1 cs
+
+tail : {a : U} -> List a -> List a
+tail Nil = Nil
+tail (x :: xs) = xs
+
+-- TODO I used @ patterns in Lean
+digits2 : List Char -> List Int
+digits2 xs = case xs of
+    ('o' :: 'n' :: 'e' :: _) => 1 :: digits2 (tail xs)
+    ('t' :: 'w' :: 'o' :: _) => 2 :: digits2 (tail xs)
+    ('t' :: 'h' :: 'r' :: 'e' :: 'e' :: _) => 3 :: digits2 (tail xs)
+    ('f' :: 'o' :: 'u' :: 'r' :: _) => 4 :: digits2 (tail xs)
+    ('f' :: 'i' :: 'v' :: 'e' :: _) => 5 :: digits2 (tail xs)
+    ('s' :: 'i' :: 'x' :: _) => 6 :: digits2 (tail xs)
+    ('s' :: 'e' :: 'v' :: 'e' :: 'n' :: _) => 7 :: digits2 (tail xs)
+    ('e' :: 'i' :: 'g' :: 'h' :: 't' :: _) => 8 :: digits2 (tail xs)
+    ('n' :: 'i' :: 'n' :: 'e' :: _) => 9 :: digits2 (tail xs)
+    (c :: cs) => let x = ord c in
+        case x < 58 of
+          True => case 48 < x of
+            True => x - 48 :: digits2 cs
+            False => digits2 cs
+          False => digits2 cs
+    Nil => Nil
+
+
+combine : List Int -> Int
+combine Nil = 0
+combine (x :: Nil) = x * 10 + x
+combine (x :: y :: Nil) = x * 10 + y
+combine (x :: y :: xs) = combine (x :: xs)
+
+part1 : String -> (String -> List Int) -> Int
+part1 text digits =
+  let lines = split (trim text) "\n" in
+  let nums = map combine $ map digits lines in
+  foldl _+_ 0 nums
+
+-- Hack from before I had support for typeclasses
+infixl 1 _>>_
+_>>_ : {A B : U} -> A -> B -> B
+a >> b = b
+
+
+runFile : String -> Dummy
+runFile fn =
+  let text = readFile fn in
+  log fn >>
+  log "part1" >>
+  log (part1 text (digits1 . unpack)) >>
+  log "part2" >>
+  log (part1 text (digits2 . unpack)) >>
+  log ""
+
+
+-- Argument is a hack to keep it from running at startup.  Need to add IO
+main : Int -> Dummy
+main _ =
+  runFile "aoc2023/day1/eg.txt" >>
+  runFile "aoc2023/day1/eg2.txt" >>
+  runFile "aoc2023/day1/input.txt"
+

playground/samples/Day2.newt

@@ -0,0 +1,105 @@
+module Day2
+
+-- Need to visit Lib.newt for this to work in playground
+import Lib
+
+Draw : U
+Draw = Pair Int (Pair Int Int)
+
+data Game : U where
+  MkGame : Int -> List Draw -> Game
+
+-- Original had class and instance...
+-- Add, Sub, Mul, Neg
+
+-- NB this is not lazy!
+infixl 5 _&&_
+
+_&&_ : Bool -> Bool -> Bool
+a && b = case a of
+  False => False
+  True => b
+
+max : Int -> Int -> Int
+max x y = case x < y of
+  True => y
+  False => x
+
+pfunc repr : {a : U} -> a -> String := "(a,o) => ''+o"
+pfunc jrepr : {a : U} -> a -> String := "(a,o) => JSON.stringify(o, null, '  ')"
+pfunc toInt : String -> Int := "s => Number(s)"
+
+mapM : {a b c : U} -> (a -> Either b c) -> List a -> Either b (List c)
+mapM f Nil = Right Nil
+mapM f (x :: xs) = case f x of
+  Left msg => Left msg
+  Right v => case mapM f xs of
+    Left msg => Left msg
+    Right vs => Right $ v :: vs
+
+maxd : Draw -> Draw -> Draw
+maxd (a,b,c) (d,e,f) = (max a d, max b e, max c f)
+
+lte : Draw -> Draw -> Bool
+lte (a,b,c) (d,e,f) = a <= d && b <= e && c <= f
+
+parseColor : String -> Either String Draw
+parseColor line = case split line " " of
+  (n :: "red" :: Nil) => Right (toInt n,0,0)
+  (n :: "green" :: Nil) => Right (0,toInt n,0)
+  (n :: "blue" :: Nil) => Right (0,0,toInt n)
+  x => Left $ "Bad draw" ++ repr x
+
+parseDraw : String -> Either String Draw
+parseDraw line = case mapM parseColor $ split line ", " of
+  Right parts => Right $ foldl maxd (0,0,0) parts
+  Left err => Left err
+
+parseGame : String -> Either String Game
+parseGame line =
+  -- Need the Idris | sugar...
+  case split line ": " of
+    -- this is splitting on the Nil instead of the a
+    (a :: b :: Nil) => case split a " " of
+      ("Game" :: ns :: Nil) =>
+        let num = toInt ns in
+        case mapM parseDraw $ split b "; " of
+          Right parts => Right $ MkGame num parts
+          Left err => Left err
+      _ => Left "No Game"
+    _ => Left $ "No colon in " ++ line
+
+infixl 1 _>>_
+
+_>>_ : {A B : U} -> A -> B -> B
+a >> b = b
+
+part1 : List Game -> Int
+part1 Nil = 0
+part1 (MkGame n parts :: rest) =
+  let total = foldl maxd (0,0,0) parts in
+  case lte total (12,13,14) of
+    True => n + part1 rest
+    False => part1 rest
+
+part2 : List Game -> Int
+part2 Nil = 0
+part2 (MkGame n parts :: rest) =
+  case foldl maxd (0,0,0) parts of
+    (a,b,c) => a * b * c + part2 rest
+
+run : String -> Dummy
+run fn =
+  let text = readFile fn in
+  case mapM parseGame (split (trim text) "\n") of
+    Left err => log $ "fail " ++ err
+    Right games =>
+      log "part1" >>
+      log (part1 games) >>
+      log "part2" >>
+      log (part2 games)
+
+main : Dummy -> Dummy
+main _ =
+  run "aoc2023/day2/eg.txt" >>
+  run "aoc2023/day2/input.txt"

playground/samples/Lib.newt

@@ -0,0 +1,162 @@
+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 Int
+ptype String
+
+ptype Char
+
+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)

playground/samples/Prelude.newt

@@ -0,0 +1,47 @@
+module Prelude
+
+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
+
+-- TODO this is special cased in some languages, maybe for easier
+-- inference? Figure out why.
+
+infixr 0 _$_
+
+-- Currently very noisy in generated code
+_$_ : {a b : U} -> (a -> b) -> a -> b
+f $ a = f a
+
+
+-- Monad
+
+-- 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
+
+-- IO
+
+

playground/samples/Tree.newt

@@ -0,0 +1,96 @@
+module Tree
+
+-- adapted from Conor McBride's 2-3 tree example
+-- youtube video: https://youtu.be/v2yXrOkzt5w?t=3013
+
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Unit : U where
+  MkUnit : Unit
+
+data Void : U where
+
+infixl 4 _+_
+
+data _+_ : U -> U -> U where
+  inl : {A B : U} -> A -> A + B
+  inr : {A B : U} -> B -> A + B
+
+infix 4 _<=_
+
+_<=_ : Nat -> Nat -> U
+Z <= y = Unit
+S x <= Z = Void
+S x <= S y = x <= y
+
+cmp : (x y : Nat) -> (x <= y) + (y <= x)
+cmp Z y = inl MkUnit
+cmp (S z) Z = inr MkUnit
+cmp (S x) (S y) = cmp x y
+
+-- 53:21
+
+data Bnd : U where
+  Bot : Bnd
+  N : Nat -> Bnd
+  Top : Bnd
+
+infix 4 _<<=_
+
+_<<=_ : Bnd -> Bnd -> U
+Bot <<= _ = Unit
+N x <<= N y = x <= y
+_ <<= Top = Unit
+_ <<= _ = Void
+
+data Intv : Bnd -> Bnd -> U where
+  intv : {l u : Bnd} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
+
+data T23 : Bnd -> Bnd -> Nat -> U where
+  leaf : {l u : Bnd} {h : Nat} (lu : l <<= u) -> T23 l u Z
+  node2 : {l u : Bnd} {h : Nat} (x : _)
+    (tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
+    T23 l u (S h)
+  node3 : {l u : Bnd} {h : Nat} (x y : _)
+    (tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
+    T23 l u (S h)
+
+-- 56:
+
+infixl 5 _*_
+infixr 1 _,_
+data Sg : (A : U) -> (A -> U) -> U where
+  _,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
+
+_*_ : U -> U -> U
+A * B = Sg A (\ _ => B)
+
+TooBig : Bnd -> Bnd -> Nat -> U
+TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
+
+insert : {h : Nat} {l u : Bnd} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
+-- Agda is yellow here, needs h = x on each leaf
+-- The second arg to the second _,_ is unsolved and pi-typed
+insert (intv x lx xu) (leaf lu) = inl (x , (leaf {_} {_} {x} lx , leaf {_} {_} {x} xu))
+insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
+  -- u := N y is not solved at this time
+  inl xy => case insert (intv {_} {N y} x lx xy) tly of
+    inl (z , (tlz , tzy)) => inr (node3 z y tlz tzy tyu)
+    inr tly' => inr (node2 y tly' tyu)
+  inr yx => case insert (intv {N y} x yx xu) tyu of
+    inl (z , (tyz , tzu)) => inr (node3 y z tly tyz tzu)
+    inr tyu' => inr (node2 y tly tyu')
+insert (intv x lx xu) (node3 y z tly tyz tzu) = case cmp x y of
+  inl xy => case insert (intv {_} {N y} x lx xy) tly of
+    inl (v , (tlv , tvy)) => inl (y , (node2 v tlv tvy , node2 z tyz tzu))
+    inr tly' => inr (node3 y z tly' tyz tzu)
+  inr yx => case cmp x z of
+    inl xz => case insert (intv {N y} {N z} x yx xz) tyz of
+      inl (w , (tyw , twz)) => inl (w , (node2 y tly tyw , node2 z twz tzu))
+      inr tyz' => inr (node3 y z tly tyz' tzu)
+    inr zx => case insert (intv {N z} x zx xu) tzu of
+      inl (w , (tzw , twu)) => inl (z , (node2 y tly tyz , node2 w tzw twu))
+      inr tzu' => inr (node3 y z tly tyz tzu')

playground/samples/TypeClass.newt

@@ -0,0 +1,84 @@
+module TypeClass
+
+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
+
+data Either : U -> U -> U where
+  Left : {A B : U} -> A -> Either A B
+  Right : {A B : U} -> B -> Either A B
+
+bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
+bindEither (Left a) amb = Left a
+bindEither (Right b) amb = amb b
+
+EitherMonad : {A : U} -> Monad (Either A)
+EitherMonad = MkMonad {Either A} bindEither Right
+
+data Maybe : U -> U where
+  Just    : {A : U} -> A -> Maybe A
+  Nothing : {A : U} -> Maybe A
+
+bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
+bindMaybe Nothing amb = Nothing
+bindMaybe (Just a) amb = amb a
+
+MaybeMonad : Monad Maybe
+MaybeMonad = MkMonad bindMaybe Just
+
+infixr 7 _::_
+data List : U -> U where
+  Nil : {A : U} -> List A
+  _::_ : {A : U} -> A -> List A -> List A
+
+infixl 7 _++_
+_++_ : {A : U} -> List A -> List A -> List A
+Nil ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+bindList : {A B : U} -> List A -> (A -> List B) -> List B
+bindList Nil f = Nil
+bindList (x :: xs) f = f x ++ bindList xs f
+
+singleton : {A : U} -> A -> List A
+singleton a = a :: Nil
+
+-- TODO need better error when the monad is not defined
+ListMonad : Monad List
+ListMonad = MkMonad bindList singleton
+
+infixr 1 _,_
+data Pair : U -> U -> U where
+  _,_ : {A B : U} -> A -> B -> Pair A B
+
+ptype Int
+
+test : Maybe Int
+test = pure 10
+
+foo : Int -> Maybe Int
+foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
+
+bar : Int -> Maybe Int
+bar x = do
+  let y = x
+  z <- Just x
+  pure z
+
+baz : {A B : U} -> List A -> List B -> List (Pair A B)
+baz xs ys = do
+  x <- xs
+  y <- ys
+  pure (x , y)