diff --git a/documentation/bookmark/business/decision_making.md b/documentation/bookmark/business/decision_making.md index 5467d52c0e..6907999d76 100644 --- a/documentation/bookmark/business/decision_making.md +++ b/documentation/bookmark/business/decision_making.md @@ -1,5 +1,6 @@ # Reference +0. [On the importance of non-goals](https://www.dsebastien.net/on-the-importance-of-non-goals/) 0. [Analytic hierarchy process](https://en.wikipedia.org/wiki/Analytic_hierarchy_process) 0. [Causal Explanations Considered Harmful: On the logical fallacy of causal projection](https://superbowl.substack.com/p/causal-explanations-considered-harmful) 0. [Why Developing Negative Capability is Critical in Leadership](https://www.leadingsapiens.com/developing-negative-capability-leadership/) diff --git a/documentation/bookmark/compilation/target/c++.md b/documentation/bookmark/compilation/target/c++.md index 4d472a719e..abdecd553c 100644 --- a/documentation/bookmark/compilation/target/c++.md +++ b/documentation/bookmark/compilation/target/c++.md @@ -22,6 +22,7 @@ # Reference +0. [Writing custom C++20 coroutine systems](https://www.chiark.greenend.org.uk/~sgtatham/quasiblog/coroutines-c++20/) 0. [STX](https://lamarrr.github.io/STX/) 0. [The joys and perils of C and C++ aliasing, Part 1](https://developers.redhat.com/blog/2020/06/02/the-joys-and-perils-of-c-and-c-aliasing-part-1#) 0. [The joys and perils of aliasing in C and C++, Part 2](https://developers.redhat.com/blog/2020/06/03/the-joys-and-perils-of-aliasing-in-c-and-c-part-2) diff --git a/documentation/bookmark/database.md b/documentation/bookmark/database.md index 63f40ca45e..d903456339 100644 --- a/documentation/bookmark/database.md +++ b/documentation/bookmark/database.md @@ -146,6 +146,7 @@ ## General +0. [Readings in Database Systems, 5th Edition](http://www.redbook.io/) 0. [How FoundationDB works and why it works](https://blog.the-pans.com/notes-on-the-foundationdb-paper/) 0. [FeatureBase: The First OLAP Database Built Entirely on Bitmaps](https://www.featurebase.com/) 0. [FeatureBase](https://github.com/FeatureBaseDB/featurebase) diff --git a/documentation/bookmark/health.md b/documentation/bookmark/health.md index 6034a04b24..41334dc916 100644 --- a/documentation/bookmark/health.md +++ b/documentation/bookmark/health.md @@ -1,5 +1,6 @@ # Reference +0. [From Worst-Case CANCER to Best-Case Scenario (NO CANCER)](https://www.youtube.com/watch?v=6JD_JzprK5U) 0. [How To Naturally Reverse Premature Graying of Hair](https://www.youtube.com/watch?v=LMLdClbwqhE) 0. [Contraceptive Properties of Stevia rebaudiana](https://www.science.org/doi/10.1126/science.162.3857.1007.a) 0. [The #1 Nontoxic Vegetable Wash](https://www.youtube.com/watch?v=GKLZpquBc_4) diff --git a/documentation/bookmark/play/game/engine.md b/documentation/bookmark/play/game/engine.md index 848857189d..21a19343cc 100644 --- a/documentation/bookmark/play/game/engine.md +++ b/documentation/bookmark/play/game/engine.md @@ -2,7 +2,7 @@ ## General -0. []() +0. [Books I had to read to develop a game engine](https://www.haroldserrano.com/blog/books-i-used-to-develop-a-game-engine) 0. [MonoGame: One framework for creating powerful cross-platform games](https://www.monogame.net/) 0. [Heaps.io](https://heaps.io/index.html) 0. [The Machinery](https://ourmachinery.com/) diff --git a/documentation/bookmark/tool/text_editor/code_folding.md b/documentation/bookmark/tool/text_editor/code_folding.md new file mode 100644 index 0000000000..063922f4d4 --- /dev/null +++ b/documentation/bookmark/tool/text_editor/code_folding.md @@ -0,0 +1,4 @@ +# Reference + +0. [ts-fold: Code-folding using tree-sitter](https://github.com/emacs-tree-sitter/ts-fold) + diff --git a/documentation/bookmark/type_theory/unit.md b/documentation/bookmark/type_theory/unit.md index 1a82ddf669..9dc92a34c0 100644 --- a/documentation/bookmark/type_theory/unit.md +++ b/documentation/bookmark/type_theory/unit.md @@ -1,5 +1,7 @@ # Reference +0. [uom: Units of measurement -- type-safe zero-cost dimensional analysis](https://github.com/iliekturtles/uom) +0. [Dimensional analysis](https://en.wikipedia.org/wiki/Dimensional_analysis) 0. [mp-units - A Units Library for C++](https://github.com/mpusz/units) 0. https://en.wikipedia.org/wiki/Metric_prefix#Metric_units 0. [unittyped: An extendable library for type-safe computations including units.](https://hackage.haskell.org/package/unittyped) diff --git a/stdlib/source/library/lux/control/function/predicate.lux b/stdlib/source/library/lux/control/function/predicate.lux index 5f270575fd..51b8b4d3a0 100644 --- a/stdlib/source/library/lux/control/function/predicate.lux +++ b/stdlib/source/library/lux/control/function/predicate.lux @@ -47,7 +47,8 @@ (All (_ of) (-> (Predicate of) (Predicate of))) - (|>> predicate .not)) + (|>> predicate + .not)) (alias [not] ..complement) diff --git a/stdlib/source/library/lux/control/logic.lux b/stdlib/source/library/lux/control/logic.lux index 8198d9686d..dc8c3c44e3 100644 --- a/stdlib/source/library/lux/control/logic.lux +++ b/stdlib/source/library/lux/control/logic.lux @@ -11,8 +11,7 @@ [monad (.only Monad do)]] [control - ["[0]" try (.only Try) (.use "[1]#[0]" monad)] - ["[0]" object (.only Object)]] + ["[0]" try (.only Try) (.use "[1]#[0]" monad)]] [data ["[0]" product] ["[0]" text] @@ -27,7 +26,8 @@ ["[0]" frac]]] [meta [type - ["[0]" nominal]] + ["[0]" nominal] + ["[0]" object (.only Object object)]] [macro ["^" pattern]]]]]) @@ -158,8 +158,9 @@ #unified (object.method (function (_ next again [this [reference]]) (when (object.as (object.class this) reference) - {.#Some [reference#= reference_value]} - (let [[this#= this_value] (object.state this)] + {.#Some reference} + (let [[reference#= reference_value] (object.state reference) + [this#= this_value] (object.state this)] (if (this#= reference_value this_value) ..success ..failure)) @@ -171,7 +172,7 @@ (All (_ of) (-> (Equivalence of) of (Term of))) - (object.new ..constant_class [equivalence it])) + (object ..constant_class [equivalence it])) (nominal.every (Variable of) ID @@ -300,8 +301,9 @@ #unified (object.method (function (_ next again [this [reference]]) (when (object.as (object.class this) reference) - {.#Some reference_id} - (unified_variables reference_id this) + {.#Some reference} + (let [reference_id (object.state reference)] + (unified_variables reference_id this)) {.#None} (do ..monad @@ -331,5 +333,5 @@ (function (_ context) (let [id (dictionary.size context)] (list [(dictionary.has id [equivalence {.#Left id}] context) - (object.new ..variable_class (nominal.abstraction id))])))) + (object ..variable_class (nominal.abstraction id))])))) ) diff --git a/stdlib/source/library/lux/control/pattern.lux b/stdlib/source/library/lux/control/pattern.lux new file mode 100644 index 0000000000..c0ae5782b3 --- /dev/null +++ b/stdlib/source/library/lux/control/pattern.lux @@ -0,0 +1,43 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +... ["Type-safe pattern combinators" by Morten Rhiger](https://core.ac.uk/works/9613163) +(.require + [library + [lux (.except Pattern + when) + [control + [pure (.only Pure)] + [function + [predicate (.only Predicate)]]] + [meta + ["[0]" type]]]] + [/ + ["[0]" input] + ["[0]" match] + ["[0]" pattern] + ["[0]" clause (.only Clause Pattern)]]) + +(the .public (when input clause) + (All (_ input value) + (-> input (Clause input value) + value)) + (clause input + (function (_ _) + (undefined)))) + +(the .public (match? pattern input) + (All (_ of) + (-> (Pattern of Bit Bit) + (Predicate of))) + (<| (..when input) + (all clause.or + (clause.clause pattern true) + (clause.clause pattern.any false)))) + +(the .public (abstraction pattern body) + (All (_ term input value) + (-> (Pattern input term value) term + (-> input value))) + (function (_ input) + (..when input (clause.clause pattern body)))) diff --git a/stdlib/source/library/lux/control/pattern/body.lux b/stdlib/source/library/lux/control/pattern/body.lux new file mode 100644 index 0000000000..cfecb3094b --- /dev/null +++ b/stdlib/source/library/lux/control/pattern/body.lux @@ -0,0 +1,68 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except or and) + [meta + ["[0]" type]]]] + [// + ["[0]" input] + ["[0]" output]]) + +(every .public (Then arity value) + (-> arity + value)) + +(every .public Constant + (Then input.Zero)) + +(every .public Else + Constant) + +(every .public (Body outer inner value) + (-> (Then inner value) (Else value) + (Then outer value))) + +(every .public Zero + (All (_ arity value) + (Body arity arity value))) + +(the .public success + Zero + (function (_ next exit) + next)) + +(every .public (Succ of) + (All (_ arity value) + (|> (Body arity (input.Succ of arity) value) + (output.Succ of)))) + +(the .public (succ value) + Succ + (function (_ next exit stack) + (next (input.succ value stack)))) + +(the .public failure + Body + (function (_ next exit stack) + (exit (input.zero)))) + +(the .public (or left right) + (All (_ arity_0 arity_1 value) + (type.let [choice (Body arity_0 arity_1 value)] + (-> choice choice + choice))) + (function (_ next exit stack) + (left next + (function (_ _) + (right next exit stack)) + stack))) + +(the .public (and left right) + (All (_ arity_0 arity_1 arity_2 value) + (-> (Body arity_1 arity_0 value) + (Body arity_2 arity_1 value) + (Body arity_2 arity_0 value))) + (function (_ input exit stack) + (right (left input exit) exit stack))) diff --git a/stdlib/source/library/lux/control/pattern/clause.lux b/stdlib/source/library/lux/control/pattern/clause.lux new file mode 100644 index 0000000000..cec132fc0d --- /dev/null +++ b/stdlib/source/library/lux/control/pattern/clause.lux @@ -0,0 +1,40 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except Pattern + or) + [meta + ["[0]" type]]]] + [// + ["[0]" input] + ["[0]" match] + ["[0]" body (.only Body)]]) + +(every .public (Pattern input negative value) + (Ex (_ arity) + (type.let [positive (body.Then arity value)] + [(-> match.Constant (-> negative positive)) + (-> input (Body input.Zero arity value))]))) + +(every .public (Clause input value) + (-> input (body.Else value) + value)) + +(the .public (clause pattern body) + (All (_ input term value) + (-> (Pattern input term value) term + (Clause input value))) + (function (_ input exit) + (let [[number match] pattern] + ((match input) (number match.constant body) exit [])))) + +(the .public (or left right) + (All (_ input value) + (-> (Clause input value) (Clause input value) + (Clause input value))) + (function (_ input exit) + (left input + (function (_ _) + (right input exit))))) diff --git a/stdlib/source/library/lux/control/pattern/input.lux b/stdlib/source/library/lux/control/pattern/input.lux new file mode 100644 index 0000000000..68a70b7efc --- /dev/null +++ b/stdlib/source/library/lux/control/pattern/input.lux @@ -0,0 +1,23 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except)]]) + +(every .public Zero + []) + +(the .public zero + (template (_) + [[]])) + +(every .public (One of) + of) + +(every .public (Succ of pred) + (And of pred)) + +(the .public succ + (template (_ of pred) + [[of pred]])) diff --git a/stdlib/source/library/lux/control/pattern/match.lux b/stdlib/source/library/lux/control/pattern/match.lux new file mode 100644 index 0000000000..a61819f5b4 --- /dev/null +++ b/stdlib/source/library/lux/control/pattern/match.lux @@ -0,0 +1,45 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except)]] + [// + ["[0]" input] + ["[0]" output]]) + +(every .public (Match negative positive value) + (-> negative positive + value)) + +(every .public Constant + (All (_ value) + (Match (output.One value) input.Zero + value))) + +(the .public constant + Constant + (function (_ one (input.zero)) + one)) + +(every .public (Natural negative_change positive_change) + (All (_ value negative positive) + (-> (Match negative positive + value) + (Match (negative_change negative) (positive_change positive) + value)))) + +(every .public Zero + (Natural output.One input.One)) + +(the .public zero + Zero + (|>>)) + +(every .public (Succ of) + (Natural (output.Succ of) (input.Succ of))) + +(the .public (succ pred) + Succ + (function (_ negative (input.succ ++ --)) + (pred (negative ++) --))) diff --git a/stdlib/source/library/lux/control/pattern/output.lux b/stdlib/source/library/lux/control/pattern/output.lux new file mode 100644 index 0000000000..b48d314790 --- /dev/null +++ b/stdlib/source/library/lux/control/pattern/output.lux @@ -0,0 +1,14 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except)]]) + +(every .public One + (All (_ of) + of)) + +(every .public (Succ of pred) + (-> of + pred)) diff --git a/stdlib/source/library/lux/control/pattern/pattern.lux b/stdlib/source/library/lux/control/pattern/pattern.lux new file mode 100644 index 0000000000..90aa00f76a --- /dev/null +++ b/stdlib/source/library/lux/control/pattern/pattern.lux @@ -0,0 +1,198 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except Pattern And + nat int rev + or and + is has + left right + false true) + [abstract + [equivalence (.only Equivalence)]] + [control + [pure (.only Pure)] + ["[0]" function (.only) + [predicate (.only Predicate)]]] + [data + ["[0]" bit] + ["[0]" text] + [collection + [list + ["[0]" property]]]] + [math + [number + ["[0]" nat] + ["[0]" int] + ["[0]" rev] + ["[0]" frac]]] + [meta + ["[0]" type]]]] + [// + ["[0]" input] + ["[0]" output] + ["[0]" match] + ["[0]" body (.only Body)]]) + +(every .public (Match input outer inner value) + (-> input + (Body outer inner value))) + +(every .public (Pattern composition input outer inner value) + (Record + [#composition composition + #match (Match input outer inner value)])) + +(the .public (or left right) + (All (_ number input outer inner value) + (type.let [choice (Pattern number input outer inner value)] + (-> choice choice + choice))) + (let [[number left] left + [_ right] right] + [number + (function (_ input) + (body.or (left input) + (right input)))])) + +(with_template [,tag ,side] + [(the .public (,side it) + (All (_ number + outer inner + value + left right) + (-> (Pattern number ,side outer inner value) + (Pattern number (Or left right) outer inner value))) + (let [[number it] it] + [number + (function (_ value) + (when value + {0 ,tag value} + (it value) + + _ + body.failure))]))] + + [#0 left] + [#1 right] + ) + +(the And + (template (_ ,left ,right ,pair) + [(All (_ number_0 number_1 number_2 + arity_0 arity_1 arity_2 + value) + (-> (Pattern (-> number_0 number_1) ,left arity_1 arity_2 value) + (Pattern (-> number_1 number_2) ,right arity_0 arity_1 value) + (Pattern (-> number_0 number_2) ,pair arity_0 arity_2 value)))])) + +(the .public (and left right) + (All (_ input) + (And input input + input)) + (let [[numberL left] left + [numberR right] right] + [(|>> numberL numberR) + (function (_ input) + (body.and (left input) + (right input)))])) + +(the .public (pair left right) + (All (_ left right) + (And left right + (.And left right))) + (let [[numberL leftM] left + [numberR rightM] right] + [(|>> numberL numberR) + (function (_ [leftV rightV]) + (body.and (leftM leftV) + (rightM rightV)))])) + +(the .public (item pattern) + (All (_ of number outer inner value) + (-> (Pattern number of outer inner value) + (Pattern number (List of) outer inner value))) + (let [[number match] pattern] + [number + (function (again input) + (when input + {.#End} + body.failure + + {.#Item head tail} + (body.or (match head) + (function (_ next exit stack) + ((again tail) next exit stack)))))])) + +(every .public (Zero of) + (All (_ value arity) + (Pattern match.Zero of arity (input.One arity) value))) + +(the .public none + Zero + [match.zero + (function.constant body.failure)]) + +(alias [never false] + ..none) + +(the .public any + Zero + [match.zero + (function.constant body.success)]) + +(alias [else true] + ..any) + +(the .public (is predicate) + (All (_ of) + (-> (Predicate of) + (Zero of))) + [match.zero + (function (_ input) + (if (predicate input) + body.success + body.failure))]) + +(the .public (constant = expected) + (All (_ of) + (-> (Equivalence of) of + (Zero of))) + (..is (= expected))) + +(with_template [,type ,name ,equivalence] + [(the .public ,name + (-> ,type + (Zero ,type)) + (..constant ,equivalence))] + + [Bit bit bit.equivalence] + [Nat nat nat.equivalence] + [Int int int.equivalence] + [Rev rev rev.equivalence] + [Frac frac frac.equivalence] + [Text text text.equivalence] + ) + +(every .public (Succ input of) + (All (_ value arity) + (Pattern match.Succ (input of) arity (input.Succ of arity) value))) + +(the .public variable + (Succ Pure) + [match.succ + body.succ]) + +(the .public (has key) + (-> Text + (Succ property.List)) + (..item (..pair (..text key) + ..variable))) + +(the .public (first predicate) + (All (_ of) + (-> (Predicate of) + (Succ List of))) + (..item (..and (..is predicate) + ..variable))) diff --git a/stdlib/source/library/lux/data/bit.lux b/stdlib/source/library/lux/data/bit.lux index 1dc1cd76f4..b8d53b1791 100644 --- a/stdlib/source/library/lux/data/bit.lux +++ b/stdlib/source/library/lux/data/bit.lux @@ -9,8 +9,6 @@ [equivalence (.only Equivalence)] [hash (.only Hash)] [codec (.only Codec)]] - [control - ["[0]" function]] [meta ["[0]" location]]]]) @@ -20,6 +18,10 @@ [no yes] [off on] + + ... https://en.wikipedia.org/wiki/Up_tack + ... https://en.wikipedia.org/wiki/Tee_(symbol) + [falsum verum] ) (the .public equivalence @@ -77,7 +79,3 @@ _ {.#Left ..cannot_decode})))) - -(the .public complement - (All (_ a) (-> (-> a Bit) (-> a Bit))) - (function.composite not)) diff --git a/stdlib/source/library/lux/data/collection/stream.lux b/stdlib/source/library/lux/data/collection/stream.lux index 124b77c601..c35619b256 100644 --- a/stdlib/source/library/lux/data/collection/stream.lux +++ b/stdlib/source/library/lux/data/collection/stream.lux @@ -9,9 +9,10 @@ [comonad (.only CoMonad)]] [control ["//" continuation (.only Cont)] - ["<>" parser]] + ["<>" parser] + [function + ["[0]" predicate]]] [data - ["[0]" bit] [collection ["[0]" list (.use "[1]#[0]" monad)]]] [math @@ -111,7 +112,7 @@ (the .public (partition left? xs) (All (_ a) (-> (-> a Bit) (Stream a) [(Stream a) (Stream a)])) [(..only left? xs) - (..only (bit.complement left?) xs)]) + (..only (predicate.complement left?) xs)]) (the .public functor (Functor Stream) diff --git a/stdlib/source/library/lux/math/random.lux b/stdlib/source/library/lux/math/random.lux index 19671071fd..53917d23b4 100644 --- a/stdlib/source/library/lux/math/random.lux +++ b/stdlib/source/library/lux/math/random.lux @@ -11,8 +11,7 @@ [apply (.only Apply)] ["[0]" monad (.only Monad do)]] [control - ["[0]" state (.only State)] - ["[0]" object (.only Object)]] + ["[0]" state (.only State)]] [data ["[0]" text (.use "[1]#[0]" monoid) [char (.only Char)] @@ -38,7 +37,8 @@ ["[0]" i64]]] [meta [type - [refinement (.only Refiner Refined)]]] + [refinement (.only Refiner Refined)] + ["[0]" object (.only Object object)]]] [world ["[0]" time (.only Time) ["[0]" instant (.only Instant)] @@ -387,7 +387,7 @@ (All (_ seed of) (-> (PRNG seed) seed (Random of seed) [(Object PRNG seed) of])) - (state.value (object.new prng seed) + (state.value (object prng seed) it))) (the .public (prng update return) @@ -401,7 +401,7 @@ [#number (object.method (function (_ next again [this _]) (let [seed (object.state this)] - [(object.new (prng update return) (update seed)) + [(object (prng update return) (update seed)) (return seed)])))])) (every .public PCG_32 diff --git a/stdlib/source/library/lux/control/object.lux b/stdlib/source/library/lux/meta/type/object.lux similarity index 97% rename from stdlib/source/library/lux/control/object.lux rename to stdlib/source/library/lux/meta/type/object.lux index 0dc2a58ae5..5f3cfeac8e 100644 --- a/stdlib/source/library/lux/control/object.lux +++ b/stdlib/source/library/lux/meta/type/object.lux @@ -33,7 +33,7 @@ [#class (interface state) #state state]) - (the .public (new class state) + (the .public (object class state) (All (_ interface state) (-> (interface state) state (Instance interface state))) @@ -140,7 +140,7 @@ (the .public (as class object) (All (_ interface state) (-> (interface state) (Object interface Any) - (Maybe state))) + (Maybe (Object interface state)))) (if (same? class (..class object)) - {.#Some (as_expected (..state object))} + {.#Some (as_expected object)} {.#None}))) diff --git a/stdlib/source/parser/lux/data/collection/list.lux b/stdlib/source/parser/lux/data/collection/list.lux index 88bc755bb1..ca3a015287 100644 --- a/stdlib/source/parser/lux/data/collection/list.lux +++ b/stdlib/source/parser/lux/data/collection/list.lux @@ -4,6 +4,8 @@ (.require [library [lux (.except) + [abstract + [monad (.only do)]] [control ["//" parser] ["[0]" try (.only Try)] @@ -19,20 +21,27 @@ (exception.the .public empty) -(the .public (one it) +(the .public any (All (_ of) - (-> (Predicate of) - (Parser of of))) + (Parser of of)) (function (_ state) (when state (/.partial head tail) - (if (it head) - {try.#Success [tail head]} - (exception.except ..invalid [])) + {try.#Success [tail head]} (list) (exception.except ..empty [])))) +(the .public (one it) + (All (_ of) + (-> (Predicate of) + (Parser of of))) + (do //.monad + [head ..any] + (if (it head) + (in head) + (//.of_try (exception.except ..invalid []))))) + (exception.the .public left_over) (the .public (value it input) diff --git a/stdlib/source/parser/lux/meta/type/object.lux b/stdlib/source/parser/lux/meta/type/object.lux new file mode 100644 index 0000000000..3e7c03b115 --- /dev/null +++ b/stdlib/source/parser/lux/meta/type/object.lux @@ -0,0 +1,42 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except) + [abstract + [monad (.only do)]] + [control + [try (.only Try)] + ["//" parser] + ["[0]" exception]]]] + [\\library + ["[0]" /]] + [//// + [data + [collection + ["[0]" list]]]]) + +(every .public (Parser interface) + (list.Parser (/.Object interface))) + +(exception.the .public wrong_class) + +(the .public (any class) + (All (_ interface state) + (-> (interface state) + (Parser interface (/.Object interface state)))) + (do //.monad + [it list.any] + (when (/.as class it) + {.#Some it} + (in it) + + {.#None} + (//.of_try (exception.except ..wrong_class []))))) + +(the .public value + (All (_ interface of) + (-> (Parser interface of) (List (/.Object interface)) + (Try of))) + list.value) diff --git a/stdlib/source/test/lux/control.lux b/stdlib/source/test/lux/control.lux index 411de1088f..53a2fca6aa 100644 --- a/stdlib/source/test/lux/control.lux +++ b/stdlib/source/test/lux/control.lux @@ -40,10 +40,10 @@ ["[1][0]" thread] ["[1][0]" try] ["[1][0]" writer] - ["[1][0]" object] ["[1][0]" condition] ["[1][0]" pure] - ["[1][0]" logic]]) + ["[1][0]" logic] + ["[1][0]" pattern]]) (the concurrency Test @@ -91,8 +91,8 @@ /thread.test /try.test /writer.test - /object.test /condition.test /pure.test /logic.test + /pattern.test )) diff --git a/stdlib/source/test/lux/control/pattern.lux b/stdlib/source/test/lux/control/pattern.lux new file mode 100644 index 0000000000..4a8a4f2835 --- /dev/null +++ b/stdlib/source/test/lux/control/pattern.lux @@ -0,0 +1,81 @@ +... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/. + +(.require + [library + [lux (.except) + [abstract + [monad (.only do)]] + [math + ["[0]" random (.only Random)] + [number + ["[0]" int]]] + [test + ["_" property (.only Test)]]]] + [\\library + ["[0]" / (.only) + ["[0]" input] + ["[0]" output] + ["[0]" match] + ["[0]" body] + ["[0]" pattern] + ["[0]" clause]]]) + +(the .public test + Test + (<| (_.covering /._) + (do [! random.monad] + [expected_bit random.bit + expected_nat random.nat + expected_int random.int + other_int (random.only (|>> (int.= expected_int) not) + random.int)]) + (all _.and + (_.coverage [pattern.item] + (let [clause (all clause.or + (clause.clause (pattern.item (pattern.is (same? expected_int))) + true) + (clause.clause pattern.any + false))] + (and (/.when (list expected_int other_int) clause) + (/.when (list other_int expected_int) clause) + (not (/.when (list other_int other_int) clause))))) + (_.for [pattern.Zero] + (all _.and + (_.coverage [pattern.any] + (<| (/.when expected_int) + (clause.clause pattern.any true))) + (_.coverage [pattern.none] + (not (<| (/.when expected_int) + (all clause.or + (clause.clause pattern.none true) + (clause.clause pattern.any false))))) + (_.coverage [pattern.is] + (<| (/.when expected_int) + (all clause.or + (clause.clause (pattern.is (same? expected_int)) true) + (clause.clause pattern.any false)))) + )) + (_.for [pattern.Succ] + (all _.and + (_.coverage [pattern.variable] + (<| (/.when expected_int) + (clause.clause pattern.variable + (same? expected_int)))) + (_.coverage [pattern.first] + (let [clause (all clause.or + (clause.clause (pattern.first (same? expected_int)) + (same? expected_int)) + (clause.clause pattern.any + false))] + (and (/.when (list expected_int other_int) clause) + (/.when (list other_int expected_int) clause) + (not (/.when (list other_int other_int) clause))))) + )) + (_.coverage [/.when] + (<| (/.when [other_int expected_int]) + (clause.clause (all pattern.or + (pattern.pair (pattern.int other_int) pattern.variable) + (pattern.pair pattern.variable (pattern.int other_int))) + (same? expected_int)))) + ))) diff --git a/stdlib/source/test/lux/data/bit.lux b/stdlib/source/test/lux/data/bit.lux index 91a4d15c05..1bf07d1d89 100644 --- a/stdlib/source/test/lux/data/bit.lux +++ b/stdlib/source/test/lux/data/bit.lux @@ -46,7 +46,7 @@ (_.coverage [/.off /.on] (and (of /.equivalence = false /.off) (of /.equivalence = true /.on))) - (_.coverage [/.complement] - (and (not (of /.equivalence = value ((/.complement function.identity) value))) - (of /.equivalence = value ((/.complement not) value)))) + (_.coverage [/.falsum /.verum] + (and (of /.equivalence = false /.falsum) + (of /.equivalence = true /.verum))) )))) diff --git a/stdlib/source/test/lux/data/collection/list.lux b/stdlib/source/test/lux/data/collection/list.lux index 27abbc0e5a..3fe572f012 100644 --- a/stdlib/source/test/lux/data/collection/list.lux +++ b/stdlib/source/test/lux/data/collection/list.lux @@ -23,9 +23,10 @@ [control ["[0]" pipe] ["[0]" io] - ["[0]" function] ["[0]" try] - ["[0]" exception]] + ["[0]" exception] + ["[0]" function (.only) + ["[0]" predicate]]] [data ["[0]" bit] ["[0]" product] @@ -123,8 +124,8 @@ self_symmetry!)))) (_.coverage [/.every? /.any?] (if (/.every? n.even? sample) - (not (/.any? (bit.complement n.even?) sample)) - (/.any? (bit.complement n.even?) sample))) + (not (/.any? (predicate.complement n.even?) sample)) + (/.any? (predicate.complement n.even?) sample))) (_.coverage [/.sorted] (let [<<< n.< @@ -212,7 +213,7 @@ (all _.and (_.coverage [/.only] (let [positives (/.only n.even? sample) - negatives (/.only (bit.complement n.even?) sample)] + negatives (/.only (predicate.complement n.even?) sample)] (and (/.every? n.even? positives) (not (/.any? n.even? negatives)) @@ -223,7 +224,7 @@ (let [[positives negatives] (/.partition n.even? sample)] (and (/#= (/.only n.even? sample) positives) - (/#= (/.only (bit.complement n.even?) sample) + (/#= (/.only (predicate.complement n.even?) sample) negatives)))) (_.coverage [/.split_at] (let [[left right] (/.split_at idx sample)] diff --git a/stdlib/source/test/lux/data/collection/sequence.lux b/stdlib/source/test/lux/data/collection/sequence.lux index 002fb59a79..14c60cbd27 100644 --- a/stdlib/source/test/lux/data/collection/sequence.lux +++ b/stdlib/source/test/lux/data/collection/sequence.lux @@ -19,7 +19,9 @@ ["[1]T" \\test]]] [control ["[0]" try (.only Try)] - ["[0]" exception]] + ["[0]" exception] + [function + ["[0]" predicate]]] [data ["[0]" bit (.use "[1]#[0]" equivalence)] ["[0]" text (.use "[1]#[0]" equivalence)] @@ -83,8 +85,8 @@ self_symmetry!)))) (_.coverage [/.every? /.any?] (if (/.every? n.even? sample) - (not (/.any? (bit.complement n.even?) sample)) - (/.any? (bit.complement n.even?) sample))) + (not (/.any? (predicate.complement n.even?) sample)) + (/.any? (predicate.complement n.even?) sample))) ))) (the index_based @@ -195,7 +197,7 @@ symmetry!)))) (_.coverage [/.only] (let [positives (/.only n.even? sample) - negatives (/.only (bit.complement n.even?) sample)] + negatives (/.only (predicate.complement n.even?) sample)] (and (/.every? n.even? positives) (not (/.any? n.even? negatives)) diff --git a/stdlib/source/test/lux/meta/type.lux b/stdlib/source/test/lux/meta/type.lux index 5363cbca7a..91a309f48b 100644 --- a/stdlib/source/test/lux/meta/type.lux +++ b/stdlib/source/test/lux/meta/type.lux @@ -48,7 +48,8 @@ ["[1][0]" variance] ["[1][0]" poly] ["[1][0]" row] - ["[1][0]" brand]]) + ["[1][0]" brand] + ["[1][0]" object]]) (the !expect (template (_ ) @@ -675,4 +676,5 @@ /poly.test /row.test /brand.test + /object.test ))) diff --git a/stdlib/source/test/lux/control/object.lux b/stdlib/source/test/lux/meta/type/object.lux similarity index 56% rename from stdlib/source/test/lux/control/object.lux rename to stdlib/source/test/lux/meta/type/object.lux index e7ed0540a4..6419284dba 100644 --- a/stdlib/source/test/lux/control/object.lux +++ b/stdlib/source/test/lux/meta/type/object.lux @@ -6,6 +6,10 @@ [lux (.except) [abstract [monad (.only do)]] + [control + ["[0]" parser] + ["[0]" try] + ["[0]" exception]] [math ["[0]" random (.only Random)] [number @@ -16,7 +20,8 @@ [test ["_" property (.only Test)]]]] [\\library - ["[0]" /]]) + ["[0]" /]] + ["[0]" \\parser]) (/.every (Shape [] _) [#perimeter (/.Method [] Frac) @@ -64,33 +69,67 @@ scalar scalar (next [this input])))))) +(the value + (Random Frac) + (of random.functor each + (|>> (n.% 100) n.frac) + random.nat)) + +(the \\parser + Test + (<| (_.covering \\parser._) + (_.for [\\parser.Parser]) + (do [! random.monad] + [radius ..value + side ..value]) + (all _.and + (_.coverage [\\parser.any \\parser.value] + (when (\\parser.value (is (\\parser.Parser Shape Frac) + (do parser.monad + [it (\\parser.any ..circle)] + (in (/.state it)))) + (list (/.object ..circle [#radius radius]))) + {try.#Success actual} + (same? radius actual) + + {try.#Failure _} + false)) + (_.coverage [\\parser.wrong_class] + (when (\\parser.value (is (\\parser.Parser Shape Frac) + (do parser.monad + [it (\\parser.any ..circle)] + (in (/.state it)))) + (list (/.object ..square [#side side]))) + {try.#Failure error} + (exception.is? \\parser.wrong_class error) + + {try.#Success _} + false)) + ))) + (the .public test Test (<| (_.covering /._) (do [! random.monad] - [.let [value (is (Random Frac) - (of ! each - (|>> (n.% 100) n.frac) - random.nat))] - radius value - side value - scale value]) + [radius ..value + side ..value + scale ..value]) (_.for [/.Instance /.Object]) (all _.and - (_.coverage [/.new /.class] + (_.coverage [/.object /.class] (|> [#side side] - (/.new ..square) + (/.object ..square) (is (/.Object Shape Square)) /.class (same? ..square))) (_.coverage [/.state] (and (|> [#side side] - (/.new ..square) + (/.object ..square) (is (/.Object Shape Square)) /.state (same? side)) (|> [#radius radius] - (/.new ..circle) + (/.object ..circle) (is (/.Object Shape Circle)) /.state (same? radius)))) @@ -99,12 +138,14 @@ /.method /.on] (let [it (is (/.Object Shape Circle) - (/.new circle [#radius radius]))] + (/.object circle [#radius radius]))] (not (f.= (/.on #perimeter [] it) (/.on #area [] it))))) (_.coverage [/.override] - (and (f.= (/.on #perimeter [] (/.new ..square [#radius (f.* scale radius)])) - (/.on #perimeter [] (/.new (..scaled scale ..square) [#radius radius]))) - (f.= (/.on #area [] (/.new ..square [#radius (f.* scale radius)])) - (/.on #area [] (/.new (..scaled scale ..square) [#radius radius]))))) + (and (f.= (/.on #perimeter [] (/.object ..square [#radius (f.* scale radius)])) + (/.on #perimeter [] (/.object (..scaled scale ..square) [#radius radius]))) + (f.= (/.on #area [] (/.object ..square [#radius (f.* scale radius)])) + (/.on #area [] (/.object (..scaled scale ..square) [#radius radius]))))) + + ..\\parser ))) diff --git a/to_do.md b/to_do.md new file mode 100644 index 0000000000..84f2d4451f --- /dev/null +++ b/to_do.md @@ -0,0 +1,21 @@ +# References + +0. [Basic writing and formatting syntax](https://docs.github.com/en/get-started/writing-on-github/getting-started-with-writing-and-formatting-on-github/basic-writing-and-formatting-syntax) + +# Tasks + +## To Do + +0. Implement type-level naming ("Ghosts of Dependent Proofs"-style), in order to give unique names to classes, to force distinctions between them beyond their state types. +0. An anonymous type for un-tagged sums. E.g. `{3 #1 x}` = `(All (_ a b c d) (Or a b c (Or d (type_of x))))` && `{3 #0 x}` = `(All (_ a b c d) (Or a b c (Or (type_of x) d)))` +0. Re-name Codec#format to "injection" and Codec#value to "projection". +0. Re-name "Codec" to "Embedding". + * [Embedding](https://en.wikipedia.org/wiki/Embedding) +0. Implement polytypic counting/length via induction. +0. Re-implement all the current polytypic code just using induction. +0. Re-name Format to Injection. +0. Re-name Parser to Projection. +0. <- as reverse-order function syntax. + +## Done +