diff options
Diffstat (limited to '')
-rw-r--r-- | stdlib/source/lux.lux | 746 | ||||
-rw-r--r-- | stdlib/source/lux/concurrency/atom.lux | 2 | ||||
-rw-r--r-- | stdlib/source/lux/control/effect.lux | 26 | ||||
-rw-r--r-- | stdlib/source/lux/data/coll/array.lux | 2 | ||||
-rw-r--r-- | stdlib/source/lux/data/number.lux | 2 | ||||
-rw-r--r-- | stdlib/source/lux/host.js.lux | 2 | ||||
-rw-r--r-- | stdlib/source/lux/host.jvm.lux | 12 | ||||
-rw-r--r-- | stdlib/source/lux/macro/poly.lux | 58 | ||||
-rw-r--r-- | stdlib/source/lux/math/simple.lux | 4 | ||||
-rw-r--r-- | stdlib/source/lux/type.lux | 94 | ||||
-rw-r--r-- | stdlib/source/lux/type/auto.lux | 14 | ||||
-rw-r--r-- | stdlib/source/lux/type/check.lux | 62 |
12 files changed, 512 insertions, 512 deletions
diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux index 344925b1f..f530f9ca5 100644 --- a/stdlib/source/lux.lux +++ b/stdlib/source/lux.lux @@ -121,19 +121,19 @@ #Nil)))))) ## (type: #rec Type -## (#HostT Text (List Type)) -## #VoidT -## #UnitT -## (#SumT Type Type) -## (#ProdT Type Type) -## (#FunctionT Type Type) -## (#BoundT Nat) -## (#VarT Nat) -## (#ExT Nat) +## (#Host Text (List Type)) +## #Void +## #Unit +## (#Sum Type Type) +## (#Product Type Type) +## (#Function Type Type) +## (#Bound Nat) +## (#Var Nat) +## (#Ex Nat) ## (#UnivQ (List Type) Type) ## (#ExQ (List Type) Type) -## (#AppT Type Type) -## (#NamedT Ident Type) +## (#App Type Type) +## (#Named Ident Type) ## ) (_lux_def Type (+12 ["lux" "Type"] @@ -144,48 +144,48 @@ (_lux_case (+4 Type Type) TypePair (+11 (+9 #Nil - (+3 ## "lux;HostT" + (+3 ## "lux;Host" (+4 Text TypeList) - (+3 ## "lux;VoidT" + (+3 ## "lux;Void" (+2) - (+3 ## "lux;UnitT" + (+3 ## "lux;Unit" (+2) - (+3 ## "lux;SumT" + (+3 ## "lux;Sum" TypePair - (+3 ## "lux;ProdT" + (+3 ## "lux;Product" TypePair - (+3 ## "lux;FunctionT" + (+3 ## "lux;Function" TypePair - (+3 ## "lux;BoundT" + (+3 ## "lux;Bound" Nat - (+3 ## "lux;VarT" + (+3 ## "lux;Var" Nat - (+3 ## "lux;ExT" + (+3 ## "lux;Ex" Nat (+3 ## "lux;UnivQ" (+4 TypeList Type) (+3 ## "lux;ExQ" (+4 TypeList Type) - (+3 ## "lux;AppT" + (+3 ## "lux;App" TypePair - ## "lux;NamedT" + ## "lux;Named" (+4 Ident Type)))))))))))))) Void))))) (#Cons [["lux" "type?"] (+0 true)] (#Cons [["lux" "export?"] (+0 true)] - (#Cons [["lux" "tags"] (+8 (#Cons (+6 "HostT") - (#Cons (+6 "VoidT") - (#Cons (+6 "UnitT") - (#Cons (+6 "SumT") - (#Cons (+6 "ProdT") - (#Cons (+6 "FunctionT") - (#Cons (+6 "BoundT") - (#Cons (+6 "VarT") - (#Cons (+6 "ExT") + (#Cons [["lux" "tags"] (+8 (#Cons (+6 "Host") + (#Cons (+6 "Void") + (#Cons (+6 "Unit") + (#Cons (+6 "Sum") + (#Cons (+6 "Product") + (#Cons (+6 "Function") + (#Cons (+6 "Bound") + (#Cons (+6 "Var") + (#Cons (+6 "Ex") (#Cons (+6 "UnivQ") (#Cons (+6 "ExQ") - (#Cons (+6 "AppT") - (#Cons (+6 "NamedT") + (#Cons (+6 "App") + (#Cons (+6 "Named") #Nil))))))))))))))] (#Cons [["lux" "doc"] (+6 "This type represents the data-structures that are used to specify types themselves.")] (#Cons [["lux" "type-rec?"] (+0 true)] @@ -194,8 +194,8 @@ ## (type: Top ## (Ex [a] a)) (_lux_def Top - (#NamedT ["lux" "Top"] - (#ExQ #Nil (#BoundT +1))) + (#Named ["lux" "Top"] + (#ExQ #Nil (#Bound +1))) (#Cons [["lux" "type?"] (+0 true)] (#Cons [["lux" "export?"] (+0 true)] (#Cons [["lux" "doc"] (+6 "The type of things whose type does not matter. @@ -206,8 +206,8 @@ ## (type: Bottom ## (All [a] a)) (_lux_def Bottom - (#NamedT ["lux" "Bottom"] - (#UnivQ #Nil (#BoundT +1))) + (#Named ["lux" "Bottom"] + (#UnivQ #Nil (#Bound +1))) (#Cons [["lux" "type?"] (+0 true)] (#Cons [["lux" "export?"] (+0 true)] (#Cons [["lux" "doc"] (+6 "The type of things whose type is unknown or undefined. @@ -227,33 +227,33 @@ ## (#ListA (List Ann-Value)) ## (#DictA (List [Text Ann-Value]))) (_lux_def Ann-Value - (#NamedT ["lux" "Ann-Value"] - (_lux_case (#AppT (#BoundT +0) (#BoundT +1)) - Ann-Value - (#AppT (#UnivQ #Nil - (#SumT ## #BoolA - Bool - (#SumT ## #NatA - Nat - (#SumT ## #IntA - Int - (#SumT ## #DegA - Deg - (#SumT ## #RealA - Real - (#SumT ## #CharA - Char - (#SumT ## #TextA - Text - (#SumT ## #IdentA - Ident - (#SumT ## #ListA - (#AppT List Ann-Value) - ## #DictA - (#AppT List (#ProdT Text Ann-Value))))))))))) - ) - Void) - )) + (#Named ["lux" "Ann-Value"] + (_lux_case (#App (#Bound +0) (#Bound +1)) + Ann-Value + (#App (#UnivQ #Nil + (#Sum ## #BoolA + Bool + (#Sum ## #NatA + Nat + (#Sum ## #IntA + Int + (#Sum ## #DegA + Deg + (#Sum ## #RealA + Real + (#Sum ## #CharA + Char + (#Sum ## #TextA + Text + (#Sum ## #IdentA + Ident + (#Sum ## #ListA + (#App List Ann-Value) + ## #DictA + (#App List (#Product Text Ann-Value))))))))))) + ) + Void) + )) (#Cons [["lux" "type?"] (+0 true)] (#Cons [["lux" "export?"] (+0 true)] (#Cons [["lux" "tags"] (+8 (#Cons (+6 "BoolA") @@ -274,8 +274,8 @@ ## (type: Anns ## (List [Ident Ann-Value])) (_lux_def Anns - (#NamedT ["lux" "Anns"] - (#AppT List (#ProdT Ident Ann-Value))) + (#Named ["lux" "Anns"] + (#App List (#Product Ident Ann-Value))) (#Cons [["lux" "type?"] (#BoolA true)] (#Cons [["lux" "export?"] (#BoolA true)] (#Cons [["lux" "doc"] (#TextA "A set of annotations associated with a definition.")] @@ -297,8 +297,8 @@ ## (type: Def ## [Type Anns Void]) (_lux_def Def - (#NamedT ["lux" "Def"] - (#ProdT Type (#ProdT Anns Void))) + (#Named ["lux" "Def"] + (#Product Type (#Product Anns Void))) (#Cons [["lux" "doc"] (#TextA "Represents all the data associated with a definition: its type, its annotations, and its value.")] default-def-meta-exported)) @@ -306,15 +306,15 @@ ## {#counter Nat ## #mappings (List [k v])}) (_lux_def Bindings - (#NamedT ["lux" "Bindings"] - (#UnivQ #Nil - (#UnivQ #Nil - (#ProdT ## "lux;counter" - Nat - ## "lux;mappings" - (#AppT List - (#ProdT (#BoundT +3) - (#BoundT +1))))))) + (#Named ["lux" "Bindings"] + (#UnivQ #Nil + (#UnivQ #Nil + (#Product ## "lux;counter" + Nat + ## "lux;mappings" + (#App List + (#Product (#Bound +3) + (#Bound +1))))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "counter") (#Cons (#TextA "mappings") #Nil)))] @@ -326,8 +326,8 @@ ## #line Nat ## #column Nat}) (_lux_def Cursor - (#NamedT ["lux" "Cursor"] - (#ProdT Text (#ProdT Nat Nat))) + (#Named ["lux" "Cursor"] + (#Product Text (#Product Nat Nat))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "module") (#Cons (#TextA "line") (#Cons (#TextA "column") @@ -339,11 +339,11 @@ ## {#meta m ## #datum v}) (_lux_def Meta - (#NamedT ["lux" "Meta"] - (#UnivQ #Nil - (#UnivQ #Nil - (#ProdT (#BoundT +3) - (#BoundT +1))))) + (#Named ["lux" "Meta"] + (#UnivQ #Nil + (#UnivQ #Nil + (#Product (#Bound +3) + (#Bound +1))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "meta") (#Cons (#TextA "datum") #Nil)))] @@ -355,11 +355,11 @@ ## (#Local Nat) ## (#Captured Nat)) (_lux_def Ref - (#NamedT ["lux" "Ref"] - (#SumT ## Local - Nat - ## Captured - Nat)) + (#Named ["lux" "Ref"] + (#Sum ## Local + Nat + ## Captured + Nat)) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "Local") (#Cons (#TextA "Captured") #Nil)))] @@ -371,15 +371,15 @@ ## #locals (Bindings Text [Type Nat]) ## #captured (Bindings Text [Type Ref])}) (_lux_def Scope - (#NamedT ["lux" "Scope"] - (#ProdT ## name - (#AppT List Text) - (#ProdT ## inner - Nat - (#ProdT ## locals - (#AppT (#AppT Bindings Text) (#ProdT Type Nat)) - ## captured - (#AppT (#AppT Bindings Text) (#ProdT Type Ref)))))) + (#Named ["lux" "Scope"] + (#Product ## name + (#App List Text) + (#Product ## inner + Nat + (#Product ## locals + (#App (#App Bindings Text) (#Product Type Nat)) + ## captured + (#App (#App Bindings Text) (#Product Type Ref)))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "name") (#Cons (#TextA "inner") (#Cons (#TextA "locals") @@ -401,40 +401,40 @@ ## (#Tuple (List (w (AST' w)))) ## (#Record (List [(w (AST' w)) (w (AST' w))]))) (_lux_def AST' - (#NamedT ["lux" "AST'"] - (_lux_case (#AppT (#BoundT +1) - (#AppT (#BoundT +0) - (#BoundT +1))) - AST - (_lux_case (#AppT [List AST]) - AST-List - (#UnivQ #Nil - (#SumT ## "lux;Bool" - Bool - (#SumT ## "lux;Nat" - Nat - (#SumT ## "lux;Int" - Int - (#SumT ## "lux;Deg" - Deg - (#SumT ## "lux;Real" - Real - (#SumT ## "lux;Char" - Char - (#SumT ## "lux;Text" - Text - (#SumT ## "lux;Symbol" + (#Named ["lux" "AST'"] + (_lux_case (#App (#Bound +1) + (#App (#Bound +0) + (#Bound +1))) + AST + (_lux_case (#App [List AST]) + AST-List + (#UnivQ #Nil + (#Sum ## "lux;Bool" + Bool + (#Sum ## "lux;Nat" + Nat + (#Sum ## "lux;Int" + Int + (#Sum ## "lux;Deg" + Deg + (#Sum ## "lux;Real" + Real + (#Sum ## "lux;Char" + Char + (#Sum ## "lux;Text" + Text + (#Sum ## "lux;Symbol" + Ident + (#Sum ## "lux;Tag" Ident - (#SumT ## "lux;Tag" - Ident - (#SumT ## "lux;Form" + (#Sum ## "lux;Form" + AST-List + (#Sum ## "lux;Tuple" AST-List - (#SumT ## "lux;Tuple" - AST-List - ## "lux;Record" - (#AppT List (#ProdT AST AST)) - ))))))))))) - )))) + ## "lux;Record" + (#App List (#Product AST AST)) + ))))))))))) + )))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "Bool") (#Cons (#TextA "Nat") (#Cons (#TextA "Int") @@ -454,28 +454,28 @@ ## (type: AST ## (Meta Cursor (AST' (Meta Cursor)))) (_lux_def AST - (#NamedT ["lux" "AST"] - (_lux_case (#AppT Meta Cursor) - w - (#AppT w (#AppT AST' w)))) + (#Named ["lux" "AST"] + (_lux_case (#App Meta Cursor) + w + (#App w (#App AST' w)))) (#Cons [["lux" "doc"] (#TextA "The type of AST nodes for Lux syntax.")] default-def-meta-exported)) (_lux_def AST-List - (#AppT List AST) + (#App List AST) default-def-meta-unexported) ## (type: (Either l r) ## (#Left l) ## (#Right r)) (_lux_def Either - (#NamedT ["lux" "Either"] - (#UnivQ #Nil - (#UnivQ #Nil - (#SumT ## "lux;Left" - (#BoundT +3) - ## "lux;Right" - (#BoundT +1))))) + (#Named ["lux" "Either"] + (#UnivQ #Nil + (#UnivQ #Nil + (#Sum ## "lux;Left" + (#Bound +3) + ## "lux;Right" + (#Bound +1))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "Left") (#Cons (#TextA "Right") #Nil)))] @@ -486,8 +486,8 @@ ## (type: Source ## [Cursor Text]) (_lux_def Source - (#NamedT ["lux" "Source"] - (#ProdT Cursor Text)) + (#Named ["lux" "Source"] + (#Product Cursor Text)) default-def-meta-exported) ## (type: Module-State @@ -495,15 +495,15 @@ ## #Compiled ## #Cached) (_lux_def Module-State - (#NamedT ["lux" "Module-State"] - (#SumT - ## #Active + (#Named ["lux" "Module-State"] + (#Sum + ## #Active + Unit + (#Sum + ## #Compiled Unit - (#SumT - ## #Compiled - Unit - ## #Cached - Unit))) + ## #Cached + Unit))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "Active") (#Cons (#TextA "Compiled") (#Cons (#TextA "Cached") @@ -520,33 +520,33 @@ ## #module-anns Anns ## #module-state Module-State}) (_lux_def Module - (#NamedT ["lux" "Module"] - (#ProdT ## "lux;module-hash" - Nat - (#ProdT ## "lux;module-aliases" - (#AppT List (#ProdT Text Text)) - (#ProdT ## "lux;defs" - (#AppT List (#ProdT Text + (#Named ["lux" "Module"] + (#Product ## "lux;module-hash" + Nat + (#Product ## "lux;module-aliases" + (#App List (#Product Text Text)) + (#Product ## "lux;defs" + (#App List (#Product Text Def)) - (#ProdT ## "lux;imports" - (#AppT List Text) - (#ProdT ## "lux;tags" - (#AppT List - (#ProdT Text - (#ProdT Nat - (#ProdT (#AppT List Ident) - (#ProdT Bool - Type))))) - (#ProdT ## "lux;types" - (#AppT List - (#ProdT Text - (#ProdT (#AppT List Ident) - (#ProdT Bool - Type)))) - (#ProdT ## "lux;module-anns" - Anns - Module-State)) - )))))) + (#Product ## "lux;imports" + (#App List Text) + (#Product ## "lux;tags" + (#App List + (#Product Text + (#Product Nat + (#Product (#App List Ident) + (#Product Bool + Type))))) + (#Product ## "lux;types" + (#App List + (#Product Text + (#Product (#App List Ident) + (#Product Bool + Type)))) + (#Product ## "lux;module-anns" + Anns + Module-State)) + )))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "module-hash") (#Cons (#TextA "module-aliases") (#Cons (#TextA "defs") @@ -564,15 +564,15 @@ ## #var-counter Nat ## #var-bindings (List [Nat (Maybe Type)])}) (_lux_def Type-Context - (#NamedT ["lux" "Type-Context"] - (#ProdT ## ex-counter + (#Named ["lux" "Type-Context"] + (#Product ## ex-counter + Nat + (#Product ## var-counter Nat - (#ProdT ## var-counter - Nat - ## var-bindings - (#AppT List - (#ProdT Nat - (#AppT Maybe Type)))))) + ## var-bindings + (#App List + (#Product Nat + (#App Maybe Type)))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "ex-counter") (#Cons (#TextA "var-counter") (#Cons (#TextA "var-bindings") @@ -584,13 +584,13 @@ ## #Eval ## #REPL) (_lux_def Compiler-Mode - (#NamedT ["lux" "Compiler-Mode"] - (#SumT ## Build - #UnitT - (#SumT ## Eval - #UnitT - ## REPL - #UnitT))) + (#Named ["lux" "Compiler-Mode"] + (#Sum ## Build + #Unit + (#Sum ## Eval + #Unit + ## REPL + #Unit))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "Build") (#Cons (#TextA "Eval") (#Cons (#TextA "REPL") @@ -602,11 +602,11 @@ ## {#compiler-version Text ## #compiler-mode Compiler-Mode}) (_lux_def Compiler-Info - (#NamedT ["lux" "Compiler-Info"] - (#ProdT ## "lux;compiler-version" - Text - ## "lux;compiler-mode" - Compiler-Mode)) + (#Named ["lux" "Compiler-Info"] + (#Product ## "lux;compiler-version" + Text + ## "lux;compiler-mode" + Compiler-Mode)) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "compiler-version") (#Cons (#TextA "compiler-mode") #Nil)))] @@ -625,28 +625,28 @@ ## #scope-type-vars (List Nat) ## #host Void}) (_lux_def Compiler - (#NamedT ["lux" "Compiler"] - (#ProdT ## "lux;info" - Compiler-Info - (#ProdT ## "lux;source" - Source - (#ProdT ## "lux;cursor" - Cursor - (#ProdT ## "lux;modules" - (#AppT List (#ProdT Text + (#Named ["lux" "Compiler"] + (#Product ## "lux;info" + Compiler-Info + (#Product ## "lux;source" + Source + (#Product ## "lux;cursor" + Cursor + (#Product ## "lux;modules" + (#App List (#Product Text Module)) - (#ProdT ## "lux;scopes" - (#AppT List Scope) - (#ProdT ## "lux;type-context" - Type-Context - (#ProdT ## "lux;expected" - (#AppT Maybe Type) - (#ProdT ## "lux;seed" - Nat - (#ProdT ## scope-type-vars - (#AppT List Nat) - ## "lux;host" - Void)))))))))) + (#Product ## "lux;scopes" + (#App List Scope) + (#Product ## "lux;type-context" + Type-Context + (#Product ## "lux;expected" + (#App Maybe Type) + (#Product ## "lux;seed" + Nat + (#Product ## scope-type-vars + (#App List Nat) + ## "lux;host" + Void)))))))))) (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "info") (#Cons (#TextA "source") (#Cons (#TextA "cursor") @@ -668,11 +668,11 @@ ## (type: (Lux a) ## (-> Compiler (Either Text [Compiler a]))) (_lux_def Lux - (#NamedT ["lux" "Lux"] - (#UnivQ #Nil - (#FunctionT Compiler - (#AppT (#AppT Either Text) - (#ProdT Compiler (#BoundT +1)))))) + (#Named ["lux" "Lux"] + (#UnivQ #Nil + (#Function Compiler + (#App (#App Either Text) + (#Product Compiler (#Bound +1)))))) (#Cons [["lux" "doc"] (#TextA "Computations that can have access to the state of the compiler. These computations may fail, or modify the state of the compiler.")] @@ -682,8 +682,8 @@ ## (type: Macro ## (-> (List AST) (Lux (List AST)))) (_lux_def Macro - (#NamedT ["lux" "Macro"] - (#FunctionT AST-List (#AppT Lux AST-List))) + (#Named ["lux" "Macro"] + (#Function AST-List (#App Lux AST-List))) (#Cons [["lux" "doc"] (#TextA "Functions that run at compile-time and allow you to transform and extend the language in powerful ways.")] default-def-meta-exported)) @@ -693,20 +693,20 @@ #Nil) (_lux_def _meta - (_lux_: (#FunctionT (#AppT AST' - (#AppT Meta Cursor)) - AST) + (_lux_: (#Function (#App AST' + (#App Meta Cursor)) + AST) (_lux_function _ data [_cursor data])) #Nil) (_lux_def return (_lux_: (#UnivQ #Nil - (#FunctionT (#BoundT +1) - (#FunctionT Compiler - (#AppT (#AppT Either Text) - (#ProdT Compiler - (#BoundT +1)))))) + (#Function (#Bound +1) + (#Function Compiler + (#App (#App Either Text) + (#Product Compiler + (#Bound +1)))))) (_lux_function _ val (_lux_function _ state (#Right state val)))) @@ -714,73 +714,73 @@ (_lux_def fail (_lux_: (#UnivQ #Nil - (#FunctionT Text - (#FunctionT Compiler - (#AppT (#AppT Either Text) - (#ProdT Compiler - (#BoundT +1)))))) + (#Function Text + (#Function Compiler + (#App (#App Either Text) + (#Product Compiler + (#Bound +1)))))) (_lux_function _ msg (_lux_function _ state (#Left msg)))) #Nil) (_lux_def bool$ - (_lux_: (#FunctionT Bool AST) + (_lux_: (#Function Bool AST) (_lux_function _ value (_meta (#Bool value)))) #Nil) (_lux_def nat$ - (_lux_: (#FunctionT Nat AST) + (_lux_: (#Function Nat AST) (_lux_function _ value (_meta (#Nat value)))) #Nil) (_lux_def int$ - (_lux_: (#FunctionT Int AST) + (_lux_: (#Function Int AST) (_lux_function _ value (_meta (#Int value)))) #Nil) (_lux_def deg$ - (_lux_: (#FunctionT Deg AST) + (_lux_: (#Function Deg AST) (_lux_function _ value (_meta (#Deg value)))) #Nil) (_lux_def real$ - (_lux_: (#FunctionT Real AST) + (_lux_: (#Function Real AST) (_lux_function _ value (_meta (#Real value)))) #Nil) (_lux_def char$ - (_lux_: (#FunctionT Char AST) + (_lux_: (#Function Char AST) (_lux_function _ value (_meta (#Char value)))) #Nil) (_lux_def text$ - (_lux_: (#FunctionT Text AST) + (_lux_: (#Function Text AST) (_lux_function _ text (_meta (#Text text)))) #Nil) (_lux_def symbol$ - (_lux_: (#FunctionT Ident AST) + (_lux_: (#Function Ident AST) (_lux_function _ ident (_meta (#Symbol ident)))) #Nil) (_lux_def tag$ - (_lux_: (#FunctionT Ident AST) + (_lux_: (#Function Ident AST) (_lux_function _ ident (_meta (#Tag ident)))) #Nil) (_lux_def form$ - (_lux_: (#FunctionT (#AppT List AST) AST) + (_lux_: (#Function (#App List AST) AST) (_lux_function _ tokens (_meta (#Form tokens)))) #Nil) (_lux_def tuple$ - (_lux_: (#FunctionT (#AppT List AST) AST) + (_lux_: (#Function (#App List AST) AST) (_lux_function _ tokens (_meta (#Tuple tokens)))) #Nil) (_lux_def record$ - (_lux_: (#FunctionT (#AppT List (#ProdT AST AST)) AST) + (_lux_: (#Function (#App List (#Product AST AST)) AST) (_lux_function _ tokens (_meta (#Record tokens)))) #Nil) @@ -869,7 +869,7 @@ #Nil) (_lux_def with-export-meta - (_lux_: (#FunctionT AST AST) + (_lux_: (#Function AST AST) (function'' [tail] (form$ (#Cons (tag$ ["lux" "Cons"]) (#Cons export?-meta @@ -877,7 +877,7 @@ #Nil) (_lux_def with-hidden-meta - (_lux_: (#FunctionT AST AST) + (_lux_: (#Function AST AST) (function'' [tail] (form$ (#Cons (tag$ ["lux" "Cons"]) (#Cons hidden?-meta @@ -885,7 +885,7 @@ #Nil) (_lux_def with-macro-meta - (_lux_: (#FunctionT AST AST) + (_lux_: (#Function AST AST) (function'' [tail] (form$ (#Cons (tag$ ["lux" "Cons"]) (#Cons macro?-meta @@ -1003,7 +1003,7 @@ (#Cons x (#Cons y xs)) (return (#Cons (form$ (#Cons (symbol$ ["lux" "$'"]) - (#Cons (form$ (#Cons (tag$ ["lux" "AppT"]) + (#Cons (form$ (#Cons (tag$ ["lux" "App"]) (#Cons x (#Cons y #Nil)))) xs))) #Nil)) @@ -1015,9 +1015,9 @@ #Nil (#UnivQ #Nil (#UnivQ #Nil - (#FunctionT (#FunctionT (#BoundT +3) (#BoundT +1)) - (#FunctionT ($' List (#BoundT +3)) - ($' List (#BoundT +1)))))) + (#Function (#Function (#Bound +3) (#Bound +1)) + (#Function ($' List (#Bound +3)) + ($' List (#Bound +1)))))) (_lux_case xs #Nil #Nil @@ -1028,11 +1028,11 @@ (def:'' RepEnv #Nil Type - ($' List (#ProdT Text AST))) + ($' List (#Product Text AST))) (def:'' (make-env xs ys) #Nil - (#FunctionT ($' List Text) (#FunctionT ($' List AST) RepEnv)) + (#Function ($' List Text) (#Function ($' List AST) RepEnv)) (_lux_case [xs ys] [(#Cons x xs') (#Cons y ys')] (#Cons [x y] (make-env xs' ys')) @@ -1042,12 +1042,12 @@ (def:'' (Text/= x y) #Nil - (#FunctionT Text (#FunctionT Text Bool)) + (#Function Text (#Function Text Bool)) (_lux_proc ["text" "="] [x y])) (def:'' (get-rep key env) #Nil - (#FunctionT Text (#FunctionT RepEnv ($' Maybe AST))) + (#Function Text (#Function RepEnv ($' Maybe AST))) (_lux_case env #Nil #None @@ -1062,7 +1062,7 @@ (def:'' (replace-syntax reps syntax) #Nil - (#FunctionT RepEnv (#FunctionT AST AST)) + (#Function RepEnv (#Function AST AST)) (_lux_case syntax [_ (#Symbol "" name)] (_lux_case (get-rep name reps) @@ -1079,7 +1079,7 @@ [meta (#Tuple (map (replace-syntax reps) members))] [meta (#Record slots)] - [meta (#Record (map (_lux_: (#FunctionT (#ProdT AST AST) (#ProdT AST AST)) + [meta (#Record (map (_lux_: (#Function (#Product AST AST) (#Product AST AST)) (function'' [slot] (_lux_case slot [k v] @@ -1092,20 +1092,20 @@ (def:'' (update-bounds ast) #Nil - (#FunctionT AST AST) + (#Function AST AST) (_lux_case ast [_ (#Tuple members)] (tuple$ (map update-bounds members)) [_ (#Record pairs)] - (record$ (map (_lux_: (#FunctionT (#ProdT AST AST) (#ProdT AST AST)) + (record$ (map (_lux_: (#Function (#Product AST AST) (#Product AST AST)) (function'' [pair] (let'' [name val] pair [name (update-bounds val)]))) pairs)) - [_ (#Form (#Cons [_ (#Tag "lux" "BoundT")] (#Cons [_ (#Nat idx)] #Nil)))] - (form$ (#Cons (tag$ ["lux" "BoundT"]) (#Cons (nat$ (_lux_proc ["nat" "+"] [+2 idx])) #Nil))) + [_ (#Form (#Cons [_ (#Tag "lux" "Bound")] (#Cons [_ (#Nat idx)] #Nil)))] + (form$ (#Cons (tag$ ["lux" "Bound"]) (#Cons (nat$ (_lux_proc ["nat" "+"] [+2 idx])) #Nil))) [_ (#Form members)] (form$ (map update-bounds members)) @@ -1116,10 +1116,10 @@ (def:'' (parse-quantified-args args next) #Nil ## (-> (List AST) (-> (List Text) (Lux (List AST))) (Lux (List AST))) - (#FunctionT ($' List AST) - (#FunctionT (#FunctionT ($' List Text) (#AppT Lux ($' List AST))) - (#AppT Lux ($' List AST)) - )) + (#Function ($' List AST) + (#Function (#Function ($' List Text) (#App Lux ($' List AST))) + (#App Lux ($' List AST)) + )) (_lux_case args #Nil (next #Nil) @@ -1133,18 +1133,18 @@ (def:'' (make-bound idx) #Nil - (#FunctionT Nat AST) - (form$ (#Cons (tag$ ["lux" "BoundT"]) (#Cons (nat$ idx) #Nil)))) + (#Function Nat AST) + (form$ (#Cons (tag$ ["lux" "Bound"]) (#Cons (nat$ idx) #Nil)))) (def:'' (fold f init xs) #Nil ## (All [a b] (-> (-> b a a) a (List b) a)) - (#UnivQ #Nil (#UnivQ #Nil (#FunctionT (#FunctionT (#BoundT +1) - (#FunctionT (#BoundT +3) - (#BoundT +3))) - (#FunctionT (#BoundT +3) - (#FunctionT ($' List (#BoundT +1)) - (#BoundT +3)))))) + (#UnivQ #Nil (#UnivQ #Nil (#Function (#Function (#Bound +1) + (#Function (#Bound +3) + (#Bound +3))) + (#Function (#Bound +3) + (#Function ($' List (#Bound +1)) + (#Bound +3)))))) (_lux_case xs #Nil init @@ -1155,7 +1155,7 @@ (def:'' (length list) #Nil (#UnivQ #Nil - (#FunctionT ($' List (#BoundT +1)) Int)) + (#Function ($' List (#Bound +1)) Int)) (fold (function'' [_ acc] (_lux_proc ["int" "+"] [1 acc])) 0 list)) (macro:' #export (All tokens) @@ -1178,7 +1178,7 @@ (#Cons [_ (#Tuple args)] (#Cons body #Nil)) (parse-quantified-args args (function'' [names] - (let'' body' (fold (_lux_: (#FunctionT Text (#FunctionT AST AST)) + (let'' body' (fold (_lux_: (#Function Text (#Function AST AST)) (function'' [name' body'] (form$ (#Cons (tag$ ["lux" "UnivQ"]) (#Cons (tag$ ["lux" "Nil"]) @@ -1229,7 +1229,7 @@ (#Cons [_ (#Tuple args)] (#Cons body #Nil)) (parse-quantified-args args (function'' [names] - (let'' body' (fold (_lux_: (#FunctionT Text (#FunctionT AST AST)) + (let'' body' (fold (_lux_: (#Function Text (#Function AST AST)) (function'' [name' body'] (form$ (#Cons (tag$ ["lux" "ExQ"]) (#Cons (tag$ ["lux" "Nil"]) @@ -1260,7 +1260,7 @@ (def:'' (reverse list) #Nil - (All [a] (#FunctionT ($' List a) ($' List a))) + (All [a] (#Function ($' List a) ($' List a))) (fold (function'' [head tail] (#Cons head tail)) #Nil list)) @@ -1273,8 +1273,8 @@ #;Nil) (_lux_case (reverse tokens) (#Cons output inputs) - (return (#Cons (fold (_lux_: (#FunctionT AST (#FunctionT AST AST)) - (function'' [i o] (form$ (#Cons (tag$ ["lux" "FunctionT"]) (#Cons i (#Cons o #Nil)))))) + (return (#Cons (fold (_lux_: (#Function AST (#Function AST AST)) + (function'' [i o] (form$ (#Cons (tag$ ["lux" "Function"]) (#Cons i (#Cons o #Nil)))))) output inputs) #Nil)) @@ -1319,10 +1319,10 @@ #;Nil) (_lux_case (reverse tokens) #Nil - (return (list (tag$ ["lux" "UnitT"]))) + (return (list (tag$ ["lux" "Unit"]))) (#Cons last prevs) - (return (list (fold (function'' [left right] (form$ (list (tag$ ["lux" "ProdT"]) left right))) + (return (list (fold (function'' [left right] (form$ (list (tag$ ["lux" "Product"]) left right))) last prevs))) )) @@ -1336,10 +1336,10 @@ #;Nil) (_lux_case (reverse tokens) #Nil - (return (list (tag$ ["lux" "VoidT"]))) + (return (list (tag$ ["lux" "Void"]))) (#Cons last prevs) - (return (list (fold (function'' [left right] (form$ (list (tag$ ["lux" "SumT"]) left right))) + (return (list (fold (function'' [left right] (form$ (list (tag$ ["lux" "Sum"]) left right))) last prevs))) )) @@ -1553,12 +1553,12 @@ (list& [["lux" "tags"] (#ListA (list (#TextA "wrap") (#TextA "bind")))] default-def-meta-unexported) Type - (#NamedT ["lux" "Monad"] - (All [m] - (& (All [a] (-> a ($' m a))) - (All [a b] (-> (-> a ($' m b)) - ($' m a) - ($' m b))))))) + (#Named ["lux" "Monad"] + (All [m] + (& (All [a] (-> a ($' m a))) + (All [a b] (-> (-> a ($' m b)) + ($' m a) + ($' m b))))))) (def:''' Monad<Maybe> #Nil @@ -1762,7 +1762,7 @@ (do Monad<Lux> [=elem (untemplate elem)] (wrap (form$ (list (symbol$ ["" "_lux_:"]) - (form$ (list (tag$ ["lux" "AppT"]) (tuple$ (list (symbol$ ["lux" "List"]) (symbol$ ["lux" "AST"]))))) + (form$ (list (tag$ ["lux" "App"]) (tuple$ (list (symbol$ ["lux" "List"]) (symbol$ ["lux" "AST"]))))) (form$ (list (tag$ ["lux" "Cons"]) (tuple$ (list =elem (tag$ ["lux" "Nil"])))))))))))) elems))] (wrap (wrap-meta (form$ (list tag @@ -1868,10 +1868,10 @@ (host java.util.List [java.lang.Long])")]) (_lux_case tokens (#Cons [_ (#Symbol "" class-name)] #Nil) - (return (list (form$ (list (tag$ ["lux" "HostT"]) (text$ class-name) (tag$ ["lux" "Nil"]))))) + (return (list (form$ (list (tag$ ["lux" "Host"]) (text$ class-name) (tag$ ["lux" "Nil"]))))) (#Cons [_ (#Symbol "" class-name)] (#Cons [_ (#Tuple params)] #Nil)) - (return (list (form$ (list (tag$ ["lux" "HostT"]) (text$ class-name) (untemplate-list params))))) + (return (list (form$ (list (tag$ ["lux" "Host"]) (text$ class-name) (untemplate-list params))))) _ (fail "Wrong syntax for host"))) @@ -2494,7 +2494,7 @@ [_ (#Form (#Cons type-fn args))] (fold (_lux_: (-> AST AST AST) - (function' [arg type-fn] (` (#;AppT (~ type-fn) (~ arg))))) + (function' [arg type-fn] (` (#;App (~ type-fn) (~ arg))))) (walk-type type-fn) (map walk-type args)) @@ -2576,7 +2576,7 @@ (#Cons type #Nil) (_lux_case type [_ (#Tag "" member-name)] - (return [(` #;UnitT) (#;Some (list member-name))]) + (return [(` #;Unit) (#;Some (list member-name))]) [_ (#Form (#Cons [_ (#Tag "" member-name)] member-types))] (return [(` (& (~@ member-types))) (#;Some (list member-name))]) @@ -2631,9 +2631,9 @@ [Int (List Self)])")]) (_lux_case tokens (#Cons [_ (#Symbol "" name)] (#Cons body #Nil)) - (let' [body' (replace-syntax (list [name (` (#AppT (~ (make-bound +0)) (~ (make-bound +1))))]) + (let' [body' (replace-syntax (list [name (` (#App (~ (make-bound +0)) (~ (make-bound +1))))]) (update-bounds body))] - (return (list (` (#AppT (#UnivQ #Nil (~ body')) Void))))) + (return (list (` (#App (#UnivQ #Nil (~ body')) Void))))) _ (fail "Wrong syntax for Rec"))) @@ -3375,14 +3375,14 @@ (def: (beta-reduce env type) (-> (List Type) Type Type) (case type - (#SumT left right) - (#SumT (beta-reduce env left) (beta-reduce env right)) + (#Sum left right) + (#Sum (beta-reduce env left) (beta-reduce env right)) - (#ProdT left right) - (#ProdT (beta-reduce env left) (beta-reduce env right)) + (#Product left right) + (#Product (beta-reduce env left) (beta-reduce env right)) - (#AppT ?type-fn ?type-arg) - (#AppT (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) + (#App ?type-fn ?type-arg) + (#App (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) (#UnivQ ?local-env ?local-def) (case ?local-env @@ -3400,10 +3400,10 @@ _ type) - (#FunctionT ?input ?output) - (#FunctionT (beta-reduce env ?input) (beta-reduce env ?output)) + (#Function ?input ?output) + (#Function (beta-reduce env ?input) (beta-reduce env ?output)) - (#BoundT idx) + (#Bound idx) (case (nth (_lux_proc ["nat" "to-int"] [idx]) env) (#Some bound) bound @@ -3411,7 +3411,7 @@ _ type) - (#NamedT name type) + (#Named name type) (beta-reduce env type) _ @@ -3427,12 +3427,12 @@ (#ExQ env body) (#Some (beta-reduce (list& type-fn param env) body)) - (#AppT F A) + (#App F A) (do Monad<Maybe> [type-fn* (apply-type F A)] (apply-type type-fn* param)) - (#NamedT name type) + (#Named name type) (apply-type type param) _ @@ -3448,19 +3448,19 @@ _ (list type)))] - [flatten-variant #;SumT] - [flatten-tuple #;ProdT] - [flatten-lambda #;FunctionT] - [flatten-app #;AppT] + [flatten-variant #;Sum] + [flatten-tuple #;Product] + [flatten-lambda #;Function] + [flatten-app #;App] ) (def: (resolve-struct-type type) (-> Type (Maybe (List Type))) (case type - (#ProdT _) + (#Product _) (#Some (flatten-tuple type)) - (#AppT fun arg) + (#App fun arg) (do Monad<Maybe> [output (apply-type fun arg)] (resolve-struct-type output)) @@ -3471,10 +3471,10 @@ (#ExQ _ body) (resolve-struct-type body) - (#NamedT name type) + (#Named name type) (resolve-struct-type type) - (#SumT _) + (#Sum _) #None _ @@ -3515,7 +3515,7 @@ (def: (resolve-type-tags type) (-> Type (Lux (Maybe [(List Ident) (List Type)]))) (case type - (#AppT fun arg) + (#App fun arg) (resolve-type-tags fun) (#UnivQ env body) @@ -3524,12 +3524,12 @@ (#ExQ env body) (resolve-type-tags body) - (#NamedT [module name] _) + (#Named [module name] _) (do Monad<Lux> [=module (find-module module) #let [{#module-hash _ #module-aliases _ #defs bindings #imports _ #tags tags #types types #module-anns _ #module-state _} =module]] (case (get name types) - (#Some [tags exported? (#NamedT _ _type)]) + (#Some [tags exported? (#Named _ _type)]) (case (resolve-struct-type _type) (#Some members) (return (#Some [tags members])) @@ -3771,9 +3771,9 @@ type-meta meta)) Type - (#;NamedT [(~ (text$ module-name)) - (~ (text$ name))] - (type (~ type''))))))) + (#;Named [(~ (text$ module-name)) + (~ (text$ name))] + (type (~ type''))))))) #None (fail "Wrong syntax for type:")))) @@ -4226,7 +4226,7 @@ (def: (Type/show type) (-> Type Text) (case type - (#HostT name params) + (#Host name params) (case params #;Nil name @@ -4234,28 +4234,28 @@ _ ($_ Text/append "(" name " " (|> params (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")) - #VoidT + #Void "Void" - #UnitT + #Unit "Unit" - (#SumT _) + (#Sum _) ($_ Text/append "(| " (|> (flatten-variant type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")") - (#ProdT _) + (#Product _) ($_ Text/append "[" (|> (flatten-tuple type) (map Type/show) (interpose " ") reverse (fold Text/append "")) "]") - (#FunctionT _) + (#Function _) ($_ Text/append "(-> " (|> (flatten-lambda type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")") - (#BoundT id) + (#Bound id) (Nat/encode id) - (#VarT id) + (#Var id) ($_ Text/append "⌈v:" (Nat/encode id) "⌋") - (#ExT id) + (#Ex id) ($_ Text/append "⟨e:" (Nat/encode id) "⟩") (#UnivQ env body) @@ -4264,10 +4264,10 @@ (#ExQ env body) ($_ Text/append "(Ex " (Type/show body) ")") - (#AppT _) + (#App _) ($_ Text/append "(" (|> (flatten-app type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")") - (#NamedT [prefix name] _) + (#Named [prefix name] _) ($_ Text/append prefix ";" name) )) @@ -4845,19 +4845,19 @@ (def: (beta-reduce env type) (-> (List Type) Type Type) (case type - (#;HostT name params) - (#;HostT name (List/map (beta-reduce env) params)) + (#;Host name params) + (#;Host name (List/map (beta-reduce env) params)) (^template [<tag>] (<tag> left right) (<tag> (beta-reduce env left) (beta-reduce env right))) - ([#;SumT] [#;ProdT]) + ([#;Sum] [#;Product]) (^template [<tag>] (<tag> left right) (<tag> (beta-reduce env left) (beta-reduce env right))) - ([#;FunctionT] - [#;AppT]) + ([#;Function] + [#;App]) (^template [<tag>] (<tag> old-env def) @@ -4870,7 +4870,7 @@ ([#;UnivQ] [#;ExQ]) - (#;BoundT idx) + (#;Bound idx) (default type (list;nth idx env)) _ @@ -5116,31 +5116,31 @@ (def: (type-to-ast type) (-> Type AST) (case type - (#HostT name params) - (` (#HostT (~ (text$ name)) (~ (untemplate-list (map type-to-ast params))))) + (#Host name params) + (` (#Host (~ (text$ name)) (~ (untemplate-list (map type-to-ast params))))) - #VoidT - (` #VoidT) + #Void + (` #Void) - #UnitT - (` #UnitT) + #Unit + (` #Unit) (^template [<tag>] (<tag> left right) (` (<tag> (~ (type-to-ast left)) (~ (type-to-ast right))))) - ([#SumT] [#ProdT]) + ([#Sum] [#Product]) - (#FunctionT in out) - (` (#FunctionT (~ (type-to-ast in)) (~ (type-to-ast out)))) + (#Function in out) + (` (#Function (~ (type-to-ast in)) (~ (type-to-ast out)))) - (#BoundT idx) - (` (#BoundT (~ (nat$ idx)))) + (#Bound idx) + (` (#Bound (~ (nat$ idx)))) - (#VarT id) - (` (#VarT (~ (nat$ id)))) + (#Var id) + (` (#Var (~ (nat$ id)))) - (#ExT id) - (` (#ExT (~ (nat$ id)))) + (#Ex id) + (` (#Ex (~ (nat$ id)))) (#UnivQ env type) (let [env' (untemplate-list (map type-to-ast env))] @@ -5150,11 +5150,11 @@ (let [env' (untemplate-list (map type-to-ast env))] (` (#ExQ (~ env') (~ (type-to-ast type))))) - (#AppT fun arg) - (` (#AppT (~ (type-to-ast fun)) (~ (type-to-ast arg)))) + (#App fun arg) + (` (#App (~ (type-to-ast fun)) (~ (type-to-ast arg)))) - (#NamedT [module name] type) - (` (#NamedT [(~ (text$ module)) (~ (text$ name))] (~ (type-to-ast type)))) + (#Named [module name] type) + (` (#Named [(~ (text$ module)) (~ (text$ name))] (~ (type-to-ast type)))) )) (macro: #export (loop tokens) @@ -5324,7 +5324,7 @@ (-> Type Type) (case type (^template [<name>] - (#NamedT ["lux" <name>] _) + (#Named ["lux" <name>] _) type) (["Bool"] ["Nat"] @@ -5334,7 +5334,7 @@ ["Char"] ["Text"]) - (#NamedT _ type') + (#Named _ type') type' _ @@ -5347,7 +5347,7 @@ #let [[type value] type+value]] (case (flatten-alias type) (^template [<name> <type> <wrapper>] - (#NamedT ["lux" <name>] _) + (#Named ["lux" <name>] _) (wrap (<wrapper> (:! <type> value)))) (["Bool" Bool bool$] ["Nat" Nat nat$] @@ -5419,7 +5419,7 @@ _ (fail "Wrong syntax for ^~"))) -(type: MultiLevelCase +(type: Multi-Level-Case [AST (List [AST AST])]) (def: (case-level^ level) @@ -5433,7 +5433,7 @@ )) (def: (multi-level-case^ levels) - (-> (List AST) (Lux MultiLevelCase)) + (-> (List AST) (Lux Multi-Level-Case)) (case levels #;Nil (fail "Multi-level patterns cannot be empty.") @@ -5444,7 +5444,7 @@ (wrap [init extras'])))) (def: (multi-level-case$ g!_ [[init-pattern levels] body]) - (-> AST [MultiLevelCase AST] (List AST)) + (-> AST [Multi-Level-Case AST] (List AST)) (let [inner-pattern-body (fold (function [[calculation pattern] success] (` (case (~ calculation) (~ pattern) @@ -5482,7 +5482,7 @@ expected get-expected-type g!temp (gensym "temp")] (let [output (list g!temp - (` (;_lux_case (;_lux_: (#;AppT Maybe (~ (type-to-ast expected))) + (` (;_lux_case (;_lux_: (#;App Maybe (~ (type-to-ast expected))) (case (~ g!temp) (~@ (multi-level-case$ g!temp [mlc body])) @@ -5561,7 +5561,7 @@ [stvs get-scope-type-vars] (case (list-at idx (reverse stvs)) (#;Some var-id) - (wrap (list (` (#ExT (~ (nat$ var-id)))))) + (wrap (list (` (#Ex (~ (nat$ var-id)))))) #;None (fail (Text/append "Indexed-type does not exist: " (Nat/encode idx))))) diff --git a/stdlib/source/lux/concurrency/atom.lux b/stdlib/source/lux/concurrency/atom.lux index 209dec8db..27bbe25fd 100644 --- a/stdlib/source/lux/concurrency/atom.lux +++ b/stdlib/source/lux/concurrency/atom.lux @@ -4,7 +4,7 @@ (type: #export (Atom a) {#;doc "Atomic references that are safe to mutate concurrently."} - (#;HostT "#Atom" (#;Cons a #;Nil))) + (#;Host "#Atom" (#;Cons a #;Nil))) (def: #export (atom value) (All [a] (-> a (Atom a))) diff --git a/stdlib/source/lux/control/effect.lux b/stdlib/source/lux/control/effect.lux index fd0973470..668b3a30e 100644 --- a/stdlib/source/lux/control/effect.lux +++ b/stdlib/source/lux/control/effect.lux @@ -227,7 +227,7 @@ (def: (un-apply type-app) (-> Type Type) (case type-app - (#;AppT effect value) + (#;App effect value) effect _ @@ -263,21 +263,21 @@ (def: (flatten-effect-stack stack) (-> Type (List Type)) (case stack - (#;SumT left right) + (#;Sum left right) (List/append (flatten-effect-stack left) (flatten-effect-stack right)) - (^ (#;AppT branches (#;VarT _))) + (^ (#;App branches (#;Var _))) (flatten-effect-stack branches) - (^ (#;AppT (#;AppT (#;NamedT (ident-for ;;|@) _) - left) - right)) + (^ (#;App (#;App (#;Named (ident-for ;;|@) _) + left) + right)) (#;Cons left (flatten-effect-stack right)) - (^ (#;AppT (#;AppT (#;NamedT (ident-for M;Free) _) - effect) - param)) + (^ (#;App (#;App (#;Named (ident-for M;Free) _) + effect) + param)) (list effect) _ @@ -286,7 +286,7 @@ (def: (same-effect? expected actual) (case [expected actual] - [(#;NamedT e-name _) (#;NamedT a-name _)] + [(#;Named e-name _) (#;Named a-name _)] (Ident/= e-name a-name) _ @@ -319,10 +319,10 @@ [input (macro;find-type var) output macro;expected-type] (case [input output] - (^=> [(#;AppT eff0 _) (#;AppT stackT0 recT0)] + (^=> [(#;App eff0 _) (#;App stackT0 recT0)] [(type;apply-type stackT0 recT0) (#;Some unfoldT0)] - [stackT0 (^ (#;AppT (#;NamedT (ident-for M;Free) _) - stackT1))] + [stackT0 (^ (#;App (#;Named (ident-for M;Free) _) + stackT1))] [(type;apply-type stackT1 recT0) (#;Some unfoldT1)] [(flatten-effect-stack unfoldT1) stack] [(|> stack list;enumerate diff --git a/stdlib/source/lux/data/coll/array.lux b/stdlib/source/lux/data/coll/array.lux index 304bd6ec7..8631f154d 100644 --- a/stdlib/source/lux/data/coll/array.lux +++ b/stdlib/source/lux/data/coll/array.lux @@ -14,7 +14,7 @@ ## [Types] (type: #export (Array a) {#;doc "Mutable arrays."} - (#;HostT "#Array" (#;Cons a #;Nil))) + (#;Host "#Array" (#;Cons a #;Nil))) ## [Functions] (def: #export (new size) diff --git a/stdlib/source/lux/data/number.lux b/stdlib/source/lux/data/number.lux index ee343e6ee..9f2c01d0e 100644 --- a/stdlib/source/lux/data/number.lux +++ b/stdlib/source/lux/data/number.lux @@ -626,7 +626,7 @@ (-> Nat Nat Nat) (bit-or (bit-shift-left idx +1) input)) -(type: Digits (#;HostT "#Array" (#;Cons Nat #;Nil))) +(type: Digits (#;Host "#Array" (#;Cons Nat #;Nil))) (def: (make-digits _) (-> Top Digits) diff --git a/stdlib/source/lux/host.js.lux b/stdlib/source/lux/host.js.lux index c1bb5f1f8..39e15f780 100644 --- a/stdlib/source/lux/host.js.lux +++ b/stdlib/source/lux/host.js.lux @@ -8,7 +8,7 @@ )) (do-template [<name> <type>] - [(type: #export <name> (#;HostT <type> #;Nil))] + [(type: #export <name> (#;Host <type> #;Nil))] [Object "object"] [Function "function"] diff --git a/stdlib/source/lux/host.jvm.lux b/stdlib/source/lux/host.jvm.lux index 5efeb05c5..2aa352cf7 100644 --- a/stdlib/source/lux/host.jvm.lux +++ b/stdlib/source/lux/host.jvm.lux @@ -66,7 +66,7 @@ ## Types (do-template [<class> <name>] [(type: #export <name> - (#;HostT <class> #;Nil))] + (#;Host <class> #;Nil))] ["[Z" Boolean-Array] ["[B" Byte-Array] @@ -2001,10 +2001,10 @@ (def: (type->class-name type) (-> Type (Lux Text)) (case type - (#;HostT name params) + (#;Host name params) (:: Monad<Lux> wrap name) - (#;AppT F A) + (#;App F A) (case (type;apply-type F A) #;None (macro;fail (format "Cannot apply type: " (type;to-text F) " to " (type;to-text A))) @@ -2012,13 +2012,13 @@ (#;Some type') (type->class-name type')) - (#;NamedT _ type') + (#;Named _ type') (type->class-name type') - #;UnitT + #;Unit (:: Monad<Lux> wrap "java.lang.Object") - (^or #;VoidT (#;VarT _) (#;ExT _) (#;BoundT _) (#;SumT _) (#;ProdT _) (#;FunctionT _) (#;UnivQ _) (#;ExQ _)) + (^or #;Void (#;Var _) (#;Ex _) (#;Bound _) (#;Sum _) (#;Product _) (#;Function _) (#;UnivQ _) (#;ExQ _)) (macro;fail (format "Cannot convert to JvmType: " (type;to-text type))) )) diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux index 96158a80e..3252cfeeb 100644 --- a/stdlib/source/lux/macro/poly.lux +++ b/stdlib/source/lux/macro/poly.lux @@ -36,8 +36,8 @@ _ (macro;fail (format "Not " <name> " type: " (%type :type:))))))] - [void "Void" #;VoidT] - [unit "Unit" #;UnitT] + [void "Void" #;Void] + [unit "Unit" #;Unit] ) (do-template [<combinator> <name>] @@ -45,7 +45,7 @@ (Matcher Unit) (;function [:type:] (case (type;un-alias :type:) - (#;NamedT ["lux" <name>] _) + (#;Named ["lux" <name>] _) (:: macro;Monad<Lux> wrap []) _ @@ -102,19 +102,19 @@ (:: macro;Monad<Lux> wrap members) (macro;fail (format "Not a " ($AST$ <tag>) " type: " (%type :type:)))))))] - [sum sum+ type;flatten-variant #;SumT] - [prod prod+ type;flatten-tuple #;ProdT] + [sum sum+ type;flatten-variant #;Sum] + [prod prod+ type;flatten-tuple #;Product] ) (def: #export func (Matcher [Type Type]) (;function [:type:] (case (type;un-name :type:) - (#;FunctionT :left: :right:) + (#;Function :left: :right:) (:: macro;Monad<Lux> wrap [:left: :right:]) _ - (macro;fail (format "Not a FunctionT type: " (%type :type:)))))) + (macro;fail (format "Not a Function type: " (%type :type:)))))) (def: #export func+ (Matcher [(List Type) Type]) @@ -122,13 +122,13 @@ (let [[ins out] (type;flatten-function (type;un-name :type:))] (if (n.> +0 (list;size ins)) (:: macro;Monad<Lux> wrap [ins out]) - (macro;fail (format "Not a FunctionT type: " (%type :type:))))))) + (macro;fail (format "Not a Function type: " (%type :type:))))))) (def: #export tagged (Matcher [(List Ident) Type]) (;function [:type:] (case (type;un-alias :type:) - (#;NamedT type-name :def:) + (#;Named type-name :def:) (do macro;Monad<Lux> [tags (macro;tags-of type-name)] (wrap [tags :def:])) @@ -158,7 +158,7 @@ (do macro;Monad<Lux> [[tags :type:] (tagged :type:) _ (macro;assert "Records and variants must have tags." - (n.> +0 (list;size tags))) + (n.> +0 (list;size tags))) [vars :type:] (polymorphic :type:) members (<sub-comb> :type:) #let [num-tags (list;size tags) @@ -195,7 +195,7 @@ (do macro;Monad<Lux> [#let [[:func: :args:] (loop [:type: (type;un-name :type:)] (case :type: - (#;AppT :func: :arg:) + (#;App :func: :arg:) (let [[:func:' :args:] (recur :func:)] [:func:' (list& :arg: :args:)]) @@ -213,8 +213,8 @@ (Matcher Type) (;function [:type:] (case (type;un-name :type:) - (^=> (#;AppT :quant: :arg:) - [(type;un-alias :quant:) (#;NamedT ["lux" <name>] _)]) + (^=> (#;App :quant: :arg:) + [(type;un-alias :quant:) (#;Named ["lux" <name>] _)]) (:: macro;Monad<Lux> wrap :arg:) _ @@ -235,7 +235,7 @@ (-> Env (Matcher AST)) (;function [:type:] (case :type: - (#;BoundT idx) + (#;Bound idx) (case (dict;get (adjusted-idx env idx) env) (#;Some [poly-type poly-ast]) (:: macro;Monad<Lux> wrap poly-ast) @@ -252,13 +252,13 @@ (do Monad<Lux> [[t-func t-args] (apply :type:)] (case t-func - (^=> (#;BoundT t-func-idx) + (^=> (#;Bound t-func-idx) (n.= +0 (adjusted-idx env t-func-idx)) [(do maybe;Monad<Maybe> [=func (dict;get +0 env) =args (mapM @ (;function [t-arg] (case t-arg - (#;BoundT idx) + (#;Bound idx) (dict;get (adjusted-idx env idx) env) _ @@ -276,7 +276,7 @@ (-> Env Nat (Matcher Unit)) (;function [:type:] (case :type: - (^=> (#;BoundT idx) + (^=> (#;Bound idx) (n.= var-id (adjusted-idx env idx))) (:: macro;Monad<Lux> wrap []) @@ -295,7 +295,7 @@ (|> env (dict;put current-size [funcT funcA]) (dict;put (n.inc current-size) [varT varA]) - (extend-env [(#;AppT funcT varT) (` (#;AppT (~ funcA) (~ varA)))] + (extend-env [(#;App funcT varT) (` (#;App (~ funcA) (~ varA)))] type-vars') )))) @@ -365,21 +365,21 @@ (def: (to-ast env type) (-> Env Type AST) (case type - (#;HostT name params) - (` (#;HostT (~ (ast;text name)) - (list (~@ (List/map (to-ast env) params))))) + (#;Host name params) + (` (#;Host (~ (ast;text name)) + (list (~@ (List/map (to-ast env) params))))) (^template [<tag>] <tag> (` <tag>)) - ([#;VoidT] [#;UnitT]) + ([#;Void] [#;Unit]) (^template [<tag>] (<tag> idx) (` (<tag> (~ (ast;nat idx))))) - ([#;VarT] [#;ExT]) + ([#;Var] [#;Ex]) - (#;BoundT idx) + (#;Bound idx) (let [idx (adjusted-idx env idx)] (if (n.= +0 idx) (|> (dict;get idx env) (default (undefined)) product;left (to-ast env)) @@ -389,15 +389,15 @@ (<tag> left right) (` (<tag> (~ (to-ast env left)) (~ (to-ast env right))))) - ([#;FunctionT] [#;AppT]) + ([#;Function] [#;App]) (^template [<tag> <macro> <flattener>] (<tag> left right) (` (<macro> (~@ (List/map (to-ast env) (<flattener> type)))))) - ([#;SumT | type;flatten-variant] - [#;ProdT & type;flatten-tuple]) + ([#;Sum | type;flatten-variant] + [#;Product & type;flatten-tuple]) - (#;NamedT name sub-type) + (#;Named name sub-type) (ast;symbol name) (^template [<tag>] @@ -421,4 +421,4 @@ (def: #export (type-var-indices num-vars) (-> Nat (List Type)) - (|> num-vars list;indices (List/map (|>. #;BoundT)))) + (|> num-vars list;indices (List/map (|>. #;Bound)))) diff --git a/stdlib/source/lux/math/simple.lux b/stdlib/source/lux/math/simple.lux index 6e6e23592..359a2d23b 100644 --- a/stdlib/source/lux/math/simple.lux +++ b/stdlib/source/lux/math/simple.lux @@ -16,7 +16,7 @@ (get@ #;var-bindings env)) (#;Some [_ (#;Some type)]) (case type - (#;VarT id') + (#;Var id') (find-type-var id' env) _ @@ -35,7 +35,7 @@ [raw-type (macro;find-type var-name) compiler macro;get-compiler] (case raw-type - (#;VarT id) + (#;Var id) (find-type-var id (get@ #;type-context compiler)) _ diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux index d125b8b98..186cfac81 100644 --- a/stdlib/source/lux/type.lux +++ b/stdlib/source/lux/type.lux @@ -14,14 +14,14 @@ (def: (beta-reduce env type) (-> (List Type) Type Type) (case type - (#;HostT name params) - (#;HostT name (List/map (beta-reduce env) params)) + (#;Host name params) + (#;Host name (List/map (beta-reduce env) params)) (^template [<tag>] (<tag> left right) (<tag> (beta-reduce env left) (beta-reduce env right))) - ([#;SumT] [#;ProdT] - [#;FunctionT] [#;AppT]) + ([#;Sum] [#;Product] + [#;Function] [#;App]) (^template [<tag>] (<tag> old-env def) @@ -34,7 +34,7 @@ ([#;UnivQ] [#;ExQ]) - (#;BoundT idx) + (#;Bound idx) (default (error! (Text/append "Unknown type var: " (Nat/encode idx))) (list;nth idx env)) @@ -46,7 +46,7 @@ (struct: #export _ (Eq Type) (def: (= x y) (case [x y] - [(#;HostT xname xparams) (#;HostT yname yparams)] + [(#;Host xname xparams) (#;Host yname yparams)] (and (Text/= xname yname) (n.= (list;size yparams) (list;size xparams)) (List/fold (;function [[x y] prev] (and prev (= x y))) @@ -56,26 +56,26 @@ (^template [<tag>] [<tag> <tag>] true) - ([#;VoidT] [#;UnitT]) + ([#;Void] [#;Unit]) (^template [<tag>] [(<tag> xid) (<tag> yid)] (n.= yid xid)) - ([#;VarT] [#;ExT] [#;BoundT]) + ([#;Var] [#;Ex] [#;Bound]) - (^or [(#;FunctionT xleft xright) (#;FunctionT yleft yright)] - [(#;AppT xleft xright) (#;AppT yleft yright)]) + (^or [(#;Function xleft xright) (#;Function yleft yright)] + [(#;App xleft xright) (#;App yleft yright)]) (and (= xleft yleft) (= xright yright)) - [(#;NamedT xname xtype) (#;NamedT yname ytype)] + [(#;Named xname xtype) (#;Named yname ytype)] (and (Ident/= xname yname) (= xtype ytype)) (^template [<tag>] [(<tag> xL xR) (<tag> yL yR)] (and (= xL yL) (= xR yR))) - ([#;SumT] [#;ProdT]) + ([#;Sum] [#;Product]) (^or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)] [(#;ExQ xenv xbody) (#;ExQ yenv ybody)]) @@ -109,7 +109,7 @@ (def: #export (flatten-function type) (-> Type [(List Type) Type]) (case type - (#;FunctionT in out') + (#;Function in out') (let [[ins out] (flatten-function out')] [(list& in ins) out]) @@ -119,7 +119,7 @@ (def: #export (flatten-application type) (-> Type [Type (List Type)]) (case type - (#;AppT left' right) + (#;App left' right) (let [[left rights] (flatten-application left')] [left (List/append rights (list right))]) @@ -136,8 +136,8 @@ _ (list type)))] - [flatten-variant #;SumT] - [flatten-tuple #;ProdT] + [flatten-variant #;Sum] + [flatten-tuple #;Product] ) (def: #export (apply-type type-func param) @@ -148,12 +148,12 @@ (#;Some (beta-reduce (list& type-func param env) body))) ([#;UnivQ] [#;ExQ]) - (#;AppT F A) + (#;App F A) (do Monad<Maybe> [type-fn* (apply-type F A)] (apply-type type-fn* param)) - (#;NamedT name type) + (#;Named name type) (apply-type type param) _ @@ -162,33 +162,33 @@ (def: #export (to-ast type) (-> Type AST) (case type - (#;HostT name params) - (` (#;HostT (~ (ast;text name)) - (list (~@ (List/map to-ast params))))) + (#;Host name params) + (` (#;Host (~ (ast;text name)) + (list (~@ (List/map to-ast params))))) (^template [<tag>] <tag> (` <tag>)) - ([#;VoidT] [#;UnitT]) + ([#;Void] [#;Unit]) (^template [<tag>] (<tag> idx) (` (<tag> (~ (ast;nat idx))))) - ([#;VarT] [#;ExT] [#;BoundT]) + ([#;Var] [#;Ex] [#;Bound]) (^template [<tag>] (<tag> left right) (` (<tag> (~ (to-ast left)) (~ (to-ast right))))) - ([#;FunctionT] [#;AppT]) + ([#;Function] [#;App]) (^template [<tag> <macro> <flattener>] (<tag> left right) (` (<macro> (~@ (List/map to-ast (<flattener> type)))))) - ([#;SumT | flatten-variant] - [#;ProdT & flatten-tuple]) + ([#;Sum | flatten-variant] + [#;Product & flatten-tuple]) - (#;NamedT name sub-type) + (#;Named name sub-type) (ast;symbol name) (^template [<tag>] @@ -201,7 +201,7 @@ (def: #export (to-text type) (-> Type Text) (case type - (#;HostT name params) + (#;Host name params) (case params #;Nil ($_ Text/append "(host " name ")") @@ -209,10 +209,10 @@ _ ($_ Text/append "(host " name " " (|> params (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")")) - #;VoidT + #;Void "Void" - #;UnitT + #;Unit "Unit" (^template [<tag> <open> <close> <flatten>] @@ -224,10 +224,10 @@ (list;interpose " ") (List/fold Text/append "")) <close>)) - ([#;SumT "(| " ")" flatten-variant] - [#;ProdT "[" "]" flatten-tuple]) + ([#;Sum "(| " ")" flatten-variant] + [#;Product "[" "]" flatten-tuple]) - (#;FunctionT input output) + (#;Function input output) (let [[ins out] (flatten-function type)] ($_ Text/append "(-> " (|> ins @@ -237,16 +237,16 @@ (List/fold Text/append "")) " " (to-text out) ")")) - (#;BoundT idx) + (#;Bound idx) (Nat/encode idx) - (#;VarT id) + (#;Var id) ($_ Text/append "⌈v:" (Nat/encode id) "⌋") - (#;ExT id) + (#;Ex id) ($_ Text/append "⟨e:" (Nat/encode id) "⟩") - (#;AppT fun param) + (#;App fun param) (let [[type-func type-args] (flatten-application type)] ($_ Text/append "(" (to-text type-func) " " (|> type-args (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")")) @@ -256,15 +256,15 @@ ([#;UnivQ "All"] [#;ExQ "Ex"]) - (#;NamedT [module name] type) + (#;Named [module name] type) ($_ Text/append module ";" name) )) (def: #export (un-alias type) (-> Type Type) (case type - (#;NamedT _ (#;NamedT ident type')) - (un-alias (#;NamedT ident type')) + (#;Named _ (#;Named ident type')) + (un-alias (#;Named ident type')) _ type)) @@ -272,7 +272,7 @@ (def: #export (un-name type) (-> Type Type) (case type - (#;NamedT ident type') + (#;Named ident type') (un-name type') _ @@ -291,8 +291,8 @@ (#;Cons type types') (<ctor> type (<name> types'))))] - [variant Void #;SumT] - [tuple Unit #;ProdT] + [variant Void #;Sum] + [tuple Unit #;Product] ) (def: #export (function inputs output) @@ -302,7 +302,7 @@ output (#;Cons input inputs') - (#;FunctionT input (function inputs' output)))) + (#;Function input (function inputs' output)))) (def: #export (application quant params) (-> Type (List Type) Type) @@ -311,7 +311,7 @@ quant (#;Cons param params') - (application (#;AppT quant param) params'))) + (application (#;App quant param) params'))) (do-template [<name> <tag>] [(def: #export (<name> size body) @@ -327,10 +327,10 @@ (def: #export (quantified? type) (-> Type Bool) (case type - (#;NamedT [module name] _type) + (#;Named [module name] _type) (quantified? _type) - (#;AppT F A) + (#;App F A) (default false (do Monad<Maybe> [applied (apply-type F A)] diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux index 6a2991fa5..6ba7cdb8b 100644 --- a/stdlib/source/lux/type/auto.lux +++ b/stdlib/source/lux/type/auto.lux @@ -22,7 +22,7 @@ (get@ #;var-bindings env)) (#;Some [_ (#;Some type)]) (case type - (#;VarT id') + (#;Var id') (find-type-var id' env) _ @@ -41,7 +41,7 @@ [raw-type (macro;find-type var-name) compiler macro;get-compiler] (case raw-type - (#;VarT id) + (#;Var id) (find-type-var id (get@ #;type-context compiler)) _ @@ -50,10 +50,10 @@ (def: (find-member-type idx sig-type) (-> Nat Type (Check Type)) (case sig-type - (#;NamedT _ sig-type') + (#;Named _ sig-type') (find-member-type idx sig-type') - (#;AppT func arg) + (#;App func arg) (case (type;apply-type func arg) #;None (tc;fail (format "Cannot apply type " (%type func) " to type " (%type arg))) @@ -61,7 +61,7 @@ (#;Some sig-type') (find-member-type idx sig-type')) - (#;ProdT left right) + (#;Product left right) (if (n.= +0 idx) (:: Monad<Check> wrap left) (find-member-type (n.dec idx) right)) @@ -149,7 +149,7 @@ (def: (apply-function-type func arg) (-> Type Type (Check Type)) (case func - (#;NamedT _ func') + (#;Named _ func') (apply-function-type func' arg) (#;UnivQ _) @@ -159,7 +159,7 @@ (type;apply-type func var)) arg)) - (#;FunctionT input output) + (#;Function input output) (do Monad<Check> [_ (tc;check input arg)] (wrap output)) diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux index 1fec0891a..5db2059fa 100644 --- a/stdlib/source/lux/type/check.lux +++ b/stdlib/source/lux/type/check.lux @@ -145,7 +145,7 @@ (function [context] (let [id (get@ #;ex-counter context)] (#;Right [(update@ #;ex-counter n.inc context) - [id (#;ExT id)]])))) + [id (#;Ex id)]])))) (def: #export (bound? id) (-> Nat (Check Bool)) @@ -212,7 +212,7 @@ (def: #export (clean t-id type) (-> Nat Type (Check Type)) (case type - (#;VarT id) + (#;Var id) (if (n.= t-id id) (do Monad<Check> [? (bound? id)] @@ -226,7 +226,7 @@ [=type (read-var id) ==type (clean t-id =type)] (case ==type - (#;VarT =id) + (#;Var =id) (if (n.= t-id =id) (do Monad<Check> [_ (clear-var id)] @@ -241,10 +241,10 @@ (wrap type)))) (wrap type)))) - (#;HostT name params) + (#;Host name params) (do Monad<Check> [=params (mapM @ (clean t-id) params)] - (wrap (#;HostT name =params))) + (wrap (#;Host name =params))) (^template [<tag>] (<tag> left right) @@ -252,16 +252,16 @@ [=left (clean t-id left) =right (clean t-id right)] (wrap (<tag> =left =right)))) - ([#;FunctionT] - [#;AppT] - [#;ProdT] - [#;SumT]) + ([#;Function] + [#;App] + [#;Product] + [#;Sum]) (^template [<tag>] (<tag> env body) (do Monad<Check> [=env (mapM @ (clean t-id) env) - =body (clean t-id body)] ## TODO: DON'T CLEAN THE BODY + =body (clean t-id body)] ## TODO: DO NOT CLEAN THE BODY (wrap (<tag> =env =body)))) ([#;UnivQ] [#;ExQ]) @@ -277,7 +277,7 @@ (#;Right [(|> context (update@ #;var-counter n.inc) (update@ #;var-bindings (var::put id #;None))) - [id (#;VarT id)]])))) + [id (#;Var id)]])))) (def: get-bindings (Check (List [Nat (Maybe Type)])) @@ -311,7 +311,7 @@ (#;Some b-type') (case b-type' - (#;VarT t-id) + (#;Var t-id) (if (n.= id t-id) (wrap [b-id #;None]) (wrap binding)) @@ -387,7 +387,7 @@ (if (is expected actual) (Check/wrap fixed) (case [expected actual] - [(#;VarT e-id) (#;VarT a-id)] + [(#;Var e-id) (#;Var a-id)] (if (n.= e-id a-id) (Check/wrap fixed) (do Monad<Check> @@ -408,7 +408,7 @@ [(#;Some etype) (#;Some atype)] (check' etype atype fixed)))) - [(#;VarT id) _] + [(#;Var id) _] (either (do Monad<Check> [_ (write-var id actual)] (wrap fixed)) @@ -416,7 +416,7 @@ [bound (read-var id)] (check' bound actual fixed))) - [_ (#;VarT id)] + [_ (#;Var id)] (either (do Monad<Check> [_ (write-var id expected)] (wrap fixed)) @@ -424,32 +424,32 @@ [bound (read-var id)] (check' expected bound fixed))) - [(#;AppT (#;ExT eid) eA) (#;AppT (#;ExT aid) aA)] + [(#;App (#;Ex eid) eA) (#;App (#;Ex aid) aA)] (if (n.= eid aid) (check' eA aA fixed) (fail-check expected actual)) - [(#;AppT (#;VarT id) A1) (#;AppT F2 A2)] + [(#;App (#;Var id) A1) (#;App F2 A2)] (either (do Monad<Check> [F1 (read-var id)] - (check' (#;AppT F1 A1) actual fixed)) + (check' (#;App F1 A1) actual fixed)) (do Monad<Check> - [fixed (check' (#;VarT id) F2 fixed) + [fixed (check' (#;Var id) F2 fixed) e' (apply-type! F2 A1) a' (apply-type! F2 A2)] (check' e' a' fixed))) - [(#;AppT F1 A1) (#;AppT (#;VarT id) A2)] + [(#;App F1 A1) (#;App (#;Var id) A2)] (either (do Monad<Check> [F2 (read-var id)] - (check' expected (#;AppT F2 A2) fixed)) + (check' expected (#;App F2 A2) fixed)) (do Monad<Check> - [fixed (check' F1 (#;VarT id) fixed) + [fixed (check' F1 (#;Var id) fixed) e' (apply-type! F1 A1) a' (apply-type! F1 A2)] (check' e' a' fixed))) - [(#;AppT F A) _] + [(#;App F A) _] (let [fx-pair [expected actual]] (case (fx-get fx-pair fixed) (#;Some ?) @@ -462,7 +462,7 @@ [expected' (apply-type! F A)] (check' expected' actual (fx-put fx-pair true fixed))))) - [_ (#;AppT F A)] + [_ (#;App F A)] (do Monad<Check> [actual' (apply-type! F A)] (check' expected actual' fixed)) @@ -497,7 +497,7 @@ actual' (apply-type! actual ex)] (check' expected actual' fixed)) - [(#;HostT e-name e-params) (#;HostT a-name a-params)] + [(#;Host e-name e-params) (#;Host a-name a-params)] (if (and (Text/= e-name a-name) (n.= (list;size e-params) (list;size a-params))) @@ -517,23 +517,23 @@ (do Monad<Check> [fixed (check' eL aL fixed)] (check' eR aR fixed))) - ([#;VoidT #;SumT] - [#;UnitT #;ProdT]) + ([#;Void #;Sum] + [#;Unit #;Product]) - [(#;FunctionT eI eO) (#;FunctionT aI aO)] + [(#;Function eI eO) (#;Function aI aO)] (do Monad<Check> [fixed (check' aI eI fixed)] (check' eO aO fixed)) - [(#;ExT e!id) (#;ExT a!id)] + [(#;Ex e!id) (#;Ex a!id)] (if (n.= e!id a!id) (Check/wrap fixed) (fail-check expected actual)) - [(#;NamedT _ ?etype) _] + [(#;Named _ ?etype) _] (check' ?etype actual fixed) - [_ (#;NamedT _ ?atype)] + [_ (#;Named _ ?atype)] (check' expected ?atype fixed) _ |