From 5c76363c5ea48ff3972225e6e9fabec25191e963 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Tue, 7 May 2024 01:12:20 -0400 Subject: [PATCH] New type for `Type` (part 5). --- stdlib/source/library/lux.lux | 259 ++++++++---------- .../language/lux/phase/analysis/when.lux | 3 +- stdlib/source/library/lux/compiler/type.lux | 2 +- stdlib/source/library/lux/meta/label.lux | 20 +- 4 files changed, 133 insertions(+), 151 deletions(-) diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux index 04054d429..39b3fb9fd 100644 --- a/stdlib/source/library/lux.lux +++ b/stdlib/source/library/lux.lux @@ -24,7 +24,7 @@ (.is# Type {5 #1 [..prelude "Bit"] - {#0 (.type_name# "bit") (.list#)}}) + {0 #0 (.type_name# "bit") (.list#)}}) #1) (.def# false @@ -92,12 +92,12 @@ ..public) (.def# abstraction - (.is# Quantification + (.is# Parameter #0) ..public) (.def# argument - (.is# Quantification + (.is# Parameter #1) ..public) @@ -105,8 +105,8 @@ (.is# Type {5 #1 [..prelude "Natural"] - {#0 (.type_name# "i64") - (.list# [..co_variant {#0 (.type_name# "natural") (.list#)}])}}) + {0 #0 (.type_name# "i64") + (.list# [..co_variant {#0 (.type_name# "natural") (.list#)}])}}) ..public) ... (every .public Any @@ -238,34 +238,38 @@ (.function# _ it (.as# Slot it))) ..private) +(.def# List + (.is# Type + {5 #1 [..prelude "List"] + {4 #0 .universal {#0} + {0 #0 (.type_name# "list") (.list# [..co_variant {1 #0 1}])}}}) + .public) + (.def# maybe_tags - (.is# {5 #0 Name Stack} - {#1 [[..prelude "#None"] - {#1 [[..prelude "#Some"] - {#0}]}]}) + (.is# {5 #0 Name List} + (.list# [..prelude "#None"] + [..prelude "#Some"])) ..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# {5 #0 Name Stack} - {#1 [[..prelude "#Empty"] - {#1 [[..prelude "#Top"] - {#0}]}]}) + (.is# {5 #0 Name List} + (.list# [..prelude "#Empty"] + [..prelude "#Top"])) ..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# {5 #0 Name Stack} - {#1 [[..prelude "#Nominal"] - {#1 [[..prelude "#Parameter"] - {#1 [[..prelude "#Variable"] - {#1 [[..prelude "#Opaque"] - {#1 [[..prelude "#Quantification"] - {#1 [[..prelude "#Reification"] - {#1 [[..prelude "#Named"] - {#0}]}]}]}]}]}]}]}) + (.is# {5 #0 Name List} + (.list# [..prelude "#Nominal"] + [..prelude "#Parameter"] + [..prelude "#Variable"] + [..prelude "#Opaque"] + [..prelude "#Quantification"] + [..prelude "#Reification"] + [..prelude "#Named"])) ..private) (.def# #Nominal (..tag [{#Some [0 #0 ..type_tags]} Type]) ..public) (.def# #Parameter (..tag [{#Some [1 #0 ..type_tags]} Type]) ..public) @@ -338,11 +342,10 @@ (.type# "provenance")}) ..public) (.def# provenance_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#module"] - {#Top [..prelude "#line"] - {#Top [..prelude "#column"] - {#Empty}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#module"] + [..prelude "#line"] + [..prelude "#column"])) ..private) (.def# #module (slot [{#Some [0 #0 ..provenance_slots]} Provenance]) ..public) (.def# #line (slot [{#Some [1 #0 ..provenance_slots]} Provenance]) ..public) @@ -361,10 +364,9 @@ {#Parameter 1})}}}) ..public) (.def# ann_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#meta"] - {#Top [..prelude "#datum"] - {#Empty}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#meta"] + [..prelude "#datum"])) ..private) (.def# #meta (slot [{#Some [0 #0 ..ann_slots]} Annotated]) ..public) (.def# #datum (slot [{#Some [0 #1 ..ann_slots]} Annotated]) ..public) @@ -375,18 +377,17 @@ (.type# "code")}) ..public) (.def# code_tags - (.is# {#Reification Name Stack} - {#Top [..prelude "#Bit"] - {#Top [..prelude "#Natural"] - {#Top [..prelude "#Integer"] - {#Top [..prelude "#Revolution"] - {#Top [..prelude "#Decimal"] - {#Top [..prelude "#Text"] - {#Top [..prelude "#Name"] - {#Top [..prelude "#Form"] - {#Top [..prelude "#Variant"] - {#Top [..prelude "#Tuple"] - {#Empty}}}}}}}}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#Bit"] + [..prelude "#Natural"] + [..prelude "#Integer"] + [..prelude "#Revolution"] + [..prelude "#Decimal"] + [..prelude "#Text"] + [..prelude "#Name"] + [..prelude "#Form"] + [..prelude "#Variant"] + [..prelude "#Tuple"])) ..private) (.def# #Bit (tag [{#Some [0 #0 ..code_tags]} Code]) ..public) (.def# #Natural (tag [{#Some [1 #0 ..code_tags]} Code]) ..public) @@ -455,13 +456,6 @@ (.function# _ name {#Name (annotated ["" name])})) ..private) -(.def# List - (.is# Type - {#Named [..prelude "List"] - {#Quantification .universal {#Empty} - {#Nominal (.type_name# "list") (.list# [..co_variant {#Parameter 1}])}}}) - .public) - (.def# code#form (.is# (Function {#Reification Code List} Code) @@ -513,11 +507,10 @@ .public) (.def# global_tags - (.is# {#Reification Name Stack} - {#Top [..prelude "#Definition"] - {#Top [..prelude "#Alias"] - {#Top [..prelude "#Default"] - {#Empty}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#Definition"] + [..prelude "#Alias"] + [..prelude "#Default"])) ..private) (.def# #Definition (tag [{#Some [0 #0 ..global_tags]} Global]) .public) (.def# #Alias (tag [{#Some [1 #0 ..global_tags]} Global]) .public) @@ -530,10 +523,9 @@ .public) (.def# bindings_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#counter"] - {#Top [..prelude "#mappings"] - {#Empty}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#counter"] + [..prelude "#mappings"])) ..private) (.def# #counter (slot [{#Some [0 #0 ..bindings_slots]} Bindings]) .public) (.def# #mappings (slot [{#Some [0 #1 ..bindings_slots]} Bindings]) .public) @@ -549,10 +541,9 @@ .public) (.def# ref_tags - (.is# {#Reification Name Stack} - {#Top [..prelude "#Local"] - {#Top [..prelude "#Captured"] - {#Empty}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#Local"] + [..prelude "#Captured"])) ..private) (.def# #Local (tag [{#Some [0 #0 ..ref_tags]} Ref]) .public) (.def# #Captured (tag [{#Some [0 #1 ..ref_tags]} Ref]) .public) @@ -564,10 +555,9 @@ .public) (.def# scope_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#locals"] - {#Top [..prelude "#captured"] - {#Empty}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#locals"] + [..prelude "#captured"])) ..private) (.def# #locals (slot [{#Some [0 #0 ..scope_slots]} Scope]) .public) (.def# #captured (slot [{#Some [0 #1 ..scope_slots]} Scope]) .public) @@ -586,10 +576,9 @@ .public) (.def# either_tags - (.is# {#Reification Name Stack} - {#Top [..prelude "#Left"] - {#Top [..prelude "#Right"] - {#Empty}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#Left"] + [..prelude "#Right"])) ..private) (.def# #Left (tag [{#Some [0 #0 ..either_tags]} Either]) .public) (.def# #Right (tag [{#Some [0 #1 ..either_tags]} Either]) .public) @@ -616,11 +605,10 @@ .public) (.def# module_state_tags - (.is# {#Reification Name Stack} - {#Top [..prelude "#Active"] - {#Top [..prelude "#Compiled"] - {#Top [..prelude "#Cached"] - {#Empty}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#Active"] + [..prelude "#Compiled"] + [..prelude "#Cached"])) ..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) @@ -633,13 +621,12 @@ .public) (.def# module_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#module_hash"] - {#Top [..prelude "#module_aliases"] - {#Top [..prelude "#definitions"] - {#Top [..prelude "#imports"] - {#Top [..prelude "#module_state"] - {#Empty}}}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#module_hash"] + [..prelude "#module_aliases"] + [..prelude "#definitions"] + [..prelude "#imports"] + [..prelude "#module_state"])) ..private) (.def# #module_hash (slot [{#Some [0 #0 ..module_slots]} Module]) .public) (.def# #module_aliases (slot [{#Some [1 #0 ..module_slots]} Module]) .public) @@ -654,11 +641,10 @@ .public) (.def# type_context_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#ex_counter"] - {#Top [..prelude "#var_counter"] - {#Top [..prelude "#var_bindings"] - {#Empty}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#ex_counter"] + [..prelude "#var_counter"] + [..prelude "#var_bindings"])) ..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) @@ -678,11 +664,10 @@ .public) (.def# mode_tags - (.is# {#Reification Name Stack} - {#Top [..prelude "#Build"] - {#Top [..prelude "#Eval"] - {#Top [..prelude "#Interpreter"] - {#Empty}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#Build"] + [..prelude "#Eval"] + [..prelude "#Interpreter"])) ..private) (.def# #Build (tag [{#Some [0 #0 ..mode_tags]} Mode]) .public) (.def# #Eval (tag [{#Some [1 #0 ..mode_tags]} Mode]) .public) @@ -694,12 +679,11 @@ .public) (.def# info_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#target"] - {#Top [..prelude "#version"] - {#Top [..prelude "#mode"] - {#Top [..prelude "#configuration"] - {#Empty}}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#target"] + [..prelude "#version"] + [..prelude "#mode"] + [..prelude "#configuration"])) ..private) (.def# #target (slot [{#Some [0 #0 ..info_slots]} Info]) .public) (.def# #version (slot [{#Some [1 #0 ..info_slots]} Info]) .public) @@ -713,18 +697,17 @@ .public) (.def# lux_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#info"] - {#Top [..prelude "#source"] - {#Top [..prelude "#provenance"] - {#Top [..prelude "#current_module"] - {#Top [..prelude "#modules"] - {#Top [..prelude "#scopes"] - {#Top [..prelude "#type_context"] - {#Top [..prelude "#expected"] - {#Top [..prelude "#seed"] - {#Top [..prelude "#eval"] - {#Empty}}}}}}}}}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#info"] + [..prelude "#source"] + [..prelude "#provenance"] + [..prelude "#current_module"] + [..prelude "#modules"] + [..prelude "#scopes"] + [..prelude "#type_context"] + [..prelude "#expected"] + [..prelude "#seed"] + [..prelude "#eval"])) ..private) (.def# #info (slot [{#Some [0 #0 ..lux_slots]} Lux]) .public) (.def# #source (slot [{#Some [1 #0 ..lux_slots]} Lux]) .public) @@ -1570,10 +1553,9 @@ #0) (.def# monad_slots - (.is# {#Reification Name Stack} - {#Top [..prelude "#in"] - {#Top [..prelude "#then"] - {#Empty}}}) + (.is# {#Reification Name List} + (.list# [..prelude "#in"] + [..prelude "#then"])) ..private) (.def# #in (slot [{#Some [0 #0 ..monad_slots]} Monad]) .private) (.def# #then (slot [{#Some [0 #1 ..monad_slots]} Monad]) .private) @@ -4122,7 +4104,7 @@ (the (slot_family expected_module expected_record) (-> Text Type - (Meta (Maybe (Stack Name)))) + (Meta (Maybe (List Name)))) (do meta#monad [module (..module expected_module) actual_module ..current_module_name @@ -4132,7 +4114,7 @@ ..#imports _ ..#module_state _] module]] (in ((is (-> (Stack [Text [Bit Global]]) - (Maybe (Stack Name))) + (Maybe (List Name))) (function (again remaining) (when remaining {#Top [slot head] tail} @@ -4143,12 +4125,12 @@ (text#= expected_module actual_module))) (let [[label actual_record] (as Label value)] (if (type#= expected_record actual_record) - (when label - {#Some [lefts right? family]} - {#Some family} - - {#None} - {#Some (stack [expected_module slot])}) + {#Some (when label + {#Some [lefts right? family]} + family + + {#None} + (list [expected_module slot]))} (again tail))) (again tail)) @@ -4161,7 +4143,7 @@ (the (record_slots type) (-> Type - (Meta (Maybe [(Stack Name) (Stack Type)]))) + (Meta (Maybe [(List Name) (Stack Type)]))) (when type {#Reification arg func} (record_slots func) @@ -4265,7 +4247,7 @@ [tokens' (monad#each#meta complete_expansion (list#as_stack tokens)) implementation_type ..expected_type tags+type (record_slots implementation_type) - tags (is (Meta (Stack Name)) + tags (is (Meta (List Name)) (when tags+type {#Some [tags _]} (meta#in tags) @@ -4277,7 +4259,7 @@ (list#each (function (_ tag) [(product#right tag) (code#name tag)]) - (list#of_stack tags)))] + tags))] members (monad#each#meta (is (-> Code (Meta (Stack Code))) (function (_ token) (when token @@ -4483,10 +4465,10 @@ (stack#partial right lefts) (stack#partial (` (the (, family) - (Stack Name) - (stack (,* (list#of_stack (stack#each (function (_ it) - (` [(, (code#text module)) (, (code#text it))])) - labels)))))) + (List Name) + (list (,* (list#of_stack (stack#each (function (_ it) + (` [(, (code#text module)) (, (code#text it))])) + labels)))))) (` (the (, export_policy) (, (code#local right)) (<| (as (, label_type)) (is Label) @@ -5055,7 +5037,7 @@ {#Empty})) (every Implementation_Interface - [(Stack Name) (Stack Type)]) + [(List Name) (Stack Type)]) (the (open_layer alias [tags members]) (-> Text Implementation_Interface @@ -5069,7 +5051,7 @@ (in [(stack (code#name slot) (code#name local)) [local implementation]]))) - (zipped_2 tags members))] + (zipped_2 (list#as_stack tags) members))] (in [(|> pattern (stack#each product#left) stack#conjoint @@ -5191,7 +5173,7 @@ .let [idx (if right? (is Natural (.i64_+# 1 lefts)) lefts) - pattern (|> (enumeration family) + pattern (|> (enumeration (list#as_stack family)) (stack#each (is (-> [Natural Name] (Stack Code)) (function (_ [r_idx slot]) (stack (code#name slot) @@ -5218,13 +5200,14 @@ (failure ..wrong_syntax)))) (the (open_declaration imported_module alias tags my_tag_index [module proper] source type) - (-> Text Text (Stack Name) Natural Name Code Type + (-> Text Text (List Name) Natural Name Code Type (Meta (Stack Code))) (do meta#monad [output (record_slots type) '_ (..generated_name "'_") .let ['output (code#local proper) pattern (|> tags + list#as_stack enumeration (stack#each (function (_ [tag_idx tag]) (if (.i64_=# my_tag_index tag_idx) @@ -5239,7 +5222,7 @@ [decls' (monad#each#meta (is (-> [Natural Name Type] (Meta (Stack Code))) (function (_ [sub_tag_index sname stype]) (open_declaration imported_module alias tags' sub_tag_index sname source+ stype))) - (enumeration (zipped_2 tags' members')))] + (enumeration (zipped_2 (list#as_stack tags') members')))] (in (stack#conjoint decls'))) _ @@ -5260,7 +5243,7 @@ declarations (monad#each#meta (is (-> [Natural Name Type] (Meta (Stack Code))) (function (_ [index slot_label slot_type]) (open_declaration imported_module alias slots index slot_label 'implementation slot_type))) - (enumeration (zipped_2 slots terms)))] + (enumeration (zipped_2 (list#as_stack slots) terms)))] (in (stack#conjoint declarations))) _ @@ -5431,7 +5414,7 @@ (do meta#monad ['slot (..generated_name "")] (in [r_slot_name r_idx 'slot])))) - (enumeration family)) + (enumeration (list#as_stack family))) .let [pattern (|> pattern' (stack#each (is (-> [Name Natural Code] (Stack Code)) (function (_ [r_slot_name r_idx r_var]) @@ -5517,7 +5500,7 @@ (do meta#monad ['slot (..generated_name "")] (in [r_slot_name r_idx 'slot])))) - (enumeration family)) + (enumeration (list#as_stack family))) .let [pattern (|> pattern' (stack#each (is (-> [Name Natural Code] (Stack Code)) (function (_ [r_slot_name r_idx r_var]) 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 c70e00bfe..1e8100727 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 @@ -29,8 +29,7 @@ ["[0]" check (.only Check)]] ["[0]" meta (.only) ["[0]" binding] - ["[0]" code] - ["[0]" label]]]] + ["[0]" code]]]] ["[0]" // ["[1][0]" complex] [/// diff --git a/stdlib/source/library/lux/compiler/type.lux b/stdlib/source/library/lux/compiler/type.lux index 10817c319..b9cbbe40a 100644 --- a/stdlib/source/library/lux/compiler/type.lux +++ b/stdlib/source/library/lux/compiler/type.lux @@ -294,7 +294,7 @@ [(.Or .Any ,it)])) (every .public Label - [(..Maybe [..Natural ..Bit (.Stack ..Name)]) + [(..Maybe [..Natural ..Bit (..List' ..Name)]) ..Type]) (the Try diff --git a/stdlib/source/library/lux/meta/label.lux b/stdlib/source/library/lux/meta/label.lux index 2e28c43a6..6ae0532b7 100644 --- a/stdlib/source/library/lux/meta/label.lux +++ b/stdlib/source/library/lux/meta/label.lux @@ -75,7 +75,7 @@ (the .public (,plural type_name) (-> Name - (Meta (Stack Name))) + (Meta (List Name))) (do //.monad [type_name (binding.normal type_name) module (module.by_name (name.module type_name))] @@ -92,8 +92,8 @@ family {.#None} - (stack [(name.module type_name) - proper]))} + (list [(name.module type_name) + proper]))} {.#None}) _ @@ -115,7 +115,7 @@ (the .public (tag_stacks module) (-> module.Name - (Meta (Stack [(Stack Name) Type]))) + (Meta (Stack [(List Name) Type]))) (do //.monad [=module (module.by_name module) [this_module_name _] module.current] @@ -129,19 +129,19 @@ (let [[label type] (as Label value)] (when label {.#Some [lefts right? family]} - (when family - (stack.partial [_ proper] _) + (when (list.item 0 family) + {try.#Success [_ proper]} (property.has proper [family type] output) - (stack) - (property.has proper [(stack [module proper]) type] output)) + {try.#Failure _} + (property.has proper [(list [module proper]) type] output)) {.#None} - (property.has proper [(stack [module proper]) type] output))) + (property.has proper [(list [module proper]) type] output))) output) _ output)) - (is (property.List [(Stack Name) Type]) + (is (property.List [(List Name) Type]) (list)) (its .#definitions =module)))))))