diff options
Diffstat (limited to 'stdlib/source/library/lux/type/implicit.lux')
| -rw-r--r-- | stdlib/source/library/lux/type/implicit.lux | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/stdlib/source/library/lux/type/implicit.lux b/stdlib/source/library/lux/type/implicit.lux index 13b1d4c90..fb06527c8 100644 --- a/stdlib/source/library/lux/type/implicit.lux +++ b/stdlib/source/library/lux/type/implicit.lux @@ -26,7 +26,7 @@ ["[0]" type (.open: "[1]#[0]" equivalence) ["[0]" check (.only Check)]]]]) -(def: (type_var id env) +(def (type_var id env) (-> Nat Type_Context (Meta Type)) (case (list.example (|>> product.left (n.= id)) (the .#var_bindings env)) @@ -45,7 +45,7 @@ (meta.failure (format "Unknown type-var " (%.nat id))) )) -(def: (implicit_type var_name) +(def (implicit_type var_name) (-> Symbol (Meta Type)) (do meta.monad [raw_type (meta.type var_name) @@ -57,7 +57,7 @@ _ (in raw_type)))) -(def: (member_type idx sig_type) +(def (member_type idx sig_type) (-> Nat Type (Check Type)) (case sig_type {.#Named _ sig_type'} @@ -81,7 +81,7 @@ (at check.monad in sig_type) (check.failure (format "Cannot find member type " (%.nat idx) " for " (%.type sig_type)))))) -(def: (member_name member) +(def (member_name member) (-> Symbol (Meta Symbol)) (case member ["" simple_name] @@ -109,14 +109,14 @@ _ (at meta.monad in member))) -(def: (implicit_member 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) +(def (compatible_type? interface candidate) (-> Type Type Bit) (with_expansions [<found?> (type#= interface candidate)] (<| (or <found?>) @@ -133,7 +133,7 @@ (let [candidate (type.de_aliased candidate)]) <found?>))) -(def: (available_definitions sig_type source_module target_module constants aggregate) +(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) @@ -144,7 +144,7 @@ aggregate constants)) -(def: (local_env sig_type) +(def (local_env sig_type) (-> Type (Meta (List [Symbol Type]))) (do meta.monad [local_batches meta.locals @@ -160,14 +160,14 @@ {.#Some [["" name] type]} {.#None}))))))) -(def: (local_structs sig_type) +(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) +(def (imported_structs sig_type) (-> Type (Meta (List [Symbol Type]))) (do [! meta.monad] [this_module_name meta.current_module_name @@ -178,7 +178,7 @@ {.#End} (list.zipped_2 imported_modules accessible_definitions))))) -(def: (on_argument arg func) +(def (on_argument arg func) (-> Type Type (Check Type)) (case func {.#Named _ func'} @@ -200,7 +200,7 @@ _ (check.failure (format "Invalid function type: " (%.type func))))) -(def: (concrete_type type) +(def (concrete_type type) (-> Type (Check [(List Nat) Type])) (case type {.#UnivQ _} @@ -213,7 +213,7 @@ _ (at check.monad in [(list) type]))) -(def: (ensure_function_application! member_type input_types expected_output) +(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)] @@ -225,7 +225,7 @@ [#constructor Symbol #dependencies (List Instance)]))) -(def: (candidate_provision provision context dep alts) +(def (candidate_provision provision context dep alts) (-> (-> Lux Type_Context Type (Check Instance)) Type_Context Type (List [Symbol Type]) (Meta (List Instance))) @@ -253,7 +253,7 @@ found (in found)))) -(def: (provision sig_type compiler context dep) +(def (provision sig_type compiler context dep) (-> Type Lux Type_Context Type (Check Instance)) (case (meta.result compiler (all meta.either @@ -275,7 +275,7 @@ (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) +(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 @@ -304,7 +304,7 @@ found (in found)))) -(def: (alternatives sig_type member_idx input_types output_type) +(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 @@ -312,7 +312,7 @@ (do meta.monad [alts (..local_structs sig_type)] (test alts)) (do meta.monad [alts (..imported_structs sig_type)] (test alts))))) -(def: (var? input) +(def (var? input) (-> Code Bit) (case input [_ {.#Symbol _}] @@ -321,11 +321,11 @@ _ #0)) -(def: (pair_list [l r]) +(def (pair_list [l r]) (All (_ a) (-> [a a] (List a))) (list l r)) -(def: (instance$ [constructor dependencies]) +(def (instance$ [constructor dependencies]) (-> Instance Code) (case dependencies {.#End} @@ -334,7 +334,7 @@ _ (` ((~ (code.symbol constructor)) (~+ (list#each instance$ dependencies)))))) -(def: .public a/an +(def .public a/an (syntax (_ [member <code>.symbol args (<>.or (<>.and (<>.some <code>.symbol) <code>.end) (<>.and (<>.some <code>.any) <code>.end))]) @@ -370,16 +370,16 @@ (..a/an (~ (code.symbol member)) (~+ labels))))))) ))) -(def: .public a ..a/an) -(def: .public an ..a/an) +(def .public a ..a/an) +(def .public an ..a/an) -(def: (implicit_bindings amount) +(def (implicit_bindings amount) (-> Nat (Meta (List Code))) (|> (macro.symbol "g!implicit") (list.repeated amount) (monad.all meta.monad))) -(def: .public with +(def .public with (syntax (_ [implementations (<code>.tuple (<>.many <code>.any)) body <code>.any]) (do meta.monad @@ -390,11 +390,11 @@ list#conjoint))] (~ body)))))))) -(def: .public implicitly +(def .public implicitly (syntax (_ [implementations (<>.many <code>.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) + (` (def .private (~ g!implicit) (~ implementation)))))))))) |