more

unfinished/day3.quox

@@ -0,0 +1,96 @@
+load "string.quox"
+
+
+def0 Symbol : ★ = Char × ℕ × ℕ -- value, x, y
+def0 Number : ★ = ℕ × ℕ × ℕ × ℕ -- value, start_x, end_x, y
+
+namespace symbol {
+  def value : ω.Symbol → Char = λ s ⇒ fst s
+  def x     : ω.Symbol → ℕ    = λ s ⇒ fst (snd s)
+  def y     : ω.Symbol → ℕ    = λ s ⇒ snd (snd s)
+}
+
+namespace number {
+  def value : ω.Number → ℕ = λ n ⇒ fst n
+  def sx    : ω.Number → ℕ = λ n ⇒ fst (snd n)
+  def ex    : ω.Number → ℕ = λ n ⇒ fst (snd (snd n))
+  def y     : ω.Number → ℕ = λ n ⇒ snd (snd (snd n))
+}
+
+namespace element {
+  def0 Tag : ★ = {symbol, number}
+
+  def0 Body : Tag → ★ =
+    λ t ⇒ case t return ★ of { 'symbol ⇒ Symbol; 'number ⇒ Number }
+}
+
+def0 Element : ★ = (t : element.Tag) × element.Body t
+
+def make-symbol : (value : Char) → (x y : ℕ) → Element =
+  λ c x y ⇒ ('symbol, c, x, y)
+
+def make-number : (value start_x end_x y : ℕ) → Element =
+  λ v sx ex y ⇒ ('number, v, sx, ex, y)
+
+def dot = char.from-ℕ 0x2e
+
+
+def adj-x : ω.(nx sx ex : ℕ) → Bool =
+  λ nx sx ex ⇒ bool.and (nat.ge (succ nx) sx) (nat.le nx (succ ex))
+
+def adj-y : ω.(ny sy : ℕ) → Bool =
+  λ ny sy ⇒ bool.and (nat.ge (succ ny) sy) (nat.le ny (succ sy))
+
+
+def adjacent : ω.Symbol → ω.Number → Bool =
+  λ s n ⇒
+  bool.and (adj-x (symbol.x s) (number.sx n) (number.ex n))
+           (adj-y (symbol.y s) (number.y n))
+
+def any : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → Bool =
+  λ A p ⇒ list.foldlω A Bool 'false (λ b x ⇒ bool.or b (p x))
+
+def is-label : ω.(List Symbol) → ω.Number → Bool =
+  λ ss n ⇒ any Symbol (λ s ⇒ adjacent s n) ss
+
+
+namespace read {
+  def0 Digits : ★ = Maybe (List ℕ)
+
+  def0 State : ★ =
+    -- current number, x, y
+    Digits × ℕ × ℕ ×
+    -- stuff seen so far
+    List Number × List Symbol
+
+  def Cons = list.Cons
+  def Nil  = list.Nil
+
+  def add-digit : ℕ → Digits → Digits =
+    λ d ds ⇒
+    maybe.fold (List ℕ) (ℕ → Digits)
+      (λ    d ⇒ Just (List ℕ) (Cons ℕ d (Nil ℕ)))
+      (λ ds d ⇒ Just (List ℕ) (Cons ℕ d ds))
+      ds d
+
+  def next-col : State → State =
+    λ s ⇒
+    case s return State of { (ds, rest) ⇒
+      case rest return State of { (x, rest) ⇒ (ds, succ x, rest) }
+    }
+
+  def next-row : State → State =
+    λ s ⇒
+    case s return State of { (ds, rest) ⇒
+      case rest return State of { (x, rest) ⇒
+        nat.drop State x
+          (case rest return State of { (y, rest) ⇒ (ds, 0, succ y, rest) })
+      }
+    }
+
+  def seen-digit : Char → State → State =
+    λ c s ⇒
+    case s return State of {
+      (ds, rest) ⇒ (add-digit (char.digit c) ds, rest)
+    }
+}

unfinished/day8.quox

@@ -0,0 +1,50 @@
+load "bool.quox"
+load "string.quox"
+load "maybe.quox"
+load "io.quox"
+
+def if = bool.if
+
+def Nil = list.Nil; def Cons = list.Cons
+
+def0 Direction : ★ = {left, right}
+
+namespace direction {
+  def from-char : Char → Maybe Direction =
+    λ c ⇒
+      let0 Res = Maybe Direction in
+      letω L = char.from-ℕ 0x4C; R = char.from-ℕ 0x52 in
+      case char.dup c return Res of { [c] ⇒
+        if Res (char.eq c L) (Just Direction 'left)
+          (if Res (char.eq c R) (Just Direction 'right)
+            (Nothing Direction))
+      }
+
+  -- skips unknown characters, e.g. spaces
+  def from-string : String → List Direction =
+    let0 Res = List Direction in
+    λ str ⇒
+      list.foldr Char Res (Nil Direction)
+        (λ c ⇒ maybe.fold Direction (Res → Res)
+          (λ lst ⇒ lst) (Cons Direction) (from-char c))
+        (string.to-list str)
+}
+
+def which : 0.(A : ★) → ω.(A × A) → Direction → A =
+  λ A xy d ⇒ case d return A of { 'left ⇒ fst xy; 'right ⇒ snd xy }
+
+def lookup : 0.(A B : ★) → ω.(ω.A → Bool) → ω.(List (A × B)) → Maybe B =
+  λ A B p ⇒
+    list.foldlω (A × B) (Maybe B) (Nothing B)
+      (λ st x ⇒ maybe.foldω B (Maybe B)
+        (if (Maybe B) (p (fst x)) (Just B (snd x)) (Nothing B))
+        (λ ok ⇒ Just B ok) st)
+
+def0 Map : ★ = List (String × String × String)
+
+def next : ω.Map → ω.String → ω.Direction → Maybe String =
+  λ map here d ⇒
+    maybe.foldω (String × String) (Maybe String)
+      (Nothing String)
+      (λ res ⇒ Just String (which String res d))
+      (lookup String (String × String) (string.eq here) map)