From a8d76e48df01d0f5326faa8456797f91cb2cbeba Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 30 Jun 2022 22:53:23 -0400 Subject: Alternative names for (un)quoting macros. --- stdlib/source/library/lux.lux | 52 +- .../source/library/lux/control/concatenative.lux | 6 +- .../library/lux/control/concurrency/actor.lux | 5 +- .../library/lux/control/concurrency/async.lux | 7 +- .../library/lux/control/concurrency/atom.lux | 7 +- .../source/library/lux/control/concurrency/frp.lux | 5 +- .../library/lux/control/concurrency/semaphore.lux | 7 +- .../source/library/lux/control/concurrency/stm.lux | 7 +- .../source/library/lux/control/function/memo.lux | 5 +- stdlib/source/library/lux/control/io.lux | 7 +- stdlib/source/library/lux/control/lazy.lux | 5 +- .../library/lux/control/security/capability.lux | 5 +- .../source/library/lux/control/security/policy.lux | 5 +- stdlib/source/library/lux/control/thread.lux | 7 +- .../source/library/lux/data/collection/array.lux | 5 +- .../library/lux/data/collection/queue/priority.lux | 5 +- .../library/lux/data/collection/set/multi.lux | 5 +- .../library/lux/data/collection/set/ordered.lux | 5 +- .../source/library/lux/data/collection/stack.lux | 5 +- .../library/lux/data/collection/tree/finger.lux | 5 +- stdlib/source/library/lux/data/color.lux | 5 +- stdlib/source/library/lux/data/format/css.lux | 5 +- .../source/library/lux/data/format/css/class.lux | 5 +- stdlib/source/library/lux/data/format/css/id.lux | 5 +- .../library/lux/data/format/css/property.lux | 9 +- .../source/library/lux/data/format/css/query.lux | 5 +- .../library/lux/data/format/css/selector.lux | 7 +- .../source/library/lux/data/format/css/style.lux | 5 +- .../source/library/lux/data/format/css/value.lux | 5 +- stdlib/source/library/lux/data/format/html.lux | 5 +- stdlib/source/library/lux/data/format/markdown.lux | 7 +- stdlib/source/library/lux/data/format/tar.lux | 5 +- stdlib/source/library/lux/data/text/buffer.lux | 5 +- stdlib/source/library/lux/data/text/encoding.lux | 5 +- .../source/library/lux/data/text/unicode/block.lux | 5 +- .../source/library/lux/data/text/unicode/set.lux | 5 +- stdlib/source/library/lux/data/trace.lux | 3 +- stdlib/source/library/lux/debug.lux | 5 +- stdlib/source/library/lux/documentation.lux | 4 +- stdlib/source/library/lux/ffi.jvm.lux | 5 +- stdlib/source/library/lux/ffi.lux | 5 +- stdlib/source/library/lux/ffi.old.lux | 4 +- stdlib/source/library/lux/ffi.php.lux | 8 +- stdlib/source/library/lux/ffi.scm.lux | 8 +- stdlib/source/library/lux/locale.lux | 5 +- stdlib/source/library/lux/locale/language.lux | 7 +- stdlib/source/library/lux/locale/territory.lux | 7 +- stdlib/source/library/lux/math.lux | 5 +- stdlib/source/library/lux/math/modular.lux | 5 +- stdlib/source/library/lux/math/modulus.lux | 5 +- stdlib/source/library/lux/math/number/i16.lux | 3 +- stdlib/source/library/lux/math/number/i32.lux | 5 +- stdlib/source/library/lux/math/number/i8.lux | 5 +- stdlib/source/library/lux/math/random.lux | 5 +- stdlib/source/library/lux/meta/type.lux | 515 +++++++++++++ stdlib/source/library/lux/meta/type/check.lux | 829 +++++++++++++++++++++ stdlib/source/library/lux/meta/type/dynamic.lux | 56 ++ stdlib/source/library/lux/meta/type/implicit.lux | 400 ++++++++++ stdlib/source/library/lux/meta/type/poly.lux | 89 +++ stdlib/source/library/lux/meta/type/primitive.lux | 105 +++ stdlib/source/library/lux/meta/type/quotient.lux | 69 ++ stdlib/source/library/lux/meta/type/refinement.lux | 105 +++ stdlib/source/library/lux/meta/type/resource.lux | 188 +++++ stdlib/source/library/lux/meta/type/unit.lux | 103 +++ stdlib/source/library/lux/meta/type/unit/scale.lux | 78 ++ stdlib/source/library/lux/meta/type/variance.lux | 45 ++ stdlib/source/library/lux/target/common_lisp.lux | 5 +- stdlib/source/library/lux/target/js.lux | 5 +- .../library/lux/target/jvm/bytecode/address.lux | 5 +- .../jvm/bytecode/environment/limit/registry.lux | 5 +- .../jvm/bytecode/environment/limit/stack.lux | 5 +- .../lux/target/jvm/bytecode/instruction.lux | 5 +- stdlib/source/library/lux/target/jvm/constant.lux | 5 +- .../source/library/lux/target/jvm/constant/tag.lux | 5 +- .../library/lux/target/jvm/encoding/name.lux | 5 +- .../library/lux/target/jvm/encoding/signed.lux | 5 +- .../library/lux/target/jvm/encoding/unsigned.lux | 5 +- stdlib/source/library/lux/target/jvm/index.lux | 5 +- stdlib/source/library/lux/target/jvm/modifier.lux | 5 +- .../library/lux/target/jvm/modifier/inner.lux | 5 +- stdlib/source/library/lux/target/jvm/type.lux | 5 +- .../library/lux/target/jvm/type/category.lux | 5 +- .../library/lux/target/jvm/type/descriptor.lux | 5 +- stdlib/source/library/lux/target/jvm/type/lux.lux | 7 +- .../library/lux/target/jvm/type/reflection.lux | 5 +- .../library/lux/target/jvm/type/signature.lux | 5 +- stdlib/source/library/lux/target/lua.lux | 5 +- stdlib/source/library/lux/target/php.lux | 5 +- stdlib/source/library/lux/target/python.lux | 5 +- stdlib/source/library/lux/target/r.lux | 5 +- stdlib/source/library/lux/target/ruby.lux | 5 +- stdlib/source/library/lux/target/scheme.lux | 5 +- stdlib/source/library/lux/time.lux | 5 +- stdlib/source/library/lux/time/date.lux | 5 +- stdlib/source/library/lux/time/duration.lux | 5 +- stdlib/source/library/lux/time/instant.lux | 5 +- stdlib/source/library/lux/time/year.lux | 5 +- .../library/lux/tool/compiler/default/platform.lux | 6 +- .../compiler/language/lux/analysis/evaluation.lux | 6 +- .../compiler/language/lux/analysis/inference.lux | 5 +- .../tool/compiler/language/lux/analysis/type.lux | 5 +- .../compiler/language/lux/phase/analysis/case.lux | 6 +- .../language/lux/phase/analysis/complex.lux | 9 +- .../language/lux/phase/analysis/function.lux | 6 +- .../language/lux/phase/extension/analysis/js.lux | 5 +- .../language/lux/phase/extension/analysis/jvm.lux | 6 +- .../language/lux/phase/extension/analysis/lua.lux | 5 +- .../language/lux/phase/extension/analysis/lux.lux | 5 +- .../language/lux/phase/extension/analysis/php.lux | 5 +- .../lux/phase/extension/analysis/python.lux | 5 +- .../language/lux/phase/extension/analysis/r.lux | 5 +- .../language/lux/phase/extension/analysis/ruby.lux | 5 +- .../lux/phase/extension/analysis/scheme.lux | 5 +- .../library/lux/tool/compiler/meta/archive.lux | 5 +- .../library/lux/tool/compiler/meta/archive/key.lux | 5 +- .../tool/compiler/meta/archive/module/document.lux | 5 +- .../lux/tool/compiler/meta/archive/registry.lux | 5 +- stdlib/source/library/lux/type.lux | 515 ------------- stdlib/source/library/lux/type/check.lux | 829 --------------------- stdlib/source/library/lux/type/dynamic.lux | 56 -- stdlib/source/library/lux/type/implicit.lux | 400 ---------- stdlib/source/library/lux/type/poly.lux | 89 --- stdlib/source/library/lux/type/primitive.lux | 105 --- stdlib/source/library/lux/type/quotient.lux | 69 -- stdlib/source/library/lux/type/refinement.lux | 105 --- stdlib/source/library/lux/type/resource.lux | 188 ----- stdlib/source/library/lux/type/unit.lux | 103 --- stdlib/source/library/lux/type/unit/scale.lux | 78 -- stdlib/source/library/lux/type/variance.lux | 45 -- stdlib/source/library/lux/world/file/watch.lux | 17 +- 130 files changed, 2947 insertions(+), 2842 deletions(-) create mode 100644 stdlib/source/library/lux/meta/type.lux create mode 100644 stdlib/source/library/lux/meta/type/check.lux create mode 100644 stdlib/source/library/lux/meta/type/dynamic.lux create mode 100644 stdlib/source/library/lux/meta/type/implicit.lux create mode 100644 stdlib/source/library/lux/meta/type/poly.lux create mode 100644 stdlib/source/library/lux/meta/type/primitive.lux create mode 100644 stdlib/source/library/lux/meta/type/quotient.lux create mode 100644 stdlib/source/library/lux/meta/type/refinement.lux create mode 100644 stdlib/source/library/lux/meta/type/resource.lux create mode 100644 stdlib/source/library/lux/meta/type/unit.lux create mode 100644 stdlib/source/library/lux/meta/type/unit/scale.lux create mode 100644 stdlib/source/library/lux/meta/type/variance.lux delete mode 100644 stdlib/source/library/lux/type.lux delete mode 100644 stdlib/source/library/lux/type/check.lux delete mode 100644 stdlib/source/library/lux/type/dynamic.lux delete mode 100644 stdlib/source/library/lux/type/implicit.lux delete mode 100644 stdlib/source/library/lux/type/poly.lux delete mode 100644 stdlib/source/library/lux/type/primitive.lux delete mode 100644 stdlib/source/library/lux/type/quotient.lux delete mode 100644 stdlib/source/library/lux/type/refinement.lux delete mode 100644 stdlib/source/library/lux/type/resource.lux delete mode 100644 stdlib/source/library/lux/type/unit.lux delete mode 100644 stdlib/source/library/lux/type/unit/scale.lux delete mode 100644 stdlib/source/library/lux/type/variance.lux (limited to 'stdlib/source/library') diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux index 439fb69e3..d142387b3 100644 --- a/stdlib/source/library/lux.lux +++ b/stdlib/source/library/lux.lux @@ -1326,9 +1326,9 @@ (p x))} xs)) -(def' .private (with_location location content) - (-> Location Code Code) - (let' [[module line column] location] +(def' .private (with_location content) + (-> Code Code) + (let' [[module line column] ..dummy_location] (tuple$ (list (tuple$ (list (text$ module) (nat$ line) (nat$ column))) content)))) @@ -1587,9 +1587,9 @@ (symbol$ [..prelude "List"])))] (form$ (list (text$ "lux type check") type expression)))) -(def' .private (untemplated_text location value) - (-> Location Text Code) - (with_location location (variant$ (list (symbol$ [..prelude "#Text"]) (text$ value))))) +(def' .private (untemplated_text value) + (-> Text Code) + (with_location (variant$ (list (symbol$ [..prelude "#Text"]) (text$ value))))) (def' .public UnQuote Type @@ -1902,7 +1902,7 @@ (do meta#monad [=elements (monad#each meta#monad (untemplated replace? subst) elements)] (in (untemplated_list =elements)))) - .let' [[_ output'] (with_location @composite (variant$ (list (symbol$ [..prelude tag]) output)))]] + .let' [[_ output'] (with_location (variant$ (list (symbol$ [..prelude tag]) output)))]] (in [@composite output']))) (def' .private untemplated_form @@ -1923,22 +1923,22 @@ (def' .private (untemplated replace? subst token) (-> Bit Text Code ($' Meta Code)) ({[_ [@token {#Bit value}]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Bit"]) (bit$ value))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Bit"]) (bit$ value))))) [_ [@token {#Nat value}]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Nat"]) (nat$ value))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Nat"]) (nat$ value))))) [_ [@token {#Int value}]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Int"]) (int$ value))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Int"]) (int$ value))))) [_ [@token {#Rev value}]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Rev"]) (rev$ value))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Rev"]) (rev$ value))))) [_ [@token {#Frac value}]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Frac"]) (frac$ value))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Frac"]) (frac$ value))))) [_ [@token {#Text value}]] - (meta#in (untemplated_text @token value)) + (meta#in (untemplated_text value)) [#1 [@token {#Symbol [module name]}]] (do meta#monad @@ -1951,10 +1951,10 @@ (in [module name])} module) .let' [[module name] real_name]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Symbol"]) (tuple$ (list (text$ module) (text$ name)))))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Symbol"]) (tuple$ (list (text$ module) (text$ name)))))))) [#0 [@token {#Symbol [module name]}]] - (meta#in (with_location @token (variant$ (list (symbol$ [..prelude "#Symbol"]) (tuple$ (list (text$ module) (text$ name))))))) + (meta#in (with_location (variant$ (list (symbol$ [..prelude "#Symbol"]) (tuple$ (list (text$ module) (text$ name))))))) [#1 [@composite {#Form {#Item [@symbol {#Symbol global}] parameters}}]] (do meta#monad @@ -2011,6 +2011,8 @@ (failure (wrong_syntax_error [..prelude "`"]))} tokens))) +(def' .public syntax_quote Macro `) + (def' .public `' Macro (macro (_ tokens) @@ -2023,6 +2025,8 @@ (failure (wrong_syntax_error [..prelude "`'"]))} tokens))) +(def' .public partial_quote Macro `') + (def' .public ' Macro (macro (_ tokens) @@ -2035,6 +2039,8 @@ (failure (wrong_syntax_error [..prelude "'"]))} tokens))) +(def' .public literal_quote Macro ') + (def' .public ~ UnQuote (..unquote @@ -2048,6 +2054,8 @@ (failure (wrong_syntax_error [..prelude "~"]))} tokens)))) +(def' .public but UnQuote ~) + (def' .public ~! UnQuote (..unquote @@ -2056,15 +2064,17 @@ (do meta#monad [current_module ..current_module_name independent (untemplated #1 current_module [@token dependent])] - (in (list (with_location @token (variant$ (list (symbol$ [..prelude "#Form"]) - (untemplated_list (list (untemplated_text dummy_location "lux in-module") - (untemplated_text dummy_location current_module) - independent)))))))) + (in (list (with_location (variant$ (list (symbol$ [..prelude "#Form"]) + (untemplated_list (list (untemplated_text "lux in-module") + (untemplated_text current_module) + independent)))))))) _ (failure (wrong_syntax_error [..prelude "~!"]))} tokens)))) +(def' .public specifically UnQuote ~!) + (def' .public ~' UnQuote (..unquote @@ -2079,6 +2089,8 @@ (failure (wrong_syntax_error [..prelude "~'"]))} tokens)))) +(def' .public literally UnQuote ~') + (def' .public ~+ Spliced_UnQuote (let' [g!list#composite (form$ (list (text$ "lux in-module") @@ -2093,6 +2105,8 @@ (failure (wrong_syntax_error [..prelude "~+"]))} tokens))))) +(def' .public also Spliced_UnQuote ~+) + (def' .public |> Macro (macro (_ tokens) diff --git a/stdlib/source/library/lux/control/concatenative.lux b/stdlib/source/library/lux/control/concatenative.lux index 4e900a860..3a24dedfc 100644 --- a/stdlib/source/library/lux/control/concatenative.lux +++ b/stdlib/source/library/lux/control/concatenative.lux @@ -1,8 +1,6 @@ (.require [library [lux (.except Alias if loop left right) - ["[0]" meta] - ["[0]" type] [abstract ["[0]" monad]] [control @@ -23,7 +21,9 @@ ["n" nat] ["i" int] ["r" rev] - ["f" frac]]]]] + ["f" frac]]] + ["[0]" meta (.only) + ["[0]" type]]]] [// ["<>" parser (.use "[1]#[0]" monad)]]) diff --git a/stdlib/source/library/lux/control/concurrency/actor.lux b/stdlib/source/library/lux/control/concurrency/actor.lux index ce8daea6a..f6141f32d 100644 --- a/stdlib/source/library/lux/control/concurrency/actor.lux +++ b/stdlib/source/library/lux/control/concurrency/actor.lux @@ -13,8 +13,9 @@ ["[0]" product]] [macro ["[0]" local]] - [type (.only sharing) - [primitive (.only primitive representation abstraction)]]]] + [meta + [type (.only sharing) + [primitive (.only primitive representation abstraction)]]]]] [// ["[0]" atom (.only Atom atom)] ["[0]" async (.only Async Resolver)] diff --git a/stdlib/source/library/lux/control/concurrency/async.lux b/stdlib/source/library/lux/control/concurrency/async.lux index 40b2760b0..0098f0f1b 100644 --- a/stdlib/source/library/lux/control/concurrency/async.lux +++ b/stdlib/source/library/lux/control/concurrency/async.lux @@ -14,9 +14,10 @@ ["[0]" product]] [macro ["^" pattern]] - [type (.only sharing) - [primitive (.except)] - ["[0]" variance (.only Mutable)]]]] + [meta + [type (.only sharing) + [primitive (.except)] + ["[0]" variance (.only Mutable)]]]]] [// ["[0]" thread] ["[0]" atom (.only Atom atom)]]) diff --git a/stdlib/source/library/lux/control/concurrency/atom.lux b/stdlib/source/library/lux/control/concurrency/atom.lux index 65a981c44..3c81d2841 100644 --- a/stdlib/source/library/lux/control/concurrency/atom.lux +++ b/stdlib/source/library/lux/control/concurrency/atom.lux @@ -13,9 +13,10 @@ [collection ["[0]" array ["[1]" \\unsafe]]]] - [type - [primitive (.except)] - ["[0]" variance (.only Mutable)]]]]) + [meta + [type + [primitive (.except)] + ["[0]" variance (.only Mutable)]]]]]) (with_expansions [ (these (ffi.import (java/util/concurrent/atomic/AtomicReference a) "[1]::[0]" diff --git a/stdlib/source/library/lux/control/concurrency/frp.lux b/stdlib/source/library/lux/control/concurrency/frp.lux index 3cf496cf1..1311d9b3d 100644 --- a/stdlib/source/library/lux/control/concurrency/frp.lux +++ b/stdlib/source/library/lux/control/concurrency/frp.lux @@ -11,8 +11,9 @@ ["[0]" try (.only Try)] ["[0]" exception (.only exception)] ["[0]" io (.only IO io)]] - [type (.only sharing) - ["[0]" variance (.only Mutable)]]]] + [meta + [type (.only sharing) + ["[0]" variance (.only Mutable)]]]]] [// ["[0]" atom (.only Atom)] ["[0]" async (.only Async Async') (.use "[1]#[0]" monad)]]) diff --git a/stdlib/source/library/lux/control/concurrency/semaphore.lux b/stdlib/source/library/lux/control/concurrency/semaphore.lux index db74c0728..2b6b0692f 100644 --- a/stdlib/source/library/lux/control/concurrency/semaphore.lux +++ b/stdlib/source/library/lux/control/concurrency/semaphore.lux @@ -17,9 +17,10 @@ [number ["n" nat] ["i" int]]] - [type - ["[0]" primitive (.except)] - ["[0]" refinement]]]] + [meta + [type + ["[0]" primitive (.except)] + ["[0]" refinement]]]]] [// ["[0]" atom (.only Atom)] ["[0]" async (.only Async Resolver)]]) diff --git a/stdlib/source/library/lux/control/concurrency/stm.lux b/stdlib/source/library/lux/control/concurrency/stm.lux index 3dfeeec5c..3beedf568 100644 --- a/stdlib/source/library/lux/control/concurrency/stm.lux +++ b/stdlib/source/library/lux/control/concurrency/stm.lux @@ -15,9 +15,10 @@ ["[0]" list]]] [macro ["^" pattern]] - [type (.only sharing) - [primitive (.except)] - ["[0]" variance (.only Mutable)]]]] + [meta + [type (.only sharing) + [primitive (.except)] + ["[0]" variance (.only Mutable)]]]]] [// ["[0]" atom (.only Atom atom)] ["[0]" async (.only Async Resolver)] diff --git a/stdlib/source/library/lux/control/function/memo.lux b/stdlib/source/library/lux/control/function/memo.lux index f39cb33e3..3328720e2 100644 --- a/stdlib/source/library/lux/control/function/memo.lux +++ b/stdlib/source/library/lux/control/function/memo.lux @@ -4,7 +4,6 @@ (.require [library [lux (.except open) - ["[0]" type] [abstract [hash (.only Hash)] [monad (.only do)]] @@ -13,7 +12,9 @@ [data ["[0]" product] [collection - ["[0]" dictionary (.only Dictionary)]]]]] + ["[0]" dictionary (.only Dictionary)]]] + [meta + ["[0]" type]]]] ["[0]" // ["[1]" mixin (.only Mixin Recursive)]]) diff --git a/stdlib/source/library/lux/control/io.lux b/stdlib/source/library/lux/control/io.lux index 609814844..13eda4b75 100644 --- a/stdlib/source/library/lux/control/io.lux +++ b/stdlib/source/library/lux/control/io.lux @@ -5,13 +5,14 @@ [functor (.only Functor)] [apply (.only Apply)] [monad (.only Monad do)]] - [type - [primitive (.except)]] [macro (.only with_symbols) [syntax (.only syntax)] ["[0]" template] ["[0]" code - ["<[1]>" \\parser]]]]]) + ["<[1]>" \\parser]]] + [meta + [type + [primitive (.except)]]]]]) (primitive .public (IO a) (-> Any a) diff --git a/stdlib/source/library/lux/control/lazy.lux b/stdlib/source/library/lux/control/lazy.lux index b20711ba7..d2bf0531f 100644 --- a/stdlib/source/library/lux/control/lazy.lux +++ b/stdlib/source/library/lux/control/lazy.lux @@ -14,8 +14,9 @@ [syntax (.only syntax)] ["[0]" code ["<[1]>" \\parser]]] - [type (.only sharing) - [primitive (.except)]]]]) + [meta + [type (.only sharing) + [primitive (.except)]]]]]) (primitive .public (Lazy a) (-> [] a) diff --git a/stdlib/source/library/lux/control/security/capability.lux b/stdlib/source/library/lux/control/security/capability.lux index 96813f726..90a503c3a 100644 --- a/stdlib/source/library/lux/control/security/capability.lux +++ b/stdlib/source/library/lux/control/security/capability.lux @@ -13,8 +13,9 @@ ["%" \\format (.only format)]] [collection ["[0]" list (.use "[1]#[0]" functor)]]] - [type - [primitive (.except)]] + [meta + [type + [primitive (.except)]]] ["[0]" meta] ["[0]" macro (.only) ["[0]" code (.only) diff --git a/stdlib/source/library/lux/control/security/policy.lux b/stdlib/source/library/lux/control/security/policy.lux index 963f0377f..2aa55af59 100644 --- a/stdlib/source/library/lux/control/security/policy.lux +++ b/stdlib/source/library/lux/control/security/policy.lux @@ -5,8 +5,9 @@ [functor (.only Functor)] [apply (.only Apply)] [monad (.only Monad)]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public (Policy brand value label) value diff --git a/stdlib/source/library/lux/control/thread.lux b/stdlib/source/library/lux/control/thread.lux index 69591de05..0b43c9344 100644 --- a/stdlib/source/library/lux/control/thread.lux +++ b/stdlib/source/library/lux/control/thread.lux @@ -12,9 +12,10 @@ [collection ["[0]" array ["[1]" \\unsafe (.only Array)]]]] - [type - [primitive (.except)] - ["[0]" variance (.only Mutable)]]]]) + [meta + [type + [primitive (.except)] + ["[0]" variance (.only Mutable)]]]]]) (type .public (Thread ! a) (-> ! a)) diff --git a/stdlib/source/library/lux/data/collection/array.lux b/stdlib/source/library/lux/data/collection/array.lux index 06704ae38..40e8c6599 100644 --- a/stdlib/source/library/lux/data/collection/array.lux +++ b/stdlib/source/library/lux/data/collection/array.lux @@ -12,8 +12,9 @@ [data [collection ["[0]" list]]] - [type - [variance (.only)]]]] + [meta + [type + [variance (.only)]]]]] ["!" \\unsafe]) (def .public type_name diff --git a/stdlib/source/library/lux/data/collection/queue/priority.lux b/stdlib/source/library/lux/data/collection/queue/priority.lux index c860daae8..0d02d0a09 100644 --- a/stdlib/source/library/lux/data/collection/queue/priority.lux +++ b/stdlib/source/library/lux/data/collection/queue/priority.lux @@ -13,8 +13,9 @@ [math [number ["n" nat (.use "[1]#[0]" interval)]]] - [type (.only by_example) - [primitive (.only primitive abstraction representation)]]]]) + [meta + [type (.only by_example) + [primitive (.only primitive abstraction representation)]]]]]) (type .public Priority Nat) diff --git a/stdlib/source/library/lux/data/collection/set/multi.lux b/stdlib/source/library/lux/data/collection/set/multi.lux index 82c89f817..0b0f1735e 100644 --- a/stdlib/source/library/lux/data/collection/set/multi.lux +++ b/stdlib/source/library/lux/data/collection/set/multi.lux @@ -13,8 +13,9 @@ [math [number ["n" nat]]] - [type - ["[0]" primitive (.only primitive abstraction representation)]]]] + [meta + [type + ["[0]" primitive (.only primitive abstraction representation)]]]]] ["[0]" // (.only) [// ["[0]" list (.use "[1]#[0]" mix monoid)] diff --git a/stdlib/source/library/lux/data/collection/set/ordered.lux b/stdlib/source/library/lux/data/collection/set/ordered.lux index f24c059bd..dc209c092 100644 --- a/stdlib/source/library/lux/data/collection/set/ordered.lux +++ b/stdlib/source/library/lux/data/collection/set/ordered.lux @@ -9,8 +9,9 @@ ["[0]" list (.use "[1]#[0]" mix)] [dictionary ["/" ordered]]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public (Set a) (/.Dictionary a a) diff --git a/stdlib/source/library/lux/data/collection/stack.lux b/stdlib/source/library/lux/data/collection/stack.lux index 726cdada0..c53ba235a 100644 --- a/stdlib/source/library/lux/data/collection/stack.lux +++ b/stdlib/source/library/lux/data/collection/stack.lux @@ -7,8 +7,9 @@ [data [collection ["//" list]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public (Stack a) (List a) diff --git a/stdlib/source/library/lux/data/collection/tree/finger.lux b/stdlib/source/library/lux/data/collection/tree/finger.lux index 72ef03d8e..b8a654516 100644 --- a/stdlib/source/library/lux/data/collection/tree/finger.lux +++ b/stdlib/source/library/lux/data/collection/tree/finger.lux @@ -9,8 +9,9 @@ [data [collection ["[0]" list (.use "[1]#[0]" monoid)]]] - [type - [primitive (.only primitive abstraction representation)]]]]) + [meta + [type + [primitive (.only primitive abstraction representation)]]]]]) ... https://en.wikipedia.org/wiki/Finger_tree (primitive .public (Tree @ t v) diff --git a/stdlib/source/library/lux/data/color.lux b/stdlib/source/library/lux/data/color.lux index de3ee1d99..bbccf6b7b 100644 --- a/stdlib/source/library/lux/data/color.lux +++ b/stdlib/source/library/lux/data/color.lux @@ -15,8 +15,9 @@ ["[0]" int] ["[0]" rev (.use "[1]#[0]" interval)] ["[0]" i64]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def rgb_limit 256) (def top (-- rgb_limit)) diff --git a/stdlib/source/library/lux/data/format/css.lux b/stdlib/source/library/lux/data/format/css.lux index 30e9c4153..80b0623cd 100644 --- a/stdlib/source/library/lux/data/format/css.lux +++ b/stdlib/source/library/lux/data/format/css.lux @@ -12,8 +12,9 @@ [math [number ["[0]" nat]]] - [type - [primitive (.except Frame pattern)]] + [meta + [type + [primitive (.except Frame pattern)]]] [world [net (.only URL)]]]] ["[0]" / diff --git a/stdlib/source/library/lux/data/format/css/class.lux b/stdlib/source/library/lux/data/format/css/class.lux index a2aa3d00d..95ecbb9dc 100644 --- a/stdlib/source/library/lux/data/format/css/class.lux +++ b/stdlib/source/library/lux/data/format/css/class.lux @@ -10,8 +10,9 @@ [macro [syntax (.only syntax)] ["[0]" code]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public Class Text diff --git a/stdlib/source/library/lux/data/format/css/id.lux b/stdlib/source/library/lux/data/format/css/id.lux index 7d833ca6c..d4ce16d6a 100644 --- a/stdlib/source/library/lux/data/format/css/id.lux +++ b/stdlib/source/library/lux/data/format/css/id.lux @@ -10,8 +10,9 @@ [macro [syntax (.only syntax)] ["[0]" code]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public ID Text diff --git a/stdlib/source/library/lux/data/format/css/property.lux b/stdlib/source/library/lux/data/format/css/property.lux index 6d4413240..089e117c2 100644 --- a/stdlib/source/library/lux/data/format/css/property.lux +++ b/stdlib/source/library/lux/data/format/css/property.lux @@ -6,12 +6,13 @@ ["s" code]]] [data ["[0]" text]] - [type - [primitive (.except)]] [macro + [syntax (.only syntax)] ["[0]" template] - ["[0]" code] - [syntax (.only syntax)]]]] + ["[0]" code]] + [meta + [type + [primitive (.except)]]]]] [// [value (.only All Number diff --git a/stdlib/source/library/lux/data/format/css/query.lux b/stdlib/source/library/lux/data/format/css/query.lux index cce106c61..ec39e8425 100644 --- a/stdlib/source/library/lux/data/format/css/query.lux +++ b/stdlib/source/library/lux/data/format/css/query.lux @@ -11,8 +11,9 @@ ["[0]" template] ["[0]" code] [syntax (.only syntax)]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1][0]" value (.only Value Length Count Resolution Ratio Orientation Scan Boolean Update diff --git a/stdlib/source/library/lux/data/format/css/selector.lux b/stdlib/source/library/lux/data/format/css/selector.lux index 5993f5c89..1e8d3e0b9 100644 --- a/stdlib/source/library/lux/data/format/css/selector.lux +++ b/stdlib/source/library/lux/data/format/css/selector.lux @@ -8,10 +8,11 @@ [math [number ["i" int]]] - [type - [primitive (.except)]] [macro - ["[0]" template]]]] + ["[0]" template]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1][0]" id (.only ID)] ["[1][0]" class (.only Class)]]) diff --git a/stdlib/source/library/lux/data/format/css/style.lux b/stdlib/source/library/lux/data/format/css/style.lux index 1f055636f..4e459fd17 100644 --- a/stdlib/source/library/lux/data/format/css/style.lux +++ b/stdlib/source/library/lux/data/format/css/style.lux @@ -6,8 +6,9 @@ ["%" \\format (.only format)]] [collection ["[0]" list (.use "[1]#[0]" mix)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1][0]" value (.only Value)] ["[1][0]" property (.only Property)]]) diff --git a/stdlib/source/library/lux/data/format/css/value.lux b/stdlib/source/library/lux/data/format/css/value.lux index 6dab6619e..14d2a2cec 100644 --- a/stdlib/source/library/lux/data/format/css/value.lux +++ b/stdlib/source/library/lux/data/format/css/value.lux @@ -21,8 +21,9 @@ ["i" int] ["r" rev] ["f" frac]]] - [type - [primitive (.except)]] + [meta + [type + [primitive (.except)]]] [world [net (.only URL)]]]] [// diff --git a/stdlib/source/library/lux/data/format/html.lux b/stdlib/source/library/lux/data/format/html.lux index f27ec9173..d6560ccfe 100644 --- a/stdlib/source/library/lux/data/format/html.lux +++ b/stdlib/source/library/lux/data/format/html.lux @@ -12,10 +12,11 @@ ["[0]" list (.use "[1]#[0]" functor mix)]]] [macro ["[0]" template]] + [meta + [type + [primitive (.except)]]] [target ["[0]" js]] - [type - [primitive (.except)]] [world [net (.only URL)]]]] [// diff --git a/stdlib/source/library/lux/data/format/markdown.lux b/stdlib/source/library/lux/data/format/markdown.lux index 21843dd90..ad8a20186 100644 --- a/stdlib/source/library/lux/data/format/markdown.lux +++ b/stdlib/source/library/lux/data/format/markdown.lux @@ -6,10 +6,11 @@ ["%" \\format (.only format)]] [collection ["[0]" list (.use "[1]#[0]" functor)]]] - [type - [primitive (.except)]] [world - [net (.only URL)]]]]) + [net (.only URL)]] + [meta + [type + [primitive (.except)]]]]]) ... https://www.markdownguide.org/basic-syntax/ diff --git a/stdlib/source/library/lux/data/format/tar.lux b/stdlib/source/library/lux/data/format/tar.lux index 07c493b97..e0ed3924f 100644 --- a/stdlib/source/library/lux/data/format/tar.lux +++ b/stdlib/source/library/lux/data/format/tar.lux @@ -35,8 +35,9 @@ ["[0]" duration]] [world ["[0]" file]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (type Size Nat) diff --git a/stdlib/source/library/lux/data/text/buffer.lux b/stdlib/source/library/lux/data/text/buffer.lux index fbb58c96f..e8b4e496f 100644 --- a/stdlib/source/library/lux/data/text/buffer.lux +++ b/stdlib/source/library/lux/data/text/buffer.lux @@ -15,8 +15,9 @@ [math [number ["n" nat]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" //]) (with_expansions [ (these (import java/lang/CharSequence diff --git a/stdlib/source/library/lux/data/text/encoding.lux b/stdlib/source/library/lux/data/text/encoding.lux index 836fc8a49..25b91cfc0 100644 --- a/stdlib/source/library/lux/data/text/encoding.lux +++ b/stdlib/source/library/lux/data/text/encoding.lux @@ -3,8 +3,9 @@ [lux (.except) [macro ["[0]" template]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) ... https://en.wikipedia.org/wiki/Character_encoding#Common_character_encodings (primitive .public Encoding diff --git a/stdlib/source/library/lux/data/text/unicode/block.lux b/stdlib/source/library/lux/data/text/unicode/block.lux index c08d296e4..bb61c05be 100644 --- a/stdlib/source/library/lux/data/text/unicode/block.lux +++ b/stdlib/source/library/lux/data/text/unicode/block.lux @@ -10,8 +10,9 @@ [number (.only hex) ["n" nat (.use "[1]#[0]" interval)] ["[0]" i64]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] [/// (.only Char)]) (primitive .public Block diff --git a/stdlib/source/library/lux/data/text/unicode/set.lux b/stdlib/source/library/lux/data/text/unicode/set.lux index 961b597ef..13c5d4f47 100644 --- a/stdlib/source/library/lux/data/text/unicode/set.lux +++ b/stdlib/source/library/lux/data/text/unicode/set.lux @@ -9,8 +9,9 @@ ["[0]" set (.use "[1]#[0]" equivalence)] ["[0]" tree ["[1]" finger (.only Tree)]]]] - [type (.only by_example) - [primitive (.except)]]]] + [meta + [type (.only by_example) + [primitive (.except)]]]]] ["[0]" / ["/[1]" // [// (.only Char)] diff --git a/stdlib/source/library/lux/data/trace.lux b/stdlib/source/library/lux/data/trace.lux index e7032aef1..af741e922 100644 --- a/stdlib/source/library/lux/data/trace.lux +++ b/stdlib/source/library/lux/data/trace.lux @@ -4,8 +4,7 @@ [abstract ["[0]" monoid (.only Monoid)] [functor (.only Functor)] - comonad] - function]]) + comonad]]]) (type .public (Trace t a) (Record diff --git a/stdlib/source/library/lux/debug.lux b/stdlib/source/library/lux/debug.lux index fa9e36cff..78160f4cd 100644 --- a/stdlib/source/library/lux/debug.lux +++ b/stdlib/source/library/lux/debug.lux @@ -39,8 +39,9 @@ [date (.only Date)] [month (.only Month)] [day (.only Day)]] - ["[0]" type (.only) - ["<[1]>" \\parser (.only Parser)]]]]) + [meta + ["[0]" type (.only) + ["<[1]>" \\parser (.only Parser)]]]]]) (with_expansions [ (these (import java/lang/String "[1]::[0]") diff --git a/stdlib/source/library/lux/documentation.lux b/stdlib/source/library/lux/documentation.lux index 2fd1b2bdf..3f7df3b4e 100644 --- a/stdlib/source/library/lux/documentation.lux +++ b/stdlib/source/library/lux/documentation.lux @@ -1,8 +1,6 @@ (.require [library [lux (.except Definition Module type) - ["[0]" meta] - ["[0]" type (.use "[1]#[0]" equivalence)] [abstract [monad (.only do)] ["[0]" enum]] @@ -29,6 +27,8 @@ [math [number ["n" nat]]] + ["[0]" meta (.only) + ["[0]" type (.use "[1]#[0]" equivalence)]] [tool [compiler [language diff --git a/stdlib/source/library/lux/ffi.jvm.lux b/stdlib/source/library/lux/ffi.jvm.lux index a31b1df99..69090b80f 100644 --- a/stdlib/source/library/lux/ffi.jvm.lux +++ b/stdlib/source/library/lux/ffi.jvm.lux @@ -40,8 +40,9 @@ ["[0]" signature] ["[0]" reflection] ["[0]" parser]]]] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check]]]]) + [meta + ["[0]" type (.use "[1]#[0]" equivalence) + ["[0]" check]]]]]) (def internal (-> External Text) diff --git a/stdlib/source/library/lux/ffi.lux b/stdlib/source/library/lux/ffi.lux index 103d2babd..44e4e685e 100644 --- a/stdlib/source/library/lux/ffi.lux +++ b/stdlib/source/library/lux/ffi.lux @@ -22,8 +22,9 @@ ["<[1]>" \\parser (.only Parser)]]] ["@" target (.only) ["[0]" js]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (with_expansions [ (for @.js "js constant" @.python "python constant" diff --git a/stdlib/source/library/lux/ffi.old.lux b/stdlib/source/library/lux/ffi.old.lux index a199b5012..f713ebf1c 100644 --- a/stdlib/source/library/lux/ffi.old.lux +++ b/stdlib/source/library/lux/ffi.old.lux @@ -1,7 +1,6 @@ (.require [library [lux (.except is as type) - ["[0]" type (.use "[1]#[0]" equivalence)] [abstract ["[0]" monad (.only Monad do)] ["[0]" enum]] @@ -25,7 +24,8 @@ ["[0]" template] ["[0]" code (.only) ["<[1]>" \\parser (.only Parser)]]] - ["[0]" meta]]]) + ["[0]" meta (.only) + ["[0]" type (.use "[1]#[0]" equivalence)]]]]) (with_template [ ] [(def .public ( value) diff --git a/stdlib/source/library/lux/ffi.php.lux b/stdlib/source/library/lux/ffi.php.lux index f5f357021..a720cc6f1 100644 --- a/stdlib/source/library/lux/ffi.php.lux +++ b/stdlib/source/library/lux/ffi.php.lux @@ -2,7 +2,6 @@ [library [lux (.except Alias) ["@" target] - ["[0]" meta] [abstract [monad (.only do)]] [control @@ -15,13 +14,14 @@ ["%" \\format]] [collection ["[0]" list (.use "[1]#[0]" functor)]]] - [type - abstract] [macro (.only with_symbols) [syntax (.only syntax)] ["[0]" template] ["[0]" code (.only) - ["<[1]>" \\parser (.only Parser)]]]]]) + ["<[1]>" \\parser (.only Parser)]]] + ["[0]" meta (.only) + [type + abstract]]]]) (primitive .public (Object brand) Any) diff --git a/stdlib/source/library/lux/ffi.scm.lux b/stdlib/source/library/lux/ffi.scm.lux index 27f8c4f4f..679a9b58e 100644 --- a/stdlib/source/library/lux/ffi.scm.lux +++ b/stdlib/source/library/lux/ffi.scm.lux @@ -2,7 +2,6 @@ [library [lux (.except Alias) ["@" target] - ["[0]" meta] [abstract [monad (.only do)]] [control @@ -15,13 +14,14 @@ ["%" \\format (.only format)]] [collection ["[0]" list (.use "[1]#[0]" functor)]]] - [type - abstract] [macro (.only with_symbols) [syntax (.only syntax)] ["[0]" template] ["[0]" code (.only) - ["<[1]>" \\parser (.only Parser)]]]]]) + ["<[1]>" \\parser (.only Parser)]]] + ["[0]" meta (.only) + [type + abstract]]]]) (primitive .public (Object brand) Any) diff --git a/stdlib/source/library/lux/locale.lux b/stdlib/source/library/lux/locale.lux index d1c97493d..6cd384586 100644 --- a/stdlib/source/library/lux/locale.lux +++ b/stdlib/source/library/lux/locale.lux @@ -10,8 +10,9 @@ ["[0]" text (.only) ["%" \\format (.only format)] ["[0]" encoding (.only Encoding)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] [/ ["[0]" language (.only Language)] ["[0]" territory (.only Territory)]]) diff --git a/stdlib/source/library/lux/locale/language.lux b/stdlib/source/library/lux/locale/language.lux index bab86a699..f5d9b051f 100644 --- a/stdlib/source/library/lux/locale/language.lux +++ b/stdlib/source/library/lux/locale/language.lux @@ -6,10 +6,11 @@ [hash (.only Hash)]] [data ["[0]" text]] - [type - [primitive (.except)]] [macro - ["[0]" template]]]]) + ["[0]" template]] + [meta + [type + [primitive (.except)]]]]]) ... https://en.wikipedia.org/wiki/List_of_ISO_639-2_codes (primitive .public Language diff --git a/stdlib/source/library/lux/locale/territory.lux b/stdlib/source/library/lux/locale/territory.lux index 9688d691d..f89f8a619 100644 --- a/stdlib/source/library/lux/locale/territory.lux +++ b/stdlib/source/library/lux/locale/territory.lux @@ -6,10 +6,11 @@ [hash (.only Hash)]] [data ["[0]" text]] - [type - [primitive (.except)]] [macro - ["[0]" template]]]]) + ["[0]" template]] + [meta + [type + [primitive (.except)]]]]]) ... https://en.wikipedia.org/wiki/ISO_3166-1 (primitive .public Territory diff --git a/stdlib/source/library/lux/math.lux b/stdlib/source/library/lux/math.lux index 63f2e931c..d5b8f2629 100644 --- a/stdlib/source/library/lux/math.lux +++ b/stdlib/source/library/lux/math.lux @@ -29,8 +29,9 @@ ["[0]" type]]]] [meta [archive (.only Archive)]]]] - [type - ["[0]" check]]]] + [meta + [type + ["[0]" check]]]]] [/ ["[0]" random] [number diff --git a/stdlib/source/library/lux/math/modular.lux b/stdlib/source/library/lux/math/modular.lux index 489f798ab..b2ae0a5b3 100644 --- a/stdlib/source/library/lux/math/modular.lux +++ b/stdlib/source/library/lux/math/modular.lux @@ -21,8 +21,9 @@ [math [number ["i" int (.use "[1]#[0]" decimal)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1]" modulus (.only Modulus)]]) diff --git a/stdlib/source/library/lux/math/modulus.lux b/stdlib/source/library/lux/math/modulus.lux index d440669ae..333946b3d 100644 --- a/stdlib/source/library/lux/math/modulus.lux +++ b/stdlib/source/library/lux/math/modulus.lux @@ -14,8 +14,9 @@ [math [number ["i" int]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (exception .public zero_cannot_be_a_modulus) diff --git a/stdlib/source/library/lux/math/number/i16.lux b/stdlib/source/library/lux/math/number/i16.lux index 446e5f71b..b83bf1f72 100644 --- a/stdlib/source/library/lux/math/number/i16.lux +++ b/stdlib/source/library/lux/math/number/i16.lux @@ -5,7 +5,8 @@ [equivalence (.only Equivalence)]] [control ["[0]" maybe]] - [type (.only by_example)]]] + [meta + [type (.only by_example)]]]] [// ["[0]" i64 (.only Sub)]]) diff --git a/stdlib/source/library/lux/math/number/i32.lux b/stdlib/source/library/lux/math/number/i32.lux index 262dc3eb4..4423f3098 100644 --- a/stdlib/source/library/lux/math/number/i32.lux +++ b/stdlib/source/library/lux/math/number/i32.lux @@ -1,11 +1,12 @@ (.require [library [lux (.except i64) - [type (.only by_example)] [abstract [equivalence (.only Equivalence)]] [control - ["[0]" maybe]]]] + ["[0]" maybe]] + [meta + [type (.only by_example)]]]] [// ["[0]" i64 (.only Sub)]]) diff --git a/stdlib/source/library/lux/math/number/i8.lux b/stdlib/source/library/lux/math/number/i8.lux index 0ea292821..49ccad042 100644 --- a/stdlib/source/library/lux/math/number/i8.lux +++ b/stdlib/source/library/lux/math/number/i8.lux @@ -1,11 +1,12 @@ (.require [library [lux (.except i64) - [type (.only by_example)] [abstract [equivalence (.only Equivalence)]] [control - ["[0]" maybe]]]] + ["[0]" maybe]] + [meta + [type (.only by_example)]]]] [// ["[0]" i64 (.only Sub)]]) diff --git a/stdlib/source/library/lux/math/random.lux b/stdlib/source/library/lux/math/random.lux index 89ae2ef53..7ebf577d7 100644 --- a/stdlib/source/library/lux/math/random.lux +++ b/stdlib/source/library/lux/math/random.lux @@ -34,8 +34,9 @@ ["[0]" duration (.only Duration)] ["[0]" month (.only Month)] ["[0]" day (.only Day)]] - [type - [refinement (.only Refiner Refined)]]]]) + [meta + [type + [refinement (.only Refiner Refined)]]]]]) (type .public PRNG (Rec PRNG diff --git a/stdlib/source/library/lux/meta/type.lux b/stdlib/source/library/lux/meta/type.lux new file mode 100644 index 000000000..00afaddc0 --- /dev/null +++ b/stdlib/source/library/lux/meta/type.lux @@ -0,0 +1,515 @@ +(.require + [library + [lux (.except function as let) + ["@" target] + [abstract + [equivalence (.only Equivalence)] + [monad (.only Monad do)]] + [control + ["<>" parser] + ["[0]" function] + ["[0]" maybe]] + [data + ["[0]" product] + ["[0]" text (.use "[1]#[0]" monoid equivalence)] + [collection + ["[0]" array] + ["[0]" list (.use "[1]#[0]" monad monoid mix)]]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["^" pattern] + ["[0]" code (.only) + ["<[1]>" \\parser (.only Parser)]]] + [math + [number + ["n" nat (.use "[1]#[0]" decimal)]]] + ["[0]" meta (.only) + ["[0]" location] + ["[0]" symbol (.use "[1]#[0]" equivalence codec)]]]]) + +(with_template [ ] + [(def .public ( type) + (-> Type [Nat Type]) + (loop (again [num_args 0 + type type]) + (case type + { env sub_type} + (again (++ num_args) sub_type) + + _ + [num_args type])))] + + [flat_univ_q .#UnivQ] + [flat_ex_q .#ExQ] + ) + +(def .public (flat_function type) + (-> Type [(List Type) Type]) + (case type + {.#Function in out'} + (.let [[ins out] (flat_function out')] + [(list.partial in ins) out]) + + _ + [(list) type])) + +(def .public (flat_application type) + (-> Type [Type (List Type)]) + (case type + {.#Apply arg func'} + (.let [[func args] (flat_application func')] + [func (list#composite args (list arg))]) + + _ + [type (list)])) + +(with_template [ ] + [(def .public ( type) + (-> Type (List Type)) + (case type + { left right} + (list.partial left ( right)) + + _ + (list type)))] + + [flat_variant .#Sum] + [flat_tuple .#Product] + ) + +(def .public (format type) + (-> Type Text) + (case type + {.#Primitive name params} + (all text#composite + "(Primitive " + (text.enclosed' text.double_quote name) + (|> params + (list#each (|>> format (text#composite " "))) + (list#mix (function.flipped text#composite) "")) + ")") + + (^.with_template [ ] + [{ _} + (all text#composite + (|> ( type) + (list#each format) + list.reversed + (list.interposed " ") + (list#mix text#composite "")) + )]) + ([.#Sum "(Or " ")" flat_variant] + [.#Product "[" "]" flat_tuple]) + + {.#Function input output} + (.let [[ins out] (flat_function type)] + (all text#composite "(-> " + (|> ins + (list#each format) + list.reversed + (list.interposed " ") + (list#mix text#composite "")) + " " (format out) ")")) + + {.#Parameter idx} + (n#encoded idx) + + {.#Var id} + (all text#composite "-" (n#encoded id)) + + {.#Ex id} + (all text#composite "+" (n#encoded id)) + + {.#Apply param fun} + (.let [[type_func type_args] (flat_application type)] + (all text#composite "(" (format type_func) " " (|> type_args (list#each format) list.reversed (list.interposed " ") (list#mix text#composite "")) ")")) + + (^.with_template [ ] + [{ env body} + (all text#composite "(" " {" (|> env (list#each format) (text.interposed " ")) "} " (format body) ")")]) + ([.#UnivQ "All"] + [.#ExQ "Ex"]) + + {.#Named [module name] type} + (all text#composite module "." name) + )) + +... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction +(def (reduced env type) + (-> (List Type) Type Type) + (case type + {.#Primitive name params} + {.#Primitive name (list#each (reduced env) params)} + + (^.with_template [] + [{ left right} + { (reduced env left) (reduced env right)}]) + ([.#Sum] [.#Product] + [.#Function] [.#Apply]) + + (^.with_template [] + [{ old_env def} + (case old_env + {.#End} + { env def} + + _ + { (list#each (reduced env) old_env) def})]) + ([.#UnivQ] + [.#ExQ]) + + {.#Parameter idx} + (maybe.else (panic! (all text#composite + "Unknown type parameter" text.new_line + " Index: " (n#encoded idx) text.new_line + "Environment: " (|> env + list.enumeration + (list#each (.function (_ [index type]) + (all text#composite + (n#encoded index) + " " (..format type)))) + (text.interposed (text#composite text.new_line " "))))) + (list.item idx env)) + + _ + type + )) + +(def .public equivalence + (Equivalence Type) + (implementation + (def (= x y) + (or (for @.php + ... TODO: Remove this once JPHP is gone. + false + (same? x y)) + (case [x y] + [{.#Primitive xname xparams} {.#Primitive yname yparams}] + (and (text#= xname yname) + (n.= (list.size yparams) (list.size xparams)) + (list#mix (.function (_ [x y] prev) (and prev (= x y))) + #1 + (list.zipped_2 xparams yparams))) + + (^.with_template [] + [[{ xid} { yid}] + (n.= yid xid)]) + ([.#Var] [.#Ex] [.#Parameter]) + + (^.or [{.#Function xleft xright} {.#Function yleft yright}] + [{.#Apply xleft xright} {.#Apply yleft yright}]) + (and (= xleft yleft) + (= xright yright)) + + [{.#Named xname xtype} {.#Named yname ytype}] + (and (symbol#= xname yname) + (= xtype ytype)) + + (^.with_template [] + [[{ xL xR} { yL yR}] + (and (= xL yL) (= xR yR))]) + ([.#Sum] [.#Product]) + + (^.or [{.#UnivQ xenv xbody} {.#UnivQ yenv ybody}] + [{.#ExQ xenv xbody} {.#ExQ yenv ybody}]) + (and (n.= (list.size yenv) (list.size xenv)) + (= xbody ybody) + (list#mix (.function (_ [x y] prev) (and prev (= x y))) + #1 + (list.zipped_2 xenv yenv))) + + _ + #0 + ))))) + +(def .public (applied params func) + (-> (List Type) Type (Maybe Type)) + (case params + {.#End} + {.#Some func} + + {.#Item param params'} + (case func + (^.with_template [] + [{ env body} + (|> body + (reduced (list.partial func param env)) + (applied params'))]) + ([.#UnivQ] [.#ExQ]) + + {.#Apply A F} + (applied (list.partial A params) F) + + {.#Named name unnamed} + (applied params unnamed) + + _ + {.#None}))) + +(def .public (code type) + (-> Type Code) + (case type + {.#Primitive name params} + (` {.#Primitive (~ (code.text name)) + (.list (~+ (list#each code params)))}) + + (^.with_template [] + [{ idx} + (` { (~ (code.nat idx))})]) + ([.#Var] [.#Ex] [.#Parameter]) + + (^.with_template [] + [{ left right} + (` { (~ (code left)) + (~ (code right))})]) + ([.#Sum] [.#Product] [.#Function] [.#Apply]) + + {.#Named name sub_type} + (code.symbol name) + + (^.with_template [] + [{ env body} + (` { (.list (~+ (list#each code env))) + (~ (code body))})]) + ([.#UnivQ] [.#ExQ]) + )) + +(def .public (de_aliased type) + (-> Type Type) + (case type + {.#Named _ {.#Named name type'}} + (de_aliased {.#Named name type'}) + + _ + type)) + +(def .public (anonymous type) + (-> Type Type) + (case type + {.#Named name type'} + (anonymous type') + + _ + type)) + +(with_template [ ] + [(def .public ( types) + (-> (List Type) Type) + (case types + {.#End} + + + {.#Item type {.#End}} + type + + {.#Item type types'} + { type ( types')}))] + + [variant Nothing .#Sum] + [tuple Any .#Product] + ) + +(def .public (function inputs output) + (-> (List Type) Type Type) + (case inputs + {.#End} + output + + {.#Item input inputs'} + {.#Function input (function inputs' output)})) + +(def .public (application params quant) + (-> (List Type) Type Type) + (case params + {.#End} + quant + + {.#Item param params'} + (application params' {.#Apply param quant}))) + +(with_template [ ] + [(def .public ( size body) + (-> Nat Type Type) + (case size + 0 body + _ (|> body ( (-- size)) { (list)})))] + + [univ_q .#UnivQ] + [ex_q .#ExQ] + ) + +(def .public (quantified? type) + (-> Type Bit) + (case type + {.#Named [module name] _type} + (quantified? _type) + + {.#Apply A F} + (|> (..applied (list A) F) + (at maybe.monad each quantified?) + (maybe.else #0)) + + (^.or {.#UnivQ _} {.#ExQ _}) + #1 + + _ + #0)) + +(def .public (array depth element_type) + (-> Nat Type Type) + (case depth + 0 element_type + _ (|> element_type + (array (-- depth)) + (list) + {.#Primitive array.type_name}))) + +(def .public (flat_array type) + (-> Type [Nat Type]) + (case type + (^.multi (pattern {.#Primitive name (list element_type)}) + (text#= array.type_name name)) + (.let [[depth element_type] (flat_array element_type)] + [(++ depth) element_type]) + + _ + [0 type])) + +(def .public array? + (-> Type Bit) + (|>> ..flat_array + product.left + (n.> 0))) + +(def new_secret_marker + (syntax (_ []) + (macro.with_symbols [g!_secret_marker_] + (in (list g!_secret_marker_))))) + +(def secret_marker + (`` (symbol (~~ (new_secret_marker))))) + +(def .public log! + (syntax (_ [input (<>.or (<>.and .symbol + (<>.maybe (<>.after (.this_symbol ..secret_marker) .any))) + .any)]) + (case input + {.#Left [valueN valueC]} + (do meta.monad + [location meta.location + valueT (meta.type valueN) + .let [_ ("lux io log" + (all text#composite + (symbol#encoded (symbol ..log!)) " " (location.format location) text.new_line + "Expression: " (case valueC + {.#Some valueC} + (code.format valueC) + + {.#None} + (symbol#encoded valueN)) + text.new_line + " Type: " (..format valueT)))]] + (in (list (code.symbol valueN)))) + + {.#Right valueC} + (macro.with_symbols [g!value] + (in (list (` (.let [(~ g!value) (~ valueC)] + (..log! (~ valueC) (~ (code.symbol ..secret_marker)) (~ g!value)))))))))) + +(def type_parameters + (Parser (List Text)) + (.tuple (<>.some .local))) + +(def .public as + (syntax (_ [type_vars type_parameters + input .any + output .any + value (<>.maybe .any)]) + (macro.with_symbols [g!_] + (.let [casterC (` (is (All ((~ g!_) (~+ (list#each code.local type_vars))) + (-> (~ input) (~ output))) + (|>> as_expected)))] + (case value + {.#None} + (in (list casterC)) + + {.#Some value} + (in (list (` ((~ casterC) (~ value)))))))))) + +(type Typed + (Record + [#type Code + #expression Code])) + +(def (typed lux) + (-> Lux (Parser Typed)) + (do <>.monad + [it .any + type_check (<>.lifted (meta.result lux (macro.expansion it)))] + (<| (.locally type_check) + .form + (<>.after (.this (` "lux type check"))) + (<>.and .any .any)))) + +... TODO: Make sure the generated code always gets optimized away. +(def .public sharing + (syntax (_ lux [type_vars ..type_parameters + exemplar (..typed lux) + computation (..typed lux)]) + (macro.with_symbols [g!_] + (.let [typeC (` (All ((~ g!_) (~+ (list#each code.local type_vars))) + (-> (~ (the #type exemplar)) + (~ (the #type computation))))) + shareC (` (is (~ typeC) + (.function ((~ g!_) (~ g!_)) + (~ (the #expression computation)))))] + (in (list (` ((~ shareC) (~ (the #expression exemplar)))))))))) + +(def .public by_example + (syntax (_ lux [type_vars ..type_parameters + exemplar (..typed lux) + extraction .any]) + (in (list (` (.type_of ((~! ..sharing) [(~+ (list#each code.local type_vars))] + (is (~ (the #type exemplar)) + (~ (the #expression exemplar))) + (is (~ extraction) + ... The value of this expression will never be relevant, so it doesn't matter what it is. + (.as .Nothing []))))))))) + +(def .public (replaced before after) + (-> Type Type Type Type) + (.function (again it) + (if (at ..equivalence = before it) + after + (case it + {.#Primitive name co_variant} + {.#Primitive name (list#each again co_variant)} + + (^.with_template [] + [{ left right} + { (again left) (again right)}]) + ([.#Sum] + [.#Product] + [.#Function] + [.#Apply]) + + (^.with_template [] + [{ env body} + { (list#each again env) (again body)}]) + ([.#UnivQ] + [.#ExQ]) + + (^.or {.#Parameter _} + {.#Var _} + {.#Ex _} + {.#Named _}) + it)))) + +(def .public let + (syntax (_ [bindings (.tuple (<>.some (<>.and .any .any))) + bodyT .any]) + (in (list (` (..with_expansions [(~+ (|> bindings + (list#each (.function (_ [localT valueT]) + (list localT (` (.these (~ valueT)))))) + list#conjoint))] + (~ bodyT))))))) diff --git a/stdlib/source/library/lux/meta/type/check.lux b/stdlib/source/library/lux/meta/type/check.lux new file mode 100644 index 000000000..cb49cc6e4 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/check.lux @@ -0,0 +1,829 @@ +(.require + [library + [lux (.except try except with) + ["@" target] + [abstract + [functor (.only Functor)] + [apply (.only Apply)] + ["[0]" monad (.only Monad do)]] + [control + ["[0]" maybe] + ["[0]" try (.only Try)] + ["[0]" exception (.only Exception exception)]] + [data + ["[0]" product] + ["[0]" text (.use "[1]#[0]" monoid equivalence)] + [collection + ["[0]" list (.use "[1]#[0]" mix)] + ["[0]" set (.only Set)]]] + [macro + ["^" pattern]] + [math + [number + ["n" nat (.use "[1]#[0]" decimal)]]]]] + ["[0]" // (.use "[1]#[0]" equivalence)]) + +(def !n#= + (template (_ reference subject) + [("lux i64 =" reference subject)])) + +(def !text#= + (template (_ reference subject) + [("lux text =" reference subject)])) + +(exception .public (unknown_type_var [id Nat]) + (exception.report + "ID" (n#encoded id))) + +(exception .public (unbound_type_var [id Nat]) + (exception.report + "ID" (n#encoded id))) + +(exception .public (invalid_type_application [funcT Type + argT Type]) + (exception.report + "Type function" (//.format funcT) + "Type argument" (//.format argT))) + +(exception .public (cannot_rebind_var [id Nat + type Type + bound Type]) + (exception.report + "Var" (n#encoded id) + "Wanted Type" (//.format type) + "Current Type" (//.format bound))) + +(exception .public (type_check_failed [expected Type + actual Type]) + (exception.report + "Expected" (//.format expected) + "Actual" (//.format actual))) + +(type .public Var + Nat) + +(type Assumption + [Type Type]) + +(type .public (Check a) + (-> Type_Context (Try [Type_Context a]))) + +(type (Checker a) + (-> (List Assumption) a a (Check (List Assumption)))) + +(type Type_Vars + (List [Var (Maybe Type)])) + +(def .public functor + (Functor Check) + (implementation + (def (each f fa) + (function (_ context) + (case (fa context) + {try.#Success [context' output]} + {try.#Success [context' (f output)]} + + {try.#Failure error} + {try.#Failure error}))))) + +(def .public apply + (Apply Check) + (implementation + (def functor ..functor) + + (def (on fa ff) + (function (_ context) + (case (ff context) + {try.#Success [context' f]} + (case (fa context') + {try.#Success [context'' a]} + {try.#Success [context'' (f a)]} + + {try.#Failure error} + {try.#Failure error}) + + {try.#Failure error} + {try.#Failure error} + ))) + )) + +(def .public monad + (Monad Check) + (implementation + (def functor ..functor) + + (def (in x) + (function (_ context) + {try.#Success [context x]})) + + (def (conjoint ffa) + (function (_ context) + (case (ffa context) + {try.#Success [context' fa]} + (case (fa context') + {try.#Success [context'' a]} + {try.#Success [context'' a]} + + {try.#Failure error} + {try.#Failure error}) + + {try.#Failure error} + {try.#Failure error} + ))) + )) + +(use "check#[0]" ..monad) + +(def (var::new id property_list) + (-> Var Type_Vars Type_Vars) + {.#Item [id {.#None}] property_list}) + +(def (var::get id property_list) + (-> Var Type_Vars (Maybe (Maybe Type))) + (case property_list + {.#Item [var_id var_type] + property_list'} + (if (!n#= id var_id) + {.#Some var_type} + (var::get id property_list')) + + {.#End} + {.#None})) + +(def (var::put id value property_list) + (-> Var (Maybe Type) Type_Vars Type_Vars) + (case property_list + {.#End} + (list [id value]) + + {.#Item [var_id var_type] + property_list'} + (if (!n#= id var_id) + {.#Item [var_id value] + property_list'} + {.#Item [var_id var_type] + (var::put id value property_list')}))) + +(def .public (result context proc) + (All (_ a) (-> Type_Context (Check a) (Try a))) + (case (proc context) + {try.#Success [context' output]} + {try.#Success output} + + {try.#Failure error} + {try.#Failure error})) + +(def .public (failure message) + (All (_ a) (-> Text (Check a))) + (function (_ context) + {try.#Failure message})) + +(def .public (assertion message test) + (-> Text Bit (Check Any)) + (function (_ context) + (if test + {try.#Success [context []]} + {try.#Failure message}))) + +(def .public (except exception message) + (All (_ e a) (-> (Exception e) e (Check a))) + (..failure (exception.error exception message))) + +(def .public existential + (Check [Nat Type]) + (function (_ context) + (let [id (the .#ex_counter context)] + {try.#Success [(revised .#ex_counter ++ context) + [id {.#Ex id}]]}))) + +(with_template [ ] + [(def .public ( id) + (-> Var (Check )) + (function (_ context) + (case (|> context (the .#var_bindings) (var::get id)) + (^.or {.#Some {.#Some {.#Var _}}} + {.#Some {.#None}}) + {try.#Success [context ]} + + {.#Some {.#Some bound}} + {try.#Success [context ]} + + {.#None} + (exception.except ..unknown_type_var id))))] + + [bound? Bit false true] + [peek (Maybe Type) {.#None} {.#Some bound}] + ) + +(def .public (read id) + (-> Var (Check Type)) + (do ..monad + [?type (peek id)] + (case ?type + {.#Some type} + (in type) + + {.#None} + (..except ..unbound_type_var id)))) + +(def (bound id) + (-> Var (Check Type)) + (function (_ context) + (case (|> context (the .#var_bindings) (var::get id)) + {.#Some {.#Some bound}} + {try.#Success [context bound]} + + {.#Some _} + (exception.except ..unbound_type_var id) + + _ + (exception.except ..unknown_type_var id)))) + +(def .public (bind type id) + (-> Type Var (Check Any)) + (function (_ context) + (case (|> context (the .#var_bindings) (var::get id)) + {.#Some {.#None}} + {try.#Success [(revised .#var_bindings (var::put id {.#Some type}) context) + []]} + + {.#Some {.#Some bound}} + (exception.except ..cannot_rebind_var [id type bound]) + + _ + (exception.except ..unknown_type_var id)))) + +(def (re_bind' ?type id) + (-> (Maybe Type) Var (Check Any)) + (function (_ context) + (case (|> context (the .#var_bindings) (var::get id)) + {.#Some _} + {try.#Success [(revised .#var_bindings (var::put id ?type) context) + []]} + + _ + (exception.except ..unknown_type_var id)))) + +(def (re_bind type id) + (-> Type Var (Check Any)) + (re_bind' {.#Some type} id)) + +(def .public var + (Check [Var Type]) + (function (_ context) + (let [id (the .#var_counter context)] + {try.#Success [(|> context + (revised .#var_counter ++) + (revised .#var_bindings (var::new id))) + [id {.#Var id}]]}))) + +(def (on argT funcT) + (-> Type Type (Check Type)) + (case funcT + {.#Var func_id} + (do ..monad + [?funcT' (peek func_id)] + (case ?funcT' + {.#Some funcT'} + (on argT funcT') + + _ + (except ..invalid_type_application [funcT argT]))) + + {.#Apply argT' funcT'} + (do ..monad + [funcT'' (on argT' funcT')] + (on argT funcT'')) + + _ + (case (//.applied (list argT) funcT) + {.#Some output} + (check#in output) + + _ + (except ..invalid_type_application [funcT argT])))) + +(def .public (ring' start) + (-> Var (Check (List Var))) + (function (_ context) + (loop (again [current start + output (list start)]) + (case (|> context (the .#var_bindings) (var::get current)) + {.#Some {.#Some type}} + (case type + {.#Var next} + (if (!n#= start next) + {try.#Success [context output]} + (again next (list.partial next output))) + + _ + {try.#Success [context (list)]}) + + {.#Some {.#None}} + {try.#Success [context output]} + + {.#None} + (exception.except ..unknown_type_var current))))) + +... TODO: Optimize this by not using sets anymore. +(def ring + (-> Var (Check (Set Var))) + (|>> ..ring' + (check#each (set.of_list n.hash)))) + +(def .public (linked? @0 @1) + (-> Var Var (Check Bit)) + (check#each (function (_ it) + (set.member? it @1)) + (..ring @0))) + +(exception .public (cannot_identify [var Var]) + (exception.report + "Var" (n#encoded var))) + +(def .public (identity aliases @) + (-> (List Var) Var (Check Type)) + (do [! ..monad] + [:bound: (..peek @)] + (case :bound: + {.#Some :bound:} + (in :bound:) + + {.#None} + (do ! + [existing_aliases (..ring @)] + (if (n.< 2 (set.size existing_aliases)) + (..except ..cannot_identify [@]) + (do ! + [.let [forbidden_aliases (set.of_list n.hash (list.partial @ aliases)) + allowed_aliases (set.difference forbidden_aliases existing_aliases)]] + (case (set.list allowed_aliases) + {.#Item identity _} + (in {.#Var identity}) + + {.#None} + (..except ..cannot_identify [@])))))))) + +(def (erase! @) + (-> Var (Check Any)) + (function (_ context) + {try.#Success [(revised .#var_bindings + (list#mix (is (//.let [binding [Nat (Maybe Type)]] + (-> binding + (List binding) + (List binding))) + (function (_ in out) + (let [[@var :var:] in] + (if (n.= @ @var) + out + (list.partial in out))))) + (is (List [Nat (Maybe Type)]) + (list))) + context) + []]})) + +(def .public (forget! @) + (-> Var (Check Any)) + (do [! ..monad] + [ring (..ring' @)] + (case ring + (pattern (list)) + (in []) + + (pattern (list @me)) + (erase! @me) + + (pattern (list @other @me)) + (do ! + [_ (re_bind' {.#None} @other)] + (erase! @me)) + + (pattern (list.partial @prev _)) + (case (list.reversed ring) + (pattern (list.partial @me @next _)) + (do ! + [_ (re_bind {.#Var @next} @prev) + _ (re_bind {.#Var @prev} @next)] + (erase! @me)) + + _ + (undefined))))) + +(def .public (try it) + (All (_ a) (-> (Check a) (Check (Try a)))) + (function (_ context) + (case (it context) + {try.#Success [context' output]} + {try.#Success [context' {try.#Success output}]} + + {try.#Failure error} + {try.#Success [context {try.#Failure error}]}))) + +(def .public fresh_context + Type_Context + [.#var_counter 0 + .#ex_counter 0 + .#var_bindings (list)]) + +(def (either left right) + (All (_ a) (-> (Check a) (Check a) (Check a))) + (function (_ context) + (case (left context) + {try.#Failure _} + (right context) + + output + output))) + +(def (assumed? [e a] assumptions) + (-> Assumption (List Assumption) Bit) + (list.any? (function (_ [e' a']) + (and (//#= e e') + (//#= a a'))) + assumptions)) + +... TODO: "if_can_bind" can be optimized... +(def (if_can_bind id type then else) + (All (_ a) + (-> Var Type (Check a) (-> Type (Check a)) + (Check a))) + (all either + (do ..monad + [_ (..bind type id)] + then) + (do [! ..monad] + [ring (..ring id) + _ (..assertion "" (n.> 1 (set.size ring))) + _ (monad.each ! (re_bind type) (set.list ring))] + then) + (do ..monad + [?bound (peek id)] + (else (maybe.else {.#Var id} ?bound))))) + +... TODO: "link/2" can be optimized... +(def (link/2 left right) + (-> Var Var (Check Any)) + (do ..monad + [_ (..bind {.#Var right} left)] + (..bind {.#Var left} right))) + +... TODO: "link/3" can be optimized... +(def (link/3 interpose to from) + (-> Var Var Var (Check Any)) + (do ..monad + [_ (re_bind {.#Var interpose} from)] + (re_bind {.#Var to} interpose))) + +... TODO: "check_vars" can be optimized... +(def (check_vars check' assumptions idE idA) + (-> (Checker Type) (Checker Var)) + (if (!n#= idE idA) + (check#in assumptions) + (do [! ..monad] + [ebound (..try (..bound idE)) + abound (..try (..bound idA))] + (case [ebound abound] + ... Link the 2 variables circularly + [{try.#Failure _} {try.#Failure _}] + (do ! + [_ (link/2 idE idA)] + (in assumptions)) + + ... Interpose new variable between 2 existing links + [{try.#Success etype} {try.#Failure _}] + (case etype + {.#Var targetE} + (do ! + [_ (link/3 idA targetE idE)] + (in assumptions)) + + _ + (check' assumptions etype {.#Var idA})) + + ... Interpose new variable between 2 existing links + [{try.#Failure _} {try.#Success atype}] + (case atype + {.#Var targetA} + (do ! + [_ (link/3 idE targetA idA)] + (in assumptions)) + + _ + (check' assumptions {.#Var idE} atype)) + + [{try.#Success etype} {try.#Success atype}] + (case [etype atype] + [{.#Var targetE} {.#Var targetA}] + (do ! + [ringE (..ring idE) + ringA (..ring idA)] + (if (at set.equivalence = ringE ringA) + (in assumptions) + ... Fuse 2 rings + (do ! + [_ (monad.mix ! (function (_ interpose to) + (do ! + [_ (link/3 interpose to idE)] + (in interpose))) + targetE + (set.list ringA))] + (in assumptions)))) + + (^.with_template [ ] + [ + (do ! + [ring (..ring ) + _ (monad.each ! (re_bind ) (set.list ring))] + (in assumptions))]) + ([[{.#Var _} _] idE atype] + [[_ {.#Var _}] idA etype]) + + _ + (check' assumptions etype atype)))))) + +(def silent_failure! + (All (_ a) (Check a)) + (..failure "")) + +... TODO: "check_apply" can be optimized... +(def (check_apply check' assumptions expected actual) + (-> (Checker Type) (Checker [Type Type])) + (let [[expected_input expected_function] expected + [actual_input actual_function] actual] + (case [expected_function actual_function] + [{.#Ex exE} {.#Ex exA}] + (if (!n#= exE exA) + (check' assumptions expected_input actual_input) + ..silent_failure!) + + [{.#UnivQ _ _} {.#Ex _}] + (do ..monad + [expected' (..on expected_input expected_function)] + (check' assumptions expected' {.#Apply actual})) + + [{.#Ex _} {.#UnivQ _ _}] + (do ..monad + [actual' (..on actual_input actual_function)] + (check' assumptions {.#Apply expected} actual')) + + [{.#Apply [expected_input' expected_function']} {.#Ex _}] + (do ..monad + [expected_function'' (..on expected_input' expected_function')] + (check' assumptions {.#Apply [expected_input expected_function'']} {.#Apply actual})) + + [{.#Ex _} {.#Apply [actual_input' actual_function']}] + (do ..monad + [actual_function'' (..on actual_input' actual_function')] + (check' assumptions {.#Apply expected} {.#Apply [actual_input actual_function'']})) + + (^.or [{.#Ex _} _] [_ {.#Ex _}]) + (do ..monad + [assumptions (check' assumptions expected_function actual_function)] + (check' assumptions expected_input actual_input)) + + [{.#Var id} _] + (function (_ context) + (case ((do ..monad + [expected_function' (..read id)] + (check' assumptions {.#Apply expected_input expected_function'} {.#Apply actual})) + context) + {try.#Success output} + {try.#Success output} + + {try.#Failure _} + (case actual_function + {.#UnivQ _ _} + ((do ..monad + [actual' (..on actual_input actual_function)] + (check' assumptions {.#Apply expected} actual')) + context) + + {.#Ex exA} + ((do ..monad + [assumptions (check' assumptions expected_function actual_function)] + (check' assumptions expected_input actual_input)) + context) + + _ + ((do ..monad + [assumptions (check' assumptions expected_function actual_function) + expected' (..on expected_input actual_function) + actual' (..on actual_input actual_function)] + (check' assumptions expected' actual')) + context)))) + + [_ {.#Var id}] + (function (_ context) + (case ((do ..monad + [actual_function' (read id)] + (check' assumptions {.#Apply expected} {.#Apply actual_input actual_function'})) + context) + {try.#Success output} + {try.#Success output} + + _ + ((do ..monad + [assumptions (check' assumptions expected_function actual_function) + expected' (..on expected_input expected_function) + actual' (..on actual_input expected_function)] + (check' assumptions expected' actual')) + context))) + + _ + ..silent_failure!))) + +(def (with_exception exception parameter check) + (All (_ e a) (-> (Exception e) e (Check a) (Check a))) + (|>> check + (exception.with exception parameter))) + +... TODO: "check'" can be optimized... +... Type-check to ensure that the 'expected' type subsumes the 'actual' type. +(def (check' assumptions expected actual) + (Checker Type) + (if (for @.php + ... TODO: Remove this once JPHP is gone. + false + (same? expected actual)) + (check#in assumptions) + (with_exception ..type_check_failed [expected actual] + (case [expected actual] + [{.#Var idE} {.#Var idA}] + (check_vars check' assumptions idE idA) + + [{.#Var id} _] + (if_can_bind id actual + (check#in assumptions) + (function (_ bound) + (check' assumptions bound actual))) + + [_ {.#Var id}] + (if_can_bind id expected + (check#in assumptions) + (function (_ bound) + (check' assumptions expected bound))) + + (^.with_template [ ] + [[{.#Apply aE } {.#Apply aA }] + (check_apply check' assumptions [aE ] [aA ])]) + ([F1 {.#Ex ex}] + [{.#Ex exE} fA] + [fE {.#Var idA}] + [{.#Var idE} fA]) + + [{.#Apply A F} _] + (let [new_assumption [expected actual]] + (if (assumed? new_assumption assumptions) + (check#in assumptions) + (do ..monad + [expected' (..on A F)] + (check' {.#Item new_assumption assumptions} expected' actual)))) + + [_ {.#Apply A F}] + (do ..monad + [actual' (..on A F)] + (check' assumptions expected actual')) + + ... TODO: Refactor-away as cold-code + (^.with_template [ ] + [[{ _} _] + (do ..monad + [[_ paramT] + expected' (..on paramT expected)] + (check' assumptions expected' actual))]) + ([.#UnivQ ..existential] + [.#ExQ ..var]) + + ... TODO: Refactor-away as cold-code + (^.with_template [ ] + [[_ { _}] + (do ..monad + [[_ paramT] + actual' (..on paramT actual)] + (check' assumptions expected actual'))]) + ([.#UnivQ ..var] + [.#ExQ ..existential]) + + [{.#Primitive e_name e_params} {.#Primitive a_name a_params}] + (if (!text#= e_name a_name) + (loop (again [assumptions assumptions + e_params e_params + a_params a_params]) + (case [e_params a_params] + [{.#End} {.#End}] + (check#in assumptions) + + [{.#Item e_head e_tail} {.#Item a_head a_tail}] + (do ..monad + [assumptions' (check' assumptions e_head a_head)] + (again assumptions' e_tail a_tail)) + + _ + ..silent_failure!)) + ..silent_failure!) + + (^.with_template [] + [[{ eL eR} { aL aR}] + (do ..monad + [assumptions (check' assumptions eL aL)] + (check' assumptions eR aR))]) + ([.#Sum] + [.#Product]) + + [{.#Function eI eO} {.#Function aI aO}] + (do ..monad + [assumptions (check' assumptions aI eI)] + (check' assumptions eO aO)) + + [{.#Ex e!id} {.#Ex a!id}] + (if (!n#= e!id a!id) + (check#in assumptions) + ..silent_failure!) + + [{.#Named _ ?etype} _] + (check' assumptions ?etype actual) + + [_ {.#Named _ ?atype}] + (check' assumptions expected ?atype) + + _ + ..silent_failure!)))) + +(def .public (check expected actual) + (-> Type Type (Check Any)) + (check' (list) expected actual)) + +(def .public (subsumes? expected actual) + (-> Type Type Bit) + (case (..result ..fresh_context + (..check expected actual)) + {try.#Failure _} + false + + {try.#Success _} + true)) + +(def .public context + (Check Type_Context) + (function (_ context) + {try.#Success [context context]})) + +(def .public (with context) + (-> Type_Context (Check Any)) + (function (_ _) + {try.#Success [context []]})) + +(def .public (clean aliases inputT) + (-> (List Var) Type (Check Type)) + (case inputT + {.#Primitive name paramsT+} + (|> paramsT+ + (monad.each ..monad (clean aliases)) + (check#each (|>> {.#Primitive name}))) + + (^.or {.#Parameter _} {.#Ex _} {.#Named _}) + (check#in inputT) + + (^.with_template [] + [{ leftT rightT} + (do ..monad + [leftT' (clean aliases leftT)] + (|> (clean aliases rightT) + (check#each (|>> { leftT'}))))]) + ([.#Sum] [.#Product] [.#Function] [.#Apply]) + + {.#Var @it} + (case aliases + (pattern (list)) + (do ..monad + [?actualT (..peek @it)] + (case ?actualT + {.#Some actualT} + (clean aliases actualT) + + _ + (in inputT))) + + _ + (do ..monad + [:it: (..try (..identity aliases @it))] + (case :it: + {try.#Success :it:} + (case :it: + {.#Var _} + (in inputT) + + _ + (clean aliases :it:)) + + failure + (in inputT)))) + + (^.with_template [] + [{ envT+ unquantifiedT} + (do [! ..monad] + [envT+' (monad.each ! (clean aliases) envT+) + unquantifiedT' (clean aliases unquantifiedT)] + (in { envT+' unquantifiedT'}))]) + ([.#UnivQ] [.#ExQ]) + )) diff --git a/stdlib/source/library/lux/meta/type/dynamic.lux b/stdlib/source/library/lux/meta/type/dynamic.lux new file mode 100644 index 000000000..86ccf5753 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/dynamic.lux @@ -0,0 +1,56 @@ +(.require + [library + [lux (.except static) + ["[0]" debug] + [control + ["[0]" try (.only Try)] + ["[0]" exception (.only exception)]] + [data + [text + ["%" \\format]]] + [macro (.only with_symbols) + ["[0]" syntax (.only syntax)] + ["[0]" code + ["<[1]>" \\parser]]]]] + ["[0]" // (.only) + ["[0]" primitive (.only primitive)]]) + +(exception .public (wrong_type [expected Type + actual Type]) + (exception.report + "Expected" (%.type expected) + "Actual" (%.type actual))) + +(primitive .public Dynamic + [Type Any] + + (def abstraction + (-> [Type Any] Dynamic) + (|>> primitive.abstraction)) + + (def representation + (-> Dynamic [Type Any]) + (|>> primitive.representation)) + + (def .public dynamic + (syntax (_ [value .any]) + (with_symbols [g!value] + (in (list (` (.let [(~ g!value) (~ value)] + ((~! ..abstraction) [(.type_of (~ g!value)) (~ g!value)])))))))) + + (def .public static + (syntax (_ [type .any + value .any]) + (with_symbols [g!type g!value] + (in (list (` (.let [[(~ g!type) (~ g!value)] ((~! ..representation) (~ value))] + (.is ((~! try.Try) (~ type)) + (.if (.at (~! //.equivalence) (~' =) + (.type_literal (~ type)) (~ g!type)) + {try.#Success (.as (~ type) (~ g!value))} + ((~! exception.except) ..wrong_type [(.type_literal (~ type)) (~ g!type)])))))))))) + + (def .public (format value) + (-> Dynamic (Try Text)) + (let [[type value] (primitive.representation value)] + (debug.representation type value))) + ) diff --git a/stdlib/source/library/lux/meta/type/implicit.lux b/stdlib/source/library/lux/meta/type/implicit.lux new file mode 100644 index 000000000..977467202 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/implicit.lux @@ -0,0 +1,400 @@ +(.require + [library + [lux (.except with) + [abstract + ["[0]" monad (.only do)] + ["[0]" equivalence]] + [control + ["<>" parser] + ["[0]" maybe] + ["[0]" try]] + [data + ["[0]" product] + ["[0]" text (.use "[1]#[0]" equivalence) + ["%" \\format (.only format)]] + [collection + ["[0]" list (.use "[1]#[0]" monad mix)] + ["[0]" dictionary (.only Dictionary)]]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" code (.only) + ["<[1]>" \\parser (.only Parser)]]] + [math + ["[0]" number (.only) + ["n" nat]]]]] + ["[0]" // (.use "[1]#[0]" equivalence) + ["/[1]" //] + ["[0]" check (.only Check)]]) + +(def (type_var id env) + (-> Nat Type_Context (Meta Type)) + (case (list.example (|>> product.left (n.= id)) + (the .#var_bindings env)) + {.#Some [_ {.#Some type}]} + (case type + {.#Var id'} + (type_var id' env) + + _ + (at ///.monad in type)) + + {.#Some [_ {.#None}]} + (///.failure (format "Unbound type-var " (%.nat id))) + + {.#None} + (///.failure (format "Unknown type-var " (%.nat id))) + )) + +(def (implicit_type var_name) + (-> Symbol (Meta Type)) + (do ///.monad + [raw_type (///.type var_name) + compiler ///.compiler_state] + (case raw_type + {.#Var id} + (type_var id (the .#type_context compiler)) + + _ + (in raw_type)))) + +(def (member_type idx sig_type) + (-> Nat Type (Check Type)) + (case sig_type + {.#Named _ sig_type'} + (member_type idx sig_type') + + {.#Apply arg func} + (case (//.applied (list arg) func) + {.#None} + (check.failure (format "Cannot apply type " (%.type func) " to type " (%.type arg))) + + {.#Some sig_type'} + (member_type idx sig_type')) + + {.#Product left right} + (if (n.= 0 idx) + (at check.monad in left) + (member_type (-- idx) right)) + + _ + (if (n.= 0 idx) + (at check.monad in sig_type) + (check.failure (format "Cannot find member type " (%.nat idx) " for " (%.type sig_type)))))) + +(def (member_name member) + (-> Symbol (Meta Symbol)) + (case member + ["" simple_name] + (///.either (do ///.monad + [member (///.normal member) + _ (///.slot member)] + (in member)) + (do [! ///.monad] + [this_module_name ///.current_module_name + imp_mods (///.imported_modules this_module_name) + tag_lists (monad.each ! ///.tag_lists imp_mods) + .let [tag_lists (|> tag_lists list#conjoint (list#each product.left) list#conjoint) + candidates (list.only (|>> product.right (text#= simple_name)) + tag_lists)]] + (case candidates + {.#End} + (///.failure (format "Unknown tag: " (%.symbol member))) + + {.#Item winner {.#End}} + (in winner) + + _ + (///.failure (format "Too many candidate tags: " (%.list %.symbol candidates)))))) + + _ + (at ///.monad in member))) + +(def (implicit_member member) + (-> Symbol (Meta [Nat Type])) + (do ///.monad + [member (member_name member) + [idx tag_list sig_type] (///.slot member)] + (in [idx sig_type]))) + +(def (compatible_type? interface candidate) + (-> Type Type Bit) + (with_expansions [ (//#= interface candidate)] + (<| (or ) + + (let [[parameters candidate] (//.flat_univ_q candidate)]) + (or ) + + (let [[inputs candidate] (//.flat_function candidate)]) + (or ) + + (let [[candidate parameters] (//.flat_application candidate)]) + (or ) + + (let [candidate (//.de_aliased candidate)]) + ))) + +(def (available_definitions sig_type source_module target_module constants aggregate) + (-> Type Text Text (List [Text Definition]) (-> (List [Symbol Type]) (List [Symbol Type]))) + (list#mix (function (_ [name [exported? def_type def_value]] aggregate) + (if (and (or (text#= target_module source_module) + exported?) + (compatible_type? sig_type def_type)) + {.#Item [[source_module name] def_type] aggregate} + aggregate)) + aggregate + constants)) + +(def (local_env sig_type) + (-> Type (Meta (List [Symbol Type]))) + (do ///.monad + [local_batches ///.locals + .let [total_locals (list#mix (function (_ [name type] table) + (try.else table (dictionary.has' name type table))) + (is (Dictionary Text Type) + (dictionary.empty text.hash)) + (list#conjoint local_batches))]] + (in (|> total_locals + dictionary.entries + (list.all (function (_ [name type]) + (if (compatible_type? sig_type type) + {.#Some [["" name] type]} + {.#None}))))))) + +(def (local_structs sig_type) + (-> Type (Meta (List [Symbol Type]))) + (do [! ///.monad] + [this_module_name ///.current_module_name + definitions (///.definitions this_module_name)] + (in (available_definitions sig_type this_module_name this_module_name definitions {.#End})))) + +(def (imported_structs sig_type) + (-> Type (Meta (List [Symbol Type]))) + (do [! ///.monad] + [this_module_name ///.current_module_name + imported_modules (///.imported_modules this_module_name) + accessible_definitions (monad.each ! ///.definitions imported_modules)] + (in (list#mix (function (_ [imported_module definitions] tail) + (available_definitions sig_type imported_module this_module_name definitions tail)) + {.#End} + (list.zipped_2 imported_modules accessible_definitions))))) + +(def (on_argument arg func) + (-> Type Type (Check Type)) + (case func + {.#Named _ func'} + (on_argument arg func') + + {.#UnivQ _} + (do check.monad + [[id var] check.var] + (|> func + (//.applied (list var)) + maybe.trusted + (on_argument arg))) + + {.#Function input output} + (do check.monad + [_ (check.check input arg)] + (in output)) + + _ + (check.failure (format "Invalid function type: " (%.type func))))) + +(def (concrete_type type) + (-> Type (Check [(List Nat) Type])) + (case type + {.#UnivQ _} + (do check.monad + [[id var] check.var + [ids final_output] (concrete_type (maybe.trusted (//.applied (list var) type)))] + (in [{.#Item id ids} + final_output])) + + _ + (at check.monad in [(list) type]))) + +(def (ensure_function_application! member_type input_types expected_output) + (-> Type (List Type) Type (Check [])) + (do check.monad + [actual_output (monad.mix check.monad ..on_argument member_type input_types)] + (check.check expected_output actual_output))) + +(type Instance + (Rec Instance + (Record + [#constructor Symbol + #dependencies (List Instance)]))) + +(def (candidate_provision provision context dep alts) + (-> (-> Lux Type_Context Type (Check Instance)) + Type_Context Type (List [Symbol Type]) + (Meta (List Instance))) + (do ///.monad + [compiler ///.compiler_state] + (case (|> alts + (list#each (function (_ [alt_name alt_type]) + (case (check.result context + (do [! check.monad] + [[tvars alt_type] (concrete_type alt_type) + .let [[deps alt_type] (//.flat_function alt_type)] + _ (check.check dep alt_type) + context' check.context + =deps (monad.each ! (provision compiler context') deps)] + (in =deps))) + {.#Left error} + (list) + + {.#Right =deps} + (list [alt_name =deps])))) + list#conjoint) + {.#End} + (///.failure (format "No candidates for provisioning: " (%.type dep))) + + found + (in found)))) + +(def (provision sig_type compiler context dep) + (-> Type Lux Type_Context Type (Check Instance)) + (case (///.result compiler + (all ///.either + (do ///.monad [alts (..local_env sig_type)] (..candidate_provision (provision sig_type) context dep alts)) + (do ///.monad [alts (..local_structs sig_type)] (..candidate_provision (provision sig_type) context dep alts)) + (do ///.monad [alts (..imported_structs sig_type)] (..candidate_provision (provision sig_type) context dep alts)))) + {.#Left error} + (check.failure error) + + {.#Right candidates} + (case candidates + {.#End} + (check.failure (format "No candidates for provisioning: " (%.type dep))) + + {.#Item winner {.#End}} + (at check.monad in winner) + + _ + (check.failure (format "Too many candidates for provisioning: " (%.type dep) " --- " (%.list (|>> product.left %.symbol) candidates)))) + )) + +(def (candidate_alternatives sig_type member_idx input_types output_type alts) + (-> Type Nat (List Type) Type (List [Symbol Type]) (Meta (List Instance))) + (do ///.monad + [compiler ///.compiler_state + context ///.type_context] + (case (|> alts + (list#each (function (_ [alt_name alt_type]) + (case (<| (check.result context) + (do [! check.monad] + [[tvars alt_type] (concrete_type alt_type) + .let [[deps alt_type] (//.flat_function alt_type)] + _ (check.check alt_type sig_type) + member_type (member_type member_idx alt_type) + _ (ensure_function_application! member_type input_types output_type) + context' check.context + =deps (monad.each ! (provision sig_type compiler context') deps)] + (in =deps))) + {.#Left error} + (list) + + {.#Right =deps} + (list [alt_name =deps])))) + list#conjoint) + {.#End} + (///.failure (format "No alternatives for " (%.type (//.function input_types output_type)))) + + found + (in found)))) + +(def (alternatives sig_type member_idx input_types output_type) + (-> Type Nat (List Type) Type (Meta (List Instance))) + (let [test (candidate_alternatives sig_type member_idx input_types output_type)] + (all ///.either + (do ///.monad [alts (..local_env sig_type)] (test alts)) + (do ///.monad [alts (..local_structs sig_type)] (test alts)) + (do ///.monad [alts (..imported_structs sig_type)] (test alts))))) + +(def (var? input) + (-> Code Bit) + (case input + [_ {.#Symbol _}] + #1 + + _ + #0)) + +(def (pair_list [l r]) + (All (_ a) (-> [a a] (List a))) + (list l r)) + +(def (instance$ [constructor dependencies]) + (-> Instance Code) + (case dependencies + {.#End} + (code.symbol constructor) + + _ + (` ((~ (code.symbol constructor)) (~+ (list#each instance$ dependencies)))))) + +(def .public a/an + (syntax (_ [member .symbol + args (<>.or (<>.and (<>.some .symbol) .end) + (<>.and (<>.some .any) .end))]) + (case args + {.#Left [args _]} + (do [! ///.monad] + [[member_idx sig_type] (..implicit_member member) + input_types (monad.each ! ..implicit_type args) + output_type ///.expected_type + chosen_ones (alternatives sig_type member_idx input_types output_type)] + (case chosen_ones + {.#End} + (///.failure (format "No implementation could be found for member: " (%.symbol member))) + + {.#Item chosen {.#End}} + (in (list (` (.at (~ (instance$ chosen)) + (~ (code.local (product.right member))) + (~+ (list#each code.symbol args)))))) + + _ + (///.failure (format "Too many implementations available: " + (|> chosen_ones + (list#each (|>> product.left %.symbol)) + (text.interposed ", ")) + " --- for type: " (%.type sig_type))))) + + {.#Right [args _]} + (do [! ///.monad] + [labels (|> (macro.symbol "g!parameter") + (list.repeated (list.size args)) + (monad.all !))] + (in (list (` (let [(~+ (|> args (list.zipped_2 labels) (list#each ..pair_list) list#conjoint))] + (..a/an (~ (code.symbol member)) (~+ labels))))))) + ))) + +(def .public a ..a/an) +(def .public an ..a/an) + +(def (implicit_bindings amount) + (-> Nat (Meta (List Code))) + (|> (macro.symbol "g!implicit") + (list.repeated amount) + (monad.all ///.monad))) + +(def .public with + (syntax (_ [implementations (.tuple (<>.many .any)) + body .any]) + (do ///.monad + [g!implicit+ (implicit_bindings (list.size implementations))] + (in (list (` (let [(~+ (|> (list.zipped_2 g!implicit+ implementations) + (list#each (function (_ [g!implicit implementation]) + (list g!implicit implementation))) + list#conjoint))] + (~ body)))))))) + +(def .public implicitly + (syntax (_ [implementations (<>.many .any)]) + (do ///.monad + [g!implicit+ (implicit_bindings (list.size implementations))] + (in (|> (list.zipped_2 g!implicit+ implementations) + (list#each (function (_ [g!implicit implementation]) + (` (def .private (~ g!implicit) + (~ implementation)))))))))) diff --git a/stdlib/source/library/lux/meta/type/poly.lux b/stdlib/source/library/lux/meta/type/poly.lux new file mode 100644 index 000000000..95d9f8ea7 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/poly.lux @@ -0,0 +1,89 @@ +(.require + [library + [lux (.except) + [abstract + ["[0]" monad (.only do)]] + [control + ["<>" parser (.use "[1]#[0]" monad)] + ["[0]" maybe]] + [data + ["[0]" product] + ["[0]" text] + [collection + ["[0]" list (.use "[1]#[0]" functor)] + ["[0]" dictionary]]] + [macro (.only with_symbols) + [syntax (.only syntax)] + ["^" pattern] + ["[0]" code (.only) + ["<[1]>" \\parser (.only Parser)]]] + [math + [number + ["n" nat]]]]] + ["[0]" // (.only) + ["<[1]>" \\parser (.only Env)] + ["/[1]" //]]) + +(def .public polytypic + (syntax (_ [name .local + body .any]) + (with_symbols [g!_ g!type g!output] + (let [g!name (code.symbol ["" name])] + (in (.list (` ((~! syntax) ((~ g!_) [(~ g!type) (~! .any)]) + ((~! do) (~! ///.monad) + [(~ g!type) ((~! ///.eval) .Type (~ g!type))] + (case (is (.Either .Text .Code) + ((~! .result) ((~! <>.rec) + (function ((~ g!_) (~ g!name)) + (~ body))) + (.as .Type (~ g!type)))) + {.#Right (~ g!output)} + ((~' in) (.list (~ g!output))) + + {.#Left (~ g!output)} + ((~! ///.failure) (~ g!output)))))))))))) + +(def .public (code env type) + (-> Env Type Code) + (case type + {.#Primitive name params} + (` {.#Primitive (~ (code.text name)) + (.list (~+ (list#each (code env) params)))}) + + (^.with_template [] + [{ idx} + (` { (~ (code.nat idx))})]) + ([.#Var] [.#Ex]) + + {.#Parameter idx} + (let [idx (.argument env idx)] + (if (n.= 0 idx) + (|> (dictionary.value idx env) maybe.trusted product.left (code env)) + (` (.$ (~ (code.nat (-- idx))))))) + + {.#Apply {.#Primitive "" {.#End}} + {.#Parameter idx}} + (case (.argument env idx) + 0 (|> env (dictionary.value 0) maybe.trusted product.left (code env)) + idx (undefined)) + + (^.with_template [] + [{ left right} + (` { (~ (code env left)) + (~ (code env right))})]) + ([.#Function] [.#Apply]) + + (^.with_template [ ] + [{ left right} + (` ( (~+ (list#each (code env) ( type)))))]) + ([.Union .#Sum //.flat_variant] + [.Tuple .#Product //.flat_tuple]) + + {.#Named name sub_type} + (code.symbol name) + + (^.with_template [] + [{ scope body} + (` { (.list (~+ (list#each (code env) scope))) + (~ (code env body))})]) + ([.#UnivQ] [.#ExQ]))) diff --git a/stdlib/source/library/lux/meta/type/primitive.lux b/stdlib/source/library/lux/meta/type/primitive.lux new file mode 100644 index 000000000..50c288e1c --- /dev/null +++ b/stdlib/source/library/lux/meta/type/primitive.lux @@ -0,0 +1,105 @@ +(.require + [library + [lux (.except) + ["[0]" meta] + [abstract + [monad (.only do)]] + [control + ["<>" parser (.use "[1]#[0]" monad)]] + [data + ["[0]" text (.use "[1]#[0]" equivalence)] + [collection + ["[0]" list (.use "[1]#[0]" functor)]]] + ["[0]" macro (.only) + ["^" pattern] + ["[0]" context] + ["[0]" code (.only) + ["<[1]>" \\parser (.only Parser)]] + [syntax (.only syntax) + ["|[0]|" export]]] + [meta + ["[0]" symbol (.use "[1]#[0]" codec)]]]] + ["[0]" //]) + +(type .public Frame + (Record + [#name Text + #type_vars (List Code) + #abstraction Code + #representation Code])) + +(context.def [frames expression declaration] Frame) + +(.def .public current + (Meta Frame) + (context.peek ..frames)) + +(.def .public (specific name) + (-> Text (Meta Frame)) + (context.search ..frames (|>> (the #name) (text#= name)))) + +(def cast + (Parser [(Maybe Text) Code]) + (<>.either (<>.and (<>.maybe .local) .any) + (<>.and (<>#in {.#None}) .any))) + +(with_template [ ] + [(def .public + (syntax (_ [[frame value] ..cast]) + (do meta.monad + [[name type_vars abstraction representation] (case frame + {.#Some frame} + (..specific frame) + + {.#None} + ..current)] + (in (list (` ((~! //.as) [(~+ type_vars)] (~ ) (~ ) + (~ value))))))))] + + [abstraction representation abstraction] + [representation abstraction representation] + ) + +(def declarationP + (Parser [Text (List Text)]) + (<>.either (.form (<>.and .local (<>.some .local))) + (<>.and .local (at <>.monad in (list))))) + +(def abstract + (Parser [Code [Text (List Text)] Code (List Code)]) + (|export|.parser + (all <>.and + ..declarationP + .any + (<>.some .any) + ))) + +... TODO: Make sure the generated code always gets optimized away. +... (This applies to uses of "abstraction" and "representation") +(def .public primitive + (syntax (_ [[export_policy [name type_vars] representation_type primitives] + ..abstract]) + (do meta.monad + [current_module meta.current_module_name + g!Representation (macro.symbol "Representation") + .let [type_varsC (list#each code.local type_vars) + abstraction_declaration (` ((~ (code.local name)) (~+ type_varsC))) + representation_declaration (` ((~ g!Representation) (~+ type_varsC)))]] + (..declaration [name type_varsC abstraction_declaration representation_declaration] + (` (.these (type (~ export_policy) (~ abstraction_declaration) + (Primitive (~ (code.text (symbol#encoded [current_module name]))) + [(~+ type_varsC)])) + (type (~ representation_declaration) + (~ representation_type)) + (~+ primitives))))))) + +(def selection + (Parser [(List Code) Code]) + (<>.either (<>.and (<>#each (|>> list) .any) .any) + (<>.and (<>#in (list)) .any))) + +(def .public transmutation + (syntax (_ [[specific value] ..selection]) + (in (list (` (.|> (~ value) + (..representation (~+ specific)) + (..abstraction (~+ specific)))))))) diff --git a/stdlib/source/library/lux/meta/type/quotient.lux b/stdlib/source/library/lux/meta/type/quotient.lux new file mode 100644 index 000000000..72088cd46 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/quotient.lux @@ -0,0 +1,69 @@ +(.require + [library + [lux (.except type) + [abstract + [equivalence (only Equivalence)]] + [macro (.only with_symbols) + [syntax (.only syntax)] + ["[0]" code + ["<[1]>" \\parser]]]]] + ["[0]" // (.only) + [primitive (.except)]]) + +(primitive .public (Class t c %) + (-> t c) + + (def .public class + (All (_ t c) + (Ex (_ %) + (-> (-> t c) (Class t c %)))) + (|>> abstraction)) + + (primitive .public (Quotient t c %) + (Record + [#value t + #label c]) + + (def .public (quotient class value) + (All (_ t c %) + (-> (Class t c %) t + (Quotient t c %))) + (abstraction [#value value + #label ((representation Class class) value)])) + + (with_template [ ] + [(def .public + (All (_ t c %) (-> (Quotient t c %) )) + (|>> representation (the )))] + + [value t #value] + [label c #label] + ) + ) + ) + +(def .public type + (syntax (_ [class .any]) + ... TODO: Switch to the cleaner approach ASAP. + (with_symbols [g!t g!c g!% g!_ g!:quotient:] + (in (list (` (let [ ... (~ g!_) (.is (.Ex ((~ g!_) (~ g!t) (~ g!c) (~ g!%)) + ... (..Class (~ g!t) (~ g!c) (~ g!%))) + ... (~ class)) + ] + (.case (.type_of (~ class)) + {.#Apply (~ g!%) {.#Apply (~ g!c) {.#Apply (~ g!t) (~ g!:quotient:)}}} + (.type_literal (..Quotient (~ g!t) (~ g!c) (~ g!%))) + + (~ g!_) + (.undefined)))) + ... (` ((~! //.by_example) [(~ g!t) (~ g!c) (~ g!%)] + ... (is (..Class (~ g!t) (~ g!c) (~ g!%)) + ... (~ class)) + ... (..Quotient (~ g!t) (~ g!c) (~ g!%)))) + ))))) + +(def .public (equivalence super) + (All (_ t c %) (-> (Equivalence c) (Equivalence (..Quotient t c %)))) + (implementation + (def (= reference sample) + (at super = (..label reference) (..label sample))))) diff --git a/stdlib/source/library/lux/meta/type/refinement.lux b/stdlib/source/library/lux/meta/type/refinement.lux new file mode 100644 index 000000000..24e0aa2e2 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/refinement.lux @@ -0,0 +1,105 @@ +(.require + [library + [lux (.except only type) + [control + [function + [predicate (.only Predicate)]]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" code + ["<[1]>" \\parser]]]]] + ["[0]" // (.only) + [primitive (.except)]]) + +(primitive .public (Refined t %) + (Record + [#value t + #predicate (Predicate t)]) + + (.type .public (Refiner t %) + (-> t (Maybe (Refined t %)))) + + (def .public (refiner predicate) + (All (_ t) + (Ex (_ %) + (-> (Predicate t) (Refiner t %)))) + (function (_ value) + (if (predicate value) + {.#Some (abstraction [#value value + #predicate predicate])} + {.#None}))) + + (with_template [ ] + [(def .public + (All (_ t %) (-> (Refined t %) )) + (|>> representation (the )))] + + [value t #value] + [predicate (Predicate t) #predicate] + ) + + (def .public (lifted transform) + (All (_ t %) + (-> (-> t t) + (-> (Refined t %) (Maybe (Refined t %))))) + (function (_ refined) + (let [(open "_[0]") (representation refined) + value' (transform _#value)] + (if (_#predicate value') + {.#Some (abstraction [..#value value' + ..#predicate _#predicate])} + {.#None})))) + ) + +(def .public (only refiner values) + (All (_ t %) + (-> (Refiner t %) (List t) (List (Refined t %)))) + (case values + {.#End} + {.#End} + + {.#Item head tail} + (case (refiner head) + {.#Some refined} + {.#Item refined (only refiner tail)} + + {.#None} + (only refiner tail)))) + +(def .public (partition refiner values) + (All (_ t %) + (-> (Refiner t %) (List t) [(List (Refined t %)) (List t)])) + (case values + {.#End} + [{.#End} {.#End}] + + {.#Item head tail} + (let [[yes no] (partition refiner tail)] + (case (refiner head) + {.#Some refined} + [{.#Item refined yes} + no] + + {.#None} + [yes + {.#Item head no}])))) + +(def .public type + (syntax (_ [refiner .any]) + ... TODO: Switch to the cleaner approach ASAP. + (macro.with_symbols [g!t g!% g!_ g!:refiner:] + (in (list (` (let [ ... (~ g!_) (.is (.Ex ((~ g!_) (~ g!t) (~ g!%)) + ... (..Refined (~ g!t) (~ g!%))) + ... (~ refiner)) + ] + (.case (.type_of (~ refiner)) + {.#Apply (~ g!%) {.#Apply (~ g!t) (~ g!:refiner:)}} + (.type_literal (..Refined (~ g!t) (~ g!%))) + + (~ g!_) + (.undefined)))) + ... (` ((~! //.by_example) [(~ g!t) (~ g!%)] + ... (is (..Refiner (~ g!t) (~ g!%)) + ... (~ refiner)) + ... (..Refined (~ g!t) (~ g!%)))) + ))))) diff --git a/stdlib/source/library/lux/meta/type/resource.lux b/stdlib/source/library/lux/meta/type/resource.lux new file mode 100644 index 000000000..bd9e71c08 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/resource.lux @@ -0,0 +1,188 @@ +(.require + [library + [lux (.except) + ["[0]" meta] + [abstract + ["[0]" monad (.only Monad do) + [indexed (.only IxMonad)]]] + [control + ["<>" parser] + ["[0]" maybe] + ["[0]" exception (.only exception)]] + [data + [text + ["%" \\format (.only format)]] + [collection + ["[0]" set] + ["[0]" sequence (.only Sequence)] + ["[0]" list (.use "[1]#[0]" functor mix)]]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" code + ["<[1]>" \\parser (.only Parser)]]] + [math + [number + ["n" nat]]]]] + [// + [primitive (.except)]]) + +(type .public (Procedure monad input output value) + (-> input (monad [output value]))) + +(type .public (Linear monad value) + (All (_ keys) + (Procedure monad keys keys value))) + +(type .public (Affine monad permissions value) + (All (_ keys) + (Procedure monad keys [permissions keys] value))) + +(type .public (Relevant monad permissions value) + (All (_ keys) + (Procedure monad [permissions keys] keys value))) + +(def .public (monad monad) + (All (_ !) (-> (Monad !) (IxMonad (Procedure !)))) + (implementation + (def (in value) + (function (_ keys) + (at monad in [keys value]))) + + (def (then f input) + (function (_ keysI) + (do monad + [[keysT value] (input keysI)] + ((f value) keysT)))))) + +(def .public (run! monad procedure) + (All (_ ! v) (-> (Monad !) (Linear ! v) (! v))) + (do monad + [[_ output] (procedure [])] + (in output))) + +(def .public (lifted monad procedure) + (All (_ ! v) (-> (Monad !) (! v) (Linear ! v))) + (function (_ keys) + (do monad + [output procedure] + (in [keys output])))) + +(primitive .public Ordered Any) +(primitive .public Commutative Any) + +(primitive .public (Key mode key) + Any + + (with_template [ ] + [(def + (Ex (_ k) (-> Any (Key k))) + (|>> abstraction))] + + [ordered_key Ordered] + [commutative_key Commutative] + )) + +(primitive .public (Res key value) + value + + (with_template [ ] + [(def .public ( monad value) + (All (_ ! v) (Ex (_ k) (-> (Monad !) v (Affine ! (Key k) (Res k v))))) + (function (_ keys) + (at monad in [[( []) keys] (abstraction value)])))] + + [ordered Ordered ..ordered_key] + [commutative Commutative ..commutative_key] + ) + + (def .public (read monad resource) + (All (_ ! v k m) + (-> (Monad !) (Res k v) (Relevant ! (Key m k) v))) + (function (_ [key keys]) + (at monad in [keys (representation resource)]))) + ) + +(exception .public (index_cannot_be_repeated [index Nat]) + (exception.report + "Index" (%.nat index))) + +(exception .public amount_cannot_be_zero) + +(def indices + (Parser (List Nat)) + (.tuple (loop (again [seen (set.empty n.hash)]) + (do [! <>.monad] + [done? .end?] + (if done? + (in (list)) + (do ! + [head .nat + _ (<>.assertion (exception.error ..index_cannot_be_repeated head) + (not (set.member? seen head))) + tail (again (set.has head seen))] + (in (list.partial head tail)))))))) + +(def (no_op monad) + (All (_ m) (-> (Monad m) (Linear m Any))) + (function (_ context) + (at monad in [context []]))) + +(def .public exchange + (syntax (_ [swaps ..indices]) + (macro.with_symbols [g!_ g!context g!!] + (case swaps + {.#End} + (in (list (` (~! no_op)))) + + {.#Item head tail} + (do [! meta.monad] + [.let [max_idx (list#mix n.max head tail)] + g!inputs (<| (monad.all !) (list.repeated (++ max_idx)) (macro.symbol "input")) + .let [g!outputs (|> (monad.mix maybe.monad + (function (_ from to) + (do maybe.monad + [input (list.item from g!inputs)] + (in (sequence.suffix input to)))) + (is (Sequence Code) sequence.empty) + swaps) + maybe.trusted + sequence.list) + g!inputsT+ (list#each (|>> (~) (..Key ..Commutative) (`)) g!inputs) + g!outputsT+ (list#each (|>> (~) (..Key ..Commutative) (`)) g!outputs)]] + (in (list (` (is (All ((~ g!_) (~ g!!) (~+ g!inputs) (~ g!context)) + (-> ((~! monad.Monad) (~ g!!)) + (Procedure (~ g!!) + [(~+ g!inputsT+) (~ g!context)] + [(~+ g!outputsT+) (~ g!context)] + .Any))) + (function ((~ g!_) (~ g!!) [(~+ g!inputs) (~ g!context)]) + (at (~ g!!) (~' in) [[(~+ g!outputs) (~ g!context)] []]))))))))))) + +(def amount + (Parser Nat) + (do <>.monad + [raw .nat + _ (<>.assertion (exception.error ..amount_cannot_be_zero []) + (n.> 0 raw))] + (in raw))) + +(with_template [ ] + [(def .public + (syntax (_ [amount ..amount]) + (macro.with_symbols [g!_ g!context g!!] + (do [! meta.monad] + [g!keys (|> (macro.symbol "keys") + (list.repeated amount) + (monad.all !))] + (in (list (` (is (All ((~ g!_) (~ g!!) (~+ g!keys) (~ g!context)) + (-> ((~! monad.Monad) (~ g!!)) + (Procedure (~ g!!) + [ (~ g!context)] + [ (~ g!context)] + .Any))) + (function ((~ g!_) (~ g!!) [ (~ g!context)]) + (at (~ g!!) (~' in) [[ (~ g!context)] []]))))))))))] + + [group (~+ g!keys) [(~+ g!keys)]] + [un_group [(~+ g!keys)] (~+ g!keys)] + ) diff --git a/stdlib/source/library/lux/meta/type/unit.lux b/stdlib/source/library/lux/meta/type/unit.lux new file mode 100644 index 000000000..994e7ad11 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/unit.lux @@ -0,0 +1,103 @@ +(.require + [library + [lux (.except type) + [abstract + [equivalence (.only Equivalence)] + [order (.only Order)] + [enum (.only Enum)]] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" code + ["<[1]>" \\parser]]] + [math + [number + ["i" int]]]]] + ["[0]" // (.only) + [primitive (.except)]]) + +(primitive .public (Measure scale unit) + Int + + (def .public measure + (All (_ scale unit) (-> Int (Measure scale unit))) + (|>> abstraction)) + + (def .public number + (All (_ scale unit) (-> (Measure scale unit) Int)) + (|>> representation)) + + (def .public equivalence + (All (_ scale unit) (Equivalence (Measure scale unit))) + (implementation + (def (= reference sample) + (i.= (representation reference) (representation sample))))) + + (def .public order + (All (_ scale unit) (Order (Measure scale unit))) + (implementation + (def equivalence ..equivalence) + + (def (< reference sample) + (i.< (representation reference) (representation sample))))) + + (def .public enum + (All (_ scale unit) (Enum (Measure scale unit))) + (implementation + (def order ..order) + (def succ (|>> representation ++ abstraction)) + (def pred (|>> representation -- abstraction)))) + + (with_template [ ] + [(def .public ( param subject) + (All (_ scale unit) (-> (Measure scale unit) (Measure scale unit) (Measure scale unit))) + (abstraction ( (representation param) + (representation subject))))] + + [+ i.+] + [- i.-] + ) + + (with_template [

] + [(def .public ( param subject) + (All (_ scale p s) (-> (Measure scale

) (Measure scale ) (Measure scale ))) + (abstraction ( (representation param) + (representation subject))))] + + [* i.* p s [p s]] + [/ i./ p [p s] s] + ) + + (.type .public (Unit a) + (Interface + (is (-> Int (Measure Any a)) + in) + (is (-> (Measure Any a) Int) + out))) + + (def .public (unit _) + (Ex (_ a) (-> Any (Unit a))) + (implementation + (def in ..measure) + (def out ..number))) + ) + +(def .public type + (syntax (_ [it .any]) + (macro.with_symbols [g!a] + (in (list (` ((~! //.by_example) [(~ g!a)] + (is (..Unit (~ g!a)) + (~ it)) + (~ g!a)))))))) + +(with_template [ ] + [(def .public + (..unit [])) + + (.type .public + (~ (..type )))] + + [gram Gram] + [meter Meter] + [litre Litre] + [second Second] + ) diff --git a/stdlib/source/library/lux/meta/type/unit/scale.lux b/stdlib/source/library/lux/meta/type/unit/scale.lux new file mode 100644 index 000000000..b7f598d13 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/unit/scale.lux @@ -0,0 +1,78 @@ +(.require + [library + [lux (.except type) + [control] + ["[0]" macro (.only) + [syntax (.only syntax)] + ["[0]" code + ["<[1]>" \\parser]]] + [math + [number + ["i" int] + ["[0]" ratio (.only Ratio)]]]]] + ["[0]" // (.only) + ["/[1]" //]]) + +(.type .public (Scale s) + (Interface + (is (All (_ u) (-> (//.Measure Any u) (//.Measure s u))) + up) + (is (All (_ u) (-> (//.Measure s u) (//.Measure Any u))) + down) + (is Ratio + ratio))) + +(def .public (scale ratio) + (Ex (_ s) (-> Ratio (Scale s))) + (let [(open "/[0]") ratio] + (implementation + (def up + (|>> //.number + (i.* (.int /#numerator)) + (i./ (.int /#denominator)) + //.measure)) + (def down + (|>> //.number + (i.* (.int /#denominator)) + (i./ (.int /#numerator)) + //.measure)) + (def ratio + ratio)))) + +(def .public (re_scaled from to measure) + (All (_ si so u) (-> (Scale si) (Scale so) (//.Measure si u) (//.Measure so u))) + (let [(open "/[0]") (ratio./ (at from ratio) + (at to ratio))] + (|> measure + //.number + (i.* (.int /#numerator)) + (i./ (.int /#denominator)) + //.measure))) + +(def .public type + (syntax (_ [it .any]) + (macro.with_symbols [g!a] + (in (list (` ((~! ///.by_example) [(~ g!a)] + (is (..Scale (~ g!a)) + (~ it)) + (~ g!a)))))))) + +(with_template [ ] + [(def .public + (scale [ratio.#numerator + ratio.#denominator 1])) + + (.type .public + (~ (..type ))) + + (def .public + (scale [ratio.#numerator 1 + ratio.#denominator ])) + + (.type .public + (~ (..type )))] + + [ 1,000 kilo Kilo milli Milli] + [ 1,000,000 mega Mega micro Micro] + [1,000,000,000 giga Giga nano Nano ] + ) diff --git a/stdlib/source/library/lux/meta/type/variance.lux b/stdlib/source/library/lux/meta/type/variance.lux new file mode 100644 index 000000000..ac7e120d4 --- /dev/null +++ b/stdlib/source/library/lux/meta/type/variance.lux @@ -0,0 +1,45 @@ +(.require + [library + [lux (.except) + [meta + ["[0]" symbol]]]]) + +(type .public (Co it) + (-> Any it)) + +(type .public (Contra it) + (-> it Any)) + +(type .public (In it) + (-> it it)) + +(type .public (Mutable r w) + (Primitive "#Mutable" [(-> w r)])) + +(with_template [ ] + [(def .public + (template ( it) + [((.is (.All (_ r w) ) + (.|>> .as_expected)) + it)]))] + + [read (.-> (..Mutable r w) r)] + [write (.-> w (..Mutable r w))] + ) + +(type .public (Read_Only a) + (Mutable a Nothing)) + +(type .public (Write_Only a) + (Mutable Any a)) + +(with_template [ ] + [(def .public + (template ( it) + [((.is (.All (_ r w) ) + (.|>>)) + it)]))] + + [read_only (.-> (..Mutable r w) (..Read_Only r))] + [write_only (.-> (..Mutable r w) (..Write_Only w))] + ) diff --git a/stdlib/source/library/lux/target/common_lisp.lux b/stdlib/source/library/lux/target/common_lisp.lux index 7f93025a2..06fca5f8c 100644 --- a/stdlib/source/library/lux/target/common_lisp.lux +++ b/stdlib/source/library/lux/target/common_lisp.lux @@ -13,8 +13,9 @@ [math [number ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def as_form (-> Text Text) diff --git a/stdlib/source/library/lux/target/js.lux b/stdlib/source/library/lux/target/js.lux index 8665f2ce4..0c275562d 100644 --- a/stdlib/source/library/lux/target/js.lux +++ b/stdlib/source/library/lux/target/js.lux @@ -14,8 +14,9 @@ [number ["i" int] ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def expression (text.enclosed ["(" ")"])) diff --git a/stdlib/source/library/lux/target/jvm/bytecode/address.lux b/stdlib/source/library/lux/target/jvm/bytecode/address.lux index f1b07aa77..66b50f65a 100644 --- a/stdlib/source/library/lux/target/jvm/bytecode/address.lux +++ b/stdlib/source/library/lux/target/jvm/bytecode/address.lux @@ -14,8 +14,9 @@ [math [number ["n" nat]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [jump (.only Big_Jump)] ["/[1]" // diff --git a/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/registry.lux b/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/registry.lux index f1cc6058d..3f16fa4a2 100644 --- a/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/registry.lux +++ b/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/registry.lux @@ -13,8 +13,9 @@ [math [number ["n" nat]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" ///// [encoding ["[1][0]" unsigned (.only U1 U2)]] diff --git a/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/stack.lux b/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/stack.lux index daf9da304..7c7e0472e 100644 --- a/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/stack.lux +++ b/stdlib/source/library/lux/target/jvm/bytecode/environment/limit/stack.lux @@ -11,8 +11,9 @@ ["%" \\format]] [binary [\\format (.only Format)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" ///// [encoding ["[1][0]" unsigned (.only U2)]]]) diff --git a/stdlib/source/library/lux/target/jvm/bytecode/instruction.lux b/stdlib/source/library/lux/target/jvm/bytecode/instruction.lux index 1c654dae9..3b613b206 100644 --- a/stdlib/source/library/lux/target/jvm/bytecode/instruction.lux +++ b/stdlib/source/library/lux/target/jvm/bytecode/instruction.lux @@ -21,8 +21,9 @@ [math [number (.only hex) ["n" nat]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1][0]" address (.only Address)] ["[1][0]" jump (.only Jump Big_Jump)] diff --git a/stdlib/source/library/lux/target/jvm/constant.lux b/stdlib/source/library/lux/target/jvm/constant.lux index 516930b9d..ae57d805f 100644 --- a/stdlib/source/library/lux/target/jvm/constant.lux +++ b/stdlib/source/library/lux/target/jvm/constant.lux @@ -21,8 +21,9 @@ ["[0]" i64] ["[0]" int] ["[0]" frac]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" / ["[1][0]" tag] ["/[1]" // diff --git a/stdlib/source/library/lux/target/jvm/constant/tag.lux b/stdlib/source/library/lux/target/jvm/constant/tag.lux index 2b12af966..bcd1d4209 100644 --- a/stdlib/source/library/lux/target/jvm/constant/tag.lux +++ b/stdlib/source/library/lux/target/jvm/constant/tag.lux @@ -8,8 +8,9 @@ [data [binary [\\format (.only Format)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" /// [encoding ["[1][0]" unsigned (.only U1) (.use "u1//[0]" equivalence)]]]) diff --git a/stdlib/source/library/lux/target/jvm/encoding/name.lux b/stdlib/source/library/lux/target/jvm/encoding/name.lux index 246bb0575..7516cdc46 100644 --- a/stdlib/source/library/lux/target/jvm/encoding/name.lux +++ b/stdlib/source/library/lux/target/jvm/encoding/name.lux @@ -4,8 +4,9 @@ [data ["[0]" text (.only) ["%" \\format (.only format)]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def .public internal_separator "/") (def .public external_separator ".") diff --git a/stdlib/source/library/lux/target/jvm/encoding/signed.lux b/stdlib/source/library/lux/target/jvm/encoding/signed.lux index 30ec9a567..ba6304a39 100644 --- a/stdlib/source/library/lux/target/jvm/encoding/signed.lux +++ b/stdlib/source/library/lux/target/jvm/encoding/signed.lux @@ -19,8 +19,9 @@ ["[0]" i64] ["n" nat] ["i" int]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public (Signed brand) Int diff --git a/stdlib/source/library/lux/target/jvm/encoding/unsigned.lux b/stdlib/source/library/lux/target/jvm/encoding/unsigned.lux index eee130b27..bbc331384 100644 --- a/stdlib/source/library/lux/target/jvm/encoding/unsigned.lux +++ b/stdlib/source/library/lux/target/jvm/encoding/unsigned.lux @@ -18,8 +18,9 @@ [number ["n" nat] ["[0]" i64]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public (Unsigned brand) Nat diff --git a/stdlib/source/library/lux/target/jvm/index.lux b/stdlib/source/library/lux/target/jvm/index.lux index 1bae3b814..05489792b 100644 --- a/stdlib/source/library/lux/target/jvm/index.lux +++ b/stdlib/source/library/lux/target/jvm/index.lux @@ -6,8 +6,9 @@ [data [binary [\\format (.only Format)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [encoding ["[1][0]" unsigned (.only U2)]]]) diff --git a/stdlib/source/library/lux/target/jvm/modifier.lux b/stdlib/source/library/lux/target/jvm/modifier.lux index 05df8f292..9d135aa55 100644 --- a/stdlib/source/library/lux/target/jvm/modifier.lux +++ b/stdlib/source/library/lux/target/jvm/modifier.lux @@ -17,8 +17,9 @@ [math ["[0]" number (.only hex) ["[0]" i64]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [encoding ["[1][0]" unsigned]]]) diff --git a/stdlib/source/library/lux/target/jvm/modifier/inner.lux b/stdlib/source/library/lux/target/jvm/modifier/inner.lux index 1537dbe10..c61569575 100644 --- a/stdlib/source/library/lux/target/jvm/modifier/inner.lux +++ b/stdlib/source/library/lux/target/jvm/modifier/inner.lux @@ -1,8 +1,9 @@ (.require [library [lux (.except static) - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] [// (.only modifiers)]) (primitive .public Inner Any) diff --git a/stdlib/source/library/lux/target/jvm/type.lux b/stdlib/source/library/lux/target/jvm/type.lux index 3bb1f6411..9b90e6c28 100644 --- a/stdlib/source/library/lux/target/jvm/type.lux +++ b/stdlib/source/library/lux/target/jvm/type.lux @@ -14,8 +14,9 @@ [math [number ["n" nat]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [encoding ["[1][0]" name (.only External)]]] diff --git a/stdlib/source/library/lux/target/jvm/type/category.lux b/stdlib/source/library/lux/target/jvm/type/category.lux index 62a0a3a45..bbef2f241 100644 --- a/stdlib/source/library/lux/target/jvm/type/category.lux +++ b/stdlib/source/library/lux/target/jvm/type/category.lux @@ -3,8 +3,9 @@ [lux (.except Primitive) [macro ["[0]" template]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive Void' Any) (primitive .public (Value' kind) Any) diff --git a/stdlib/source/library/lux/target/jvm/type/descriptor.lux b/stdlib/source/library/lux/target/jvm/type/descriptor.lux index 332a1c128..a3635d767 100644 --- a/stdlib/source/library/lux/target/jvm/type/descriptor.lux +++ b/stdlib/source/library/lux/target/jvm/type/descriptor.lux @@ -13,8 +13,9 @@ [math [number ["n" nat]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [category (.only Void Value Return Method Primitive Object Class Array Var Parameter Declaration)] ["/[1]" // diff --git a/stdlib/source/library/lux/target/jvm/type/lux.lux b/stdlib/source/library/lux/target/jvm/type/lux.lux index 6f2ab6b47..724092721 100644 --- a/stdlib/source/library/lux/target/jvm/type/lux.lux +++ b/stdlib/source/library/lux/target/jvm/type/lux.lux @@ -15,9 +15,10 @@ [collection ["[0]" array] ["[0]" dictionary (.only Dictionary)]]] - [type - [":" primitive] - ["[0]" check (.only Check) (.use "[1]#[0]" monad)]]]] + [meta + [type + [":" primitive] + ["[0]" check (.only Check) (.use "[1]#[0]" monad)]]]]] ["[0]" // (.only) [category (.only Void Value Return Method Primitive Object Class Array Var Parameter)] ["[1][0]" descriptor] diff --git a/stdlib/source/library/lux/target/jvm/type/reflection.lux b/stdlib/source/library/lux/target/jvm/type/reflection.lux index cac395b22..de151b35d 100644 --- a/stdlib/source/library/lux/target/jvm/type/reflection.lux +++ b/stdlib/source/library/lux/target/jvm/type/reflection.lux @@ -6,8 +6,9 @@ [data ["[0]" text (.use "[1]#[0]" equivalence) ["%" \\format (.only format)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [category (.only Void Value Return Method Primitive Object Class Array Var Parameter Declaration)] ["[1][0]" descriptor] diff --git a/stdlib/source/library/lux/target/jvm/type/signature.lux b/stdlib/source/library/lux/target/jvm/type/signature.lux index cbde0203a..6afc33607 100644 --- a/stdlib/source/library/lux/target/jvm/type/signature.lux +++ b/stdlib/source/library/lux/target/jvm/type/signature.lux @@ -11,8 +11,9 @@ ["%" \\format (.only format)]] [collection ["[0]" list (.use "[1]#[0]" functor)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // [category (.only Void Value Return Method Primitive Object Class Array Var Parameter Declaration Inheritance)] ["[1][0]" descriptor] diff --git a/stdlib/source/library/lux/target/lua.lux b/stdlib/source/library/lux/target/lua.lux index f12cfbac6..8f8a3ed42 100644 --- a/stdlib/source/library/lux/target/lua.lux +++ b/stdlib/source/library/lux/target/lua.lux @@ -23,8 +23,9 @@ ["n" nat] ["i" int] ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) ... Added the carriage return for better Windows compatibility. (def \n+ diff --git a/stdlib/source/library/lux/target/php.lux b/stdlib/source/library/lux/target/php.lux index 2ad1863b6..2e11466f9 100644 --- a/stdlib/source/library/lux/target/php.lux +++ b/stdlib/source/library/lux/target/php.lux @@ -22,8 +22,9 @@ [number ["n" nat] ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def input_separator ", ") (def statement_suffix ";") diff --git a/stdlib/source/library/lux/target/python.lux b/stdlib/source/library/lux/target/python.lux index ddc601161..3237a638c 100644 --- a/stdlib/source/library/lux/target/python.lux +++ b/stdlib/source/library/lux/target/python.lux @@ -23,8 +23,9 @@ [number ["n" nat] ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (.def input_separator ", ") diff --git a/stdlib/source/library/lux/target/r.lux b/stdlib/source/library/lux/target/r.lux index 6d56eea58..4c6d87403 100644 --- a/stdlib/source/library/lux/target/r.lux +++ b/stdlib/source/library/lux/target/r.lux @@ -18,8 +18,9 @@ [math [number ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (primitive .public (Code kind) Text diff --git a/stdlib/source/library/lux/target/ruby.lux b/stdlib/source/library/lux/target/ruby.lux index 5a5f5af9d..b2dee4ea6 100644 --- a/stdlib/source/library/lux/target/ruby.lux +++ b/stdlib/source/library/lux/target/ruby.lux @@ -22,8 +22,9 @@ [number ["n" nat] ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def input_separator ", ") (def statement_suffix ";") diff --git a/stdlib/source/library/lux/target/scheme.lux b/stdlib/source/library/lux/target/scheme.lux index 0a2d66b7d..4173b4241 100644 --- a/stdlib/source/library/lux/target/scheme.lux +++ b/stdlib/source/library/lux/target/scheme.lux @@ -18,8 +18,9 @@ [number ["n" nat] ["f" frac]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) ... Added the carriage return for better Windows compatibility. (def \n+ diff --git a/stdlib/source/library/lux/time.lux b/stdlib/source/library/lux/time.lux index 3f57e5889..e020c4069 100644 --- a/stdlib/source/library/lux/time.lux +++ b/stdlib/source/library/lux/time.lux @@ -18,8 +18,9 @@ [math [number ["n" nat (.use "[1]#[0]" decimal)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] [/ ["[0]" duration (.only Duration)]]) diff --git a/stdlib/source/library/lux/time/date.lux b/stdlib/source/library/lux/time/date.lux index 78bd79237..8140b076b 100644 --- a/stdlib/source/library/lux/time/date.lux +++ b/stdlib/source/library/lux/time/date.lux @@ -22,8 +22,9 @@ [number ["n" nat (.use "[1]#[0]" decimal)] ["i" int]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1][0]" year (.only Year)] ["[1][0]" month (.only Month)]]) diff --git a/stdlib/source/library/lux/time/duration.lux b/stdlib/source/library/lux/time/duration.lux index b8ed4f776..00a7c1d1e 100644 --- a/stdlib/source/library/lux/time/duration.lux +++ b/stdlib/source/library/lux/time/duration.lux @@ -18,8 +18,9 @@ [number ["i" int] ["[0]" nat (.use "[1]#[0]" decimal)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[1][0]" year]]) diff --git a/stdlib/source/library/lux/time/instant.lux b/stdlib/source/library/lux/time/instant.lux index a453d5f58..2b58b5bf2 100644 --- a/stdlib/source/library/lux/time/instant.lux +++ b/stdlib/source/library/lux/time/instant.lux @@ -20,8 +20,9 @@ [number ["i" int] ["f" frac]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // (.only Time) ["[0]" duration (.only Duration)] ["[0]" year (.only Year)] diff --git a/stdlib/source/library/lux/time/year.lux b/stdlib/source/library/lux/time/year.lux index 494f3355b..02062e6aa 100644 --- a/stdlib/source/library/lux/time/year.lux +++ b/stdlib/source/library/lux/time/year.lux @@ -17,8 +17,9 @@ [number ["n" nat (.use "[1]#[0]" decimal)] ["i" int (.use "[1]#[0]" decimal)]]] - [type - [primitive (.except)]]]]) + [meta + [type + [primitive (.except)]]]]]) (def (internal year) (-> Int Int) diff --git a/stdlib/source/library/lux/tool/compiler/default/platform.lux b/stdlib/source/library/lux/tool/compiler/default/platform.lux index 492644edc..af29859b7 100644 --- a/stdlib/source/library/lux/tool/compiler/default/platform.lux +++ b/stdlib/source/library/lux/tool/compiler/default/platform.lux @@ -27,9 +27,9 @@ ["[0]" set (.only Set)] ["[0]" list (.use "[1]#[0]" monoid functor mix)]]] ["[0]" meta (.only) - ["[0]" configuration (.only Configuration)]] - [type (.only sharing) - ["[0]" check]] + ["[0]" configuration (.only Configuration)] + [type (.only sharing) + ["[0]" check]]] [world ["[0]" file (.only Path)] ["[0]" console]]]] diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/evaluation.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/evaluation.lux index d25341b39..402cf563a 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/evaluation.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/evaluation.lux @@ -1,8 +1,6 @@ (.require [library [lux (.except) - [type (.only sharing)] - ["[0]" meta] [abstract [monad (.only do)]] [control @@ -16,7 +14,9 @@ ["[0]" dictionary (.only Dictionary)]]] [math [number - ["n" nat]]]]] + ["n" nat]]] + ["[0]" meta (.only) + [type (.only sharing)]]]] ["[0]" // (.only Operation) [macro (.only Expander)] ["[1][0]" type] diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux index da4761411..e13058163 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux @@ -20,8 +20,9 @@ [math [number ["n" nat]]] - ["[0]" type (.only) - ["[0]" check]]]] + [meta + ["[0]" type (.only) + ["[0]" check]]]]] ["/" // (.only Analysis Operation Phase) ["[1][0]" type] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux index 182199934..6cfad0d9f 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux @@ -17,8 +17,9 @@ [math [number ["n" nat]]] - [type - ["[0]" check (.only Check)]]]] + [meta + [type + ["[0]" check (.only Check)]]]]] ["/" // (.only Operation) [// [phase diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/case.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/case.lux index ba5d13ca3..6f3c13d65 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/case.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/case.lux @@ -1,7 +1,6 @@ (.require [library [lux (.except case) - ["[0]" meta] [abstract ["[0]" monad (.only do)]] [control @@ -20,8 +19,9 @@ [macro ["^" pattern] ["[0]" code]] - ["[0]" type (.only) - ["[0]" check (.only Check)]]]] + ["[0]" meta (.only) + ["[0]" type (.only) + ["[0]" check (.only Check)]]]]] ["[0]" / ["/[1]" // ["[1][0]" complex] diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux index 3293fb170..c355ad0d1 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux @@ -1,7 +1,6 @@ (.require [library [lux (.except) - ["[0]" meta] [abstract ["[0]" monad (.only do)]] [control @@ -21,10 +20,10 @@ [math [number ["n" nat]]] - [meta - ["[0]" symbol]] - ["[0]" type (.only) - ["[0]" check]]]] + ["[0]" meta (.only) + ["[0]" symbol] + ["[0]" type (.only) + ["[0]" check]]]]] ["[0]" // ["[1][0]" simple] ["/[1]" // diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux index 4354f10a1..68d8ed9e4 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux @@ -1,7 +1,6 @@ (.require [library [lux (.except function) - ["[0]" meta] [abstract [monad (.only do)]] [control @@ -17,8 +16,9 @@ [math [number ["n" nat]]] - ["[0]" type (.only) - ["[0]" check]]]] + ["[0]" meta (.only) + ["[0]" type (.only) + ["[0]" check]]]]] ["[0]" /// ["[1][0]" extension] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/js.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/js.lux index 102e5adcf..580faf086 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/js.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/js.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target (.only) ["_" js]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux index d22d74aaf..cad6fe27b 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux @@ -2,7 +2,6 @@ [library [lux (.except Type Module Primitive char int type) ["[0]" ffi (.only import)] - ["[0]" meta] [abstract ["[0]" monad (.only do)]] [control @@ -57,8 +56,9 @@ ["[0]" parser] ["[0]" alias (.only Aliasing)] ["[0]T" lux (.only Mapping)]]]] - ["[0]" type (.only) - ["[0]" check (.only Check) (.use "[1]#[0]" monad)]]]] + ["[0]" meta (.only) + ["[0]" type (.only) + ["[0]" check (.only Check) (.use "[1]#[0]" monad)]]]]] ["[0]" // ["[1][0]" lux (.only custom)] ["/[1]" // (.only) diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lua.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lua.lux index 3c0e4cc86..d62efd51f 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lua.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lua.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target (.only) ["_" lua]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux index 75e4e8516..37ba8abe9 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux @@ -21,8 +21,9 @@ [math [number ["n" nat]]] - [type - ["[0]" check]] + [meta + [type + ["[0]" check]]] ["[0]" meta]]] ["[0]" /// (.only) ["[1][0]" bundle] diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/php.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/php.lux index 3852d2b24..3417bf78a 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/php.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/php.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target (.only) ["_" php]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/python.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/python.lux index 3c6e4b452..0712fe644 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/python.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/python.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target (.only) ["_" python]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/r.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/r.lux index a53133555..67f44e35a 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/r.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/r.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target ["_" r]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/ruby.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/ruby.lux index 3029aec9d..965f580b1 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/ruby.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/ruby.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target (.only) ["_" ruby]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/scheme.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/scheme.lux index bf1493940..5768379ce 100644 --- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/scheme.lux +++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/scheme.lux @@ -14,8 +14,9 @@ [macro ["[0]" code ["<[1]>" \\parser (.only Parser)]]] - ["[0]" type (.only) - ["[0]" check]] + [meta + ["[0]" type (.only) + ["[0]" check]]] ["@" target (.only) ["_" scheme]]]] [// diff --git a/stdlib/source/library/lux/tool/compiler/meta/archive.lux b/stdlib/source/library/lux/tool/compiler/meta/archive.lux index fd8a0c817..75612d11a 100644 --- a/stdlib/source/library/lux/tool/compiler/meta/archive.lux +++ b/stdlib/source/library/lux/tool/compiler/meta/archive.lux @@ -25,8 +25,9 @@ [math [number ["n" nat (.use "[1]#[0]" equivalence)]]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] [/ ["[0]" artifact] ["[0]" registry (.only Registry)] diff --git a/stdlib/source/library/lux/tool/compiler/meta/archive/key.lux b/stdlib/source/library/lux/tool/compiler/meta/archive/key.lux index 0e26e7718..24db1094f 100644 --- a/stdlib/source/library/lux/tool/compiler/meta/archive/key.lux +++ b/stdlib/source/library/lux/tool/compiler/meta/archive/key.lux @@ -1,8 +1,9 @@ (.require [library [lux (.except) - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] [// [signature (.only Signature)]]) diff --git a/stdlib/source/library/lux/tool/compiler/meta/archive/module/document.lux b/stdlib/source/library/lux/tool/compiler/meta/archive/module/document.lux index 64fae1ab4..46f7e2d5e 100644 --- a/stdlib/source/library/lux/tool/compiler/meta/archive/module/document.lux +++ b/stdlib/source/library/lux/tool/compiler/meta/archive/module/document.lux @@ -13,8 +13,9 @@ ["[0]" binary [\\parser (.only Parser)] ["[1]" \\format (.only Format)]]] - [type (.only sharing) - [primitive (.except)]]]] + [meta + [type (.only sharing) + [primitive (.except)]]]]] [/// ["[0]" signature (.only Signature) (.use "[1]#[0]" equivalence)] ["[0]" key (.only Key)]]) diff --git a/stdlib/source/library/lux/tool/compiler/meta/archive/registry.lux b/stdlib/source/library/lux/tool/compiler/meta/archive/registry.lux index ec61e4b79..b7c1e2e35 100644 --- a/stdlib/source/library/lux/tool/compiler/meta/archive/registry.lux +++ b/stdlib/source/library/lux/tool/compiler/meta/archive/registry.lux @@ -22,8 +22,9 @@ ["[0]" dictionary (.only Dictionary)]]] [macro ["^" pattern]] - [type - [primitive (.except)]]]] + [meta + [type + [primitive (.except)]]]]] ["[0]" // ["[0]" unit] ["[1]" artifact (.only Artifact ID) diff --git a/stdlib/source/library/lux/type.lux b/stdlib/source/library/lux/type.lux deleted file mode 100644 index 00afaddc0..000000000 --- a/stdlib/source/library/lux/type.lux +++ /dev/null @@ -1,515 +0,0 @@ -(.require - [library - [lux (.except function as let) - ["@" target] - [abstract - [equivalence (.only Equivalence)] - [monad (.only Monad do)]] - [control - ["<>" parser] - ["[0]" function] - ["[0]" maybe]] - [data - ["[0]" product] - ["[0]" text (.use "[1]#[0]" monoid equivalence)] - [collection - ["[0]" array] - ["[0]" list (.use "[1]#[0]" monad monoid mix)]]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["^" pattern] - ["[0]" code (.only) - ["<[1]>" \\parser (.only Parser)]]] - [math - [number - ["n" nat (.use "[1]#[0]" decimal)]]] - ["[0]" meta (.only) - ["[0]" location] - ["[0]" symbol (.use "[1]#[0]" equivalence codec)]]]]) - -(with_template [ ] - [(def .public ( type) - (-> Type [Nat Type]) - (loop (again [num_args 0 - type type]) - (case type - { env sub_type} - (again (++ num_args) sub_type) - - _ - [num_args type])))] - - [flat_univ_q .#UnivQ] - [flat_ex_q .#ExQ] - ) - -(def .public (flat_function type) - (-> Type [(List Type) Type]) - (case type - {.#Function in out'} - (.let [[ins out] (flat_function out')] - [(list.partial in ins) out]) - - _ - [(list) type])) - -(def .public (flat_application type) - (-> Type [Type (List Type)]) - (case type - {.#Apply arg func'} - (.let [[func args] (flat_application func')] - [func (list#composite args (list arg))]) - - _ - [type (list)])) - -(with_template [ ] - [(def .public ( type) - (-> Type (List Type)) - (case type - { left right} - (list.partial left ( right)) - - _ - (list type)))] - - [flat_variant .#Sum] - [flat_tuple .#Product] - ) - -(def .public (format type) - (-> Type Text) - (case type - {.#Primitive name params} - (all text#composite - "(Primitive " - (text.enclosed' text.double_quote name) - (|> params - (list#each (|>> format (text#composite " "))) - (list#mix (function.flipped text#composite) "")) - ")") - - (^.with_template [ ] - [{ _} - (all text#composite - (|> ( type) - (list#each format) - list.reversed - (list.interposed " ") - (list#mix text#composite "")) - )]) - ([.#Sum "(Or " ")" flat_variant] - [.#Product "[" "]" flat_tuple]) - - {.#Function input output} - (.let [[ins out] (flat_function type)] - (all text#composite "(-> " - (|> ins - (list#each format) - list.reversed - (list.interposed " ") - (list#mix text#composite "")) - " " (format out) ")")) - - {.#Parameter idx} - (n#encoded idx) - - {.#Var id} - (all text#composite "-" (n#encoded id)) - - {.#Ex id} - (all text#composite "+" (n#encoded id)) - - {.#Apply param fun} - (.let [[type_func type_args] (flat_application type)] - (all text#composite "(" (format type_func) " " (|> type_args (list#each format) list.reversed (list.interposed " ") (list#mix text#composite "")) ")")) - - (^.with_template [ ] - [{ env body} - (all text#composite "(" " {" (|> env (list#each format) (text.interposed " ")) "} " (format body) ")")]) - ([.#UnivQ "All"] - [.#ExQ "Ex"]) - - {.#Named [module name] type} - (all text#composite module "." name) - )) - -... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction -(def (reduced env type) - (-> (List Type) Type Type) - (case type - {.#Primitive name params} - {.#Primitive name (list#each (reduced env) params)} - - (^.with_template [] - [{ left right} - { (reduced env left) (reduced env right)}]) - ([.#Sum] [.#Product] - [.#Function] [.#Apply]) - - (^.with_template [] - [{ old_env def} - (case old_env - {.#End} - { env def} - - _ - { (list#each (reduced env) old_env) def})]) - ([.#UnivQ] - [.#ExQ]) - - {.#Parameter idx} - (maybe.else (panic! (all text#composite - "Unknown type parameter" text.new_line - " Index: " (n#encoded idx) text.new_line - "Environment: " (|> env - list.enumeration - (list#each (.function (_ [index type]) - (all text#composite - (n#encoded index) - " " (..format type)))) - (text.interposed (text#composite text.new_line " "))))) - (list.item idx env)) - - _ - type - )) - -(def .public equivalence - (Equivalence Type) - (implementation - (def (= x y) - (or (for @.php - ... TODO: Remove this once JPHP is gone. - false - (same? x y)) - (case [x y] - [{.#Primitive xname xparams} {.#Primitive yname yparams}] - (and (text#= xname yname) - (n.= (list.size yparams) (list.size xparams)) - (list#mix (.function (_ [x y] prev) (and prev (= x y))) - #1 - (list.zipped_2 xparams yparams))) - - (^.with_template [] - [[{ xid} { yid}] - (n.= yid xid)]) - ([.#Var] [.#Ex] [.#Parameter]) - - (^.or [{.#Function xleft xright} {.#Function yleft yright}] - [{.#Apply xleft xright} {.#Apply yleft yright}]) - (and (= xleft yleft) - (= xright yright)) - - [{.#Named xname xtype} {.#Named yname ytype}] - (and (symbol#= xname yname) - (= xtype ytype)) - - (^.with_template [] - [[{ xL xR} { yL yR}] - (and (= xL yL) (= xR yR))]) - ([.#Sum] [.#Product]) - - (^.or [{.#UnivQ xenv xbody} {.#UnivQ yenv ybody}] - [{.#ExQ xenv xbody} {.#ExQ yenv ybody}]) - (and (n.= (list.size yenv) (list.size xenv)) - (= xbody ybody) - (list#mix (.function (_ [x y] prev) (and prev (= x y))) - #1 - (list.zipped_2 xenv yenv))) - - _ - #0 - ))))) - -(def .public (applied params func) - (-> (List Type) Type (Maybe Type)) - (case params - {.#End} - {.#Some func} - - {.#Item param params'} - (case func - (^.with_template [] - [{ env body} - (|> body - (reduced (list.partial func param env)) - (applied params'))]) - ([.#UnivQ] [.#ExQ]) - - {.#Apply A F} - (applied (list.partial A params) F) - - {.#Named name unnamed} - (applied params unnamed) - - _ - {.#None}))) - -(def .public (code type) - (-> Type Code) - (case type - {.#Primitive name params} - (` {.#Primitive (~ (code.text name)) - (.list (~+ (list#each code params)))}) - - (^.with_template [] - [{ idx} - (` { (~ (code.nat idx))})]) - ([.#Var] [.#Ex] [.#Parameter]) - - (^.with_template [] - [{ left right} - (` { (~ (code left)) - (~ (code right))})]) - ([.#Sum] [.#Product] [.#Function] [.#Apply]) - - {.#Named name sub_type} - (code.symbol name) - - (^.with_template [] - [{ env body} - (` { (.list (~+ (list#each code env))) - (~ (code body))})]) - ([.#UnivQ] [.#ExQ]) - )) - -(def .public (de_aliased type) - (-> Type Type) - (case type - {.#Named _ {.#Named name type'}} - (de_aliased {.#Named name type'}) - - _ - type)) - -(def .public (anonymous type) - (-> Type Type) - (case type - {.#Named name type'} - (anonymous type') - - _ - type)) - -(with_template [ ] - [(def .public ( types) - (-> (List Type) Type) - (case types - {.#End} - - - {.#Item type {.#End}} - type - - {.#Item type types'} - { type ( types')}))] - - [variant Nothing .#Sum] - [tuple Any .#Product] - ) - -(def .public (function inputs output) - (-> (List Type) Type Type) - (case inputs - {.#End} - output - - {.#Item input inputs'} - {.#Function input (function inputs' output)})) - -(def .public (application params quant) - (-> (List Type) Type Type) - (case params - {.#End} - quant - - {.#Item param params'} - (application params' {.#Apply param quant}))) - -(with_template [ ] - [(def .public ( size body) - (-> Nat Type Type) - (case size - 0 body - _ (|> body ( (-- size)) { (list)})))] - - [univ_q .#UnivQ] - [ex_q .#ExQ] - ) - -(def .public (quantified? type) - (-> Type Bit) - (case type - {.#Named [module name] _type} - (quantified? _type) - - {.#Apply A F} - (|> (..applied (list A) F) - (at maybe.monad each quantified?) - (maybe.else #0)) - - (^.or {.#UnivQ _} {.#ExQ _}) - #1 - - _ - #0)) - -(def .public (array depth element_type) - (-> Nat Type Type) - (case depth - 0 element_type - _ (|> element_type - (array (-- depth)) - (list) - {.#Primitive array.type_name}))) - -(def .public (flat_array type) - (-> Type [Nat Type]) - (case type - (^.multi (pattern {.#Primitive name (list element_type)}) - (text#= array.type_name name)) - (.let [[depth element_type] (flat_array element_type)] - [(++ depth) element_type]) - - _ - [0 type])) - -(def .public array? - (-> Type Bit) - (|>> ..flat_array - product.left - (n.> 0))) - -(def new_secret_marker - (syntax (_ []) - (macro.with_symbols [g!_secret_marker_] - (in (list g!_secret_marker_))))) - -(def secret_marker - (`` (symbol (~~ (new_secret_marker))))) - -(def .public log! - (syntax (_ [input (<>.or (<>.and .symbol - (<>.maybe (<>.after (.this_symbol ..secret_marker) .any))) - .any)]) - (case input - {.#Left [valueN valueC]} - (do meta.monad - [location meta.location - valueT (meta.type valueN) - .let [_ ("lux io log" - (all text#composite - (symbol#encoded (symbol ..log!)) " " (location.format location) text.new_line - "Expression: " (case valueC - {.#Some valueC} - (code.format valueC) - - {.#None} - (symbol#encoded valueN)) - text.new_line - " Type: " (..format valueT)))]] - (in (list (code.symbol valueN)))) - - {.#Right valueC} - (macro.with_symbols [g!value] - (in (list (` (.let [(~ g!value) (~ valueC)] - (..log! (~ valueC) (~ (code.symbol ..secret_marker)) (~ g!value)))))))))) - -(def type_parameters - (Parser (List Text)) - (.tuple (<>.some .local))) - -(def .public as - (syntax (_ [type_vars type_parameters - input .any - output .any - value (<>.maybe .any)]) - (macro.with_symbols [g!_] - (.let [casterC (` (is (All ((~ g!_) (~+ (list#each code.local type_vars))) - (-> (~ input) (~ output))) - (|>> as_expected)))] - (case value - {.#None} - (in (list casterC)) - - {.#Some value} - (in (list (` ((~ casterC) (~ value)))))))))) - -(type Typed - (Record - [#type Code - #expression Code])) - -(def (typed lux) - (-> Lux (Parser Typed)) - (do <>.monad - [it .any - type_check (<>.lifted (meta.result lux (macro.expansion it)))] - (<| (.locally type_check) - .form - (<>.after (.this (` "lux type check"))) - (<>.and .any .any)))) - -... TODO: Make sure the generated code always gets optimized away. -(def .public sharing - (syntax (_ lux [type_vars ..type_parameters - exemplar (..typed lux) - computation (..typed lux)]) - (macro.with_symbols [g!_] - (.let [typeC (` (All ((~ g!_) (~+ (list#each code.local type_vars))) - (-> (~ (the #type exemplar)) - (~ (the #type computation))))) - shareC (` (is (~ typeC) - (.function ((~ g!_) (~ g!_)) - (~ (the #expression computation)))))] - (in (list (` ((~ shareC) (~ (the #expression exemplar)))))))))) - -(def .public by_example - (syntax (_ lux [type_vars ..type_parameters - exemplar (..typed lux) - extraction .any]) - (in (list (` (.type_of ((~! ..sharing) [(~+ (list#each code.local type_vars))] - (is (~ (the #type exemplar)) - (~ (the #expression exemplar))) - (is (~ extraction) - ... The value of this expression will never be relevant, so it doesn't matter what it is. - (.as .Nothing []))))))))) - -(def .public (replaced before after) - (-> Type Type Type Type) - (.function (again it) - (if (at ..equivalence = before it) - after - (case it - {.#Primitive name co_variant} - {.#Primitive name (list#each again co_variant)} - - (^.with_template [] - [{ left right} - { (again left) (again right)}]) - ([.#Sum] - [.#Product] - [.#Function] - [.#Apply]) - - (^.with_template [] - [{ env body} - { (list#each again env) (again body)}]) - ([.#UnivQ] - [.#ExQ]) - - (^.or {.#Parameter _} - {.#Var _} - {.#Ex _} - {.#Named _}) - it)))) - -(def .public let - (syntax (_ [bindings (.tuple (<>.some (<>.and .any .any))) - bodyT .any]) - (in (list (` (..with_expansions [(~+ (|> bindings - (list#each (.function (_ [localT valueT]) - (list localT (` (.these (~ valueT)))))) - list#conjoint))] - (~ bodyT))))))) diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux deleted file mode 100644 index cb49cc6e4..000000000 --- a/stdlib/source/library/lux/type/check.lux +++ /dev/null @@ -1,829 +0,0 @@ -(.require - [library - [lux (.except try except with) - ["@" target] - [abstract - [functor (.only Functor)] - [apply (.only Apply)] - ["[0]" monad (.only Monad do)]] - [control - ["[0]" maybe] - ["[0]" try (.only Try)] - ["[0]" exception (.only Exception exception)]] - [data - ["[0]" product] - ["[0]" text (.use "[1]#[0]" monoid equivalence)] - [collection - ["[0]" list (.use "[1]#[0]" mix)] - ["[0]" set (.only Set)]]] - [macro - ["^" pattern]] - [math - [number - ["n" nat (.use "[1]#[0]" decimal)]]]]] - ["[0]" // (.use "[1]#[0]" equivalence)]) - -(def !n#= - (template (_ reference subject) - [("lux i64 =" reference subject)])) - -(def !text#= - (template (_ reference subject) - [("lux text =" reference subject)])) - -(exception .public (unknown_type_var [id Nat]) - (exception.report - "ID" (n#encoded id))) - -(exception .public (unbound_type_var [id Nat]) - (exception.report - "ID" (n#encoded id))) - -(exception .public (invalid_type_application [funcT Type - argT Type]) - (exception.report - "Type function" (//.format funcT) - "Type argument" (//.format argT))) - -(exception .public (cannot_rebind_var [id Nat - type Type - bound Type]) - (exception.report - "Var" (n#encoded id) - "Wanted Type" (//.format type) - "Current Type" (//.format bound))) - -(exception .public (type_check_failed [expected Type - actual Type]) - (exception.report - "Expected" (//.format expected) - "Actual" (//.format actual))) - -(type .public Var - Nat) - -(type Assumption - [Type Type]) - -(type .public (Check a) - (-> Type_Context (Try [Type_Context a]))) - -(type (Checker a) - (-> (List Assumption) a a (Check (List Assumption)))) - -(type Type_Vars - (List [Var (Maybe Type)])) - -(def .public functor - (Functor Check) - (implementation - (def (each f fa) - (function (_ context) - (case (fa context) - {try.#Success [context' output]} - {try.#Success [context' (f output)]} - - {try.#Failure error} - {try.#Failure error}))))) - -(def .public apply - (Apply Check) - (implementation - (def functor ..functor) - - (def (on fa ff) - (function (_ context) - (case (ff context) - {try.#Success [context' f]} - (case (fa context') - {try.#Success [context'' a]} - {try.#Success [context'' (f a)]} - - {try.#Failure error} - {try.#Failure error}) - - {try.#Failure error} - {try.#Failure error} - ))) - )) - -(def .public monad - (Monad Check) - (implementation - (def functor ..functor) - - (def (in x) - (function (_ context) - {try.#Success [context x]})) - - (def (conjoint ffa) - (function (_ context) - (case (ffa context) - {try.#Success [context' fa]} - (case (fa context') - {try.#Success [context'' a]} - {try.#Success [context'' a]} - - {try.#Failure error} - {try.#Failure error}) - - {try.#Failure error} - {try.#Failure error} - ))) - )) - -(use "check#[0]" ..monad) - -(def (var::new id property_list) - (-> Var Type_Vars Type_Vars) - {.#Item [id {.#None}] property_list}) - -(def (var::get id property_list) - (-> Var Type_Vars (Maybe (Maybe Type))) - (case property_list - {.#Item [var_id var_type] - property_list'} - (if (!n#= id var_id) - {.#Some var_type} - (var::get id property_list')) - - {.#End} - {.#None})) - -(def (var::put id value property_list) - (-> Var (Maybe Type) Type_Vars Type_Vars) - (case property_list - {.#End} - (list [id value]) - - {.#Item [var_id var_type] - property_list'} - (if (!n#= id var_id) - {.#Item [var_id value] - property_list'} - {.#Item [var_id var_type] - (var::put id value property_list')}))) - -(def .public (result context proc) - (All (_ a) (-> Type_Context (Check a) (Try a))) - (case (proc context) - {try.#Success [context' output]} - {try.#Success output} - - {try.#Failure error} - {try.#Failure error})) - -(def .public (failure message) - (All (_ a) (-> Text (Check a))) - (function (_ context) - {try.#Failure message})) - -(def .public (assertion message test) - (-> Text Bit (Check Any)) - (function (_ context) - (if test - {try.#Success [context []]} - {try.#Failure message}))) - -(def .public (except exception message) - (All (_ e a) (-> (Exception e) e (Check a))) - (..failure (exception.error exception message))) - -(def .public existential - (Check [Nat Type]) - (function (_ context) - (let [id (the .#ex_counter context)] - {try.#Success [(revised .#ex_counter ++ context) - [id {.#Ex id}]]}))) - -(with_template [ ] - [(def .public ( id) - (-> Var (Check )) - (function (_ context) - (case (|> context (the .#var_bindings) (var::get id)) - (^.or {.#Some {.#Some {.#Var _}}} - {.#Some {.#None}}) - {try.#Success [context ]} - - {.#Some {.#Some bound}} - {try.#Success [context ]} - - {.#None} - (exception.except ..unknown_type_var id))))] - - [bound? Bit false true] - [peek (Maybe Type) {.#None} {.#Some bound}] - ) - -(def .public (read id) - (-> Var (Check Type)) - (do ..monad - [?type (peek id)] - (case ?type - {.#Some type} - (in type) - - {.#None} - (..except ..unbound_type_var id)))) - -(def (bound id) - (-> Var (Check Type)) - (function (_ context) - (case (|> context (the .#var_bindings) (var::get id)) - {.#Some {.#Some bound}} - {try.#Success [context bound]} - - {.#Some _} - (exception.except ..unbound_type_var id) - - _ - (exception.except ..unknown_type_var id)))) - -(def .public (bind type id) - (-> Type Var (Check Any)) - (function (_ context) - (case (|> context (the .#var_bindings) (var::get id)) - {.#Some {.#None}} - {try.#Success [(revised .#var_bindings (var::put id {.#Some type}) context) - []]} - - {.#Some {.#Some bound}} - (exception.except ..cannot_rebind_var [id type bound]) - - _ - (exception.except ..unknown_type_var id)))) - -(def (re_bind' ?type id) - (-> (Maybe Type) Var (Check Any)) - (function (_ context) - (case (|> context (the .#var_bindings) (var::get id)) - {.#Some _} - {try.#Success [(revised .#var_bindings (var::put id ?type) context) - []]} - - _ - (exception.except ..unknown_type_var id)))) - -(def (re_bind type id) - (-> Type Var (Check Any)) - (re_bind' {.#Some type} id)) - -(def .public var - (Check [Var Type]) - (function (_ context) - (let [id (the .#var_counter context)] - {try.#Success [(|> context - (revised .#var_counter ++) - (revised .#var_bindings (var::new id))) - [id {.#Var id}]]}))) - -(def (on argT funcT) - (-> Type Type (Check Type)) - (case funcT - {.#Var func_id} - (do ..monad - [?funcT' (peek func_id)] - (case ?funcT' - {.#Some funcT'} - (on argT funcT') - - _ - (except ..invalid_type_application [funcT argT]))) - - {.#Apply argT' funcT'} - (do ..monad - [funcT'' (on argT' funcT')] - (on argT funcT'')) - - _ - (case (//.applied (list argT) funcT) - {.#Some output} - (check#in output) - - _ - (except ..invalid_type_application [funcT argT])))) - -(def .public (ring' start) - (-> Var (Check (List Var))) - (function (_ context) - (loop (again [current start - output (list start)]) - (case (|> context (the .#var_bindings) (var::get current)) - {.#Some {.#Some type}} - (case type - {.#Var next} - (if (!n#= start next) - {try.#Success [context output]} - (again next (list.partial next output))) - - _ - {try.#Success [context (list)]}) - - {.#Some {.#None}} - {try.#Success [context output]} - - {.#None} - (exception.except ..unknown_type_var current))))) - -... TODO: Optimize this by not using sets anymore. -(def ring - (-> Var (Check (Set Var))) - (|>> ..ring' - (check#each (set.of_list n.hash)))) - -(def .public (linked? @0 @1) - (-> Var Var (Check Bit)) - (check#each (function (_ it) - (set.member? it @1)) - (..ring @0))) - -(exception .public (cannot_identify [var Var]) - (exception.report - "Var" (n#encoded var))) - -(def .public (identity aliases @) - (-> (List Var) Var (Check Type)) - (do [! ..monad] - [:bound: (..peek @)] - (case :bound: - {.#Some :bound:} - (in :bound:) - - {.#None} - (do ! - [existing_aliases (..ring @)] - (if (n.< 2 (set.size existing_aliases)) - (..except ..cannot_identify [@]) - (do ! - [.let [forbidden_aliases (set.of_list n.hash (list.partial @ aliases)) - allowed_aliases (set.difference forbidden_aliases existing_aliases)]] - (case (set.list allowed_aliases) - {.#Item identity _} - (in {.#Var identity}) - - {.#None} - (..except ..cannot_identify [@])))))))) - -(def (erase! @) - (-> Var (Check Any)) - (function (_ context) - {try.#Success [(revised .#var_bindings - (list#mix (is (//.let [binding [Nat (Maybe Type)]] - (-> binding - (List binding) - (List binding))) - (function (_ in out) - (let [[@var :var:] in] - (if (n.= @ @var) - out - (list.partial in out))))) - (is (List [Nat (Maybe Type)]) - (list))) - context) - []]})) - -(def .public (forget! @) - (-> Var (Check Any)) - (do [! ..monad] - [ring (..ring' @)] - (case ring - (pattern (list)) - (in []) - - (pattern (list @me)) - (erase! @me) - - (pattern (list @other @me)) - (do ! - [_ (re_bind' {.#None} @other)] - (erase! @me)) - - (pattern (list.partial @prev _)) - (case (list.reversed ring) - (pattern (list.partial @me @next _)) - (do ! - [_ (re_bind {.#Var @next} @prev) - _ (re_bind {.#Var @prev} @next)] - (erase! @me)) - - _ - (undefined))))) - -(def .public (try it) - (All (_ a) (-> (Check a) (Check (Try a)))) - (function (_ context) - (case (it context) - {try.#Success [context' output]} - {try.#Success [context' {try.#Success output}]} - - {try.#Failure error} - {try.#Success [context {try.#Failure error}]}))) - -(def .public fresh_context - Type_Context - [.#var_counter 0 - .#ex_counter 0 - .#var_bindings (list)]) - -(def (either left right) - (All (_ a) (-> (Check a) (Check a) (Check a))) - (function (_ context) - (case (left context) - {try.#Failure _} - (right context) - - output - output))) - -(def (assumed? [e a] assumptions) - (-> Assumption (List Assumption) Bit) - (list.any? (function (_ [e' a']) - (and (//#= e e') - (//#= a a'))) - assumptions)) - -... TODO: "if_can_bind" can be optimized... -(def (if_can_bind id type then else) - (All (_ a) - (-> Var Type (Check a) (-> Type (Check a)) - (Check a))) - (all either - (do ..monad - [_ (..bind type id)] - then) - (do [! ..monad] - [ring (..ring id) - _ (..assertion "" (n.> 1 (set.size ring))) - _ (monad.each ! (re_bind type) (set.list ring))] - then) - (do ..monad - [?bound (peek id)] - (else (maybe.else {.#Var id} ?bound))))) - -... TODO: "link/2" can be optimized... -(def (link/2 left right) - (-> Var Var (Check Any)) - (do ..monad - [_ (..bind {.#Var right} left)] - (..bind {.#Var left} right))) - -... TODO: "link/3" can be optimized... -(def (link/3 interpose to from) - (-> Var Var Var (Check Any)) - (do ..monad - [_ (re_bind {.#Var interpose} from)] - (re_bind {.#Var to} interpose))) - -... TODO: "check_vars" can be optimized... -(def (check_vars check' assumptions idE idA) - (-> (Checker Type) (Checker Var)) - (if (!n#= idE idA) - (check#in assumptions) - (do [! ..monad] - [ebound (..try (..bound idE)) - abound (..try (..bound idA))] - (case [ebound abound] - ... Link the 2 variables circularly - [{try.#Failure _} {try.#Failure _}] - (do ! - [_ (link/2 idE idA)] - (in assumptions)) - - ... Interpose new variable between 2 existing links - [{try.#Success etype} {try.#Failure _}] - (case etype - {.#Var targetE} - (do ! - [_ (link/3 idA targetE idE)] - (in assumptions)) - - _ - (check' assumptions etype {.#Var idA})) - - ... Interpose new variable between 2 existing links - [{try.#Failure _} {try.#Success atype}] - (case atype - {.#Var targetA} - (do ! - [_ (link/3 idE targetA idA)] - (in assumptions)) - - _ - (check' assumptions {.#Var idE} atype)) - - [{try.#Success etype} {try.#Success atype}] - (case [etype atype] - [{.#Var targetE} {.#Var targetA}] - (do ! - [ringE (..ring idE) - ringA (..ring idA)] - (if (at set.equivalence = ringE ringA) - (in assumptions) - ... Fuse 2 rings - (do ! - [_ (monad.mix ! (function (_ interpose to) - (do ! - [_ (link/3 interpose to idE)] - (in interpose))) - targetE - (set.list ringA))] - (in assumptions)))) - - (^.with_template [ ] - [ - (do ! - [ring (..ring ) - _ (monad.each ! (re_bind ) (set.list ring))] - (in assumptions))]) - ([[{.#Var _} _] idE atype] - [[_ {.#Var _}] idA etype]) - - _ - (check' assumptions etype atype)))))) - -(def silent_failure! - (All (_ a) (Check a)) - (..failure "")) - -... TODO: "check_apply" can be optimized... -(def (check_apply check' assumptions expected actual) - (-> (Checker Type) (Checker [Type Type])) - (let [[expected_input expected_function] expected - [actual_input actual_function] actual] - (case [expected_function actual_function] - [{.#Ex exE} {.#Ex exA}] - (if (!n#= exE exA) - (check' assumptions expected_input actual_input) - ..silent_failure!) - - [{.#UnivQ _ _} {.#Ex _}] - (do ..monad - [expected' (..on expected_input expected_function)] - (check' assumptions expected' {.#Apply actual})) - - [{.#Ex _} {.#UnivQ _ _}] - (do ..monad - [actual' (..on actual_input actual_function)] - (check' assumptions {.#Apply expected} actual')) - - [{.#Apply [expected_input' expected_function']} {.#Ex _}] - (do ..monad - [expected_function'' (..on expected_input' expected_function')] - (check' assumptions {.#Apply [expected_input expected_function'']} {.#Apply actual})) - - [{.#Ex _} {.#Apply [actual_input' actual_function']}] - (do ..monad - [actual_function'' (..on actual_input' actual_function')] - (check' assumptions {.#Apply expected} {.#Apply [actual_input actual_function'']})) - - (^.or [{.#Ex _} _] [_ {.#Ex _}]) - (do ..monad - [assumptions (check' assumptions expected_function actual_function)] - (check' assumptions expected_input actual_input)) - - [{.#Var id} _] - (function (_ context) - (case ((do ..monad - [expected_function' (..read id)] - (check' assumptions {.#Apply expected_input expected_function'} {.#Apply actual})) - context) - {try.#Success output} - {try.#Success output} - - {try.#Failure _} - (case actual_function - {.#UnivQ _ _} - ((do ..monad - [actual' (..on actual_input actual_function)] - (check' assumptions {.#Apply expected} actual')) - context) - - {.#Ex exA} - ((do ..monad - [assumptions (check' assumptions expected_function actual_function)] - (check' assumptions expected_input actual_input)) - context) - - _ - ((do ..monad - [assumptions (check' assumptions expected_function actual_function) - expected' (..on expected_input actual_function) - actual' (..on actual_input actual_function)] - (check' assumptions expected' actual')) - context)))) - - [_ {.#Var id}] - (function (_ context) - (case ((do ..monad - [actual_function' (read id)] - (check' assumptions {.#Apply expected} {.#Apply actual_input actual_function'})) - context) - {try.#Success output} - {try.#Success output} - - _ - ((do ..monad - [assumptions (check' assumptions expected_function actual_function) - expected' (..on expected_input expected_function) - actual' (..on actual_input expected_function)] - (check' assumptions expected' actual')) - context))) - - _ - ..silent_failure!))) - -(def (with_exception exception parameter check) - (All (_ e a) (-> (Exception e) e (Check a) (Check a))) - (|>> check - (exception.with exception parameter))) - -... TODO: "check'" can be optimized... -... Type-check to ensure that the 'expected' type subsumes the 'actual' type. -(def (check' assumptions expected actual) - (Checker Type) - (if (for @.php - ... TODO: Remove this once JPHP is gone. - false - (same? expected actual)) - (check#in assumptions) - (with_exception ..type_check_failed [expected actual] - (case [expected actual] - [{.#Var idE} {.#Var idA}] - (check_vars check' assumptions idE idA) - - [{.#Var id} _] - (if_can_bind id actual - (check#in assumptions) - (function (_ bound) - (check' assumptions bound actual))) - - [_ {.#Var id}] - (if_can_bind id expected - (check#in assumptions) - (function (_ bound) - (check' assumptions expected bound))) - - (^.with_template [ ] - [[{.#Apply aE } {.#Apply aA }] - (check_apply check' assumptions [aE ] [aA ])]) - ([F1 {.#Ex ex}] - [{.#Ex exE} fA] - [fE {.#Var idA}] - [{.#Var idE} fA]) - - [{.#Apply A F} _] - (let [new_assumption [expected actual]] - (if (assumed? new_assumption assumptions) - (check#in assumptions) - (do ..monad - [expected' (..on A F)] - (check' {.#Item new_assumption assumptions} expected' actual)))) - - [_ {.#Apply A F}] - (do ..monad - [actual' (..on A F)] - (check' assumptions expected actual')) - - ... TODO: Refactor-away as cold-code - (^.with_template [ ] - [[{ _} _] - (do ..monad - [[_ paramT] - expected' (..on paramT expected)] - (check' assumptions expected' actual))]) - ([.#UnivQ ..existential] - [.#ExQ ..var]) - - ... TODO: Refactor-away as cold-code - (^.with_template [ ] - [[_ { _}] - (do ..monad - [[_ paramT] - actual' (..on paramT actual)] - (check' assumptions expected actual'))]) - ([.#UnivQ ..var] - [.#ExQ ..existential]) - - [{.#Primitive e_name e_params} {.#Primitive a_name a_params}] - (if (!text#= e_name a_name) - (loop (again [assumptions assumptions - e_params e_params - a_params a_params]) - (case [e_params a_params] - [{.#End} {.#End}] - (check#in assumptions) - - [{.#Item e_head e_tail} {.#Item a_head a_tail}] - (do ..monad - [assumptions' (check' assumptions e_head a_head)] - (again assumptions' e_tail a_tail)) - - _ - ..silent_failure!)) - ..silent_failure!) - - (^.with_template [] - [[{ eL eR} { aL aR}] - (do ..monad - [assumptions (check' assumptions eL aL)] - (check' assumptions eR aR))]) - ([.#Sum] - [.#Product]) - - [{.#Function eI eO} {.#Function aI aO}] - (do ..monad - [assumptions (check' assumptions aI eI)] - (check' assumptions eO aO)) - - [{.#Ex e!id} {.#Ex a!id}] - (if (!n#= e!id a!id) - (check#in assumptions) - ..silent_failure!) - - [{.#Named _ ?etype} _] - (check' assumptions ?etype actual) - - [_ {.#Named _ ?atype}] - (check' assumptions expected ?atype) - - _ - ..silent_failure!)))) - -(def .public (check expected actual) - (-> Type Type (Check Any)) - (check' (list) expected actual)) - -(def .public (subsumes? expected actual) - (-> Type Type Bit) - (case (..result ..fresh_context - (..check expected actual)) - {try.#Failure _} - false - - {try.#Success _} - true)) - -(def .public context - (Check Type_Context) - (function (_ context) - {try.#Success [context context]})) - -(def .public (with context) - (-> Type_Context (Check Any)) - (function (_ _) - {try.#Success [context []]})) - -(def .public (clean aliases inputT) - (-> (List Var) Type (Check Type)) - (case inputT - {.#Primitive name paramsT+} - (|> paramsT+ - (monad.each ..monad (clean aliases)) - (check#each (|>> {.#Primitive name}))) - - (^.or {.#Parameter _} {.#Ex _} {.#Named _}) - (check#in inputT) - - (^.with_template [] - [{ leftT rightT} - (do ..monad - [leftT' (clean aliases leftT)] - (|> (clean aliases rightT) - (check#each (|>> { leftT'}))))]) - ([.#Sum] [.#Product] [.#Function] [.#Apply]) - - {.#Var @it} - (case aliases - (pattern (list)) - (do ..monad - [?actualT (..peek @it)] - (case ?actualT - {.#Some actualT} - (clean aliases actualT) - - _ - (in inputT))) - - _ - (do ..monad - [:it: (..try (..identity aliases @it))] - (case :it: - {try.#Success :it:} - (case :it: - {.#Var _} - (in inputT) - - _ - (clean aliases :it:)) - - failure - (in inputT)))) - - (^.with_template [] - [{ envT+ unquantifiedT} - (do [! ..monad] - [envT+' (monad.each ! (clean aliases) envT+) - unquantifiedT' (clean aliases unquantifiedT)] - (in { envT+' unquantifiedT'}))]) - ([.#UnivQ] [.#ExQ]) - )) diff --git a/stdlib/source/library/lux/type/dynamic.lux b/stdlib/source/library/lux/type/dynamic.lux deleted file mode 100644 index fd98afcdf..000000000 --- a/stdlib/source/library/lux/type/dynamic.lux +++ /dev/null @@ -1,56 +0,0 @@ -(.require - [library - [lux (.except static) - ["[0]" debug] - [control - ["[0]" try (.only Try)] - ["[0]" exception (.only exception)]] - [data - [text - ["%" \\format]]] - [macro (.only with_symbols) - ["[0]" syntax (.only syntax)] - ["[0]" code - ["<[1]>" \\parser]]] - ["[0]" type (.only) - ["[0]" primitive (.only primitive)]]]]) - -(exception .public (wrong_type [expected Type - actual Type]) - (exception.report - "Expected" (%.type expected) - "Actual" (%.type actual))) - -(primitive .public Dynamic - [Type Any] - - (def abstraction - (-> [Type Any] Dynamic) - (|>> primitive.abstraction)) - - (def representation - (-> Dynamic [Type Any]) - (|>> primitive.representation)) - - (def .public dynamic - (syntax (_ [value .any]) - (with_symbols [g!value] - (in (list (` (.let [(~ g!value) (~ value)] - ((~! ..abstraction) [(.type_of (~ g!value)) (~ g!value)])))))))) - - (def .public static - (syntax (_ [type .any - value .any]) - (with_symbols [g!type g!value] - (in (list (` (.let [[(~ g!type) (~ g!value)] ((~! ..representation) (~ value))] - (.is ((~! try.Try) (~ type)) - (.if (.at (~! type.equivalence) (~' =) - (.type_literal (~ type)) (~ g!type)) - {try.#Success (.as (~ type) (~ g!value))} - ((~! exception.except) ..wrong_type [(.type_literal (~ type)) (~ g!type)])))))))))) - - (def .public (format value) - (-> Dynamic (Try Text)) - (let [[type value] (primitive.representation value)] - (debug.representation type value))) - ) diff --git a/stdlib/source/library/lux/type/implicit.lux b/stdlib/source/library/lux/type/implicit.lux deleted file mode 100644 index f831c551b..000000000 --- a/stdlib/source/library/lux/type/implicit.lux +++ /dev/null @@ -1,400 +0,0 @@ -(.require - [library - [lux (.except with) - [abstract - ["[0]" monad (.only do)] - ["[0]" equivalence]] - [control - ["<>" parser] - ["[0]" maybe] - ["[0]" try]] - [data - ["[0]" product] - ["[0]" text (.use "[1]#[0]" equivalence) - ["%" \\format (.only format)]] - [collection - ["[0]" list (.use "[1]#[0]" monad mix)] - ["[0]" dictionary (.only Dictionary)]]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" code (.only) - ["<[1]>" \\parser (.only Parser)]]] - [math - ["[0]" number (.only) - ["n" nat]]] - ["[0]" meta] - ["[0]" type (.use "[1]#[0]" equivalence) - ["[0]" check (.only Check)]]]]) - -(def (type_var id env) - (-> Nat Type_Context (Meta Type)) - (case (list.example (|>> product.left (n.= id)) - (the .#var_bindings env)) - {.#Some [_ {.#Some type}]} - (case type - {.#Var id'} - (type_var id' env) - - _ - (at meta.monad in type)) - - {.#Some [_ {.#None}]} - (meta.failure (format "Unbound type-var " (%.nat id))) - - {.#None} - (meta.failure (format "Unknown type-var " (%.nat id))) - )) - -(def (implicit_type var_name) - (-> Symbol (Meta Type)) - (do meta.monad - [raw_type (meta.type var_name) - compiler meta.compiler_state] - (case raw_type - {.#Var id} - (type_var id (the .#type_context compiler)) - - _ - (in raw_type)))) - -(def (member_type idx sig_type) - (-> Nat Type (Check Type)) - (case sig_type - {.#Named _ sig_type'} - (member_type idx sig_type') - - {.#Apply arg func} - (case (type.applied (list arg) func) - {.#None} - (check.failure (format "Cannot apply type " (%.type func) " to type " (%.type arg))) - - {.#Some sig_type'} - (member_type idx sig_type')) - - {.#Product left right} - (if (n.= 0 idx) - (at check.monad in left) - (member_type (-- idx) right)) - - _ - (if (n.= 0 idx) - (at check.monad in sig_type) - (check.failure (format "Cannot find member type " (%.nat idx) " for " (%.type sig_type)))))) - -(def (member_name member) - (-> Symbol (Meta Symbol)) - (case member - ["" simple_name] - (meta.either (do meta.monad - [member (meta.normal member) - _ (meta.slot member)] - (in member)) - (do [! meta.monad] - [this_module_name meta.current_module_name - imp_mods (meta.imported_modules this_module_name) - tag_lists (monad.each ! meta.tag_lists imp_mods) - .let [tag_lists (|> tag_lists list#conjoint (list#each product.left) list#conjoint) - candidates (list.only (|>> product.right (text#= simple_name)) - tag_lists)]] - (case candidates - {.#End} - (meta.failure (format "Unknown tag: " (%.symbol member))) - - {.#Item winner {.#End}} - (in winner) - - _ - (meta.failure (format "Too many candidate tags: " (%.list %.symbol candidates)))))) - - _ - (at meta.monad in member))) - -(def (implicit_member member) - (-> Symbol (Meta [Nat Type])) - (do meta.monad - [member (member_name member) - [idx tag_list sig_type] (meta.slot member)] - (in [idx sig_type]))) - -(def (compatible_type? interface candidate) - (-> Type Type Bit) - (with_expansions [ (type#= interface candidate)] - (<| (or ) - - (let [[parameters candidate] (type.flat_univ_q candidate)]) - (or ) - - (let [[inputs candidate] (type.flat_function candidate)]) - (or ) - - (let [[candidate parameters] (type.flat_application candidate)]) - (or ) - - (let [candidate (type.de_aliased candidate)]) - ))) - -(def (available_definitions sig_type source_module target_module constants aggregate) - (-> Type Text Text (List [Text Definition]) (-> (List [Symbol Type]) (List [Symbol Type]))) - (list#mix (function (_ [name [exported? def_type def_value]] aggregate) - (if (and (or (text#= target_module source_module) - exported?) - (compatible_type? sig_type def_type)) - {.#Item [[source_module name] def_type] aggregate} - aggregate)) - aggregate - constants)) - -(def (local_env sig_type) - (-> Type (Meta (List [Symbol Type]))) - (do meta.monad - [local_batches meta.locals - .let [total_locals (list#mix (function (_ [name type] table) - (try.else table (dictionary.has' name type table))) - (is (Dictionary Text Type) - (dictionary.empty text.hash)) - (list#conjoint local_batches))]] - (in (|> total_locals - dictionary.entries - (list.all (function (_ [name type]) - (if (compatible_type? sig_type type) - {.#Some [["" name] type]} - {.#None}))))))) - -(def (local_structs sig_type) - (-> Type (Meta (List [Symbol Type]))) - (do [! meta.monad] - [this_module_name meta.current_module_name - definitions (meta.definitions this_module_name)] - (in (available_definitions sig_type this_module_name this_module_name definitions {.#End})))) - -(def (imported_structs sig_type) - (-> Type (Meta (List [Symbol Type]))) - (do [! meta.monad] - [this_module_name meta.current_module_name - imported_modules (meta.imported_modules this_module_name) - accessible_definitions (monad.each ! meta.definitions imported_modules)] - (in (list#mix (function (_ [imported_module definitions] tail) - (available_definitions sig_type imported_module this_module_name definitions tail)) - {.#End} - (list.zipped_2 imported_modules accessible_definitions))))) - -(def (on_argument arg func) - (-> Type Type (Check Type)) - (case func - {.#Named _ func'} - (on_argument arg func') - - {.#UnivQ _} - (do check.monad - [[id var] check.var] - (|> func - (type.applied (list var)) - maybe.trusted - (on_argument arg))) - - {.#Function input output} - (do check.monad - [_ (check.check input arg)] - (in output)) - - _ - (check.failure (format "Invalid function type: " (%.type func))))) - -(def (concrete_type type) - (-> Type (Check [(List Nat) Type])) - (case type - {.#UnivQ _} - (do check.monad - [[id var] check.var - [ids final_output] (concrete_type (maybe.trusted (type.applied (list var) type)))] - (in [{.#Item id ids} - final_output])) - - _ - (at check.monad in [(list) type]))) - -(def (ensure_function_application! member_type input_types expected_output) - (-> Type (List Type) Type (Check [])) - (do check.monad - [actual_output (monad.mix check.monad ..on_argument member_type input_types)] - (check.check expected_output actual_output))) - -(type Instance - (Rec Instance - (Record - [#constructor Symbol - #dependencies (List Instance)]))) - -(def (candidate_provision provision context dep alts) - (-> (-> Lux Type_Context Type (Check Instance)) - Type_Context Type (List [Symbol Type]) - (Meta (List Instance))) - (do meta.monad - [compiler meta.compiler_state] - (case (|> alts - (list#each (function (_ [alt_name alt_type]) - (case (check.result context - (do [! check.monad] - [[tvars alt_type] (concrete_type alt_type) - .let [[deps alt_type] (type.flat_function alt_type)] - _ (check.check dep alt_type) - context' check.context - =deps (monad.each ! (provision compiler context') deps)] - (in =deps))) - {.#Left error} - (list) - - {.#Right =deps} - (list [alt_name =deps])))) - list#conjoint) - {.#End} - (meta.failure (format "No candidates for provisioning: " (%.type dep))) - - found - (in found)))) - -(def (provision sig_type compiler context dep) - (-> Type Lux Type_Context Type (Check Instance)) - (case (meta.result compiler - (all meta.either - (do meta.monad [alts (..local_env sig_type)] (..candidate_provision (provision sig_type) context dep alts)) - (do meta.monad [alts (..local_structs sig_type)] (..candidate_provision (provision sig_type) context dep alts)) - (do meta.monad [alts (..imported_structs sig_type)] (..candidate_provision (provision sig_type) context dep alts)))) - {.#Left error} - (check.failure error) - - {.#Right candidates} - (case candidates - {.#End} - (check.failure (format "No candidates for provisioning: " (%.type dep))) - - {.#Item winner {.#End}} - (at check.monad in winner) - - _ - (check.failure (format "Too many candidates for provisioning: " (%.type dep) " --- " (%.list (|>> product.left %.symbol) candidates)))) - )) - -(def (candidate_alternatives sig_type member_idx input_types output_type alts) - (-> Type Nat (List Type) Type (List [Symbol Type]) (Meta (List Instance))) - (do meta.monad - [compiler meta.compiler_state - context meta.type_context] - (case (|> alts - (list#each (function (_ [alt_name alt_type]) - (case (<| (check.result context) - (do [! check.monad] - [[tvars alt_type] (concrete_type alt_type) - .let [[deps alt_type] (type.flat_function alt_type)] - _ (check.check alt_type sig_type) - member_type (member_type member_idx alt_type) - _ (ensure_function_application! member_type input_types output_type) - context' check.context - =deps (monad.each ! (provision sig_type compiler context') deps)] - (in =deps))) - {.#Left error} - (list) - - {.#Right =deps} - (list [alt_name =deps])))) - list#conjoint) - {.#End} - (meta.failure (format "No alternatives for " (%.type (type.function input_types output_type)))) - - found - (in found)))) - -(def (alternatives sig_type member_idx input_types output_type) - (-> Type Nat (List Type) Type (Meta (List Instance))) - (let [test (candidate_alternatives sig_type member_idx input_types output_type)] - (all meta.either - (do meta.monad [alts (..local_env sig_type)] (test alts)) - (do meta.monad [alts (..local_structs sig_type)] (test alts)) - (do meta.monad [alts (..imported_structs sig_type)] (test alts))))) - -(def (var? input) - (-> Code Bit) - (case input - [_ {.#Symbol _}] - #1 - - _ - #0)) - -(def (pair_list [l r]) - (All (_ a) (-> [a a] (List a))) - (list l r)) - -(def (instance$ [constructor dependencies]) - (-> Instance Code) - (case dependencies - {.#End} - (code.symbol constructor) - - _ - (` ((~ (code.symbol constructor)) (~+ (list#each instance$ dependencies)))))) - -(def .public a/an - (syntax (_ [member .symbol - args (<>.or (<>.and (<>.some .symbol) .end) - (<>.and (<>.some .any) .end))]) - (case args - {.#Left [args _]} - (do [! meta.monad] - [[member_idx sig_type] (..implicit_member member) - input_types (monad.each ! ..implicit_type args) - output_type meta.expected_type - chosen_ones (alternatives sig_type member_idx input_types output_type)] - (case chosen_ones - {.#End} - (meta.failure (format "No implementation could be found for member: " (%.symbol member))) - - {.#Item chosen {.#End}} - (in (list (` (.at (~ (instance$ chosen)) - (~ (code.local (product.right member))) - (~+ (list#each code.symbol args)))))) - - _ - (meta.failure (format "Too many implementations available: " - (|> chosen_ones - (list#each (|>> product.left %.symbol)) - (text.interposed ", ")) - " --- for type: " (%.type sig_type))))) - - {.#Right [args _]} - (do [! meta.monad] - [labels (|> (macro.symbol "g!parameter") - (list.repeated (list.size args)) - (monad.all !))] - (in (list (` (let [(~+ (|> args (list.zipped_2 labels) (list#each ..pair_list) list#conjoint))] - (..a/an (~ (code.symbol member)) (~+ labels))))))) - ))) - -(def .public a ..a/an) -(def .public an ..a/an) - -(def (implicit_bindings amount) - (-> Nat (Meta (List Code))) - (|> (macro.symbol "g!implicit") - (list.repeated amount) - (monad.all meta.monad))) - -(def .public with - (syntax (_ [implementations (.tuple (<>.many .any)) - body .any]) - (do meta.monad - [g!implicit+ (implicit_bindings (list.size implementations))] - (in (list (` (let [(~+ (|> (list.zipped_2 g!implicit+ implementations) - (list#each (function (_ [g!implicit implementation]) - (list g!implicit implementation))) - list#conjoint))] - (~ body)))))))) - -(def .public implicitly - (syntax (_ [implementations (<>.many .any)]) - (do meta.monad - [g!implicit+ (implicit_bindings (list.size implementations))] - (in (|> (list.zipped_2 g!implicit+ implementations) - (list#each (function (_ [g!implicit implementation]) - (` (def .private (~ g!implicit) - (~ implementation)))))))))) diff --git a/stdlib/source/library/lux/type/poly.lux b/stdlib/source/library/lux/type/poly.lux deleted file mode 100644 index 4f70bb937..000000000 --- a/stdlib/source/library/lux/type/poly.lux +++ /dev/null @@ -1,89 +0,0 @@ -(.require - [library - [lux (.except) - ["[0]" meta] - [abstract - ["[0]" monad (.only do)]] - [control - ["<>" parser (.use "[1]#[0]" monad)] - ["[0]" maybe]] - [data - ["[0]" product] - ["[0]" text] - [collection - ["[0]" list (.use "[1]#[0]" functor)] - ["[0]" dictionary]]] - [macro (.only with_symbols) - [syntax (.only syntax)] - ["^" pattern] - ["[0]" code (.only) - ["<[1]>" \\parser (.only Parser)]]] - [math - [number - ["n" nat]]] - ["[0]" type (.only) - ["<[1]>" \\parser (.only Env)]]]]) - -(def .public polytypic - (syntax (_ [name .local - body .any]) - (with_symbols [g!_ g!type g!output] - (let [g!name (code.symbol ["" name])] - (in (.list (` ((~! syntax) ((~ g!_) [(~ g!type) (~! .any)]) - ((~! do) (~! meta.monad) - [(~ g!type) ((~! meta.eval) .Type (~ g!type))] - (case (is (.Either .Text .Code) - ((~! .result) ((~! <>.rec) - (function ((~ g!_) (~ g!name)) - (~ body))) - (.as .Type (~ g!type)))) - {.#Right (~ g!output)} - ((~' in) (.list (~ g!output))) - - {.#Left (~ g!output)} - ((~! meta.failure) (~ g!output)))))))))))) - -(def .public (code env type) - (-> Env Type Code) - (case type - {.#Primitive name params} - (` {.#Primitive (~ (code.text name)) - (.list (~+ (list#each (code env) params)))}) - - (^.with_template [] - [{ idx} - (` { (~ (code.nat idx))})]) - ([.#Var] [.#Ex]) - - {.#Parameter idx} - (let [idx (.argument env idx)] - (if (n.= 0 idx) - (|> (dictionary.value idx env) maybe.trusted product.left (code env)) - (` (.$ (~ (code.nat (-- idx))))))) - - {.#Apply {.#Primitive "" {.#End}} - {.#Parameter idx}} - (case (.argument env idx) - 0 (|> env (dictionary.value 0) maybe.trusted product.left (code env)) - idx (undefined)) - - (^.with_template [] - [{ left right} - (` { (~ (code env left)) - (~ (code env right))})]) - ([.#Function] [.#Apply]) - - (^.with_template [ ] - [{ left right} - (` ( (~+ (list#each (code env) ( type)))))]) - ([.Union .#Sum type.flat_variant] - [.Tuple .#Product type.flat_tuple]) - - {.#Named name sub_type} - (code.symbol name) - - (^.with_template [] - [{ scope body} - (` { (.list (~+ (list#each (code env) scope))) - (~ (code env body))})]) - ([.#UnivQ] [.#ExQ]))) diff --git a/stdlib/source/library/lux/type/primitive.lux b/stdlib/source/library/lux/type/primitive.lux deleted file mode 100644 index 50c288e1c..000000000 --- a/stdlib/source/library/lux/type/primitive.lux +++ /dev/null @@ -1,105 +0,0 @@ -(.require - [library - [lux (.except) - ["[0]" meta] - [abstract - [monad (.only do)]] - [control - ["<>" parser (.use "[1]#[0]" monad)]] - [data - ["[0]" text (.use "[1]#[0]" equivalence)] - [collection - ["[0]" list (.use "[1]#[0]" functor)]]] - ["[0]" macro (.only) - ["^" pattern] - ["[0]" context] - ["[0]" code (.only) - ["<[1]>" \\parser (.only Parser)]] - [syntax (.only syntax) - ["|[0]|" export]]] - [meta - ["[0]" symbol (.use "[1]#[0]" codec)]]]] - ["[0]" //]) - -(type .public Frame - (Record - [#name Text - #type_vars (List Code) - #abstraction Code - #representation Code])) - -(context.def [frames expression declaration] Frame) - -(.def .public current - (Meta Frame) - (context.peek ..frames)) - -(.def .public (specific name) - (-> Text (Meta Frame)) - (context.search ..frames (|>> (the #name) (text#= name)))) - -(def cast - (Parser [(Maybe Text) Code]) - (<>.either (<>.and (<>.maybe .local) .any) - (<>.and (<>#in {.#None}) .any))) - -(with_template [ ] - [(def .public - (syntax (_ [[frame value] ..cast]) - (do meta.monad - [[name type_vars abstraction representation] (case frame - {.#Some frame} - (..specific frame) - - {.#None} - ..current)] - (in (list (` ((~! //.as) [(~+ type_vars)] (~ ) (~ ) - (~ value))))))))] - - [abstraction representation abstraction] - [representation abstraction representation] - ) - -(def declarationP - (Parser [Text (List Text)]) - (<>.either (.form (<>.and .local (<>.some .local))) - (<>.and .local (at <>.monad in (list))))) - -(def abstract - (Parser [Code [Text (List Text)] Code (List Code)]) - (|export|.parser - (all <>.and - ..declarationP - .any - (<>.some .any) - ))) - -... TODO: Make sure the generated code always gets optimized away. -... (This applies to uses of "abstraction" and "representation") -(def .public primitive - (syntax (_ [[export_policy [name type_vars] representation_type primitives] - ..abstract]) - (do meta.monad - [current_module meta.current_module_name - g!Representation (macro.symbol "Representation") - .let [type_varsC (list#each code.local type_vars) - abstraction_declaration (` ((~ (code.local name)) (~+ type_varsC))) - representation_declaration (` ((~ g!Representation) (~+ type_varsC)))]] - (..declaration [name type_varsC abstraction_declaration representation_declaration] - (` (.these (type (~ export_policy) (~ abstraction_declaration) - (Primitive (~ (code.text (symbol#encoded [current_module name]))) - [(~+ type_varsC)])) - (type (~ representation_declaration) - (~ representation_type)) - (~+ primitives))))))) - -(def selection - (Parser [(List Code) Code]) - (<>.either (<>.and (<>#each (|>> list) .any) .any) - (<>.and (<>#in (list)) .any))) - -(def .public transmutation - (syntax (_ [[specific value] ..selection]) - (in (list (` (.|> (~ value) - (..representation (~+ specific)) - (..abstraction (~+ specific)))))))) diff --git a/stdlib/source/library/lux/type/quotient.lux b/stdlib/source/library/lux/type/quotient.lux deleted file mode 100644 index 98292553c..000000000 --- a/stdlib/source/library/lux/type/quotient.lux +++ /dev/null @@ -1,69 +0,0 @@ -(.require - [library - [lux (.except type) - [abstract - [equivalence (only Equivalence)]] - [macro (.only with_symbols) - [syntax (.only syntax)] - ["[0]" code - ["<[1]>" \\parser]]] - ["[0]" type - [primitive (.except)]]]]) - -(primitive .public (Class t c %) - (-> t c) - - (def .public class - (All (_ t c) - (Ex (_ %) - (-> (-> t c) (Class t c %)))) - (|>> abstraction)) - - (primitive .public (Quotient t c %) - (Record - [#value t - #label c]) - - (def .public (quotient class value) - (All (_ t c %) - (-> (Class t c %) t - (Quotient t c %))) - (abstraction [#value value - #label ((representation Class class) value)])) - - (with_template [ ] - [(def .public - (All (_ t c %) (-> (Quotient t c %) )) - (|>> representation (the )))] - - [value t #value] - [label c #label] - ) - ) - ) - -(def .public type - (syntax (_ [class .any]) - ... TODO: Switch to the cleaner approach ASAP. - (with_symbols [g!t g!c g!% g!_ g!:quotient:] - (in (list (` (let [ ... (~ g!_) (.is (.Ex ((~ g!_) (~ g!t) (~ g!c) (~ g!%)) - ... (..Class (~ g!t) (~ g!c) (~ g!%))) - ... (~ class)) - ] - (.case (.type_of (~ class)) - {.#Apply (~ g!%) {.#Apply (~ g!c) {.#Apply (~ g!t) (~ g!:quotient:)}}} - (.type_literal (..Quotient (~ g!t) (~ g!c) (~ g!%))) - - (~ g!_) - (.undefined)))) - ... (` ((~! type.by_example) [(~ g!t) (~ g!c) (~ g!%)] - ... (is (..Class (~ g!t) (~ g!c) (~ g!%)) - ... (~ class)) - ... (..Quotient (~ g!t) (~ g!c) (~ g!%)))) - ))))) - -(def .public (equivalence super) - (All (_ t c %) (-> (Equivalence c) (Equivalence (..Quotient t c %)))) - (implementation - (def (= reference sample) - (at super = (..label reference) (..label sample))))) diff --git a/stdlib/source/library/lux/type/refinement.lux b/stdlib/source/library/lux/type/refinement.lux deleted file mode 100644 index 225edc957..000000000 --- a/stdlib/source/library/lux/type/refinement.lux +++ /dev/null @@ -1,105 +0,0 @@ -(.require - [library - [lux (.except only type) - [control - [function - [predicate (.only Predicate)]]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" code - ["<[1]>" \\parser]]] - ["[0]" type (.only) - [primitive (.except)]]]]) - -(primitive .public (Refined t %) - (Record - [#value t - #predicate (Predicate t)]) - - (.type .public (Refiner t %) - (-> t (Maybe (Refined t %)))) - - (def .public (refiner predicate) - (All (_ t) - (Ex (_ %) - (-> (Predicate t) (Refiner t %)))) - (function (_ value) - (if (predicate value) - {.#Some (abstraction [#value value - #predicate predicate])} - {.#None}))) - - (with_template [ ] - [(def .public - (All (_ t %) (-> (Refined t %) )) - (|>> representation (the )))] - - [value t #value] - [predicate (Predicate t) #predicate] - ) - - (def .public (lifted transform) - (All (_ t %) - (-> (-> t t) - (-> (Refined t %) (Maybe (Refined t %))))) - (function (_ refined) - (let [(open "_[0]") (representation refined) - value' (transform _#value)] - (if (_#predicate value') - {.#Some (abstraction [..#value value' - ..#predicate _#predicate])} - {.#None})))) - ) - -(def .public (only refiner values) - (All (_ t %) - (-> (Refiner t %) (List t) (List (Refined t %)))) - (case values - {.#End} - {.#End} - - {.#Item head tail} - (case (refiner head) - {.#Some refined} - {.#Item refined (only refiner tail)} - - {.#None} - (only refiner tail)))) - -(def .public (partition refiner values) - (All (_ t %) - (-> (Refiner t %) (List t) [(List (Refined t %)) (List t)])) - (case values - {.#End} - [{.#End} {.#End}] - - {.#Item head tail} - (let [[yes no] (partition refiner tail)] - (case (refiner head) - {.#Some refined} - [{.#Item refined yes} - no] - - {.#None} - [yes - {.#Item head no}])))) - -(def .public type - (syntax (_ [refiner .any]) - ... TODO: Switch to the cleaner approach ASAP. - (macro.with_symbols [g!t g!% g!_ g!:refiner:] - (in (list (` (let [ ... (~ g!_) (.is (.Ex ((~ g!_) (~ g!t) (~ g!%)) - ... (..Refined (~ g!t) (~ g!%))) - ... (~ refiner)) - ] - (.case (.type_of (~ refiner)) - {.#Apply (~ g!%) {.#Apply (~ g!t) (~ g!:refiner:)}} - (.type_literal (..Refined (~ g!t) (~ g!%))) - - (~ g!_) - (.undefined)))) - ... (` ((~! type.by_example) [(~ g!t) (~ g!%)] - ... (is (..Refiner (~ g!t) (~ g!%)) - ... (~ refiner)) - ... (..Refined (~ g!t) (~ g!%)))) - ))))) diff --git a/stdlib/source/library/lux/type/resource.lux b/stdlib/source/library/lux/type/resource.lux deleted file mode 100644 index 760f07dc2..000000000 --- a/stdlib/source/library/lux/type/resource.lux +++ /dev/null @@ -1,188 +0,0 @@ -(.require - [library - [lux (.except) - ["[0]" meta] - [abstract - ["[0]" monad (.only Monad do) - [indexed (.only IxMonad)]]] - [control - ["<>" parser] - ["[0]" maybe] - ["[0]" exception (.only exception)]] - [data - [text - ["%" \\format (.only format)]] - [collection - ["[0]" set] - ["[0]" sequence (.only Sequence)] - ["[0]" list (.use "[1]#[0]" functor mix)]]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" code - ["<[1]>" \\parser (.only Parser)]]] - [math - [number - ["n" nat]]] - [type - [primitive (.except)]]]]) - -(type .public (Procedure monad input output value) - (-> input (monad [output value]))) - -(type .public (Linear monad value) - (All (_ keys) - (Procedure monad keys keys value))) - -(type .public (Affine monad permissions value) - (All (_ keys) - (Procedure monad keys [permissions keys] value))) - -(type .public (Relevant monad permissions value) - (All (_ keys) - (Procedure monad [permissions keys] keys value))) - -(def .public (monad monad) - (All (_ !) (-> (Monad !) (IxMonad (Procedure !)))) - (implementation - (def (in value) - (function (_ keys) - (at monad in [keys value]))) - - (def (then f input) - (function (_ keysI) - (do monad - [[keysT value] (input keysI)] - ((f value) keysT)))))) - -(def .public (run! monad procedure) - (All (_ ! v) (-> (Monad !) (Linear ! v) (! v))) - (do monad - [[_ output] (procedure [])] - (in output))) - -(def .public (lifted monad procedure) - (All (_ ! v) (-> (Monad !) (! v) (Linear ! v))) - (function (_ keys) - (do monad - [output procedure] - (in [keys output])))) - -(primitive .public Ordered Any) -(primitive .public Commutative Any) - -(primitive .public (Key mode key) - Any - - (with_template [ ] - [(def - (Ex (_ k) (-> Any (Key k))) - (|>> abstraction))] - - [ordered_key Ordered] - [commutative_key Commutative] - )) - -(primitive .public (Res key value) - value - - (with_template [ ] - [(def .public ( monad value) - (All (_ ! v) (Ex (_ k) (-> (Monad !) v (Affine ! (Key k) (Res k v))))) - (function (_ keys) - (at monad in [[( []) keys] (abstraction value)])))] - - [ordered Ordered ..ordered_key] - [commutative Commutative ..commutative_key] - ) - - (def .public (read monad resource) - (All (_ ! v k m) - (-> (Monad !) (Res k v) (Relevant ! (Key m k) v))) - (function (_ [key keys]) - (at monad in [keys (representation resource)]))) - ) - -(exception .public (index_cannot_be_repeated [index Nat]) - (exception.report - "Index" (%.nat index))) - -(exception .public amount_cannot_be_zero) - -(def indices - (Parser (List Nat)) - (.tuple (loop (again [seen (set.empty n.hash)]) - (do [! <>.monad] - [done? .end?] - (if done? - (in (list)) - (do ! - [head .nat - _ (<>.assertion (exception.error ..index_cannot_be_repeated head) - (not (set.member? seen head))) - tail (again (set.has head seen))] - (in (list.partial head tail)))))))) - -(def (no_op monad) - (All (_ m) (-> (Monad m) (Linear m Any))) - (function (_ context) - (at monad in [context []]))) - -(def .public exchange - (syntax (_ [swaps ..indices]) - (macro.with_symbols [g!_ g!context g!!] - (case swaps - {.#End} - (in (list (` (~! no_op)))) - - {.#Item head tail} - (do [! meta.monad] - [.let [max_idx (list#mix n.max head tail)] - g!inputs (<| (monad.all !) (list.repeated (++ max_idx)) (macro.symbol "input")) - .let [g!outputs (|> (monad.mix maybe.monad - (function (_ from to) - (do maybe.monad - [input (list.item from g!inputs)] - (in (sequence.suffix input to)))) - (is (Sequence Code) sequence.empty) - swaps) - maybe.trusted - sequence.list) - g!inputsT+ (list#each (|>> (~) (..Key ..Commutative) (`)) g!inputs) - g!outputsT+ (list#each (|>> (~) (..Key ..Commutative) (`)) g!outputs)]] - (in (list (` (is (All ((~ g!_) (~ g!!) (~+ g!inputs) (~ g!context)) - (-> ((~! monad.Monad) (~ g!!)) - (Procedure (~ g!!) - [(~+ g!inputsT+) (~ g!context)] - [(~+ g!outputsT+) (~ g!context)] - .Any))) - (function ((~ g!_) (~ g!!) [(~+ g!inputs) (~ g!context)]) - (at (~ g!!) (~' in) [[(~+ g!outputs) (~ g!context)] []]))))))))))) - -(def amount - (Parser Nat) - (do <>.monad - [raw .nat - _ (<>.assertion (exception.error ..amount_cannot_be_zero []) - (n.> 0 raw))] - (in raw))) - -(with_template [ ] - [(def .public - (syntax (_ [amount ..amount]) - (macro.with_symbols [g!_ g!context g!!] - (do [! meta.monad] - [g!keys (|> (macro.symbol "keys") - (list.repeated amount) - (monad.all !))] - (in (list (` (is (All ((~ g!_) (~ g!!) (~+ g!keys) (~ g!context)) - (-> ((~! monad.Monad) (~ g!!)) - (Procedure (~ g!!) - [ (~ g!context)] - [ (~ g!context)] - .Any))) - (function ((~ g!_) (~ g!!) [ (~ g!context)]) - (at (~ g!!) (~' in) [[ (~ g!context)] []]))))))))))] - - [group (~+ g!keys) [(~+ g!keys)]] - [un_group [(~+ g!keys)] (~+ g!keys)] - ) diff --git a/stdlib/source/library/lux/type/unit.lux b/stdlib/source/library/lux/type/unit.lux deleted file mode 100644 index 994e7ad11..000000000 --- a/stdlib/source/library/lux/type/unit.lux +++ /dev/null @@ -1,103 +0,0 @@ -(.require - [library - [lux (.except type) - [abstract - [equivalence (.only Equivalence)] - [order (.only Order)] - [enum (.only Enum)]] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" code - ["<[1]>" \\parser]]] - [math - [number - ["i" int]]]]] - ["[0]" // (.only) - [primitive (.except)]]) - -(primitive .public (Measure scale unit) - Int - - (def .public measure - (All (_ scale unit) (-> Int (Measure scale unit))) - (|>> abstraction)) - - (def .public number - (All (_ scale unit) (-> (Measure scale unit) Int)) - (|>> representation)) - - (def .public equivalence - (All (_ scale unit) (Equivalence (Measure scale unit))) - (implementation - (def (= reference sample) - (i.= (representation reference) (representation sample))))) - - (def .public order - (All (_ scale unit) (Order (Measure scale unit))) - (implementation - (def equivalence ..equivalence) - - (def (< reference sample) - (i.< (representation reference) (representation sample))))) - - (def .public enum - (All (_ scale unit) (Enum (Measure scale unit))) - (implementation - (def order ..order) - (def succ (|>> representation ++ abstraction)) - (def pred (|>> representation -- abstraction)))) - - (with_template [ ] - [(def .public ( param subject) - (All (_ scale unit) (-> (Measure scale unit) (Measure scale unit) (Measure scale unit))) - (abstraction ( (representation param) - (representation subject))))] - - [+ i.+] - [- i.-] - ) - - (with_template [

] - [(def .public ( param subject) - (All (_ scale p s) (-> (Measure scale

) (Measure scale ) (Measure scale ))) - (abstraction ( (representation param) - (representation subject))))] - - [* i.* p s [p s]] - [/ i./ p [p s] s] - ) - - (.type .public (Unit a) - (Interface - (is (-> Int (Measure Any a)) - in) - (is (-> (Measure Any a) Int) - out))) - - (def .public (unit _) - (Ex (_ a) (-> Any (Unit a))) - (implementation - (def in ..measure) - (def out ..number))) - ) - -(def .public type - (syntax (_ [it .any]) - (macro.with_symbols [g!a] - (in (list (` ((~! //.by_example) [(~ g!a)] - (is (..Unit (~ g!a)) - (~ it)) - (~ g!a)))))))) - -(with_template [ ] - [(def .public - (..unit [])) - - (.type .public - (~ (..type )))] - - [gram Gram] - [meter Meter] - [litre Litre] - [second Second] - ) diff --git a/stdlib/source/library/lux/type/unit/scale.lux b/stdlib/source/library/lux/type/unit/scale.lux deleted file mode 100644 index b7f598d13..000000000 --- a/stdlib/source/library/lux/type/unit/scale.lux +++ /dev/null @@ -1,78 +0,0 @@ -(.require - [library - [lux (.except type) - [control] - ["[0]" macro (.only) - [syntax (.only syntax)] - ["[0]" code - ["<[1]>" \\parser]]] - [math - [number - ["i" int] - ["[0]" ratio (.only Ratio)]]]]] - ["[0]" // (.only) - ["/[1]" //]]) - -(.type .public (Scale s) - (Interface - (is (All (_ u) (-> (//.Measure Any u) (//.Measure s u))) - up) - (is (All (_ u) (-> (//.Measure s u) (//.Measure Any u))) - down) - (is Ratio - ratio))) - -(def .public (scale ratio) - (Ex (_ s) (-> Ratio (Scale s))) - (let [(open "/[0]") ratio] - (implementation - (def up - (|>> //.number - (i.* (.int /#numerator)) - (i./ (.int /#denominator)) - //.measure)) - (def down - (|>> //.number - (i.* (.int /#denominator)) - (i./ (.int /#numerator)) - //.measure)) - (def ratio - ratio)))) - -(def .public (re_scaled from to measure) - (All (_ si so u) (-> (Scale si) (Scale so) (//.Measure si u) (//.Measure so u))) - (let [(open "/[0]") (ratio./ (at from ratio) - (at to ratio))] - (|> measure - //.number - (i.* (.int /#numerator)) - (i./ (.int /#denominator)) - //.measure))) - -(def .public type - (syntax (_ [it .any]) - (macro.with_symbols [g!a] - (in (list (` ((~! ///.by_example) [(~ g!a)] - (is (..Scale (~ g!a)) - (~ it)) - (~ g!a)))))))) - -(with_template [ ] - [(def .public - (scale [ratio.#numerator - ratio.#denominator 1])) - - (.type .public - (~ (..type ))) - - (def .public - (scale [ratio.#numerator 1 - ratio.#denominator ])) - - (.type .public - (~ (..type )))] - - [ 1,000 kilo Kilo milli Milli] - [ 1,000,000 mega Mega micro Micro] - [1,000,000,000 giga Giga nano Nano ] - ) diff --git a/stdlib/source/library/lux/type/variance.lux b/stdlib/source/library/lux/type/variance.lux deleted file mode 100644 index ac7e120d4..000000000 --- a/stdlib/source/library/lux/type/variance.lux +++ /dev/null @@ -1,45 +0,0 @@ -(.require - [library - [lux (.except) - [meta - ["[0]" symbol]]]]) - -(type .public (Co it) - (-> Any it)) - -(type .public (Contra it) - (-> it Any)) - -(type .public (In it) - (-> it it)) - -(type .public (Mutable r w) - (Primitive "#Mutable" [(-> w r)])) - -(with_template [ ] - [(def .public - (template ( it) - [((.is (.All (_ r w) ) - (.|>> .as_expected)) - it)]))] - - [read (.-> (..Mutable r w) r)] - [write (.-> w (..Mutable r w))] - ) - -(type .public (Read_Only a) - (Mutable a Nothing)) - -(type .public (Write_Only a) - (Mutable Any a)) - -(with_template [ ] - [(def .public - (template ( it) - [((.is (.All (_ r w) ) - (.|>>)) - it)]))] - - [read_only (.-> (..Mutable r w) (..Read_Only r))] - [write_only (.-> (..Mutable r w) (..Write_Only w))] - ) diff --git a/stdlib/source/library/lux/world/file/watch.lux b/stdlib/source/library/lux/world/file/watch.lux index d21036caa..aee589f28 100644 --- a/stdlib/source/library/lux/world/file/watch.lux +++ b/stdlib/source/library/lux/world/file/watch.lux @@ -1,6 +1,6 @@ (.require [library - [lux (.except all) + [lux (.except all and) ["@" target] ["[0]" ffi (.only import)] [abstract @@ -29,8 +29,9 @@ ["n" nat]]] [time ["[0]" instant (.only Instant) (.use "[1]#[0]" equivalence)]] - [type - [primitive (.only primitive representation abstraction)]]]] + [meta + [type + [primitive (.only primitive representation abstraction)]]]]] ["[0]" //]) (primitive .public Concern @@ -66,7 +67,7 @@ false false true] ) - (def .public (also left right) + (def .public (and left right) (-> Concern Concern Concern) (abstraction [#creation (or (..creation? left) (..creation? right)) @@ -75,7 +76,7 @@ (def .public all Concern - (.all ..also + (.all ..and ..creation ..modification ..deletion @@ -339,7 +340,7 @@ (|>> java/nio/file/WatchKey::pollEvents (at io.monad each (|>> ..default_list (list#each default_event_concern) - (list#mix ..also ..none))))) + (list#mix ..and ..none))))) (import java/nio/file/WatchService "[1]::[0]" @@ -441,8 +442,8 @@ (do async.monad [?concern (stop path)] (do (try.with async.monad) - [key (..default_start (..watch_events (..also (try.else ..none ?concern) - the_concern)) + [key (..default_start (..watch_events (..and (try.else ..none ?concern) + the_concern)) watcher path)] (do async.monad -- cgit v1.2.3