From f9acd132923fde85cb70ebad07529cbd290bfa78 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 1 Dec 2023 18:52:23 +0100 Subject: [PATCH] first --- .gitignore | 2 + Makefile | 2 + day1-standalone.quox | 371 +++++++++++++++++++++++++++++++++++++++++++ day1.quox | 93 +++++++++++ day1.ss | 55 +++++++ lib/bool.quox | 39 +++++ lib/either.quox | 74 +++++++++ lib/io.quox | 80 ++++++++++ lib/list.quox | 163 +++++++++++++++++++ lib/maybe.quox | 140 ++++++++++++++++ lib/misc.quox | 92 +++++++++++ lib/nat.quox | 196 +++++++++++++++++++++++ lib/pair.quox | 74 +++++++++ lib/qty.quox | 77 +++++++++ pack.toml | 13 ++ 15 files changed, 1471 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 day1-standalone.quox create mode 100644 day1.quox create mode 100644 day1.ss create mode 100644 lib/bool.quox create mode 100644 lib/either.quox create mode 100644 lib/io.quox create mode 100644 lib/list.quox create mode 100644 lib/maybe.quox create mode 100644 lib/misc.quox create mode 100644 lib/nat.quox create mode 100644 lib/pair.quox create mode 100644 lib/qty.quox create mode 100644 pack.toml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..3ed14ca --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +*.quox.ss +in diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..fa9fcf4 --- /dev/null +++ b/Makefile @@ -0,0 +1,2 @@ +%.quox.ss: %.quox lib/*.quox + quox -i lib $< -o $@ diff --git a/day1-standalone.quox b/day1-standalone.quox new file mode 100644 index 0000000..2b1a733 --- /dev/null +++ b/day1-standalone.quox @@ -0,0 +1,371 @@ + +namespace bool { + +def0 Bool : ★ = {true, false} + +def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A = + λ A b t f ⇒ case b return A of { 'true ⇒ t; 'false ⇒ f } + +def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false; +def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; + +} + +def0 Bool = bool.Bool + +namespace unit { + +def0 Unit : ★ = {unit} + +def drop : 0.(A : ★) → A → Unit → A = + λ A x u ⇒ case u return A of { 'unit ⇒ x } + +} + +def0 Unit = unit.Unit + + +namespace maybe { + +def0 Tag : ★ = {nothing, just} + +def0 Payload : Tag → ★ → ★ = + λ tag A ⇒ case tag return ★ of { 'nothing ⇒ Unit; 'just ⇒ A } + +def0 Maybe : ★ → ★ = + λ A ⇒ (t : Tag) × Payload t A + +def Nothing : 0.(A : ★) → Maybe A = + λ _ ⇒ ('nothing, 'unit) + +def Just : 0.(A : ★) → A → Maybe A = + λ _ x ⇒ ('just, x) + + +def fold' : 0.(A B : ★) → ω.B → ω.(ω.A → B) → + ω.(t : Tag) → ω.(Payload t A) → B = + λ A B nothing just tag ⇒ + case tag return t ⇒ ω.(Payload t A) → B of { + 'nothing ⇒ λ _ ⇒ nothing; + 'just ⇒ just + } + +def fold : 0.(A B : ★) → ω.B → ω.(ω.A → B) → ω.(Maybe A) → B = + λ A B nothing just x ⇒ + caseω x return B of { (tag, payload) ⇒ fold' A B nothing just tag payload } + +def pair : 0.(A B : ★) → ω.(Maybe A) → ω.(Maybe B) → Maybe (A × B) = + λ A B x y ⇒ + fold A (Maybe (A × B)) (Nothing (A × B)) + (λ x' ⇒ fold B (Maybe (A × B)) (Nothing (A × B)) + (λ y' ⇒ Just (A × B) (x', y')) y) x + + +def check : 0.(A : ★) → (ω.A → Bool) → ω.A → Maybe A = + λ A p x ⇒ bool.if (Maybe A) (p x) (Just A x) (Nothing A) + +def or : 0.(A : ★) → ω.(Maybe A) → ω.(Maybe A) → Maybe A = + λ A l r ⇒ fold A (Maybe A) r (λ x ⇒ Just A x) l + +} + +def0 Maybe = maybe.Maybe +def Just = maybe.Just +def Nothing = maybe.Nothing + + + +namespace vec { + +def0 Vec : ℕ → ★ → ★ = + λ n A ⇒ + case n return ★ of { + 0 ⇒ Unit; + succ _, 0.Tail ⇒ A × Tail + } + +def foldr : 0.(A B : ★) → B → ω.(A → B → B) → (n : ℕ) → Vec n A → B = + λ A B nil cons len ⇒ + case len return l ⇒ Vec l A → B of { + 0 ⇒ λ u ⇒ unit.drop B nil u; + succ n, f ⇒ λ lst ⇒ + case lst return B of { (first, rest) ⇒ cons first (f rest) } + } + +-- uggh +def foldrω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.B → B) → + ω.(n : ℕ) → ω.(Vec n A) → B = + λ A B nil cons len ⇒ + caseω len return l ⇒ ω.(Vec l A) → B of { + 0 ⇒ λ _ ⇒ nil; + succ n, ω.f ⇒ λ lst ⇒ cons (fst lst) (f (snd lst)) + } + +} + + + +namespace list { + +def0 List : ★ → ★ = + λ A ⇒ (len : ℕ) × vec.Vec len A + +def Nil : 0.(A : ★) → List A = + λ A ⇒ (0, 'unit) + +def Cons : 0.(A : ★) → A → List A → List A = + λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) } + + + +def foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B = + λ A B nil cons lst ⇒ + case lst return B of { (len, elems) ⇒ vec.foldr A B nil cons len elems } + +def foldl : 0.(A B : ★) → B → ω.(B → A → B) → List A → B = + λ A B z f xs ⇒ foldr A (B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z + + +def foldrω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.B → B) → ω.(List A) → B = + λ A B nil cons lst ⇒ + caseω lst return B of { (len, elems) ⇒ vec.foldrω A B nil cons len elems } + +def foldlω : 0.(A B : ★) → ω.B → ω.(ω.B → ω.A → B) → ω.(List A) → B = + λ A B z f xs ⇒ foldrω A (ω.B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z + + +def map : 0.(A B : ★) → ω.(A → B) → List A → List B = + λ A B f ⇒ foldr A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys) + + +def reverse : 0.(A : ★) → List A → List A = + λ A ⇒ foldl A (List A) (Nil A) (λ xs x ⇒ Cons A x xs) + +def find : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → Maybe A = + λ A p ⇒ + foldlω A (Maybe A) (Nothing A) (λ m x ⇒ maybe.or A m (maybe.check A p x)) + + +postulate0 SchemeList : ★ → ★ + +#[compile-scheme + "(lambda (list) (cons (length list) (fold-right cons 'unit list)))"] +postulate from-scheme : 0.(A : ★) → SchemeList A → List A + +} + +def0 List = list.List +def Nil = list.Nil +def Cons = list.Cons + + +namespace nat { + +-- recurse over two numbers in lockstep until one reaches zero +def elim-pair : + 0.(P : ℕ → ℕ → ★) → + ω.(P 0 0) → + ω.(0.(n : ℕ) → P 0 n → P 0 (succ n)) → + ω.(0.(m : ℕ) → P m 0 → P (succ m) 0) → + ω.(0.(m n : ℕ) → P m n → P (succ m) (succ n)) → + ω.(m : ℕ) → (n : ℕ) → P m n = + λ P zz zs sz ss m ⇒ + caseω m return m' ⇒ (n : ℕ) → P m' n of { + 0 ⇒ λ n ⇒ case n return n' ⇒ P 0 n' of { + 0 ⇒ zz; + succ n', ihn ⇒ zs n' ihn + }; + succ m', ω.ihm ⇒ λ n ⇒ case n return n' ⇒ P (succ m') n' of { + 0 ⇒ sz m' (ihm 0); + succ n' ⇒ ss m' n' (ihm n') + } + } + +#[compile-scheme "(lambda (n) n)"] +def dup : ℕ → [ω. ℕ] = + λ n ⇒ + case n return n' ⇒ [ω. ℕ] of { + 0 ⇒ [0]; + succ n, d ⇒ case d return [ω.ℕ] of { [n'] ⇒ [succ n'] } + }; + +#[compile-scheme "(lambda% (m n) (+ m n))"] +def plus : ℕ → ℕ → ℕ = + λ m n ⇒ + case m return ℕ of { + 0 ⇒ n; + succ _, p ⇒ succ p + }; + +#[compile-scheme "(lambda% (m n) (* m n))"] +def timesω : ℕ → ω.ℕ → ℕ = + λ m n ⇒ + case m return ℕ of { + 0 ⇒ 0; + succ _, t ⇒ plus n t + }; + +def times : ℕ → ℕ → ℕ = + λ m n ⇒ case dup n return ℕ of { [n] ⇒ timesω m n }; + +def pred : ℕ → ℕ = + λ n ⇒ case n return ℕ of { 0 ⇒ 0; succ n ⇒ n }; + +#[compile-scheme "(lambda% (m n) (max 0 (- m n)))"] +def minus : ℕ → ℕ → ℕ = + λ m n ⇒ + case dup m return ℕ of { [m] ⇒ + elim-pair (λ _ _ ⇒ ℕ) + 0 + (λ _ p ⇒ succ p) + (λ _ p ⇒ p) + (λ _ _ p ⇒ p) + m n + } + + +def0 Ordering : ★ = {lt, eq, gt} + +def from-ordering : 0.(A : ★) → ω.A → ω.A → ω.A → Ordering → A = + λ A lt eq gt o ⇒ + case o return A of { 'lt ⇒ lt; 'eq ⇒ eq; 'gt ⇒ gt } + +def drop-ordering : 0.(A : ★) → Ordering → A → A = + λ A o x ⇒ case o return A of { 'lt ⇒ x; 'eq ⇒ x; 'gt ⇒ x } + +def compareω : ω.ℕ → ℕ → Ordering = + elim-pair (λ _ _ ⇒ Ordering) + 'eq + (λ _ o ⇒ drop-ordering Ordering o 'lt) + (λ _ o ⇒ drop-ordering Ordering o 'gt) + (λ _ _ x ⇒ x) + +def compare : ℕ → ℕ → Ordering = + λ m n ⇒ case dup m return Ordering of { [m] ⇒ compareω m n } + +def le : ω.ℕ → ω.ℕ → Bool = + λ m n ⇒ + case compare m n return Bool + of { 'lt ⇒ 'true; 'eq ⇒ 'true; 'gt ⇒ 'false } + +} + + +namespace io { + +def0 IORes : ★ → ★ = λ A ⇒ A × IOState + +def0 IO : ★ → ★ = λ A ⇒ IOState → IORes A + +def pure : 0.(A : ★) → A → IO A = λ A x s ⇒ (x, s) + +def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B = + λ A B m k s0 ⇒ + case m s0 return IORes B of { (x, s1) ⇒ k x s1 } + +def map : 0.(A B : ★) → (A → B) → IO A → IO B = + λ A B f act ⇒ bind A B act (λ x ⇒ pure B (f x)) + +def seq : 0.(B : ★) → IO Unit → IO B → IO B = + λ B x y ⇒ bind Unit B x (λ u ⇒ case u return IO B of { 'unit ⇒ y }) + +def seq' : IO Unit → IO Unit → IO Unit = seq Unit + +#[compile-scheme "(lambda (x) (builtin-io (display x) (newline)))"] +postulate dump : 0.(A : ★) → A → IO Unit + +#[compile-scheme + "(lambda (path) (builtin-io + (call-with-input-file path + (lambda (file) + (do [(line (get-line file) (get-line file)) + (acc '() (cons line acc))] + [(eof-object? line) (reverse acc)])))))"] +postulate prim-read-file-lines : + ω.(path : String) → IO (list.SchemeList String) + +def read-file-lines : ω.(path : String) → IO (List String) = + λ path ⇒ + map (list.SchemeList String) (List String) + (list.from-scheme String) + (prim-read-file-lines path) + +} + +def0 IO = io.IO + + +namespace char { + postulate0 Char : ★ + + #[compile-scheme "char->integer"] + postulate ord : Char → ℕ + + #[compile-scheme "integer->char"] + postulate chr : ℕ → Char + + #[compile-scheme "(lambda (c) c)"] + postulate dup : Char → [ω.Char] + + def le : ω.Char → ω.Char → Bool = + λ x y ⇒ nat.le (ord x) (ord y) + + def between : ω.Char → ω.Char → ω.Char → Bool = + λ lo hi c ⇒ + case dup c return Bool of { [c] ⇒ bool.and (le lo c) (le c hi) } + + def is-digit : ω.Char → Bool = + between (chr 0x30) (chr 0x39) + + def digit : Char → ℕ = + λ c ⇒ nat.minus (ord c) 0x30 + + #[compile-scheme "(lambda (c) (builtin-io (display c) (newline)))"] + postulate println : Char → IO Unit +} + +def0 Char = char.Char + + +namespace string { + #[compile-scheme "string->list"] + postulate prim-to-list : String → list.SchemeList Char + + def to-list : String → List Char = + λ str ⇒ list.from-scheme Char (prim-to-list str) + + #[compile-scheme "(lambda (str) str)"] + postulate dup : String → [ω.String] +} + + +def find-first-last : + 0.(A : ★) → + ω.(ω.A → Bool) → + ω.(List A) → Maybe (A × A) = + λ A p xs ⇒ + maybe.pair A A + (list.find A p xs) + (list.find A p (list.reverse A xs)) + +def number' : Char → Char → ℕ = + λ tens units ⇒ nat.plus (nat.times 10 (char.digit tens)) (char.digit units) + +def number : String → ℕ = + λ line ⇒ + case string.dup line return ℕ of { + [line] ⇒ + maybe.fold (Char × Char) ℕ 0 + (λ cd ⇒ case cd return ℕ of { (c, d) ⇒ number' c d }) + (find-first-last Char char.is-digit (string.to-list line)) + } + +def part1 : List String → ℕ = + list.foldr String ℕ 0 (λ str n ⇒ nat.plus (number str) n) + + +#[main] +def main : IO Unit = + io.bind (List String) Unit + (io.read-file-lines "in/day1") + (λ lines ⇒ io.dump ℕ (part1 lines)) diff --git a/day1.quox b/day1.quox new file mode 100644 index 0000000..53ec594 --- /dev/null +++ b/day1.quox @@ -0,0 +1,93 @@ +load "list.quox" +load "nat.quox" +load "io.quox" + +postulate0 Char : ★ + +namespace char { + #[compile-scheme "char->integer"] + postulate ord : Char → ℕ + + #[compile-scheme "integer->char"] + postulate chr : ℕ → Char + + #[compile-scheme "(lambda (c) (cons c 'erased))"] + postulate dup! : (c : Char) → [ω.Sing Char c] + + def dup : Char → [ω.Char] = + λ c ⇒ appω (Sing Char c) Char (λ c' ⇒ sing.val Char c c') (dup! c); + + def le : ω.Char → ω.Char → Bool = + λ x y ⇒ nat.le (ord x) (ord y) + + def between : ω.Char → ω.Char → ω.Char → Bool = + λ lo hi c ⇒ + case dup c return Bool of { [c] ⇒ bool.and (le lo c) (le c hi) } + + def is-digit : ω.Char → Bool = + between (chr 0x30) (chr 0x39) + + def digit : Char → ℕ = + λ c ⇒ nat.minus (ord c) 0x30 + + #[compile-scheme "(lambda (c) (builtin-io (display c) (newline)))"] + postulate println : Char → IO True +} + +namespace string { + #[compile-scheme "string->list"] + postulate prim-to-list : String → list.SchemeList Char + + def to-list : String → List Char = + λ str ⇒ list.from-scheme Char (prim-to-list str) + + #[compile-scheme "(lambda (str) str)"] + postulate dup : String → [ω.String] +} + + + +def find-first-last : + 0.(A : ★) → + ω.(ω.A → Bool) → + ω.(List A) → Maybe (A × A) = + λ A p xs ⇒ + maybe.pair A A + (list.find A p xs) + (list.find A p (list.reverse A xs)) + +def for-io : 0.(A : ★) → ω.(A → IO True) → List A → IO True = + λ A f xs ⇒ list.foldr A (IO True) io.pass (λ x act ⇒ io.seq' (f x) act) xs + +def find-in-string : ω.(ω.Char → Bool) → ω.String → Maybe Char = + λ p str ⇒ list.find Char p (string.to-list str) + +def number' : Char → Char → ℕ = + λ tens units ⇒ nat.plus (nat.times 10 (char.digit tens)) (char.digit units) + +def number : String → ℕ = + λ line ⇒ + case string.dup line return ℕ of { + [line] ⇒ + maybe.fold (Char × Char) ℕ 0 + (pair.uncurry' Char Char ℕ number') + (find-first-last Char char.is-digit (string.to-list line)) + } + +def part1 : List String → ℕ = + list.foldr String ℕ 0 (λ str n ⇒ nat.plus (number str) n) + +namespace nat { + #[compile-scheme "(lambda (n) (builtin-io (display n) (newline)))"] + postulate println : ℕ → IO True +} + +#[compile-scheme "(lambda (x) (builtin-io (display x) (newline)))"] +postulate dump : 0.(A : ★) → A → IO True + + +#[main] +def main : IO True = + io.bind (List String) True + (io.read-file-lines "in/day1") + (λ lines ⇒ dump ℕ (part1 lines)) diff --git a/day1.ss b/day1.ss new file mode 100644 index 0000000..44d4555 --- /dev/null +++ b/day1.ss @@ -0,0 +1,55 @@ +(import (rnrs) + (only (chezscheme) make-parameter parameterize printf)) + +(define filename (make-parameter "in/day1")) + +(define (string-reverse str) (list->string (reverse (string->list str)))) + +(define default-numbers + '(("one" . 1) ("two" . 2) ("three" . 3) ("four" . 4) ("five" . 5) + ("six" . 6) ("seven" . 7) ("eight" . 8) ("nine" . 9))) + +(define numbers (make-parameter default-numbers)) + +(define (digit? c) (and (char<=? #\0 c #\9) c)) +(define (digit-val c) (- (char->integer c) (char->integer #\0))) + +(define (at? start short&val long) + (let* [(short (car short&val)) + (val (cdr short&val)) + (end (+ start (string-length short)))] + (cond [(> end (string-length long)) #f] + [(string=? short (substring long start end)) val] + [else #f]))) + +(define (find-first str) + (let loop [(i 0)] + (cond [(digit? (string-ref str i)) => digit-val] + [(exists (lambda (n) (at? i n str)) (numbers))] + [else (loop (+ i 1))]))) + +(define (find-last str) + (let* [(rev-car (lambda (p) (cons (string-reverse (car p)) (cdr p)))) + (rnums (map rev-car (numbers))) + (rstr (string-reverse str))] + (parameterize [(numbers rnums)] (find-first rstr)))) + +(define (make-value first last) (+ (* 10 first) last)) + +(define (value line) (make-value (find-first line) (find-last line))) + +(define (value1 line) (parameterize [(numbers '())] (value line))) +(define (value2 line) (parameterize [(numbers default-numbers)] (value line))) + +(define (all-lines file) + (let [(next (lambda () (get-line file)))] + (do [(line (next) (next)) + (acc '() (cons line acc))] + [(eof-object? line) (reverse acc)]))) + +(define (input) (call-with-input-file (filename) all-lines)) + +(define (part1 input) (apply + (map value1 input))) +(define (part2 input) (apply + (map value2 input))) + +(let [(in (input))] (printf "~a~n~a~n" (part1 in) (part2 in))) diff --git a/lib/bool.quox b/lib/bool.quox new file mode 100644 index 0000000..6b53435 --- /dev/null +++ b/lib/bool.quox @@ -0,0 +1,39 @@ +load "misc.quox"; + +namespace bool { + +def0 Bool : ★ = {true, false}; + +def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b = + λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f }; + +def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A = + λ A ⇒ if-dep (λ _ ⇒ A); + +def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : A = + λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x); + +def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B = + λ A B ⇒ if-dep (λ b ⇒ if-dep¹ (λ _ ⇒ ★) b A B); + +def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False; + +def dup! : (b : Bool) → [ω. Sing Bool b] = + λ b ⇒ if-dep (λ b ⇒ [ω. Sing Bool b]) b + [('true, [δ _ ⇒ 'true])] + [('false, [δ _ ⇒ 'false])]; + +def dup : Bool → [ω. Bool] = + λ b ⇒ appω (Sing Bool b) Bool (λ b' ⇒ sing.val Bool b b') (dup! b); + +def true-not-false : Not ('true ≡ 'false : Bool) = + λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true; + + +-- [todo] infix +def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false; +def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; + +} + +def0 Bool = bool.Bool; diff --git a/lib/either.quox b/lib/either.quox new file mode 100644 index 0000000..bc222fa --- /dev/null +++ b/lib/either.quox @@ -0,0 +1,74 @@ +load "misc.quox"; +load "bool.quox"; + +namespace either { + +def0 Tag : ★ = {left, right}; + +def0 Payload : ★ → ★ → Tag → ★ = + λ A B tag ⇒ case tag return ★ of { 'left ⇒ A; 'right ⇒ B }; + +def0 Either : ★ → ★ → ★ = + λ A B ⇒ (tag : Tag) × Payload A B tag; + +def Left : 0.(A B : ★) → A → Either A B = + λ A B x ⇒ ('left, x); + +def Right : 0.(A B : ★) → B → Either A B = + λ A B x ⇒ ('right, x); + +def elim' : + 0.(A B : ★) → 0.(P : 0.(Either A B) → ★) → + ω.((x : A) → P (Left A B x)) → + ω.((x : B) → P (Right A B x)) → + (t : Tag) → (a : Payload A B t) → P (t, a) = + λ A B P f g t ⇒ + case t + return t' ⇒ (a : Payload A B t') → P (t', a) + of { 'left ⇒ f; 'right ⇒ g }; + +def elim : + 0.(A B : ★) → 0.(P : 0.(Either A B) → ★) → + ω.((x : A) → P (Left A B x)) → + ω.((x : B) → P (Right A B x)) → + (x : Either A B) → P x = + λ A B P f g e ⇒ + case e return e' ⇒ P e' of { (t, a) ⇒ elim' A B P f g t a }; + + +} + +def0 Either = either.Either; +def Left = either.Left; +def Right = either.Right; + + +namespace dec { + +def0 Dec : ★ → ★ = λ A ⇒ Either [0.A] [0.Not A]; + +def Yes : 0.(A : ★) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]; +def No : 0.(A : ★) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]; + +def0 DecEq : ★ → ★ = + λ A ⇒ ω.(x : A) → ω.(y : A) → Dec (x ≡ y : A); + +def elim : + 0.(A : ★) → 0.(P : 0.(Dec A) → ★) → + ω.(0.(y : A) → P (Yes A y)) → + ω.(0.(n : Not A) → P (No A n)) → + (x : Dec A) → P x = + λ A P f g ⇒ + either.elim [0.A] [0.Not A] P + (λ y ⇒ case0 y return y' ⇒ P (Left [0.A] [0.Not A] y') of {[y'] ⇒ f y'}) + (λ n ⇒ case0 n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'}); + +def bool : 0.(A : ★) → Dec A → Bool = + λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false); + +} + +def0 Dec = dec.Dec; +def0 DecEq = dec.DecEq; +def Yes = dec.Yes; +def No = dec.No; diff --git a/lib/io.quox b/lib/io.quox new file mode 100644 index 0000000..7bff457 --- /dev/null +++ b/lib/io.quox @@ -0,0 +1,80 @@ +load "misc.quox" +load "maybe.quox" +load "list.quox" + +namespace io { + +def0 IORes : ★ → ★ = λ A ⇒ A × IOState + +def0 IO : ★ → ★ = λ A ⇒ IOState → IORes A + +def pure : 0.(A : ★) → A → IO A = λ A x s ⇒ (x, s) + +def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B = + λ A B m k s0 ⇒ + case m s0 return IORes B of { (x, s1) ⇒ k x s1 } + +def seq : 0.(B : ★) → IO True → IO B → IO B = + λ B x y ⇒ bind True B x (λ u ⇒ case u return IO B of { 'true ⇒ y }) + +def seq' : IO True → IO True → IO True = seq True + +def pass : IO True = pure True 'true + +#[compile-scheme "(lambda (str) (builtin-io (display str) 'true))"] +postulate print : String → IO True + +def newline = print "\n" + +def println : String → IO True = + λ str ⇒ seq' (print str) newline + +#[compile-scheme "(builtin-io (get-line (current-input-port)))"] +postulate readln : IO String + + +-- [todo] errors lmao + +{- +postulate0 File : ★ + +#[compile-scheme "(lambda (path) (builtin-io (open-input-file path)))"] +postulate open-read : String → IO File + +#[compile-scheme "(lambda (file) (builtin-io (close-port file) 'true))"] +postulate close : File → IO True + +#[compile-scheme + "(lambda% (file if-eof if-line) + (builtin-io + (let ([result (get-line file)]) + (if (eof-object? result) + (cons if-eof file) + (cons (if-line result) file)))))"] +postulate prim-read-line : + File → + ω.(if-eof : Maybe [ω.String]) → + ω.(if-line : ω.String → Maybe [ω.String]) → + IO (Maybe [ω.String] × File) + +def read-line : File → IO (Maybe [ω.String] × File) = + λ f ⇒ prim-read-line f (Nothing [ω.String]) (λ x ⇒ Just [ω.String] [x]) +-} + + +#[compile-scheme + "(lambda (path) (builtin-io (call-with-input-file path get-string-all)))"] +postulate read-file : ω.(path : String) → IO String + +#[compile-scheme + "(lambda (path) (builtin-io + (call-with-input-file path + (lambda (file) + (do [(line (get-line file) (get-line file)) + (acc '() (cons line acc))] + [(eof-object? line) (reverse acc)])))))"] +postulate read-file-lines : ω.(path : String) → IO (List String) + +} + +def0 IO = io.IO diff --git a/lib/list.quox b/lib/list.quox new file mode 100644 index 0000000..58f89c9 --- /dev/null +++ b/lib/list.quox @@ -0,0 +1,163 @@ +load "nat.quox"; +load "maybe.quox"; +load "bool.quox"; + +namespace vec { + +def0 Vec : ℕ → ★ → ★ = + λ n A ⇒ + caseω n return ★ of { + zero ⇒ {nil}; + succ _, 0.Tail ⇒ A × Tail + }; + +def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) → + P 0 'nil → + ω.((x : A) → 0.(n : ℕ) → 0.(xs : Vec n A) → + P n xs → P (succ n) (x, xs)) → + (n : ℕ) → (xs : Vec n A) → P n xs = + λ A P pn pc n ⇒ + case n return n' ⇒ (xs' : Vec n' A) → P n' xs' of { + zero ⇒ λ nil ⇒ + case nil return nil' ⇒ P 0 nil' of { 'nil ⇒ pn }; + succ n, ih ⇒ λ cons ⇒ + case cons return cons' ⇒ P (succ n) cons' of { + (first, rest) ⇒ pc first n rest (ih rest) + } + }; + +-- haha gross +def elimω : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) → + ω.(P 0 'nil) → + ω.(ω.(x : A) → 0.(n : ℕ) → 0.(xs : Vec n A) → + ω.(P n xs) → P (succ n) (x, xs)) → + ω.(n : ℕ) → ω.(xs : Vec n A) → P n xs = + λ A P pn pc n ⇒ + caseω n return n' ⇒ ω.(xs' : Vec n' A) → P n' xs' of { + zero ⇒ λ nil ⇒ + caseω nil return nil' ⇒ P 0 nil' of { 'nil ⇒ pn }; + succ n, ω.ih ⇒ λ cons ⇒ + caseω cons return cons' ⇒ P (succ n) cons' of { + (first, rest) ⇒ pc first n rest (ih rest) + } + }; + +#[compile-scheme "(lambda% (n xs) xs)"] +def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A = + λ A n ⇒ + case n return n' ⇒ Vec n' A → Vec¹ n' A of { + zero ⇒ λ xs ⇒ + case xs return Vec¹ 0 A of { 'nil ⇒ 'nil }; + succ n', f' ⇒ λ xs ⇒ + case xs return Vec¹ (succ n') A of { + (first, rest) ⇒ (first, f' rest) + } + } + +} + +def0 Vec = vec.Vec; + + +namespace list { + +def0 List : ★ → ★ = + λ A ⇒ (len : ℕ) × Vec len A; + +def Nil : 0.(A : ★) → List A = + λ A ⇒ (0, 'nil); + +def Cons : 0.(A : ★) → A → List A → List A = + λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) }; + +def elim : 0.(A : ★) → 0.(P : List A → ★) → + P (Nil A) → + ω.((x : A) → 0.(xs : List A) → P xs → P (Cons A x xs)) → + (xs : List A) → P xs = + λ A P pn pc xs ⇒ + case xs return xs' ⇒ P xs' of { (len, elems) ⇒ + vec.elim A (λ n xs ⇒ P (n, xs)) + pn (λ x n xs ih ⇒ pc x (n, xs) ih) + len elems + }; + +def elimω : 0.(A : ★) → 0.(P : List A → ★) → + ω.(P (Nil A)) → + ω.(ω.(x : A) → 0.(xs : List A) → ω.(P xs) → P (Cons A x xs)) → + ω.(xs : List A) → P xs = + λ A P pn pc xs ⇒ + caseω xs return xs' ⇒ P xs' of { (len, elems) ⇒ + vec.elimω A (λ n xs ⇒ P (n, xs)) + pn (λ x n xs ih ⇒ pc x (n, xs) ih) + len elems + }; + +-- [fixme] List A <: List¹ A should be automatic, imo +#[compile-scheme "(lambda (xs) xs)"] +def up : 0.(A : ★) → List A → List¹ A = + λ A xs ⇒ + case xs return List¹ A of { (len, elems) ⇒ + case nat.dup! len return List¹ A of { [p] ⇒ + caseω p return List¹ A of { (lenω, eq0) ⇒ + case eq0 return List¹ A of { [eq] ⇒ + (lenω, vec.up A lenω (coe (𝑖 ⇒ Vec (eq @𝑖) A) @1 @0 elems)) + } + } + } + }; + +def foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B = + λ A B z f xs ⇒ elim A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs; + +def foldl : 0.(A B : ★) → B → ω.(B → A → B) → List A → B = + λ A B z f xs ⇒ + foldr A (B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z; + +def map : 0.(A B : ★) → ω.(A → B) → List A → List B = + λ A B f ⇒ foldr A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys); + + +-- ugh +def foldrω : 0.(A B : ★) → ω.B → ω.(ω.A → ω.B → B) → ω.(List A) → B = + λ A B z f xs ⇒ elimω A (λ _ ⇒ B) z (λ x _ y ⇒ f x y) xs; + +def foldlω : 0.(A B : ★) → ω.B → ω.(ω.B → ω.A → B) → ω.(List A) → B = + λ A B z f xs ⇒ + foldrω A (ω.B → B) (λ b ⇒ b) (λ a g b ⇒ g (f b a)) xs z; + +def mapω : 0.(A B : ★) → ω.(ω.A → B) → ω.(List A) → List B = + λ A B f ⇒ foldrω A (List B) (Nil B) (λ x ys ⇒ Cons B (f x) ys); + + +def0 All : (A : ★) → (P : A → ★) → List A → ★ = + λ A P xs ⇒ foldr¹ A ★ True (λ x ps ⇒ P x × ps) (up A xs); + +def append : 0.(A : ★) → List A → List A → List A = + λ A xs ys ⇒ foldr A (List A) ys (Cons A) xs; + +def reverse : 0.(A : ★) → List A → List A = + λ A ⇒ foldl A (List A) (Nil A) (λ xs x ⇒ Cons A x xs); + + +def find : 0.(A : ★) → ω.(ω.A → Bool) → ω.(List A) → Maybe A = + λ A p ⇒ + foldlω A (Maybe A) (Nothing A) (λ m x ⇒ maybe.or A m (maybe.check A p x)); + + +postulate0 SchemeList : ★ → ★ + +#[compile-scheme + "(lambda (list) (cons (length list) (fold-right cons 'nil list)))"] +postulate from-scheme : 0.(A : ★) → SchemeList A → List A + +#[compile-scheme + "(lambda (list) + (let loop [(acc '()) (list (cdr list))] + (if (pair? list) + (loop (cons (car list) acc) (cdr list)) + (reverse acc))))"] +postulate to-scheme : 0.(A : ★) → List A → SchemeList A + +} + +def0 List = list.List; diff --git a/lib/maybe.quox b/lib/maybe.quox new file mode 100644 index 0000000..4c35f38 --- /dev/null +++ b/lib/maybe.quox @@ -0,0 +1,140 @@ +load "misc.quox" +load "pair.quox" +load "either.quox" + +namespace maybe { + +def0 Tag : ★ = {nothing, just} + +def0 Payload : Tag → ★ → ★ = + λ tag A ⇒ case tag return ★ of { 'nothing ⇒ True; 'just ⇒ A } + +def0 Maybe : ★ → ★ = + λ A ⇒ (t : Tag) × Payload t A + +def tag : 0.(A : ★) → ω.(Maybe A) → Tag = + λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag } + +def Nothing : 0.(A : ★) → Maybe A = + λ _ ⇒ ('nothing, 'true) + +def Just : 0.(A : ★) → A → Maybe A = + λ _ x ⇒ ('just, x) + +def0 IsJustTag : Tag → ★ = + λ t ⇒ case t return ★ of { 'just ⇒ True; 'nothing ⇒ False } + +def0 IsJust : (A : ★) → Maybe A → ★ = + λ A x ⇒ IsJustTag (tag A x) + +def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) = + λ A x ⇒ + caseω tag A x return t ⇒ Dec (IsJustTag t) of { + 'just ⇒ Yes True 'true; + 'nothing ⇒ No False (λ x ⇒ x) + } + +def0 nothing-unique : + (A : ★) → (x : True) → ('nothing, x) ≡ Nothing A : Maybe A = + λ A x ⇒ + case x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of { + 'true ⇒ δ _ ⇒ ('nothing, 'true) + } + +def elim' : + 0.(A : ★) → + 0.(P : (t : Tag) → Payload t A → ★) → + ω.(P 'nothing 'true) → + ω.((x : A) → P 'just x) → + (t : Tag) → (x : Payload t A) → P t x = + λ A P nothing just tag ⇒ + case tag return t ⇒ (x : Payload t A) → P t x of { + 'nothing ⇒ λ x ⇒ case x return x' ⇒ P 'nothing x' of { 'true ⇒ nothing }; + 'just ⇒ just + } + +def elim : + 0.(A : ★) → + 0.(P : Maybe A → ★) → + ω.(P (Nothing A)) → + ω.((x : A) → P (Just A x)) → + (x : Maybe A) → P x = + λ A P n j x ⇒ + case x return x' ⇒ P x' of { + (tag, payload) ⇒ elim' A (λ x t ⇒ P (x, t)) n j tag payload + } + +def elimω' : + 0.(A : ★) → + 0.(P : (t : Tag) → Payload t A → ★) → + ω.(P 'nothing 'true) → + ω.(ω.(x : A) → P 'just x) → + ω.(t : Tag) → ω.(x : Payload t A) → P t x = + λ A P nothing just tag ⇒ + case tag return t ⇒ ω.(x : Payload t A) → P t x of { + 'nothing ⇒ λ x ⇒ case x return x' ⇒ P 'nothing x' of { 'true ⇒ nothing }; + 'just ⇒ just + } + +def elimω : + 0.(A : ★) → + 0.(P : Maybe A → ★) → + ω.(P (Nothing A)) → + ω.(ω.(x : A) → P (Just A x)) → + ω.(x : Maybe A) → P x = + λ A P n j x ⇒ + caseω x return x' ⇒ P x' of { + (tag, payload) ⇒ elimω' A (λ x t ⇒ P (x, t)) n j tag payload + } + +{- +-- direct elim implementation +def elim : + 0.(A : ★) → + 0.(P : Maybe A → ★) → + ω.(P (Nothing A)) → + ω.((x : A) → P (Just A x)) → + (x : Maybe A) → P x = + λ A P n j x ⇒ + case x return x' ⇒ P x' of { (tag, payload) ⇒ + (case tag + return t ⇒ + 0.(eq : tag ≡ t : Tag) → P (t, coe (𝑖 ⇒ Payload (eq @𝑖) A) payload) + of { + 'nothing ⇒ + λ eq ⇒ + case coe (𝑖 ⇒ Payload (eq @𝑖) A) payload + return p ⇒ P ('nothing, p) + of { 'true ⇒ n }; + 'just ⇒ λ eq ⇒ j (coe (𝑖 ⇒ Payload (eq @𝑖) A) payload) + }) (δ 𝑖 ⇒ tag) + } +-} + +def fold : 0.(A B : ★) → ω.B → ω.(A → B) → Maybe A → B = + λ A B ⇒ elim A (λ _ ⇒ B) + +def foldω : 0.(A B : ★) → ω.B → ω.(ω.A → B) → ω.(Maybe A) → B = + λ A B ⇒ elimω A (λ _ ⇒ B) + +def join : 0.(A : ★) → (Maybe (Maybe A)) → Maybe A = + λ A ⇒ fold (Maybe A) (Maybe A) (Nothing A) (λ x ⇒ x) + +def pair : 0.(A B : ★) → ω.(Maybe A) → ω.(Maybe B) → Maybe (A × B) = + λ A B x y ⇒ + foldω A (Maybe (A × B)) (Nothing (A × B)) + (λ x' ⇒ fold B (Maybe (A × B)) (Nothing (A × B)) + (λ y' ⇒ Just (A × B) (x', y')) y) x + + +def check : 0.(A : ★) → (ω.A → Bool) → ω.A → Maybe A = + λ A p x ⇒ bool.if (Maybe A) (p x) (Just A x) (Nothing A) + +def or : 0.(A : ★) → Maybe A → ω.(Maybe A) → Maybe A = + λ A l r ⇒ fold A (Maybe A) r (Just A) l + +} + +def0 Maybe = maybe.Maybe +def Just = maybe.Just +def Nothing = maybe.Nothing diff --git a/lib/misc.quox b/lib/misc.quox new file mode 100644 index 0000000..656b502 --- /dev/null +++ b/lib/misc.quox @@ -0,0 +1,92 @@ +def0 True : ★ = {true} + +def0 False : ★ = {} +def0 Not : ★ → ★ = λ A ⇒ ω.A → False + +def void : 0.(A : ★) → 0.False → A = + λ A v ⇒ case0 v return A of { } + +def0 All : (A : ★) → (0.A → ★) → ★ = + λ A P ⇒ (x : A) → P x + +def0 cong : + (A : ★) → (P : 0.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 @𝑖) + +def0 cong' : + (A B : ★) → (f : A → B) → + (x y : A) → (xy : x ≡ y : A) → f x ≡ f y : B = + λ A B ⇒ cong A (λ _ ⇒ B) + +def0 coherence : + (A B : ★) → (AB : A ≡ B : ★) → (x : A) → + Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) = + λ A B AB x ⇒ + δ 𝑗 ⇒ 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 → ★ = + λ 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) → + (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 } + +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 @𝑗 } + +def appω : 0.(A B : ★) → ω.(f : ω.A → B) → [ω.A] → [ω.B] = + λ A B f x ⇒ + case x return [ω.B] of { [x'] ⇒ [f x'] } + +def app2ω : 0.(A B C : ★) → ω.(f : ω.A → ω.B → C) → [ω.A] → [ω.B] → [ω.C] = + λ A B C f x y ⇒ + case x return [ω.C] of { [x'] ⇒ + case y return [ω.C] of { [y'] ⇒ [f x' y'] } + } + +def getω : 0.(A : ★) → [ω.A] → A = + λ A x ⇒ case x return A of { [x] ⇒ x } + +def0 HEq : (A B : ★) → A → B → ★¹ = + λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y + + +def0 Sing : (A : ★) → A → ★ = + λ A x ⇒ (val : A) × [0. val ≡ x : A] + +def sing : 0.(A : ★) → (x : A) → Sing A x = + λ A x ⇒ (x, [δ _ ⇒ x]) + +namespace sing { + +def val : 0.(A : ★) → 0.(x : A) → Sing A x → A = + λ A _ sg ⇒ + case sg return A of { (x, eq) ⇒ case eq return A of { [_] ⇒ x } } + +def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A = + λ A x sg ⇒ + case sg return sg' ⇒ val A x sg' ≡ x : A of { (x', eq) ⇒ + case eq return eq' ⇒ val A x (x', eq') ≡ x : A of { [eq'] ⇒ eq' } + } + +def app : 0.(A B : ★) → 0.(x : A) → + (f : A → B) → Sing A x → Sing B (f x) = + λ A B x f sg ⇒ + case sg return Sing B (f x) of { (x_, eq) ⇒ + case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) } + } + +} diff --git a/lib/nat.quox b/lib/nat.quox new file mode 100644 index 0000000..d154ee1 --- /dev/null +++ b/lib/nat.quox @@ -0,0 +1,196 @@ +load "misc.quox"; +load "bool.quox"; +load "either.quox"; + +namespace nat { + +def elim-0-1 : + 0.(P : ℕ → ★) → + ω.(P 0) → ω.(P 1) → + ω.(0.(n : ℕ) → P n → P (succ n)) → + (n : ℕ) → P n = + λ P p0 p1 ps n ⇒ + case n return n' ⇒ P n' of { + zero ⇒ p0; + succ n' ⇒ + case n' return n'' ⇒ P (succ n'') of { + zero ⇒ p1; + succ n'', IH ⇒ ps (succ n'') IH + } + } + +def elim-pair : + 0.(P : ℕ → ℕ → ★) → + ω.(P 0 0) → + ω.(0.(n : ℕ) → P 0 n → P 0 (succ n)) → + ω.(0.(m : ℕ) → P m 0 → P (succ m) 0) → + ω.(0.(m n : ℕ) → P m n → P (succ m) (succ n)) → + ω.(m : ℕ) → (n : ℕ) → P m n = + λ P zz zs sz ss m ⇒ + caseω m return m' ⇒ (n : ℕ) → P m' n of { + 0 ⇒ λ n ⇒ case n return n' ⇒ P 0 n' of { + 0 ⇒ zz; + succ n', ihn ⇒ zs n' ihn + }; + succ m', ω.ihm ⇒ λ n ⇒ case n return n' ⇒ P (succ m') n' of { + 0 ⇒ sz m' (ihm 0); + succ n' ⇒ ss m' n' (ihm n') + } + } + +#[compile-scheme "(lambda (n) (cons n 'erased))"] +def dup! : (n : ℕ) → [ω. Sing ℕ n] = + λ n ⇒ + case n return n' ⇒ [ω. Sing ℕ n'] of { + zero ⇒ [(zero, [δ _ ⇒ zero])]; + succ n, d ⇒ + appω (Sing ℕ n) (Sing ℕ (succ n)) + (λ n' ⇒ sing.app ℕ ℕ n (λ n ⇒ succ n) n') d + }; + +def dup : ℕ → [ω.ℕ] = + λ n ⇒ appω (Sing ℕ n) ℕ (λ n' ⇒ sing.val ℕ n n') (dup! n); + +#[compile-scheme "(lambda% (m n) (+ m n))"] +def plus : ℕ → ℕ → ℕ = + λ m n ⇒ + case m return ℕ of { + zero ⇒ n; + succ _, p ⇒ succ p + }; + +#[compile-scheme "(lambda% (m n) (* m n))"] +def timesω : ℕ → ω.ℕ → ℕ = + λ m n ⇒ + case m return ℕ of { + zero ⇒ zero; + succ _, t ⇒ plus n t + }; + +def times : ℕ → ℕ → ℕ = + λ m n ⇒ case dup n return ℕ of { [n] ⇒ timesω m n }; + +def pred : ℕ → ℕ = λ n ⇒ case n return ℕ of { zero ⇒ zero; succ n ⇒ n }; + +def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ = + λ n ⇒ δ 𝑖 ⇒ n; + +def0 succ-inj : (m n : ℕ) → succ m ≡ succ n : ℕ → m ≡ n : ℕ = + λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖); + +#[compile-scheme "(lambda% (m n) (max 0 (- m n)))"] +def minus : ℕ → ℕ → ℕ = + λ m n ⇒ + (case n return ℕ → ℕ of { + zero ⇒ λ m ⇒ m; + succ _, f ⇒ λ m ⇒ f (pred m) + }) m; + + +def0 IsSucc : ℕ → ★ = + λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True }; + +def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) = + λ n ⇒ + caseω n return n' ⇒ Dec (IsSucc n') of { + zero ⇒ No (IsSucc zero) (λ v ⇒ v); + succ n ⇒ Yes (IsSucc (succ n)) 'true + }; + +def zero-not-succ : 0.(m : ℕ) → Not (zero ≡ succ m : ℕ) = + λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) @1 @0 'true; + +def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) = + λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) 'true; + + +def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) = + λ m ⇒ + case m return m' ⇒ Not (m' ≡ succ m' : ℕ) of { + zero ⇒ zero-not-succ 0; + succ n, ω.ih ⇒ λ eq ⇒ ih (succ-inj n (succ n) eq) + } + + +#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"] +def eq? : DecEq ℕ = + λ m ⇒ + caseω m + return m' ⇒ ω.(n : ℕ) → Dec (m' ≡ n : ℕ) + of { + zero ⇒ λ n ⇒ + caseω n return n' ⇒ Dec (zero ≡ n' : ℕ) of { + zero ⇒ Yes (zero ≡ zero : ℕ) (δ _ ⇒ zero); + succ n' ⇒ No (zero ≡ succ n' : ℕ) (λ eq ⇒ zero-not-succ n' eq) + }; + succ m', ω.ih ⇒ λ n ⇒ + caseω n return n' ⇒ Dec (succ m' ≡ n' : ℕ) of { + zero ⇒ No (succ m' ≡ zero : ℕ) (λ eq ⇒ succ-not-zero m' eq); + succ n' ⇒ + dec.elim (m' ≡ n' : ℕ) (λ _ ⇒ Dec (succ m' ≡ succ n' : ℕ)) + (λ y ⇒ Yes (succ m' ≡ succ n' : ℕ) (δ 𝑖 ⇒ succ (y @𝑖))) + (λ n ⇒ No (succ m' ≡ succ n' : ℕ) (λ eq ⇒ n (succ-inj m' n' eq))) + (ih n') + } + }; + + +def0 Ordering : ★ = {lt, eq, gt} + +def from-ordering : 0.(A : ★) → ω.A → ω.A → ω.A → Ordering → A = + λ A lt eq gt o ⇒ + case o return A of { 'lt ⇒ lt; 'eq ⇒ eq; 'gt ⇒ gt } + +def drop-ordering : 0.(A : ★) → Ordering → A → A = + λ A o x ⇒ case o return A of { 'lt ⇒ x; 'eq ⇒ x; 'gt ⇒ x } + +def compareω : ω.ℕ → ℕ → Ordering = + elim-pair (λ _ _ ⇒ Ordering) + 'eq + (λ _ o ⇒ drop-ordering Ordering o 'lt) + (λ _ o ⇒ drop-ordering Ordering o 'gt) + (λ _ _ x ⇒ x) + +def compare : ℕ → ℕ → Ordering = + λ m n ⇒ + case dup m return Ordering of { [m] ⇒ + case dup n return Ordering of { [n] ⇒ compareω m n } } + +def lt : ω.ℕ → ω.ℕ → Bool = + λ m n ⇒ from-ordering Bool 'true 'false 'false (compare m n) + +def le : ω.ℕ → ω.ℕ → Bool = + λ m n ⇒ from-ordering Bool 'true 'true 'false (compare m n) + +def eq : ω.ℕ → ω.ℕ → Bool = + λ m n ⇒ from-ordering Bool 'false 'true 'false (compare m n) + +def gt : ω.ℕ → ω.ℕ → Bool = + λ m n ⇒ from-ordering Bool 'false 'false 'true (compare m n) + +def ge : ω.ℕ → ω.ℕ → Bool = + λ m n ⇒ from-ordering Bool 'false 'true 'true (compare m n) + + +def0 plus-zero : (m : ℕ) → m ≡ plus m 0 : ℕ = + λ m ⇒ + case m return m' ⇒ m' ≡ plus m' 0 : ℕ of { + zero ⇒ δ _ ⇒ 0; + succ m', ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖) + }; + +def0 plus-succ : (m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ = + λ m n ⇒ + case m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of { + zero ⇒ δ _ ⇒ succ n; + succ _, ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖) + }; + +def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ = + λ m ⇒ + case m return m' ⇒ 0 ≡ timesω m' 0 : ℕ of { + zero ⇒ δ _ ⇒ zero; + succ m', ih ⇒ ih + }; + +} diff --git a/lib/pair.quox b/lib/pair.quox new file mode 100644 index 0000000..4bf33c6 --- /dev/null +++ b/lib/pair.quox @@ -0,0 +1,74 @@ +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 }; +-} + +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 }; + +def uncurry' : + 0.(A B C : ★) → (A → B → C) → (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); + +def curry' : + 0.(A B C : ★) → (A × B → C) → 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) }; + +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 @𝑖); + +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 @𝑖); + +def map : + 0.(A A' : ★) → + 0.(B : A → ★) → 0.(B' : A' → ★) → + (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) }; + +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); + +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); + +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; + +} + +def0 Σ = pair.Σ; +-- def fst = pair.fst; +-- def snd = pair.snd; diff --git a/lib/qty.quox b/lib/qty.quox new file mode 100644 index 0000000..9f5e529 --- /dev/null +++ b/lib/qty.quox @@ -0,0 +1,77 @@ +def0 Qty : ★ = {"zero", one, any} + +def dup : Qty → [ω.Qty] = + λ π ⇒ case π return [ω.Qty] of { + 'zero ⇒ ['zero]; + 'one ⇒ ['one]; + 'any ⇒ ['any]; + } + +def drop : 0.(A : ★) → Qty → A → A = + λ A π x ⇒ case π return A of { + 'zero ⇒ x; + 'one ⇒ x; + 'any ⇒ x; + } + +def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A = + λ A π z nz ⇒ + case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz } + +def plus : Qty → Qty → Qty = + λ π ρ ⇒ + case π return Qty of { + 'zero ⇒ ρ; + 'one ⇒ if-zero Qty ρ 'one 'any; + 'any ⇒ drop Qty ρ 'any; + } + +def times : Qty → Qty → Qty = + λ π ρ ⇒ + case π return Qty of { + 'zero ⇒ drop Qty ρ 'zero; + 'one ⇒ ρ; + 'any ⇒ if-zero Qty ρ 'zero 'any; + } + +def0 FUN : Qty → (A : ★) → (A → ★) → ★ = + λ π A B ⇒ + case π return ★ of { + 'zero ⇒ 0.(x : A) → B x; + 'one ⇒ 1.(x : A) → B x; + 'any ⇒ ω.(x : A) → B x; + } + +def0 Fun : Qty → ★ → ★ → ★ = + λ π A B ⇒ FUN π A (λ _ ⇒ B) + +def0 Box : Qty → ★ → ★ = + λ π A ⇒ + case π return ★ of { + 'zero ⇒ [0.A]; + 'one ⇒ [1.A]; + 'any ⇒ [ω.A]; + } + +def0 unbox : (π : Qty) → (A : ★) → Box π A → A = + λ π A ⇒ + case π return π' ⇒ Box π' A → A of { + 'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x }; + 'one ⇒ λ x ⇒ case x return A of { [x] ⇒ x }; + 'any ⇒ λ x ⇒ case x return A of { [x] ⇒ x }; + } + +def0 unbox0 = unbox 'zero +def0 unbox1 = unbox 'one +def0 unboxω = unbox 'any + +def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) → + FUN π A B → (x : Box π A) → B (unbox π A x) = + λ π A B ⇒ + case π + return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x) + of { + 'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox0 A x') of { [x] ⇒ f x }; + 'one ⇒ λ f x ⇒ case x return x' ⇒ B (unbox1 A x') of { [x] ⇒ f x }; + 'any ⇒ λ f x ⇒ case x return x' ⇒ B (unboxω A x') of { [x] ⇒ f x }; + } diff --git a/pack.toml b/pack.toml new file mode 100644 index 0000000..2fdc62c --- /dev/null +++ b/pack.toml @@ -0,0 +1,13 @@ +collection = "nightly-231020" + +[custom.all.quox-lib] +type = "git" +url = "https://git.rhiannon.website/rhi/quox.git" +commit = "latest:🐉" +ipkg = "lib/quox-lib.ipkg" + +[custom.all.quox] +type = "git" +url = "https://git.rhiannon.website/rhi/quox.git" +commit = "latest:🐉" +ipkg = "exe/quox.ipkg"