From 7cc66789ab5b00f450a807a96069e23dce67b91e Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 20 Dec 2023 02:08:54 +0100 Subject: [PATCH] more, mostly quox "stdlib" (if you could call it that) tho --- aoc2023.cabal | 16 ++++ day14.hs | 60 ++++++++++--- day15.quox | 27 ++++++ day19.pl | 84 ++++++++++++++++++ lib/fin.quox | 207 +++++++++++++++++++++++++++++++++++++++++++ lib/misc.quox | 97 +++++++++++++------- lib/nat.quox | 34 ++++++- lib/pair.quox | 47 +++++----- lib/string.quox | 12 ++- lib/sub.quox | 66 ++++++++++++++ unfinished/day13.bqn | 13 +++ 11 files changed, 585 insertions(+), 78 deletions(-) create mode 100644 aoc2023.cabal create mode 100644 day15.quox create mode 100644 day19.pl create mode 100644 lib/fin.quox create mode 100644 lib/sub.quox create mode 100644 unfinished/day13.bqn diff --git a/aoc2023.cabal b/aoc2023.cabal new file mode 100644 index 0000000..e92f60a --- /dev/null +++ b/aoc2023.cabal @@ -0,0 +1,16 @@ +cabal-version: 3.0 +name: aoc2023 +version: 0.1.0.0 +build-type: Simple + +executable day14 + ghc-options: -Wall -O2 + main-is: day14.hs + -- other-modules: + -- other-extensions: + build-depends: + base ^>= 4.17.2.0, + containers ^>= 0.6.7, + array ^>= 0.5.4.0 + hs-source-dirs: . + default-language: GHC2021 diff --git a/day14.hs b/day14.hs index eab94da..3e3f5ae 100644 --- a/day14.hs +++ b/day14.hs @@ -1,13 +1,47 @@ {-# options_ghc -Wall #-} -{-# language BlockArguments #-} +{-# language BlockArguments, LambdaCase #-} import Data.List import System.Environment import qualified Data.Map as M import Data.Maybe +import qualified Data.Array as A data Block = Rock | Space | Wall deriving (Eq, Ord, Show) + +data Rotation = U | L | D | R deriving (Eq, Ord, Show, Bounded, Enum) + +left, right, opp :: Rotation -> Rotation +left = \case U -> L; L -> D; D -> R; R -> U +right = \case U -> R; R -> D; D -> L; L -> U +opp = \case U -> D; D -> U; L -> R; R -> L + +instance Semigroup Rotation where + U <> r = r + L <> r = left r + R <> r = right r + D <> r = opp r + +instance Monoid Rotation where mempty = U + +type I2 = (Int, Int) + +data RArray e = RA !Rotation !(A.Array I2 e) + +rotateI :: Rotation -> (I2, I2) -> I2 -> I2 +rotateI U _ i = i +rotateI L (_, (xhi, _)) (x, y) = (y, xhi - x - 1) +rotateI D (_, (xhi, yhi)) (x, y) = (xhi - x - 1, yhi - y - 1) +rotateI R (_, (_, yhi)) (x, y) = (yhi - y - 1, x) + +(!) :: RArray e -> I2 -> e +RA r arr ! i = arr A.! rotateI r (A.bounds arr) i + +rotate :: Rotation -> RArray e -> RArray e +rotate r1 (RA r2 arr) = RA (r1 <> r2) arr + + block :: Char -> Maybe Block block 'O' = Just Rock block '.' = Just Space @@ -100,15 +134,15 @@ main = do "2" -> print $ part2 ℓs _ -> error "usage: $0 " -example1 :: [String] -example1 = - ["O....#....", - "O.OO#....#", - ".....##...", - "OO.#O....O", - ".O.....O#.", - "O.#..O.#.#", - "..O..#O..O", - ".......O..", - "#....###..", - "#OO..#...."] +-- example1 :: [String] +-- example1 = +-- ["O....#....", +-- "O.OO#....#", +-- ".....##...", +-- "OO.#O....O", +-- ".O.....O#.", +-- "O.#..O.#.#", +-- "..O..#O..O", +-- ".......O..", +-- "#....###..", +-- "#OO..#...."] diff --git a/day15.quox b/day15.quox new file mode 100644 index 0000000..53be585 --- /dev/null +++ b/day15.quox @@ -0,0 +1,27 @@ +load "bool.quox" +load "nat.quox" +load "string.quox" +load "list.quox" +load "io.quox" + + +def hash : ω.String → ℕ = + letω hash1 : ω.ℕ → ω.Char → ℕ = + λ n c ⇒ case char.ws? c return ℕ of { + 'true ⇒ n; + 'false ⇒ nat.mod (nat.times 17 (nat.plus (char.to-ℕ c) n)) 256 + } in + string.foldlω ℕ 0 hash1 + +def split : ω.String → List String = + letω comma = char.from-ℕ 0x2C in + string.split (char.eq comma) + +#[main] +def part1 = + io.bindω String True + (io.read-fileω "in/day15") + (λ s ⇒ io.dump ℕ (list.sum (list.mapω String ℕ hash (split s)))) + + +def0 ShittyHashMap = Vec 8 (Vec 8 (Vec 8 (List (String × ℕ)))) diff --git a/day19.pl b/day19.pl new file mode 100644 index 0000000..7d14e49 --- /dev/null +++ b/day19.pl @@ -0,0 +1,84 @@ +:- use_module(library(dcg/basics)). +:- use_module(library(dcg/high_order)). + +file(W, I) --> sequence(workflow, W), blanks, sequence(item, I). + +workflow(w(L,I)) --> name(L), "{", sequence(instruction, ",", I), "}", blanks. +name(N) --> sequence(alpha_to_lower, Cs), {Cs \= [], atom_codes(N, Cs)}. + +instruction(accept) --> "A", !. +instruction(reject) --> "R", !. +instruction(goto(X)) --> name(X). +instruction(if(A, R, N, T)) --> + attr(A), relation(R), number(N), ":", instruction(T). + % e.g. if(x, >, 420, goto(label)) or if(x, >, 420, accept) + +attr(A) --> oneof([x,m,a,s], A). +relation(R) --> oneof([<,>], R). + +oneof(Xs, X) --> {member(X, Xs)}, atom(X). + +item(i(X, M, A, S)) --> + "{", field(x, X), ",", field(m, M), ",", field(a, A), ",", field(s, S), "}", + blanks. +field(L, X) --> atom(L), "=", number(X). + + +field(i(X,_,_,_), x, X). +field(i(_,M,_,_), m, M). +field(i(_,_,A,_), a, A). +field(i(_,_,_,S), s, S). + +goto([w(L, W)|_], L, W) :- !. +goto([_ |Ws], L, W) :- goto(Ws, L, W). + +run(_, [accept|_], _, accept) :- !. +run(_, [reject|_], _, reject) :- !. +run(Ws, [goto(L)|_], I, Res) :- + goto(Ws, L, W), + run(Ws, W, I, Res). +run(Ws, [if(F, R, N, T)|W], I, Res) :- + field(I, F, Val), + compare(R0, Val, N), + (R = R0 -> run(Ws, [T|W], I, Res) ; run(Ws, W, I, Res)). + +score(_, reject, 0). +score(i(X,M,A,S), accept, T) :- T is X + M + A + S. +total(Is, Rs, T) :- maplist(score, Is, Rs, Ts), foldl(plus, Ts, 0, T). + +part1(File) :- + once(phrase_from_file(file(Ws, Is), File)), + maplist(run(Ws, [goto(in)]), Is, Rs), + total(Is, Rs, T), + writeln(T), !. + + +:- use_module(library(clpfd)). + +run2(Ws, [goto(L)|_], I) :- goto(Ws, L, W), run2(Ws, W, I). +run2(Ws, [if(F, R, N, T)|_], I) :- yes(F, R, N, I), run2(Ws, [T], I). +run2(Ws, [if(F, R, N, _)|W], I) :- no(F, R, N, I), run2(Ws, W, I). +run2(_, [accept|_], i(X,M,A,S)) :- + X in 1..4000, M in 1..4000, A in 1..4000, S in 1..4000. + +yes(F, R, N, I) :- field(I, F, Val), constrain(yes, R, Val, N). +no(F, R, N, I) :- field(I, F, Val), constrain(no, R, Val, N). + +constrain(yes, <, X, Y) :- X #< Y. +constrain(yes, >, X, Y) :- X #> Y. +constrain(no, <, X, Y) :- X #>= Y. +constrain(no, >, X, Y) :- X #=< Y. + +comb_size(i(X,M,A,S), Size) :- + fd_size(X, XN), fd_size(M, MN), fd_size(A, AN), fd_size(S, SN), + Size is XN * MN * AN * SN. + +part2(File) :- + once(phrase_from_file(file(Ws, _), File)), + findall(I, run2(Ws, [goto(in)], I), Is), + maplist(comb_size, Is, Ns), + foldl(plus, Ns, 0, N), + writeln(N). + + +% vim: set ft=prolog : diff --git a/lib/fin.quox b/lib/fin.quox new file mode 100644 index 0000000..1e68c1f --- /dev/null +++ b/lib/fin.quox @@ -0,0 +1,207 @@ +load "nat.quox" +load "either.quox" +load "maybe.quox" + + +namespace fin { + +def0 LT : ℕ → ℕ → ★ = + λ m n ⇒ + nat.elim-pairω¹ (λ _ _ ⇒ ★) + False -- 0 ≮ 0 + (λ n p ⇒ True) -- 0 < succ n + (λ m p ⇒ False) -- succ m ≮ 0 + (λ m n p ⇒ p) -- succ m < succ n ⇔ m < n + m n + + +def0 lt-irr : (m n : ℕ) → (p q : LT m n) → p ≡ q : LT m n = + λ m n ⇒ + nat.elim-pairω (λ m n ⇒ (p q : LT m n) → p ≡ q : LT m n) + false.irr (λ _ _ ⇒ true.irr) (λ _ _ ⇒ false.irr) (λ _ _ p ⇒ p) m n + +def0 lt-irr-het : + (m m' n n' : ℕ) → (mm : m ≡ m' : ℕ) → (nn : n ≡ n' : ℕ) → + (p : LT m n) → (q : LT m' n') → + Eq (𝑖 ⇒ LT (mm @𝑖) (nn @𝑖)) p q = + λ m m' n n' mm nn p q ⇒ δ 𝑖 ⇒ + lt-irr (mm @𝑖) (nn @𝑖) + (coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @0 @𝑖 p) + (coe (𝑗 ⇒ LT (mm @𝑗) (nn @𝑗)) @1 @𝑖 q) @𝑖 + +def0 lt-irr-het-left : + (m m' n : ℕ) → (mm : m ≡ m' : ℕ) → (p : LT m n) → (q : LT m' n) → + Eq (𝑖 ⇒ LT (mm @𝑖) n) p q = + λ m m' n mm ⇒ lt-irr-het m m' n n mm (δ _ ⇒ n) + + +def0 lt-true : (m n : ℕ) → LT m n → LT m n ≡ True : ★ = + λ m n p ⇒ + nat.elim-pairω¹ (λ m n ⇒ LT m n → LT m n ≡ True : ★) + (λ ff ⇒ void¹ (False ≡ True : ★) ff) + (λ n p tt ⇒ δ _ ⇒ True) + (λ m p ff ⇒ void¹ (False ≡ True : ★) ff) + (λ n m p tf ⇒ p tf) + m n p + + +#[compile-scheme "(lambda% (m n) (if (< m n) dec.Yes dec.No))"] +def lt? : ω.(m n : ℕ) → Dec (LT m n) = + nat.elim-pairω (λ m n ⇒ Dec (LT m n)) + (No (LT 0 0) (λ v ⇒ v)) + (λ n p ⇒ Yes (LT 0 (succ n)) 'true) + (λ m p ⇒ No (LT (succ m) 0) (λ v ⇒ v)) + (λ m n p ⇒ + dec.elim (LT m n) (λ _ ⇒ Dec (LT (succ m) (succ n))) + (λ yes ⇒ Yes (LT (succ m) (succ n)) yes) + (λ no ⇒ No (LT (succ m) (succ n)) no) p) + + +def0 Fin : ℕ → ★ = + λ n ⇒ (i : ℕ) × [0.LT i n] + + +def to-ℕ : 0.(n : ℕ) → Fin n → ℕ = + λ n i ⇒ case i return ℕ of { (i, p) ⇒ drop0 (LT i n) ℕ p i } + +def0 to-ℕ-fst : (n : ℕ) → (i : Fin n) → to-ℕ n i ≡ fst i : ℕ = + λ n i ⇒ drop0-eq (LT (fst i) n) ℕ (snd i) (fst i) + +def0 to-ℕ-eq : (n : ℕ) → (i j : Fin n) → + to-ℕ n i ≡ to-ℕ n j : ℕ → i ≡ j : Fin n = + λ n i' j' ij' ⇒ + let i = fst i'; ilt = get0 (LT i n) (snd i'); + j = fst j'; jlt = get0 (LT j n) (snd j'); + ij : (i ≡ j : ℕ) = + coe (𝑘 ⇒ to-ℕ-fst n i' @𝑘 ≡ j : ℕ) + (coe (𝑘 ⇒ to-ℕ n i' ≡ to-ℕ-fst n j' @𝑘 : ℕ) ij'); + ltt : Eq (𝑘 ⇒ LT (ij @𝑘) n) ilt jlt = + lt-irr-het-left i j n ij ilt jlt in + δ 𝑘 ⇒ (ij @𝑘, [ltt @𝑘]) + + +def fin? : ω.(n i : ℕ) → Maybe (Fin n) = + λ n i ⇒ + dec.elim (LT i n) (λ _ ⇒ Maybe (Fin n)) + (λ yes ⇒ Just (Fin n) (i, [yes])) + (λ no ⇒ Nothing (Fin n)) + (lt? i n) + + +def F0 : 0.(n : ℕ) → Fin (succ n) = λ _ ⇒ (0, ['true]) +def FS : 0.(n : ℕ) → Fin n → Fin (succ n) = + λ n i ⇒ case i return Fin (succ n) of { (i, p) ⇒ (succ i, p) } + +def dup! : 0.(n : ℕ) → (i : Fin n) → Dup (Fin n) i = + λ n ilt ⇒ + case ilt return ilt' ⇒ Dup (Fin n) ilt' of { (i, lt0) ⇒ + case lt0 return ilt' ⇒ Dup (Fin n) (i, lt0) of { [lt] ⇒ + case nat.dup! i return Dup (Fin n) (i, lt0) of { (iω, ii0) ⇒ + case iω + return iω' ⇒ 0.(iω' ≡ iω : [ω.ℕ]) → Dup (Fin n) (i, lt0) + of { [i!] ⇒ λ iiω ⇒ + let 0.iωi : iω ≡ [i] : [ω.ℕ] = get0 (iω ≡ [i] : [ω.ℕ]) ii0; + in + 0 + } (δ _ ⇒ iω) + }}} + +{- + case ilt return ilt' ⇒ Dup (Fin n) ilt' of { (i, lt0) ⇒ + case lt0 return lt0' ⇒ Dup (Fin n) (i, lt0') of { [lt] ⇒ + case nat.dup! i return Dup (Fin n) (i, [lt]) of { (iω, eq0) ⇒ + let ω.i! = fst ieq!; + 0.ii : i! ≡ i : ℕ = get0 (i! ≡ i : ℕ) (snd ieq!); + 0.lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt; + 0.ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt = + lt-irr-het-left i! i n ii lt! lt; + ω.ilt! : Fin n = (i!, [lt!]); + 0.iltt : ilt! ≡ ilt : Fin n = + δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])]; + in + ([ilt!], [iltt]) + -- [((i!, [lt!]), [δ 𝑘 ⇒ (ii @𝑘, [ltt @𝑘])])] + }}} +-} + +{- +def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] = + λ n i ⇒ appω (Sing (Fin n) i) (Fin n) (λ p ⇒ fst p) (dup! n i) +-} + +{- +def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] = + λ n i ⇒ + + appω (Sing (Fin n) i) [0.dup n i ≡ [i] : [ω.Fin n]] + (λ p ⇒ snd p) (dup! n i) +-} + +{- +def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] = + λ n i ⇒ + case dup! n i return i' ⇒ fst i' ≡ [i] : +-} + +{- +def dup : 0.(n : ℕ) → Fin n → [ω.Fin n] = + λ n ilt ⇒ + case ilt return [ω.Fin n] of { (i, lt0) ⇒ + case lt0 return [ω.Fin n] of { [lt] ⇒ + case nat.dup i + return i' ⇒ 0.(i' ≡ [i] : [ω.ℕ]) → [ω.Fin n] + of { [i!] ⇒ λ iiω ⇒ + let0 ii : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω; + lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt in + [(i!, [lt!])] + } (nat.dup-ok i) + }} +-} + +{- +def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] = + λ n ilt ⇒ δ 𝑘 ⇒ + let i = fst ilt; lt = get0 (LT i n) (snd ilt); + in +-} + +{- +def dup-ok : 0.(n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] = + λ n i ⇒ + case i return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒ + case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒ + case nat.dup i + return i' ⇒ (i' ≡ [i] : [ω.ℕ]) → + dup n (i, [lt]) ≡ [(i, [lt])] : [ω.Fin n] + of { [i!] ⇒ λ iiω ⇒ + let0 ii : i! ≡ i : ℕ = boxω-inj ℕ i! i iiω; + lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt; + ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt = + lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt + in + δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])] + } (nat.dup-ok i) + }} +-} + + +{- +def0 dup-ok : (n : ℕ) → (i : Fin n) → dup n i ≡ [i] : [ω.Fin n] = + λ n ilt ⇒ + case ilt return i' ⇒ dup n i' ≡ [i'] : [ω.Fin n] of { (i, lt0) ⇒ + case lt0 return lt' ⇒ dup n (i, lt') ≡ [(i, lt')] : [ω.Fin n] of { [lt] ⇒ + let i! = getω ℕ (nat.dup i); + ii : i! ≡ i : ℕ = δ 𝑘 ⇒ getω ℕ (nat.dup-ok i @𝑘); + lt! : LT i! n = coe (𝑘 ⇒ LT (ii @𝑘) n) @1 @0 lt; + ltt : Eq (𝑘 ⇒ LT (ii @𝑘) n) lt! lt = + lt-irr-het i! i n n ii (δ _ ⇒ n) lt! lt + in + δ 𝑘 ⇒ [(ii @𝑘, [ltt @𝑘])] + }} +-} + +} + +def0 Fin = fin.Fin +def F0 = fin.F0 +def FS = fin.FS diff --git a/lib/misc.quox b/lib/misc.quox index f43adc4..8f239ab 100644 --- a/lib/misc.quox +++ b/lib/misc.quox @@ -1,23 +1,41 @@ -def0 True : ★ = {true} - namespace true { + def0 True : ★ = {true} + def drop : 0.(A : ★) → True → A → A = λ A t x ⇒ case t return A of { 'true ⇒ x } + + def0 eta : (s : True) → s ≡ 'true : True = + λ s ⇒ case s return s' ⇒ s' ≡ 'true : True of { 'true ⇒ δ 𝑖 ⇒ 'true } + + def0 irr : (s t : True) → s ≡ t : True = + λ s t ⇒ + coe (𝑖 ⇒ eta s @𝑖 ≡ t : True) @1 @0 + (coe (𝑖 ⇒ 'true ≡ eta t @𝑖 : True) @1 @0 (δ _ ⇒ 'true)) } +def0 True = true.True + +namespace false { + def0 False : ★ = {} + + def void : 0.(A : ★) → 0.False → A = + λ A v ⇒ case0 v return A of { } + + def0 irr : (u v : False) → u ≡ v : False = + λ u v ⇒ void (u ≡ v : False) u +} +def0 False = false.False +def void = false.void + -def0 False : ★ = {} def0 Not : ★ → ★ = λ A ⇒ ω.A → False -def void : 0.(A : ★) → 0.False → A = - λ A v ⇒ case0 v return A of { } - def0 Iff : ★ → ★ → ★ = λ A B ⇒ (A → B) × (B → A) -def0 All : (A : ★) → (0.A → ★) → ★ = +def0 All : (A : ★) → (A → ★) → ★ = λ A P ⇒ (x : A) → P x def0 cong : - (A : ★) → (P : 0.A → ★) → (p : All A P) → + (A : ★) → (P : A → ★) → (p : All A P) → (x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) = λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖) @@ -33,26 +51,31 @@ def0 coherence : δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x -def0 eq-f : - 0.(A : ★) → 0.(P : 0.A → ★) → - 0.(p : All A P) → 0.(q : All A P) → - 0.A → ★ = +def0 eq-f : (A : ★) → (P : A → ★) → (p : All A P) → (q : All A P) → A → ★ = λ A P p q x ⇒ p x ≡ q x : P x def funext : - 0.(A : ★) → 0.(P : 0.A → ★) → 0.(p q : All A P) → + 0.(A : ★) → 0.(P : A → ★) → 0.(p q : All A P) → (All A (eq-f A P p q)) → p ≡ q : All A P = λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖 def refl : 0.(A : ★) → (x : A) → x ≡ x : A = λ A x ⇒ δ _ ⇒ x def sym : 0.(A : ★) → 0.(x y : A) → (x ≡ y : A) → y ≡ x : A = - λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 } + λ A x y eq ⇒ coe (𝑗 ⇒ eq @𝑗 ≡ x : A) (δ _ ⇒ eq @0) + -- btw this uses eq @0 instead of just x because of the quantities + +def trans10 : 0.(A : ★) → 0.(x y z : A) → + 1.(x ≡ y : A) → 0.(y ≡ z : A) → x ≡ z : A = + λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ x ≡ eq2 @𝑗 : A) eq1 + +def trans01 : 0.(A : ★) → 0.(x y z : A) → + 0.(x ≡ y : A) → 1.(y ≡ z : A) → x ≡ z : A = + λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ eq1 @𝑗 ≡ z : A) @1 @0 eq2 def trans : 0.(A : ★) → 0.(x y z : A) → ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A = - λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒ - comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 } + λ A x y z eq1 eq2 ⇒ trans01 A x y z eq1 eq2 def appω : 0.(A B : ★) → ω.(f : ω.A → B) → [ω.A] → [ω.B] = λ A B f x ⇒ @@ -70,16 +93,22 @@ def getω : 0.(A : ★) → [ω.A] → A = def0 get0 : (A : ★) → [0.A] → A = λ A x ⇒ case x return A of { [x] ⇒ x } -def drop0 : 0.(A B : ★) → [0.B] → A → A = - λ A B x y ⇒ case x return A of { [_] ⇒ y } +def drop0 : 0.(A B : ★) → [0.A] → B → B = + λ A B x y ⇒ case x return B of { [_] ⇒ y } -def0 drop0-eq : (A B : ★) → (x : [0.B]) → (y : A) → drop0 A B x y ≡ y : A = +def0 drop0-eq : (A B : ★) → (x : [0.A]) → (y : B) → drop0 A B x y ≡ y : B = λ A B x y ⇒ - case x return x' ⇒ drop0 A B x' y ≡ y : A of { [_] ⇒ δ 𝑖 ⇒ y } + case x return x' ⇒ drop0 A B x' y ≡ y : B of { [_] ⇒ δ 𝑖 ⇒ y } def0 HEq : (A B : ★) → A → B → ★¹ = λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y +def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A = + λ A x y xy ⇒ δ 𝑖 ⇒ getω A (xy @𝑖) + +def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] = + λ A s ⇒ [get0 A s] + def0 Sing : (A : ★) → A → ★ = λ A x ⇒ (val : A) × [0. val ≡ x : A] @@ -88,36 +117,39 @@ def sing : 0.(A : ★) → (x : A) → Sing A x = λ A x ⇒ (x, [δ _ ⇒ x]) def0 Dup : (A : ★) → A → ★ = - λ A x ⇒ [ω. Sing A x] + λ A x ⇒ (x! : [ω.A]) × [0. x! ≡ [x] : [ω.A]] def dup-from-parts : 0.(A : ★) → (dup : A → [ω.A]) → 0.(prf : (x : A) → dup x ≡ [x] : [ω.A]) → (x : A) → Dup A x = - λ A dup prf x ⇒ - case dup x return x! ⇒ 0.(x! ≡ dup x : [ω.A]) → [ω. Sing A x] of { - [x'] ⇒ λ eq ⇒ - let0 prf'-ω : [x'] ≡ [x] : [ω.A] = - trans [ω.A] [x'] (dup x) [x] eq (prf x); - prf' : x' ≡ x : A = - δ 𝑖 ⇒ getω A (prf'-ω @𝑖) in - [(x', [prf'])] - } (δ 𝑖 ⇒ dup x) + λ A dup prf x ⇒ (dup x, [prf x]) def drop-from-dup : 0.(A : ★) → (A → [ω.A]) → 0.(B : ★) → A → B → B = λ A dup B x y ⇒ case dup x return B of { [_] ⇒ y } +def dup0 : 0.(A : ★) → [0.A] → [ω.[0.A]] = + λ A x ⇒ case x return [ω.[0.A]] of { [x] ⇒ [[x]] } + +def0 dup0-ok : (A : ★) → (x : [0.A]) → dup0 A x ≡ [x] : [ω.[0.A]] = + λ A x ⇒ + case x return x' ⇒ dup0 A x' ≡ [x'] : [ω.[0.A]] of { [x] ⇒ δ 𝑖 ⇒ [[x]] } + +def dup0! : 0.(A : ★) → (x : [0.A]) → Dup [0.A] x = + λ A ⇒ dup-from-parts [0.A] (dup0 A) (dup0-ok A) + + namespace sing { def val : 0.(A : ★) → 0.(x : A) → Sing A x → A = λ A x sg ⇒ - case sg return A of { (x', eq) ⇒ drop0 A (x' ≡ x : A) eq x' } + case sg return A of { (x', eq) ⇒ drop0 (x' ≡ x : A) A eq x' } def0 val-fst : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ fst sg : A = - λ A x sg ⇒ drop0-eq A (fst sg ≡ x : A) (snd sg) (fst sg) + λ A x sg ⇒ drop0-eq (fst sg ≡ x : A) A (snd sg) (fst sg) def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A = λ A x sg ⇒ @@ -131,5 +163,4 @@ def app : 0.(A B : ★) → 0.(x : A) → case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) } } - } diff --git a/lib/nat.quox b/lib/nat.quox index be2a178..d548213 100644 --- a/lib/nat.quox +++ b/lib/nat.quox @@ -75,7 +75,7 @@ def0 dup-ok : (n : ℕ) → dup n ≡ [n] : [ω.ℕ] = succ _, ih ⇒ δ 𝑖 ⇒ succ-boxω (ih @𝑖) } -def dup! : (n : ℕ) → [ω. Sing ℕ n] = +def dup! : (n : ℕ) → Dup ℕ n = dup-from-parts ℕ dup dup-ok @@ -152,6 +152,38 @@ def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) = } +def divmod : ℕ → ℕ → ℕ × ℕ = + -- https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.Init.Nat.html#divmod + letω divmod' : ℕ → ω.ℕ → ℕ → ℕ → ℕ × ℕ = + λ x ⇒ + case x return ω.ℕ → ℕ → ℕ → ℕ × ℕ of { + 0 ⇒ λ y q u ⇒ (q, u); + succ _, 1.f' ⇒ λ y q u ⇒ + case u return ℕ × ℕ of { + 0 ⇒ f' y (succ q) y; + succ u' ⇒ f' y q u' + } + } in + λ x y ⇒ + case y return ℕ × ℕ of { + 0 ⇒ drop (ℕ × ℕ) x (0, 0); + succ y' ⇒ + case dup y' return ℕ × ℕ of { [y'] ⇒ + case divmod' x y' 0 y' return ℕ × ℕ of { (d, m) ⇒ (d, minus y' m) } + } + } + +def div : ℕ → ℕ → ℕ = + λ x y ⇒ case divmod x y return ℕ of { (d, m) ⇒ drop ℕ m d } + +def mod : ℕ → ℕ → ℕ = + λ x y ⇒ case divmod x y return ℕ of { (d, m) ⇒ drop ℕ d m } + + +def0 div-5-2 : div 5 2 ≡ 2 : ℕ = δ 𝑖 ⇒ 2 +def0 mod-5-2 : mod 5 2 ≡ 1 : ℕ = δ 𝑖 ⇒ 1 + + #[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"] def eq? : DecEq ℕ = λ m n ⇒ diff --git a/lib/pair.quox b/lib/pair.quox index 4bf33c6..9f93009 100644 --- a/lib/pair.quox +++ b/lib/pair.quox @@ -1,54 +1,49 @@ namespace pair { -def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x; - -{- --- now builtins -def fst : 0.(A : ★) → 0.(B : A → ★) → ω.(Σ A B) → A = - λ A B p ⇒ caseω p return A of { (x, _) ⇒ x }; - -def snd : 0.(A : ★) → 0.(B : A → ★) → ω.(p : Σ A B) → B (fst A B p) = - λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y }; --} +def0 Σ : (A : ★) → (A → ★) → ★ = λ A B ⇒ (x : A) × B x def uncurry : 0.(A : ★) → 0.(B : A → ★) → 0.(C : (x : A) → (B x) → ★) → (f : (x : A) → (y : B x) → C x y) → (p : Σ A B) → C (fst p) (snd p) = λ A B C f p ⇒ - case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y }; + case p return p' ⇒ C (fst p') (snd p') of { (x, y) ⇒ f x y } def uncurry' : 0.(A B C : ★) → (A → B → C) → (A × B) → C = - λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C); + λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C) def curry : 0.(A : ★) → 0.(B : A → ★) → 0.(C : (Σ A B) → ★) → (f : (p : Σ A B) → C p) → (x : A) → (y : B x) → C (x, y) = - λ A B C f x y ⇒ f (x, y); + λ A B C f x y ⇒ f (x, y) def curry' : 0.(A B C : ★) → (A × B → C) → A → B → C = - λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C); + λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C) def0 fst-snd : (A : ★) → (B : A → ★) → (p : Σ A B) → p ≡ (fst p, snd p) : Σ A B = - λ A B p ⇒ - case p - return p' ⇒ p' ≡ (fst p', snd p') : Σ A B - of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) }; + λ A B p ⇒ δ 𝑖 ⇒ p -- η def0 fst-eq : (A : ★) → (B : A → ★) → (p q : Σ A B) → p ≡ q : Σ A B → fst p ≡ fst q : A = - λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖); + λ A B p q eq ⇒ δ 𝑖 ⇒ fst (eq @𝑖) def0 snd-eq : (A : ★) → (B : A → ★) → (p q : Σ A B) → (eq : p ≡ q : Σ A B) → Eq (𝑖 ⇒ B (fst-eq A B p q eq @𝑖)) (snd p) (snd q) = - λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖); + λ A B p q eq ⇒ δ 𝑖 ⇒ snd (eq @𝑖) + +def0 pair-eq : + (A : ★) → (B : A → ★) → + (x0 x1 : A) → (y0 : B x0) → (y1 : B x1) → + (xx : x0 ≡ x1 : A) → (yy : Eq (𝑖 ⇒ B (xx @𝑖)) y0 y1) → + (x0, y0) ≡ (x1, y1) : ((x : A) × B x) = + λ A B x0 x1 y0 y1 xx yy ⇒ δ 𝑖 ⇒ (xx @𝑖, yy @𝑖) def map : 0.(A A' : ★) → @@ -56,19 +51,17 @@ def map : (f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) → Σ A B → Σ A' B' = λ A A' B B' f g p ⇒ - case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) }; + case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) } def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' = - λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g); + λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g) def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B = - λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x); + λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x) def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' = - λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f; + λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f } -def0 Σ = pair.Σ; --- def fst = pair.fst; --- def snd = pair.snd; +def0 Σ = pair.Σ diff --git a/lib/string.quox b/lib/string.quox index ec49fb7..f59c799 100644 --- a/lib/string.quox +++ b/lib/string.quox @@ -73,6 +73,9 @@ def from-list : List Char → String = def foldl : 0.(A : ★) → A → ω.(A → Char → A) → String → A = λ A z f str ⇒ list.foldl Char A z f (to-list str) +def foldlω : 0.(A : ★) → ω.A → ω.(ω.A → ω.Char → A) → ω.String → A = + λ A z f str ⇒ list.foldlω Char A z f (to-list str) + def split : ω.(ω.Char → Bool) → ω.String → List String = λ p str ⇒ list.map (List Char) String from-list @@ -86,8 +89,9 @@ def break : ω.(ω.Char → Bool) → ω.String → String × String = def reverse : String → String = λ str ⇒ from-list (list.reverse Char (to-list str)) -#[compile-scheme "(lambda% (a b) (if (string=? a b) 'true 'false))"] -postulate eq : ω.String → ω.String → Bool +#[compile-scheme "(lambda% (y n a b) (if (string=? a b) y n))"] +postulate eq' : 0.(A : ★) → A → A → ω.String → ω.String → A +def eq : ω.String → ω.String → Bool = eq' Bool 'true 'false def null : ω.String → Bool = eq "" def not-null : ω.String → Bool = λ s ⇒ bool.not (null s) @@ -134,7 +138,7 @@ def to-ℕ-or-0 : String → ℕ = postulate uncons' : 0.(A : ★) → ω.A → ω.(Char → String → A) → String → A def uncons : String → Maybe (Char × String) = - let0 Ret : ★ = Char × String in - uncons' (Maybe Ret) (Nothing Ret) (λ c s ⇒ Just Ret (c, s)) + let0 Pair : ★ = Char × String in + uncons' (Maybe Pair) (Nothing Pair) (λ c s ⇒ Just Pair (c, s)) } diff --git a/lib/sub.quox b/lib/sub.quox new file mode 100644 index 0000000..922df34 --- /dev/null +++ b/lib/sub.quox @@ -0,0 +1,66 @@ +load "maybe.quox" + +namespace sub { + +def0 Irr : ★ → ★ = + λ A ⇒ (x y : A) → x ≡ y : A + +def0 Irr1 : (A : ★) → (A → ★) → ★ = + λ A P ⇒ (x : A) → Irr (P x) + +def0 Sub : (A : ★) → (P : A → ★) → ★ = + λ A P ⇒ (x : A) × [0. P x] + +def sub : 0.(A : ★) → 0.(P : A → ★) → (x : A) → 0.(P x) → Sub A P = + λ A P x p ⇒ (x, [p]) + +def sub? : 0.(A : ★) → 0.(P : A → ★) → (ω.(x : A) → Dec (P x)) → + ω.(x : A) → Maybe (Sub A P) = + λ A P p? x ⇒ + dec.elim (P x) (λ _ ⇒ Maybe (Sub A P)) + (λ yes ⇒ Just (Sub A P) (sub A P x yes)) + (λ no ⇒ Nothing (Sub A P)) + (p? x) + +def0 sub-eq : (A : ★) → (P : A → ★) → (Irr1 A P) → (x y : Sub A P) → + (fst x ≡ fst y : A) → (x ≡ y : Sub A P) = + λ A P pirr x y xy0 ⇒ + let x1 = get0 (P (fst x)) (snd x); y1 = get0 (P (fst y)) (snd y) in + let xy1 : Eq (𝑖 ⇒ P (xy0 @𝑖)) x1 y1 = + δ 𝑖 ⇒ pirr (xy0 @𝑖) + (coe (𝑗 ⇒ P (xy0 @𝑗)) @0 @𝑖 x1) + (coe (𝑗 ⇒ P (xy0 @𝑗)) @1 @𝑖 y1) @𝑖 in + δ 𝑖 ⇒ (xy0 @𝑖, [xy1 @𝑖]) + + +def0 SubDup : (A : ★) → (P : A → ★) → Sub A P → ★ = + λ A P s ⇒ (x! : [ω.A]) × [0. x! ≡ [fst s] : [ω.A]] + +def subdup : 0.(A : ★) → 0.(P : A → ★) → + ((x : A) → Dup A x) → (s : Sub A P) → SubDup A P s = + λ A P dupA s ⇒ + case s return s' ⇒ SubDup A P s' of { (x, p) ⇒ + drop0 (P x) (SubDup A P (x, p)) p (dupA x) + } + + +{- +type checker loop?????????????????? :( +def subdup-to-dup : + 0.(A : ★) → 0.(P : A → ★) → 0.(Irr1 A P) → + 0.(s : Sub A P) → SubDup A P s → Dup (Sub A P) s = + λ A P pirr s sd ⇒ + case sd return Dup (Sub A P) s of { (sω, ss0) ⇒ + case sω + return sω' ⇒ 0.(sω' ≡ [fst s] : [ω.A]) → Dup (Sub A P) s + of { [s!] ⇒ λ ss' ⇒ + let ω.p : [0.P (fst s)] = revive0 (P (fst s)) (snd s); + 0.ss : s! ≡ fst s : A = boxω-inj A s! (fst s) ss'; + 0.pss : [0.P s!] ≡ [0.P (fst s)] : ★ = (δ 𝑖 ⇒ [0.P (ss @𝑖)]) in + ([(s!, coe (𝑖 ⇒ pss @𝑖) @1 @0 p)], + [δ 𝑖 ⇒ [(ss @𝑖, coe (𝑗 ⇒ pss @𝑗) @1 @𝑖 p)]]) + } (δ _ ⇒ sω) + } +-} + +} diff --git a/unfinished/day13.bqn b/unfinished/day13.bqn new file mode 100644 index 0000000..5edd1c3 --- /dev/null +++ b/unfinished/day13.bqn @@ -0,0 +1,13 @@ +Tails ⇐ (1⊸↓)⍟(↕∘≠⊢) + +Sym ⇐ ∧´∘⥊ ⌽=⊢ + +Centers ⇐ { ⌊ (↕≠𝕩) { 𝕨+ 2÷˜ 𝕨-˜ ≠𝕩} 𝕩 } + +VC ⇐ (⊑/˜) Centers×Sym¨∘Tails +HC ⇐ VC⍉ + +VCenter ⇐ VC⌈(VC⌽˘) +HCenter ⇐ HC⌈(HC⌽) + +Score ⇐ (100×VCenter) + HCenter