diff --git a/stdlib/source/injection/lux/data/binary.lux b/stdlib/source/injection/lux/data/binary.lux index 326fe2bef..be7178dee 100644 --- a/stdlib/source/injection/lux/data/binary.lux +++ b/stdlib/source/injection/lux/data/binary.lux @@ -303,8 +303,7 @@ (Injection Type) (..rec (function (_ again) - (let [indexed ..natural - quantified (..and (..stack again) again)] + (let [indexed ..natural] (function (_ altV) (`` (when altV (,, (template.with [ ] @@ -321,10 +320,9 @@ [1 .#Parameter indexed] [2 .#Variable indexed] [3 .#Opaque indexed] - [4 .#Universal quantified] - [5 .#Existential quantified] - [6 .#Reification (..and again again)] - [7 .#Named (..and ..name again)])) + [4 .#Quantification (all ..and ..bit (..stack again) again)] + [5 .#Reification (..and again again)] + [6 .#Named (..and ..name again)])) ))))))) (the .public provenance diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux index 9a0a337fd..04054d429 100644 --- a/stdlib/source/library/lux.lux +++ b/stdlib/source/library/lux.lux @@ -8,91 +8,118 @@ (.def# Type (.is# (.type# "type") - {6 #1 + {5 #1 [..prelude "Type"] (.type# "type")}) #1) (.def# Name (.is# Type - {6 #1 + {5 #1 [..prelude "Name"] (.type# "name")}) #1) (.def# Bit (.is# Type - {6 #1 + {5 #1 [..prelude "Bit"] {#0 (.type_name# "bit") (.list#)}}) #1) +(.def# false + (.is# Bit + #0) + #1) + +(.def# true + (.is# Bit + #1) + #1) + +(.def# public + ..true + #1) + +(.def# private + ..false + ..public) + +(.def# local + ..private + ..public) + +(.def# global + ..public + ..public) + (.def# Polarity (.is# Type ..Bit) - #1) + ..public) (.def# contra_variant (.is# Polarity - #0) - #1) + ..false) + ..public) (.def# co_variant (.is# Polarity - #1) - #1) + ..true) + ..public) ... https://en.wikipedia.org/wiki/Quantifier_(logic) (.def# Quantification (.is# Type ..Bit) - #1) + ..public) ... https://en.wikipedia.org/wiki/Universal_quantification (.def# universal (.is# Quantification #0) - #1) + ..public) ... https://en.wikipedia.org/wiki/Existential_quantification (.def# existential (.is# Quantification #1) - #1) + ..public) (.def# Parameter (.is# Type ..Bit) - #1) + ..public) (.def# abstraction (.is# Quantification #0) - #1) + ..public) (.def# argument (.is# Quantification #1) - #1) + ..public) (.def# Natural (.is# Type - {6 #1 + {5 #1 [..prelude "Natural"] {#0 (.type_name# "i64") (.list# [..co_variant {#0 (.type_name# "natural") (.list#)}])}}) - #1) + ..public) ... (every .public Any ... (for_some (_ it) it)) (.def# Any (.is# Type - {6 #1 + {5 #1 [..prelude "Any"] - {5 #0 + {4 #0 + .existential {#0} {1 #0 1}}}) - #1) + ..public) ... (every .public (Stack it) ... (Variant @@ -100,9 +127,10 @@ ... {#Top it (Stack it)})) (.def# Stack (.is# Type - {6 #1 + {5 #1 [..prelude "Stack"] {4 #0 + .universal {#0} {0 #0 (.type_name# "sum") @@ -110,10 +138,10 @@ [..co_variant {0 #0 (.type_name# "product") (.list# [..co_variant {1 #0 1}] - [..co_variant {6 #0 + [..co_variant {5 #0 {1 #0 1} {1 #0 0}}])}])}}}) - #1) + ..public) ... (every .public (Maybe it) ... (Variant @@ -121,33 +149,34 @@ ... {#Some it})) (.def# Maybe (.is# Type - {6 #1 + {5 #1 [..prelude "Maybe"] {4 #0 + .universal {#0} {0 #0 (.type_name# "sum") (.list# [..co_variant Any] [..co_variant {1 #0 1}])}}}) - #1) + ..public) (.def# Label (.is# Type - {6 #1 [..prelude "Label"] + {5 #1 [..prelude "Label"] (.type# "label")}) - #1) + ..public) (.def# Tag (.is# Type - {6 #1 [..prelude "Tag"] + {5 #1 [..prelude "Tag"] {#0 (.type_name# "tag") (.list#)}}) - #1) + ..public) (.def# Slot (.is# Type - {6 #1 [..prelude "Slot"] + {5 #1 [..prelude "Slot"] {#0 (.type_name# "slot") (.list#)}}) - #1) + ..public) (.def# Sum (.is# {0 #0 @@ -163,7 +192,7 @@ (.type_name# "sum") (.list# [..co_variant left] [..co_variant right])}))) - #0) + ..private) (.def# Product (.is# {0 #0 @@ -179,7 +208,7 @@ (.type_name# "product") (.list# [..co_variant left] [..co_variant right])}))) - #0) + ..private) (.def# Function (.is# {0 #0 @@ -195,112 +224,108 @@ (.type_name# "function") (.list# [..contra_variant left] [..co_variant right])}))) - #0) + ..private) (.def# tag (.is# (Function Label Tag) (.function# _ it (.as# Tag it))) - #0) + ..private) (.def# slot (.is# (Function Label Slot) (.function# _ it (.as# Slot it))) - #0) + ..private) (.def# maybe_tags - (.is# {6 #0 Name Stack} + (.is# {5 #0 Name Stack} {#1 [[..prelude "#None"] {#1 [[..prelude "#Some"] {#0}]}]}) - #0) -(.def# #None (..tag [{#1 [0 #0 ..maybe_tags]} Maybe]) #1) -(.def# #Some (..tag [{#1 [0 #1 ..maybe_tags]} Maybe]) #1) + ..private) +(.def# #None (..tag [{#1 [0 #0 ..maybe_tags]} Maybe]) ..public) +(.def# #Some (..tag [{#1 [0 #1 ..maybe_tags]} Maybe]) ..public) (.def# stack_tags - (.is# {6 #0 Name Stack} + (.is# {5 #0 Name Stack} {#1 [[..prelude "#Empty"] {#1 [[..prelude "#Top"] {#0}]}]}) - #0) -(.def# #Empty (..tag [{#1 [0 #0 ..stack_tags]} Stack]) #1) -(.def# #Top (..tag [{#1 [0 #1 ..stack_tags]} Stack]) #1) + ..private) +(.def# #Empty (..tag [{#1 [0 #0 ..stack_tags]} Stack]) ..public) +(.def# #Top (..tag [{#1 [0 #1 ..stack_tags]} Stack]) ..public) (.def# type_tags - (.is# {6 #0 Name Stack} + (.is# {5 #0 Name Stack} {#1 [[..prelude "#Nominal"] {#1 [[..prelude "#Parameter"] {#1 [[..prelude "#Variable"] {#1 [[..prelude "#Opaque"] - {#1 [[..prelude "#Universal"] - {#1 [[..prelude "#Existential"] - {#1 [[..prelude "#Reification"] - {#1 [[..prelude "#Named"] - {#0}]}]}]}]}]}]}]}]}) - #0) -(.def# #Nominal (..tag [{#Some [0 #0 ..type_tags]} Type]) #1) -(.def# #Parameter (..tag [{#Some [1 #0 ..type_tags]} Type]) #1) -(.def# #Variable (..tag [{#Some [2 #0 ..type_tags]} Type]) #1) + {#1 [[..prelude "#Quantification"] + {#1 [[..prelude "#Reification"] + {#1 [[..prelude "#Named"] + {#0}]}]}]}]}]}]}]}) + ..private) +(.def# #Nominal (..tag [{#Some [0 #0 ..type_tags]} Type]) ..public) +(.def# #Parameter (..tag [{#Some [1 #0 ..type_tags]} Type]) ..public) +(.def# #Variable (..tag [{#Some [2 #0 ..type_tags]} Type]) ..public) ... https://en.wikipedia.org/wiki/Opaque_data_type -(.def# #Opaque (..tag [{#Some [3 #0 ..type_tags]} Type]) #1) -... https://en.wikipedia.org/wiki/Universal_quantification -(.def# #Universal (..tag [{#Some [4 #0 ..type_tags]} Type]) #1) -... https://en.wikipedia.org/wiki/Existential_quantification -(.def# #Existential (..tag [{#Some [5 #0 ..type_tags]} Type]) #1) -(.def# #Reification (..tag [{#Some [6 #0 ..type_tags]} Type]) #1) -(.def# #Named (..tag [{#Some [6 #1 ..type_tags]} Type]) #1) +(.def# #Opaque (..tag [{#Some [3 #0 ..type_tags]} Type]) ..public) +(.def# #Quantification (..tag [{#Some [4 #0 ..type_tags]} Type]) ..public) +(.def# #Reification (..tag [{#Some [5 #0 ..type_tags]} Type]) ..public) +(.def# #Named (..tag [{#Some [5 #1 ..type_tags]} Type]) ..public) (.def# provenance#dummy (.is# (.type# "provenance") ["" 0 0]) - #0) + ..private) ... (every .public Nothing ... (for_any (_ it) it)) (.def# Nothing (.is# Type {#Named [..prelude "Nothing"] - {#Universal {#Empty} - {#Parameter 1}}}) - #1) + {#Quantification .universal {#Empty} + {#Parameter 1}}}) + ..public) (.def# I64 (.is# Type {#Named [..prelude "I64"] - {#Universal {#Empty} - {#Nominal (.type_name# "i64") (.list# [..co_variant {#Parameter 1}])}}}) - #1) + {#Quantification .universal {#Empty} + {#Nominal (.type_name# "i64") (.list# [..co_variant {#Parameter 1}])}}}) + ..public) (.def# Integer (.is# Type {#Named [..prelude "Integer"] {#Nominal (.type_name# "i64") (.list# [..co_variant {#Nominal (.type_name# "integer") (.list#)}])}}) - #1) + ..public) (.def# Revolution (.is# Type {#Named [..prelude "Revolution"] {#Nominal (.type_name# "i64") (.list# [..co_variant {#Nominal (.type_name# "revolution") (.list#)}])}}) - #1) + ..public) (.def# Decimal (.is# Type {#Named [..prelude "Decimal"] {#Nominal (.type_name# "decimal") (.list#)}}) - #1) + ..public) (.def# Text (.is# Type {#Named [..prelude "Text"] {#Nominal (.type_name# "text") (.list#)}}) - #1) + ..public) (.def# Error (.is# Type {#Named [..prelude "Error"] ..Text}) - #1) + ..public) ... (every .public Provenance ... (Record @@ -311,17 +336,17 @@ (.is# Type {#Named [..prelude "Provenance"] (.type# "provenance")}) - #1) + ..public) (.def# provenance_slots (.is# {#Reification Name Stack} {#Top [..prelude "#module"] {#Top [..prelude "#line"] {#Top [..prelude "#column"] {#Empty}}}}) - #0) -(.def# #module (slot [{#Some [0 #0 ..provenance_slots]} Provenance]) #1) -(.def# #line (slot [{#Some [1 #0 ..provenance_slots]} Provenance]) #1) -(.def# #column (slot [{#Some [1 #1 ..provenance_slots]} Provenance]) #1) + ..private) +(.def# #module (slot [{#Some [0 #0 ..provenance_slots]} Provenance]) ..public) +(.def# #line (slot [{#Some [1 #0 ..provenance_slots]} Provenance]) ..public) +(.def# #column (slot [{#Some [1 #1 ..provenance_slots]} Provenance]) ..public) ... (every .public (Annotated m v) ... (Record @@ -330,25 +355,25 @@ (.def# Annotated (.is# Type {#Named [..prelude "Annotated"] - {#Universal {#Empty} - {#Universal {#Empty} - (Product {#Parameter 3} - {#Parameter 1})}}}) - #1) + {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Product {#Parameter 3} + {#Parameter 1})}}}) + ..public) (.def# ann_slots (.is# {#Reification Name Stack} {#Top [..prelude "#meta"] {#Top [..prelude "#datum"] {#Empty}}}) - #0) -(.def# #meta (slot [{#Some [0 #0 ..ann_slots]} Annotated]) #1) -(.def# #datum (slot [{#Some [0 #1 ..ann_slots]} Annotated]) #1) + ..private) +(.def# #meta (slot [{#Some [0 #0 ..ann_slots]} Annotated]) ..public) +(.def# #datum (slot [{#Some [0 #1 ..ann_slots]} Annotated]) ..public) (.def# Code (.is# Type {#Named [..prelude "Code"] (.type# "code")}) - #1) + ..public) (.def# code_tags (.is# {#Reification Name Stack} {#Top [..prelude "#Bit"] @@ -362,114 +387,98 @@ {#Top [..prelude "#Variant"] {#Top [..prelude "#Tuple"] {#Empty}}}}}}}}}}}) - #0) -(.def# #Bit (tag [{#Some [0 #0 ..code_tags]} Code]) #1) -(.def# #Natural (tag [{#Some [1 #0 ..code_tags]} Code]) #1) -(.def# #Integer (tag [{#Some [2 #0 ..code_tags]} Code]) #1) -(.def# #Revolution (tag [{#Some [3 #0 ..code_tags]} Code]) #1) -(.def# #Decimal (tag [{#Some [4 #0 ..code_tags]} Code]) #1) -(.def# #Text (tag [{#Some [5 #0 ..code_tags]} Code]) #1) -(.def# #Name (tag [{#Some [6 #0 ..code_tags]} Code]) #1) -(.def# #Form (tag [{#Some [7 #0 ..code_tags]} Code]) #1) -(.def# #Variant (tag [{#Some [8 #0 ..code_tags]} Code]) #1) -(.def# #Tuple (tag [{#Some [8 #1 ..code_tags]} Code]) #1) - -(.def# private - #0 - #1) - -(.def# public - #1 - #1) - -(.def# local - #0 - #1) - -(.def# global - #1 - #1) + ..private) +(.def# #Bit (tag [{#Some [0 #0 ..code_tags]} Code]) ..public) +(.def# #Natural (tag [{#Some [1 #0 ..code_tags]} Code]) ..public) +(.def# #Integer (tag [{#Some [2 #0 ..code_tags]} Code]) ..public) +(.def# #Revolution (tag [{#Some [3 #0 ..code_tags]} Code]) ..public) +(.def# #Decimal (tag [{#Some [4 #0 ..code_tags]} Code]) ..public) +(.def# #Text (tag [{#Some [5 #0 ..code_tags]} Code]) ..public) +(.def# #Name (tag [{#Some [6 #0 ..code_tags]} Code]) ..public) +(.def# #Form (tag [{#Some [7 #0 ..code_tags]} Code]) ..public) +(.def# #Variant (tag [{#Some [8 #0 ..code_tags]} Code]) ..public) +(.def# #Tuple (tag [{#Some [8 #1 ..code_tags]} Code]) ..public) (.def# annotated - (.is# {#Universal {#Empty} - (Function {#Parameter 1} - (Product Provenance {#Parameter 1}))} + (.is# {#Quantification .universal {#Empty} + (Function {#Parameter 1} + (Product Provenance {#Parameter 1}))} (.function# _ it [provenance#dummy it])) - #0) + ..private) (.def# code#bit (.is# (Function Bit Code) (.function# _ value {#Bit (annotated value)})) - #0) + ..private) (.def# code#natural (.is# (Function Natural Code) (.function# _ value {#Natural (annotated value)})) - #0) + ..private) (.def# code#integer (.is# (Function Integer Code) (.function# _ value {#Integer (annotated value)})) - #0) + ..private) (.def# code#revolution (.is# (Function Revolution Code) (.function# _ value {#Revolution (annotated value)})) - #0) + ..private) (.def# code#decimal (.is# (Function Decimal Code) (.function# _ value {#Decimal (annotated value)})) - #0) + ..private) (.def# code#text (.is# (Function Text Code) (.function# _ text {#Text (annotated text)})) - #0) + ..private) (.def# code#name (.is# (Function Name Code) (.function# _ name {#Name (annotated name)})) - #0) + ..private) (.def# code#local (.is# (Function Text Code) (.function# _ name {#Name (annotated ["" name])})) - #0) + ..private) (.def# List (.is# Type {#Named [..prelude "List"] - {#Universal {#Empty} - {#Nominal (.type_name# "list") (.list# [..co_variant {#Parameter 1}])}}}) + {#Quantification .universal {#Empty} + {#Nominal (.type_name# "list") (.list# [..co_variant {#Parameter 1}])}}}) .public) (.def# code#form (.is# (Function {#Reification Code List} Code) (.function# _ tokens {#Form (annotated tokens)})) - #0) + ..private) (.def# code#variant (.is# (Function {#Reification Code List} Code) (.function# _ tokens {#Variant (annotated tokens)})) - #0) + ..private) (.def# code#tuple (.is# (Function {#Reification Code List} Code) (.function# _ tokens {#Tuple (annotated tokens)})) - #0) + ..private) (.def# code#list (.is# (Function {#Reification Code List} @@ -477,7 +486,7 @@ (.function# _ tokens {#Form (annotated (.list_composite# (.list# (code#name [..prelude "list#"])) tokens))})) - #0) + ..private) (.def# Definition (.is# Type @@ -509,7 +518,7 @@ {#Top [..prelude "#Alias"] {#Top [..prelude "#Default"] {#Empty}}}}) - #0) + ..private) (.def# #Definition (tag [{#Some [0 #0 ..global_tags]} Global]) .public) (.def# #Alias (tag [{#Some [1 #0 ..global_tags]} Global]) .public) (.def# #Default (tag [{#Some [1 #1 ..global_tags]} Global]) .public) @@ -525,7 +534,7 @@ {#Top [..prelude "#counter"] {#Top [..prelude "#mappings"] {#Empty}}}) - #0) + ..private) (.def# #counter (slot [{#Some [0 #0 ..bindings_slots]} Bindings]) .public) (.def# #mappings (slot [{#Some [0 #1 ..bindings_slots]} Bindings]) .public) @@ -544,7 +553,7 @@ {#Top [..prelude "#Local"] {#Top [..prelude "#Captured"] {#Empty}}}) - #0) + ..private) (.def# #Local (tag [{#Some [0 #0 ..ref_tags]} Ref]) .public) (.def# #Captured (tag [{#Some [0 #1 ..ref_tags]} Ref]) .public) @@ -559,7 +568,7 @@ {#Top [..prelude "#locals"] {#Top [..prelude "#captured"] {#Empty}}}) - #0) + ..private) (.def# #locals (slot [{#Some [0 #0 ..scope_slots]} Scope]) .public) (.def# #captured (slot [{#Some [0 #1 ..scope_slots]} Scope]) .public) @@ -570,10 +579,10 @@ (.def# Either (.is# Type {#Named [..prelude "Either"] - {#Universal {#Empty} - {#Universal {#Empty} - (Sum {#Parameter 3} - {#Parameter 1})}}}) + {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Sum {#Parameter 3} + {#Parameter 1})}}}) .public) (.def# either_tags @@ -581,7 +590,7 @@ {#Top [..prelude "#Left"] {#Top [..prelude "#Right"] {#Empty}}}) - #0) + ..private) (.def# #Left (tag [{#Some [0 #0 ..either_tags]} Either]) .public) (.def# #Right (tag [{#Some [0 #1 ..either_tags]} Either]) .public) @@ -612,7 +621,7 @@ {#Top [..prelude "#Compiled"] {#Top [..prelude "#Cached"] {#Empty}}}}) - #0) + ..private) (.def# #Active (tag [{#Some [0 #0 ..module_state_tags]} Module_State]) .public) (.def# #Compiled (tag [{#Some [1 #0 ..module_state_tags]} Module_State]) .public) (.def# #Cached (tag [{#Some [1 #1 ..module_state_tags]} Module_State]) .public) @@ -631,7 +640,7 @@ {#Top [..prelude "#imports"] {#Top [..prelude "#module_state"] {#Empty}}}}}}) - #0) + ..private) (.def# #module_hash (slot [{#Some [0 #0 ..module_slots]} Module]) .public) (.def# #module_aliases (slot [{#Some [1 #0 ..module_slots]} Module]) .public) (.def# #definitions (slot [{#Some [2 #0 ..module_slots]} Module]) .public) @@ -650,7 +659,7 @@ {#Top [..prelude "#var_counter"] {#Top [..prelude "#var_bindings"] {#Empty}}}}) - #0) + ..private) (.def# #ex_counter (slot [{#Some [0 #0 ..type_context_slots]} Type_Context]) .public) (.def# #var_counter (slot [{#Some [1 #0 ..type_context_slots]} Type_Context]) .public) (.def# #var_bindings (slot [{#Some [1 #1 ..type_context_slots]} Type_Context]) .public) @@ -674,7 +683,7 @@ {#Top [..prelude "#Eval"] {#Top [..prelude "#Interpreter"] {#Empty}}}}) - #0) + ..private) (.def# #Build (tag [{#Some [0 #0 ..mode_tags]} Mode]) .public) (.def# #Eval (tag [{#Some [1 #0 ..mode_tags]} Mode]) .public) (.def# #Interpreter (tag [{#Some [1 #1 ..mode_tags]} Mode]) .public) @@ -691,7 +700,7 @@ {#Top [..prelude "#mode"] {#Top [..prelude "#configuration"] {#Empty}}}}}) - #0) + ..private) (.def# #target (slot [{#Some [0 #0 ..info_slots]} Info]) .public) (.def# #version (slot [{#Some [1 #0 ..info_slots]} Info]) .public) (.def# #mode (slot [{#Some [2 #0 ..info_slots]} Info]) .public) @@ -716,7 +725,7 @@ {#Top [..prelude "#seed"] {#Top [..prelude "#eval"] {#Empty}}}}}}}}}}}) - #0) + ..private) (.def# #info (slot [{#Some [0 #0 ..lux_slots]} Lux]) .public) (.def# #source (slot [{#Some [1 #0 ..lux_slots]} Lux]) .public) (.def# #provenance (slot [{#Some [2 #0 ..lux_slots]} Lux]) .public) @@ -733,10 +742,10 @@ (.def# Meta (.is# Type {#Named [..prelude "Meta"] - {#Universal {#Empty} - (Function Lux - {#Reification (Product Lux {#Parameter 1}) - {#Reification Text Either}})}}) + {#Quantification .universal {#Empty} + (Function Lux + {#Reification (Product Lux {#Parameter 1}) + {#Reification Text Either}})}}) .public) ... (every .public Macro' @@ -756,35 +765,35 @@ ... Base functions & macros (.def# meta#in - (.is# {#Universal {#Empty} - (Function {#Parameter 1} - {#Reification {#Parameter 1} Meta})} + (.is# {#Quantification .universal {#Empty} + (Function {#Parameter 1} + {#Reification {#Parameter 1} Meta})} (.function# _ val (.function# _ state {#Right [state val]}))) - #0) + ..private) (.def# failure - (.is# {#Universal {#Empty} - (Function Text - {#Reification {#Parameter 1} Meta})} + (.is# {#Quantification .universal {#Empty} + (Function Text + {#Reification {#Parameter 1} Meta})} (.function# _ msg (.function# _ state {#Left msg}))) - #0) + ..private) (.def# text#composite (.is# (Function Text (Function Text Text)) (.function# _ x (.function# _ y (.text_composite# x y)))) - #0) + ..private) ... https://en.wikipedia.org/wiki/Delimiter (.def# name_delimiter (.is# Text ".") - #0) + ..private) (.def# name#as (.is# (Function Name @@ -795,28 +804,28 @@ (.when# module "" name _ (.text_composite# module ..name_delimiter name))))) - #0) + ..private) (.def# \'' (.is# Text (.int_char# +34)) - #0) + ..private) (.def# wrong_syntax (.is# Error "Wrong syntax.") - #1) + ..public) (.def# list#as_stack - (.is# {#Universal {#Empty} - (Function {#Reification {#Parameter 1} List} - {#Reification {#Parameter 1} Stack})} + (.is# {#Quantification .universal {#Empty} + (Function {#Reification {#Parameter 1} List} + {#Reification {#Parameter 1} Stack})} (.function# _ it - ((.is# {#Universal {#Empty} - (Function {#Reification {#Parameter 1} List} - (Function Natural - (Function {#Reification {#Parameter 1} Stack} - {#Reification {#Parameter 1} Stack})))} + ((.is# {#Quantification .universal {#Empty} + (Function {#Reification {#Parameter 1} List} + (Function Natural + (Function {#Reification {#Parameter 1} Stack} + {#Reification {#Parameter 1} Stack})))} (.function# next it (.function# _ remaining (.function# _ value @@ -841,19 +850,19 @@ .public) (.def# list#of_stack - (.is# {#Universal {#Empty} - (Function {#Reification {#Parameter 1} Stack} - {#Reification {#Parameter 1} List})} + (.is# {#Quantification .universal {#Empty} + (Function {#Reification {#Parameter 1} Stack} + {#Reification {#Parameter 1} List})} (.function# _ it (.when# it {#Empty} (list) {#Top head tail} - ((.is# {#Universal {#Empty} - (Function {#Reification {#Parameter 1} Stack} - (Function {#Reification {#Parameter 1} List} - {#Reification {#Parameter 1} List}))} + ((.is# {#Quantification .universal {#Empty} + (Function {#Reification {#Parameter 1} Stack} + (Function {#Reification {#Parameter 1} List} + {#Reification {#Parameter 1} List}))} (.function# next it (.function# _ value (.when# it @@ -877,7 +886,7 @@ _ (failure ..wrong_syntax))))) - #0) + ..private) (.def# code#function (.is# (Function Code (Function {#Reification Code Stack} (Function Code Code))) @@ -893,7 +902,7 @@ self head (code#function (code#name ["" ""]) tail output)))))))) - #0) + ..private) (.def# function' (.as# Macro @@ -911,7 +920,7 @@ _ (failure ..wrong_syntax))))) - #0) + ..private) (.def# code#def (.is# (Function Code (Function Code (Function Code Code))) @@ -920,7 +929,7 @@ name value export_policy)))) - #0) + ..private) (.def# code#checked (.is# (Function Code (Function Code Code)) @@ -928,7 +937,7 @@ (code#form (list (code#name [..prelude "is#"]) type value)))) - #0) + ..private) (.def# code#macro (.is# (Function Code @@ -939,7 +948,7 @@ (code#form (list (code#name [..prelude "is#"]) (code#name [..prelude "Macro'"]) expression)))))) - #0) + ..private) (.def# the' (.as# Macro @@ -969,7 +978,7 @@ _ (failure ..wrong_syntax))))) - #0) + ..private) (.def# macro (.as# Macro @@ -986,7 +995,7 @@ _ (failure ..wrong_syntax))))) - #1) + ..public) (the' .public comment Macro @@ -995,14 +1004,14 @@ (the' .private (stack#mix f init xs) ... (for_any (_ a b) (-> (-> b a a) a (Stack b) a)) - {#Universal {#Empty} - {#Universal {#Empty} - (Function (Function {#Parameter 1} + {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Function (Function {#Parameter 1} + (Function {#Parameter 3} + {#Parameter 3})) (Function {#Parameter 3} - {#Parameter 3})) - (Function {#Parameter 3} - (Function {#Reification {#Parameter 1} Stack} - {#Parameter 3})))}} + (Function {#Reification {#Parameter 1} Stack} + {#Parameter 3})))}} (.when# xs {#Empty} init @@ -1026,39 +1035,39 @@ (failure ..wrong_syntax)))) (the' .private (stack#reversed stack) - {#Universal {#Empty} - (Function ($ Stack {#Parameter 1}) - ($ Stack {#Parameter 1}))} - (stack#mix (.is# {#Universal {#Empty} - (Function {#Parameter 1} (Function ($ Stack {#Parameter 1}) ($ Stack {#Parameter 1})))} + {#Quantification .universal {#Empty} + (Function ($ Stack {#Parameter 1}) + ($ Stack {#Parameter 1}))} + (stack#mix (.is# {#Quantification .universal {#Empty} + (Function {#Parameter 1} (Function ($ Stack {#Parameter 1}) ($ Stack {#Parameter 1})))} (function' (_ head tail) {#Top head tail})) {#Empty} stack)) (the' .private (stack#each f xs) - {#Universal {#Empty} - {#Universal {#Empty} - (Function (Function {#Parameter 3} {#Parameter 1}) - (Function ($ Stack {#Parameter 3}) - ($ Stack {#Parameter 1})))}} + {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Function (Function {#Parameter 3} {#Parameter 1}) + (Function ($ Stack {#Parameter 3}) + ($ Stack {#Parameter 1})))}} (stack#mix (function' (_ head tail) {#Top (f head) tail}) {#Empty} (stack#reversed xs))) (the' .private (list#each value it) - {#Universal {#Empty} - {#Universal {#Empty} - (Function (Function {#Parameter 3} {#Parameter 1}) - (Function ($ List {#Parameter 3}) - ($ List {#Parameter 1})))}} + {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Function (Function {#Parameter 3} {#Parameter 1}) + (Function ($ List {#Parameter 3}) + ($ List {#Parameter 1})))}} (list#of_stack (stack#each value (list#as_stack it)))) (the' .private (list#size it) - {#Universal {#Empty} - (Function ($ List {#Parameter 1}) - Natural)} + {#Quantification .universal {#Empty} + (Function ($ List {#Parameter 1}) + Natural)} (.list_size# it)) (the' .private (text#= expected actual) @@ -1072,9 +1081,9 @@ (.as# Integer subject)))) (the' .private (stack#size stack) - {#Universal {#Empty} - (Function ($ Stack {#Parameter 1}) - Natural)} + {#Quantification .universal {#Empty} + (Function ($ Stack {#Parameter 1}) + Natural)} (stack#mix (function' (_ _ acc) (.i64_+# 1 acc)) 0 @@ -1097,17 +1106,19 @@ head tail))) -(the' .private (code#Universal body) +(the' .private (code#universal_quantification body) (Function Code Code) - (code#variant (list (code#name [..prelude "#Universal"]) + (code#variant (list (code#name [..prelude "#Quantification"]) + (code#name [..prelude "universal"]) ..|#Empty| body))) -(the' .private (code#Existential body) +(the' .private (code#existential_quantification body) (Function Code Code) - (code#variant (list (code#name [..prelude "#Existential"]) + (code#variant (list (code#name [..prelude "#Quantification"]) + (code#name [..prelude "existential"]) ..|#Empty| body))) @@ -1164,13 +1175,9 @@ [polarity (__adjusted_quantified_type__ permission depth it)])) parameters)} - {#Universal environment body} - {#Universal environment - (__adjusted_quantified_type__ permission (next_level depth) body)} - - {#Existential environment body} - {#Existential environment - (__adjusted_quantified_type__ permission (next_level depth) body)} + {#Quantification quantification environment body} + {#Quantification quantification environment + (__adjusted_quantified_type__ permission (next_level depth) body)} {#Reification parameter function} {#Reification (__adjusted_quantified_type__ permission depth parameter) @@ -1207,25 +1214,25 @@ (the' .private (list#mix mix complete partial) ... (for_any (_ a b) (-> (-> b a a) a (List b) a)) - {#Universal {#Empty} - {#Universal {#Empty} - (Function (Function {#Parameter 1} + {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Function (Function {#Parameter 1} + (Function {#Parameter 3} + {#Parameter 3})) (Function {#Parameter 3} - {#Parameter 3})) - (Function {#Parameter 3} - (Function {#Reification {#Parameter 1} List} - {#Parameter 3})))}} + (Function {#Reification {#Parameter 1} List} + {#Parameter 3})))}} (.when# (.list_size# partial) limit - ((.is# {#Universal {#Empty} - {#Universal {#Empty} - (Function Natural - (Function (Function {#Parameter 1} + ((.is# {#Quantification .universal {#Empty} + {#Quantification .universal {#Empty} + (Function Natural + (Function (Function {#Parameter 1} + (Function {#Parameter 3} + {#Parameter 3})) (Function {#Parameter 3} - {#Parameter 3})) - (Function {#Parameter 3} - (Function {#Reification {#Parameter 1} List} - {#Parameter 3}))))}} + (Function {#Reification {#Parameter 1} List} + {#Parameter 3}))))}} (function' (list#mix item mix complete partial) (.when# (.int_<# (.as# Integer limit) (.as# Integer item)) @@ -1286,7 +1293,7 @@ [offset body'] [(.i64_+# 2 offset) (code#let parameter (quantified_type_parameter (.i64_+# offset 1)) - (code#Universal body'))])) + (code#universal_quantification body'))])) [0 (with_quantification (stack#size args) body)] args) @@ -1324,7 +1331,7 @@ [offset body'] [(.i64_+# 2 offset) (code#let parameter (quantified_type_parameter (.i64_+# offset 1)) - (code#Existential body'))])) + (code#existential_quantification body'))])) [0 (with_quantification (stack#size args) body)] args) @@ -1567,7 +1574,7 @@ {#Top [..prelude "#in"] {#Top [..prelude "#then"] {#Empty}}}) - #0) + ..private) (.def# #in (slot [{#Some [0 #0 ..monad_slots]} Monad]) .private) (.def# #then (slot [{#Some [0 #1 ..monad_slots]} Monad]) .private) @@ -2051,17 +2058,9 @@ [{#Opaque idL} {#Opaque idR}] (.i64_=# idL idR) - [{#Universal envL bodyL} {#Universal envR bodyR}] - (all and' - (.i64_=# (stack#size envL) (stack#size envR)) - (every? (function' (_ l,r) - (let' [[itL itR] l,r] - (type#= itL itR))) - (zipped_2 envL envR)) - (type#= bodyL bodyR)) - - [{#Existential envL bodyL} {#Existential envR bodyR}] + [{#Quantification quantification_of_reference envL bodyL} {#Quantification quantification_of_it envR bodyR}] (all and' + (bit#= quantification_of_reference quantification_of_it) (.i64_=# (stack#size envL) (stack#size envR)) (every? (function' (_ l,r) (let' [[itL itR] l,r] @@ -3181,8 +3180,11 @@ (-> ($ Stack it) Bit)) (.when# xs - {#Empty} #1 - _ #0)) + {#Empty} + #1 + + _ + #0)) (with_template [ ] [(the' .private ( left,right) @@ -3248,12 +3250,15 @@ {#Opaque id} (.text_composite# "+" (natural#as id)) - {#Universal env body} - (.text_composite# "(for_any " (type#as_text body) ")") + {#Quantification quantification env body} + (.text_composite# "(" + (if (bit#= .universal quantification) + "for_any" + "for_some") + " " + (type#as_text body) + ")") - {#Existential env body} - (.text_composite# "(for_some " (type#as_text body) ")") - {#Reification _} (let' [[func args] (flat_reification type)] (.text_composite# @@ -4006,18 +4011,10 @@ {#Reification arg func} {#Reification (reduced env arg) (reduced env func)} - {#Universal ?local_env ?local_def} + {#Quantification quantification ?local_env ?local_def} (when ?local_env {#Empty} - {#Universal env ?local_def} - - _ - type) - - {#Existential ?local_env ?local_def} - (when ?local_env - {#Empty} - {#Existential env ?local_def} + {#Quantification quantification env ?local_def} _ type) @@ -4041,10 +4038,7 @@ (-> Type Type (Maybe Type)) (when type_fn - {#Universal env body} - {#Some (reduced (stack#partial type_fn param env) body)} - - {#Existential env body} + {#Quantification quantification env body} {#Some (reduced (stack#partial type_fn param env) body)} {#Reification A F} @@ -4083,10 +4077,7 @@ [output (applied_type arg func)] (interface_methods output)) - {#Universal _ it} - (interface_methods it) - - {#Existential _ it} + {#Quantification quantification _ it} (interface_methods it) {#Named name it} @@ -4175,10 +4166,7 @@ {#Reification arg func} (record_slots func) - {#Universal env body} - (record_slots body) - - {#Existential env body} + {#Quantification quantification env body} (record_slots body) {#Named [module name] unnamed} @@ -4989,13 +4977,9 @@ {#Reification (clean_type variables left) (clean_type variables right)} - {#Universal environment unquantified} - {#Universal (stack#each (clean_type variables) environment) - (clean_type variables unquantified)} - - {#Existential environment unquantified} - {#Existential (stack#each (clean_type variables) environment) - (clean_type variables unquantified)} + {#Quantification quantification environment unquantified} + {#Quantification quantification (stack#each (clean_type variables) environment) + (clean_type variables unquantified)} {#Named name anonymous} it @@ -5261,7 +5245,7 @@ _ (in (stack (` (.def# (, (code#local (..module_alias (stack proper imported_module) alias))) (, source+) - #0))))))) + ..private))))))) (the (implementation_declarations imported_module alias implementation) (-> Text Text Name @@ -5333,7 +5317,7 @@ _ (do meta#monad ['implementation (..generated_name "implementation")] - (in [{#Top (` (.def# (, 'implementation) (, it) #0)) pre_defs} + (in [{#Top (` (.def# (, 'implementation) (, it) ..private)) pre_defs} {#Top 'implementation implementations}])))) [(stack) (stack)] implementations)) @@ -5667,12 +5651,11 @@ [.#Variable] [.#Opaque]) - (with_template#pattern [] - [{ env type} - (let [env' (untemplated_stack (stack#each type_code env))] - (` { (, env') (, (type_code type))}))]) - ([.#Universal] - [.#Existential]) + {.#Quantification quantification env type} + (let [env' (untemplated_stack (stack#each type_code env))] + (` {.#Quantification (, (code#bit quantification)) + (, env') + (, (type_code type))})) {#Named [module name] anonymous} ... TODO: Generate the explicit type definition instead of using @@ -6138,13 +6121,6 @@ _ (failure ..wrong_syntax)))) -(with_template [ ] - [(the .public Bit )] - - [#0 false] - [#1 true] - ) - (the .public try (macro (_ tokens) (when tokens diff --git a/stdlib/source/library/lux/compiler/language/lux.lux b/stdlib/source/library/lux/compiler/language/lux.lux index 1b3cd65e3..70224ec93 100644 --- a/stdlib/source/library/lux/compiler/language/lux.lux +++ b/stdlib/source/library/lux/compiler/language/lux.lux @@ -33,8 +33,7 @@ _.natural _.natural _.natural - (_.and (_.stack type) type) - (_.and (_.stack type) type) + (all _.and _.bit (_.stack type) type) (_.and type type) (_.and (_.and _.text _.text) type)))) @@ -73,8 +72,7 @@ .natural .natural .natural - (<>.and (.stack type) type) - (<>.and (.stack type) type) + (all <>.and .bit (.stack type) type) (<>.and type type) (<>.and (<>.and .text .text) type)))) diff --git a/stdlib/source/library/lux/compiler/language/lux/analysis/inference.lux b/stdlib/source/library/lux/compiler/language/lux/analysis/inference.lux index 94e241dce..a01c16791 100644 --- a/stdlib/source/library/lux/compiler/language/lux/analysis/inference.lux +++ b/stdlib/source/library/lux/compiler/language/lux/analysis/inference.lux @@ -81,13 +81,10 @@ {.#Parameter @parameter} :it:) - (,, (template.with [] - [{ env body} - { (stack#each (quantified @variable @parameter) env) - (quantified @variable (n.+ 2 @parameter) body)}] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env body} + {.#Quantification quantification + (stack#each (quantified @variable @parameter) env) + (quantified @variable (n.+ 2 @parameter) body)} (^.or {.#Parameter _} {.#Opaque _} @@ -119,12 +116,12 @@ {.#Named name unnamedT} (general' variables archive analyse unnamedT args) - {.#Universal _} + {.#Quantification .universal _} (do phase.monad [[@variable :variable:] (/type.check check.var)] (general' (stack.partial @variable variables) archive analyse (maybe.trusted (type.reified (list :variable:) inferT)) args)) - {.#Existential _} + {.#Quantification .existential _} (do phase.monad [:ex: /type.existential] (general' variables archive analyse (maybe.trusted (type.reified (list (@type.old :ex:)) inferT)) args)) @@ -220,13 +217,10 @@ {.#Reification left right} {.#Reification (again left) (again right)} - (,, (template.with [] - [{ environment quantified} - { (stack#each again environment) - (with_recursion (n.+ 2 @self) recursion quantified)}] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification environment quantified} + {.#Quantification quantification + (stack#each again environment) + (with_recursion (n.+ 2 @self) recursion quantified)} {.#Nominal name parameters} {.#Nominal name (list#each (function (_ [polarity it]) @@ -253,13 +247,9 @@ {.#Named name it} (again depth it) - (,, (template.with [] - [{ env it} - (phase#each (|>> { env}) - (again (++ depth) it))] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env it} + (phase#each (|>> {.#Quantification quantification env}) + (again (++ depth) it)) {.#Reification parameter abstraction} (when (type.reified (list parameter) abstraction) diff --git a/stdlib/source/library/lux/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/library/lux/compiler/language/lux/phase/analysis/complex.lux index c9662d3d3..a6566b02b 100644 --- a/stdlib/source/library/lux/compiler/language/lux/phase/analysis/complex.lux +++ b/stdlib/source/library/lux/compiler/language/lux/phase/analysis/complex.lux @@ -146,12 +146,13 @@ _ (/.except ..cannot_infer_sum [here expectedT lefts right? valueC]))) - {.#Universal _} + {.#Quantification .universal _} (do ! [[@instance :instance:] (/type.check check.existential)] (<| (/type.expecting (maybe.trusted (type.reified (list :instance:) expectedT))) (again valueC))) - {.#Existential _} + + {.#Quantification .existential _} (<| /type.with_var (function (_ [@instance :instance:])) (/type.expecting (maybe.trusted (type.reified (list :instance:) expectedT))) @@ -278,13 +279,13 @@ @ /.provenance] (in (/.tuple @ (list#each product.right membersTA)))))) - {.#Universal _} + {.#Quantification .universal _} (do ! [[@instance :instance:] (/type.check check.existential)] (<| (/type.expecting (maybe.trusted (type.reified (list :instance:) expectedT))) (product analyse archive membersC))) - {.#Existential _} + {.#Quantification .existential _} (<| /type.with_var (function (_ [@instance :instance:])) (/type.expecting (maybe.trusted (type.reified (list :instance:) expectedT))) diff --git a/stdlib/source/library/lux/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/library/lux/compiler/language/lux/phase/analysis/function.lux index b8263160d..2df35a4af 100644 --- a/stdlib/source/library/lux/compiler/language/lux/phase/analysis/function.lux +++ b/stdlib/source/library/lux/compiler/language/lux/phase/analysis/function.lux @@ -93,12 +93,12 @@ {.#None} (/.failure (exception.error ..cannot_analyse [here expectedT function_name arg_name body]))) - {.#Universal _} + {.#Quantification .universal _} (do ! [[@instance :instance:] (/type.check check.existential)] (again (maybe.trusted (type.reified (list :instance:) expectedT)))) - {.#Existential _} + {.#Quantification .existential _} (<| /type.with_var (.function (_ [@instance :instance:])) (again (maybe.trusted (type.reified (list :instance:) expectedT)))) @@ -132,7 +132,7 @@ {try.#Failure _} (|> not_quantified (/inference.quantified @input 1) - {.#Universal (stack)})))] + {.#Quantification .universal (stack)})))] (in functionA))))) _ diff --git a/stdlib/source/library/lux/compiler/language/lux/phase/analysis/when.lux b/stdlib/source/library/lux/compiler/language/lux/phase/analysis/when.lux index 0da87ea2d..c70e00bfe 100644 --- a/stdlib/source/library/lux/compiler/language/lux/phase/analysis/when.lux +++ b/stdlib/source/library/lux/compiler/language/lux/phase/analysis/when.lux @@ -97,7 +97,7 @@ baseT {.#Top head tail} - (quantified tail {.#Universal head baseT}))) + (quantified tail {.#Quantification .universal head baseT}))) ... Type-checking on the input value is done during the analysis of a ... "when" expression, to ensure that the patterns being used make @@ -133,10 +133,10 @@ {.#Named name unnamedT} (again envs unnamedT) - {.#Universal env unquantifiedT} + {.#Quantification .universal env unquantifiedT} (again {.#Top env envs} unquantifiedT) - {.#Existential _} + {.#Quantification .existential _} (do check.monad [[@head :head:] check.var [tail :tuple:] (again envs (maybe.trusted (type.reified (.list :head:) :it:)))] @@ -188,10 +188,10 @@ {.#Named name type} (list envs type) - {.#Universal env type} + {.#Quantification .universal env type} (list {.#Top env envs} type) - {.#Existential _} + {.#Quantification .existential _} (do check.monad [[@head type_of_head] check.var [tail type] (list envs (maybe.trusted (type.reified (.list type_of_head) type)))] @@ -355,7 +355,7 @@ _ (/.except ..sum_has_no_case [idx :input:]))) - {.#Universal _} + {.#Quantification .universal _} (do ! [[ex_id exT] (/type.check check.existential) it (pattern_analysis (maybe.trusted (type.reified (.list exT) :input:')) diff --git a/stdlib/source/library/lux/compiler/language/lux/phase/extension/analysis/jvm.lux b/stdlib/source/library/lux/compiler/language/lux/phase/extension/analysis/jvm.lux index e95255bf8..8ad123c5b 100644 --- a/stdlib/source/library/lux/compiler/language/lux/phase/extension/analysis/jvm.lux +++ b/stdlib/source/library/lux/compiler/language/lux/phase/extension/analysis/jvm.lux @@ -609,12 +609,8 @@ {.#Parameter id}) (phase#in (jvm.class (list) ..object_class)) - (,, (template.with [] - [{ env unquantified} - (check_parameter unquantified)] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env unquantified} + (check_parameter unquantified) {.#Reification inputT abstractionT} (when (type.reified (list inputT) abstractionT) @@ -676,12 +672,8 @@ {.#Named name anonymous} (check_jvm anonymous) - (,, (template.with [] - [{ env unquantified} - (check_jvm unquantified)] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env unquantified} + (check_jvm unquantified) {.#Reification inputT abstractionT} (when (type.reified (list inputT) abstractionT) diff --git a/stdlib/source/library/lux/compiler/language/lux/phase/extension/declaration/lux.lux b/stdlib/source/library/lux/compiler/language/lux/phase/extension/declaration/lux.lux index f3a13393e..79fbd0cb8 100644 --- a/stdlib/source/library/lux/compiler/language/lux/phase/extension/declaration/lux.lux +++ b/stdlib/source/library/lux/compiler/language/lux/phase/extension/declaration/lux.lux @@ -276,21 +276,17 @@ {.#Reification left right} {.#Reification (again left) (again right)} + + {.#Quantification quantification closure body} + {.#Quantification quantification closure (again body)} + + {.#Named name anonymous} + {.#Named name (again anonymous)} (^.or {.#Parameter _} {.#Variable _} {.#Opaque _}) - type - - (,, (template.with [] - [{ closure body} - { closure (again body)}] - - [.#Universal] - [.#Existential])) - - {.#Named name anonymous} - {.#Named name (again anonymous)}))))) + type))))) (the .public bundle Bundle diff --git a/stdlib/source/library/lux/compiler/type.lux b/stdlib/source/library/lux/compiler/type.lux index 0d357d1b1..10817c319 100644 --- a/stdlib/source/library/lux/compiler/type.lux +++ b/stdlib/source/library/lux/compiler/type.lux @@ -19,11 +19,7 @@ function Type - #Nominal - #Parameter #Variable #Opaque - #Universal #Existential - #Reification - #Named + #Nominal #Parameter #Variable #Opaque #Quantification #Reification #Named Provenance Code @@ -62,18 +58,6 @@ ["[0]" name]] ["[0]" function]]]) -... https://ncatlab.org/nlab/show/polarity+in+type+theory -(the .public Polarity - .Bit) - -(the contra_variant - Polarity - false) - -(the co_variant - Polarity - true) - (the prefix name.delimiter) @@ -86,21 +70,21 @@ (the with_template (.in_module# .prelude .with_template)) (the template#macro (.in_module# .prelude .template#macro)) -(expansion#let [,each_simple (these [bit Bit ..co_variant ..co_variant] - [decimal Decimal ..co_variant ..co_variant] - [text Text ..co_variant ..co_variant] - [tag Tag ..co_variant ..co_variant] - [slot Slot ..co_variant ..co_variant] - [macro Macro ..co_variant ..co_variant] - [eval Eval ..co_variant ..co_variant]) - ,each_complex (these [i64 I64 ..co_variant ..co_variant] - [list List ..co_variant ..co_variant]) - ,each_integer (these [natural Natural ..co_variant ..co_variant] - [integer Integer ..co_variant ..co_variant] - [revolution Revolution ..co_variant ..co_variant]) - ,each_2 (these [sum Sum ..co_variant ..co_variant] - [product Product ..co_variant ..co_variant] - [function Function ..contra_variant ..co_variant]) +(expansion#let [,each_simple (these [bit Bit .co_variant .co_variant] + [decimal Decimal .co_variant .co_variant] + [text Text .co_variant .co_variant] + [tag Tag .co_variant .co_variant] + [slot Slot .co_variant .co_variant] + [macro Macro .co_variant .co_variant] + [eval Eval .co_variant .co_variant]) + ,each_complex (these [i64 I64 .co_variant .co_variant] + [list List .co_variant .co_variant]) + ,each_integer (these [natural Natural .co_variant .co_variant] + [integer Integer .co_variant .co_variant] + [revolution Revolution .co_variant .co_variant]) + ,each_2 (these [sum Sum .co_variant .co_variant] + [product Product .co_variant .co_variant] + [function Function .contra_variant .co_variant]) ,each (these ,each_simple ,each_complex ,each_integer @@ -130,7 +114,7 @@ [(the .public ,type .Type (for_any (_ it) - {.#Nominal (its #name ,name) (.list [..co_variant it])}))] + {.#Nominal (its #name ,name) (.list [.co_variant it])}))] ,each_complex ) @@ -138,7 +122,7 @@ [(the .public ,type .Type {.#Nominal (its #name ..i64) - (.list [..co_variant {.#Nominal (its #name ,name) (.list)}])})] + (.list [.co_variant {.#Nominal (its #name ,name) (.list)}])})] ,each_integer ) @@ -163,22 +147,15 @@ (`` (the List' (<| (template#macro (_ ,it)) - [{.#Nominal (its #name ..list) (.list [(,, (static ..co_variant)) ,it])}]))) - -... https://en.wikipedia.org/wiki/Quantifier_(logic) -(the Quantification - (<| (template#macro (_ ,it)) - [[(.Stack ,it) - ,it]])) + [{.#Nominal (its #name ..list) (.list [(,, (static .co_variant)) ,it])}]))) (every .public (Type _) (Variant - {#Nominal ..Text (..List' [..Polarity (Type _)])} + {#Nominal ..Text (..List' [.Polarity (Type _)])} {#Parameter ..Natural} {#Variable ..Natural} {#Opaque ..Natural} - {#Universal (Quantification (Type _))} - {#Existential (Quantification (Type _))} + {#Quantification .Quantification (.Stack (Type _)) (Type _)} {#Reification (Type _) (Type _)} {#Named ..Name (Type _)})) @@ -205,11 +182,11 @@ ... )) ... (,, (with_template [,new ,old] - ... [{,new environment body} + ... [{#Quantification ,new environment body} ... {,old (stack#each old environment) (old body)}] - ... [#Universal .#Universal] - ... [#Existential .#Existential] + ... [.universal .#Universal] + ... [.existential .#Existential] ... )) ... (,, (with_template [,new ,old] @@ -245,10 +222,10 @@ ... (,, (with_template [,new ,old] ... [{,old environment body} - ... {,new (stack#each new environment) (new body)}] + ... {#Quantification ,new (stack#each new environment) (new body)}] - ... [#Universal .#Universal] - ... [#Existential .#Existential] + ... [.universal .#Universal] + ... [.existential .#Existential] ... )) ... (,, (with_template [,new ,old] @@ -350,32 +327,6 @@ {#Alias Alias} {#Default Default})) -(the (old_global it) - (-> ..Global - .Global) - (when it - {#Definition [type it]} - {.#Definition [(..old type) it]} - - {#Default [type it]} - {.#Default [(..old type) it]} - - {#Alias it} - {.#Alias it})) - -(the (new_global it) - (-> .Global - ..Global) - (when it - {.#Definition [type it]} - {#Definition [(..new type) it]} - - {.#Default [type it]} - {#Default [(..new type) it]} - - {.#Alias it} - {#Alias it})) - (every .public Module (Record [#module_hash ..Natural @@ -479,7 +430,7 @@ (the (nominal code [name parameters]) (-> (Injection .Type) - (Injection [Text (List [Polarity .Type])])) + (Injection [Text (List [.Polarity .Type])])) (code#variant (.list (code#natural 0) (code#bit #0) (code#tuple (.list (code#text name) @@ -502,29 +453,21 @@ [3 .#Opaque] )) - (,, (with_template [,lefts ,tag] - [{,tag closure body} - (code#variant (.list (code#natural ,lefts) - (code#bit #0) - (code#tuple (.list (code#stack code closure) - (code body)))))] - - [4 .#Universal] - [5 .#Existential] - )) + {.#Quantification quantification closure body} + (code#variant (.list (code#natural 4) + (code#bit #0) + (code#tuple (.list (code#bit quantification) + (code#stack code closure) + (code body))))) - (,, (with_template [,lefts ,tag] - [{,tag left right} - (code#variant (.list (code#natural ,lefts) - (code#bit #0) - (code#tuple (.list (code left) - (code right)))))] - - [6 .#Reification] - )) + {.#Reification left right} + (code#variant (.list (code#natural 5) + (code#bit #0) + (code#tuple (.list (code left) + (code right))))) {.#Named [module proper] anonymous} - (code#variant (.list (code#natural 6) + (code#variant (.list (code#natural 5) (code#bit #1) (code#tuple (.list (code#tuple (.list (code#text module) (code#text proper))) diff --git a/stdlib/source/library/lux/type.lux b/stdlib/source/library/lux/type.lux index 0680823e7..782f89c60 100644 --- a/stdlib/source/library/lux/type.lux +++ b/stdlib/source/library/lux/type.lux @@ -49,14 +49,14 @@ (loop (value [num_args 0 type type]) (when type - { env sub_type} + {.#Quantification env sub_type} (value (++ num_args) sub_type) _ [num_args type])))] - [flat_univ_q .#Universal] - [flat_ex_q .#Existential] + [flat_univ_q .universal] + [flat_ex_q .existential] ) (the template#macro (.in_module# .prelude .template#macro)) @@ -174,7 +174,7 @@ (text "(" (as_text' name_format type_func) " " (|> type_args (list#each (as_text' name_format)) list.reversed (list.interposed " ") (list#mix text#composite "")) ")")) (,, (with_template' [ ] - [{ env body} + [{.#Quantification env body} (text "(" " {" @@ -186,8 +186,8 @@ (as_text' name_format body) ")")] - [.#Universal "All"] - [.#Existential "Ex"])) + [.universal "for_any"] + [.existential "for_some"])) {.#Named name type} (by name_format as name) @@ -216,17 +216,15 @@ {.#Reification left right} {.#Reification (reduced env left) (reduced env right)} - (,, (with_template' [] - [{ old_env def} - (when old_env - {.#Empty} - { (list.as_stack env) def} - - _ - { (stack#each (reduced env) old_env) def})] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification old_env def} + {.#Quantification quantification + (when old_env + {.#Empty} + (list.as_stack env) + + _ + (stack#each (reduced env) old_env)) + def} {.#Parameter idx} (try.else (halt! (text "Unknown type parameter" @@ -279,14 +277,11 @@ [reference {.#Named _ it}] (= reference it) - (,, (with_template' [] - [[{ reference_closure reference_body} { it_closure it_body}] - (and (by (stack.equivalence =) = reference_closure it_closure) - (= reference_body it_body))] - - [.#Universal] - [.#Existential] - )) + [{.#Quantification quantification_of_reference reference_closure reference_body} + {.#Quantification quantification_of_it it_closure it_body}] + (and (bit.= quantification_of_reference quantification_of_it) + (by (stack.equivalence =) = reference_closure it_closure) + (= reference_body it_body)) _ false @@ -301,14 +296,10 @@ (list.mix' maybe.monad (.function (on parameter abstraction) (when abstraction - (,, (with_template' [] - [{ env body} - {.#Some (reduced (list#composite (list abstraction parameter) - (list.of_stack env)) - body)}] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env body} + {.#Some (reduced (list#composite (list abstraction parameter) + (list.of_stack env)) + body)} {.#Reification parameter' abstraction} (do maybe.monad @@ -349,13 +340,10 @@ {.#Named name sub_type} (code.name name) - (,, (with_template' [] - [{ env body} - (` { (.stack (,* (list.of_stack (stack#each code env)))) - (, (code body))})] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env body} + (` {.#Quantification (, (code.bit quantification)) + (.stack (,* (list.of_stack (stack#each code env)))) + (, (code body))}) ))) (the .public (de_aliased type) @@ -421,16 +409,19 @@ 0 body _ (|> body ( (-- size)) - { (stack)})))] + {.#Quantification (stack)})))] - [univ_q .#Universal] - [ex_q .#Existential] + [univ_q .universal] + [ex_q .existential] ) (`` (the .public (quantified? type) (-> Type Bit) (when type + {.#Quantification _} + true + {.#Named [module name] _type} (quantified? _type) @@ -439,13 +430,6 @@ (by maybe.monad each quantified?) (maybe.else false)) - (,, (with_template' [] - [ - true] - - [{.#Universal _}] - [{.#Existential _}])) - _ false))) @@ -591,13 +575,10 @@ {.#Reification (value left) (value right)} - (,, (with_template' [] - [{ env body} - { (stack#each value env) - (value body)}] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification env body} + {.#Quantification quantification + (stack#each value env) + (value body)} (,, (with_template' [] [ diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux index a36ba1fd2..baed5269e 100644 --- a/stdlib/source/library/lux/type/check.lux +++ b/stdlib/source/library/lux/type/check.lux @@ -438,12 +438,12 @@ (let [[super_parameter super_abstraction] super [sub_parameter sub_abstraction] sub] (when [super_abstraction sub_abstraction] - [{.#Universal _ _} {.#Opaque _}] + [{.#Quantification .universal _ _} {.#Opaque _}] (do ..monad [super' (..on (list super_parameter) super_abstraction)] (complete [hypotheses super' {.#Reification sub}])) - [{.#Opaque _} {.#Universal _ _}] + [{.#Opaque _} {.#Quantification .universal _ _}] (do ..monad [sub' (..on (list sub_parameter) sub_abstraction)] (complete [hypotheses {.#Reification super} sub'])) @@ -469,7 +469,7 @@ [super_abstraction' (..type id)] (complete [hypotheses {.#Reification super_parameter super_abstraction'} {.#Reification sub}])) (when sub_abstraction - {.#Universal _ _} + {.#Quantification .universal _ _} (do ..monad [sub' (..on (list sub_parameter) sub_abstraction)] (complete [hypotheses {.#Reification super} sub'])) @@ -682,25 +682,25 @@ (`` (when [super sub] ... TODO: Refactor-away as cold-code (,, (template.with [ ] - [[{ _} _] + [[{.#Quantification _} _] (do ..monad [[_ paramT] super' (..on (list paramT) super)] (complete [hypotheses super' sub]))] - [.#Universal ..existential] - [.#Existential ..var])) + [.universal ..existential] + [.existential ..var])) ... TODO: Refactor-away as cold-code (,, (template.with [ ] - [[_ { _}] + [[_ {.#Quantification _}] (do ..monad [[_ paramT] sub' (..on (list paramT) sub)] (complete [hypotheses super sub']))] - [.#Universal ..var] - [.#Existential ..existential])) + [.universal ..var] + [.existential ..existential])) _ (partial it)))))) @@ -804,13 +804,9 @@ failure (in inputT)))) - (,, (template.with [] - [{ envT+ unquantifiedT} - (do [! ..monad] - [envT+' (stack.each' ! (clean aliases) envT+) - unquantifiedT' (clean aliases unquantifiedT)] - (in { envT+' unquantifiedT'}))] - - [.#Universal] - [.#Existential])) + {.#Quantification quantification envT+ unquantifiedT} + (do [! ..monad] + [envT+' (stack.each' ! (clean aliases) envT+) + unquantifiedT' (clean aliases unquantifiedT)] + (in {.#Quantification quantification envT+' unquantifiedT'})) ))) diff --git a/stdlib/source/library/lux/type/implicit.lux b/stdlib/source/library/lux/type/implicit.lux index d7710048c..610d6c1bf 100644 --- a/stdlib/source/library/lux/type/implicit.lux +++ b/stdlib/source/library/lux/type/implicit.lux @@ -222,7 +222,7 @@ {.#Named _ func'} (on_argument arg func') - {.#Universal _} + {.#Quantification .universal _} (do check.monad [[id var] check.var] (|> func @@ -242,7 +242,7 @@ (-> Type (Check [(Stack Natural) Type])) (when type - {.#Universal _} + {.#Quantification .universal _} (do check.monad [[id var] check.var [ids final_output] (concrete_type (maybe.trusted (//.reified (list var) type)))] diff --git a/stdlib/source/library/lux/type/poly.lux b/stdlib/source/library/lux/type/poly.lux index eb758c9b0..924c751f7 100644 --- a/stdlib/source/library/lux/type/poly.lux +++ b/stdlib/source/library/lux/type/poly.lux @@ -77,7 +77,7 @@ (the recursive (template.macro (_ ,type) [{.#Reification (..recursion_parameter) - {.#Universal (stack) ,type}}])) + {.#Quantification .universal (stack) ,type}}])) (the recursion (template.macro (_) @@ -86,7 +86,7 @@ (the polymorphic (template.macro (_ ,name ,non_quantified) - [{.#Named ,name {.#Universal (stack) ,non_quantified}}])) + [{.#Named ,name {.#Quantification .universal (stack) ,non_quantified}}])) (every Context (Dictionary Natural Code)) diff --git a/stdlib/source/projection/lux/data/binary.lux b/stdlib/source/projection/lux/data/binary.lux index 84fa7c0b5..6c594707f 100644 --- a/stdlib/source/projection/lux/data/binary.lux +++ b/stdlib/source/projection/lux/data/binary.lux @@ -311,16 +311,14 @@ (Projection Type) (..rec (function (_ type) - (let [indexed ..natural - quantified (//.and (..stack type) type)] + (let [indexed ..natural] (!variant [[0 [.#Nominal] (//.and ..text (..list (//.and bit type)))] [1 [.#Parameter] indexed] [2 [.#Variable] indexed] [3 [.#Opaque] indexed] - [4 [.#Universal] quantified] - [5 [.#Existential] quantified] - [6 [.#Reification] (//.and type type)] - [7 [.#Named] (//.and ..name type)]]))))) + [4 [.#Quantification] (all //.and bit (..stack type) type)] + [5 [.#Reification] (//.and type type)] + [6 [.#Named] (//.and ..name type)]]))))) (the .public provenance (Projection Provenance) diff --git a/stdlib/source/projection/lux/type.lux b/stdlib/source/projection/lux/type.lux index d5e2b8ca2..fb4718b88 100644 --- a/stdlib/source/projection/lux/type.lux +++ b/stdlib/source/projection/lux/type.lux @@ -36,7 +36,7 @@ (the .public recursive_definition (template.macro (_ ,type) [{.#Reification (..recursion_parameter) - {.#Universal (stack) ,type}}])) + {.#Quantification .universal (stack) ,type}}])) (the .public recursive_iteration (template.macro (_)