aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux.lux224
-rw-r--r--stdlib/source/lux/control/effect.lux22
-rw-r--r--stdlib/source/lux/host.jvm.lux2
-rw-r--r--stdlib/source/lux/macro/poly.lux10
-rw-r--r--stdlib/source/lux/type.lux26
-rw-r--r--stdlib/source/lux/type/auto.lux2
-rw-r--r--stdlib/source/lux/type/check.lux49
-rw-r--r--stdlib/test/test/lux/type.lux4
-rw-r--r--stdlib/test/test/lux/type/check.lux4
9 files changed, 163 insertions, 180 deletions
diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index 54ac52b70..1a8d07922 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -95,7 +95,7 @@
(+2)
## "lux;Cons"
(+4 (+6 +1)
- (+11 (+6 +0) (+6 +1))))))
+ (+11 (+6 +1) (+6 +0))))))
(+1 [["lux" "type?"] (+0 true)]
(+1 [["lux" "export?"] (+0 true)]
(+1 [["lux" "tags"] (+8 (+1 (+6 "Nil") (+1 (+6 "Cons") (+0))))]
@@ -132,18 +132,19 @@
## (#Ex Nat)
## (#UnivQ (List Type) Type)
## (#ExQ (List Type) Type)
-## (#App Type Type)
+## (#Apply Type Type)
## (#Named Ident Type)
## )
(_lux_def Type
(+12 ["lux" "Type"]
- (_lux_case (+11 (+6 +0) (+6 +1))
+ (_lux_case (+11 (+6 +1) (+6 +0))
Type
- (_lux_case (+11 List Type)
+ (_lux_case (+11 Type List)
TypeList
(_lux_case (+4 Type Type)
TypePair
- (+11 (+9 #Nil
+ (+11 Void
+ (+9 #Nil
(+3 ## "lux;Host"
(+4 Text TypeList)
(+3 ## "lux;Void"
@@ -169,8 +170,7 @@
(+3 ## "lux;App"
TypePair
## "lux;Named"
- (+4 Ident Type))))))))))))))
- Void)))))
+ (+4 Ident Type)))))))))))))))))))
(#Cons [["lux" "type?"] (+0 true)]
(#Cons [["lux" "export?"] (+0 true)]
(#Cons [["lux" "tags"] (+8 (#Cons (+6 "Host")
@@ -184,7 +184,7 @@
(#Cons (+6 "Ex")
(#Cons (+6 "UnivQ")
(#Cons (+6 "ExQ")
- (#Cons (+6 "App")
+ (#Cons (+6 "Apply")
(#Cons (+6 "Named")
#Nil))))))))))))))]
(#Cons [["lux" "doc"] (+6 "This type represents the data-structures that are used to specify types themselves.")]
@@ -228,31 +228,31 @@
## (#DictA (List [Text Ann-Value])))
(_lux_def Ann-Value
(#Named ["lux" "Ann-Value"]
- (_lux_case (#App (#Bound +0) (#Bound +1))
+ (_lux_case (#Apply (#Bound +1) (#Bound +0))
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)
+ (#Apply Void
+ (#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
+ (#Apply Ann-Value List)
+ ## #DictA
+ (#Apply (#Product Text Ann-Value) List))))))))))
+ ))
))
(#Cons [["lux" "type?"] (+0 true)]
(#Cons [["lux" "export?"] (+0 true)]
@@ -275,7 +275,7 @@
## (List [Ident Ann-Value]))
(_lux_def Anns
(#Named ["lux" "Anns"]
- (#App List (#Product Ident Ann-Value)))
+ (#Apply (#Product Ident Ann-Value) List))
(#Cons [["lux" "type?"] (#BoolA true)]
(#Cons [["lux" "export?"] (#BoolA true)]
(#Cons [["lux" "doc"] (#TextA "A set of annotations associated with a definition.")]
@@ -312,9 +312,9 @@
(#Product ## "lux;counter"
Nat
## "lux;mappings"
- (#App List
- (#Product (#Bound +3)
- (#Bound +1)))))))
+ (#Apply (#Product (#Bound +3)
+ (#Bound +1))
+ List)))))
(#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "counter")
(#Cons (#TextA "mappings")
#Nil)))]
@@ -373,13 +373,13 @@
(_lux_def Scope
(#Named ["lux" "Scope"]
(#Product ## name
- (#App List Text)
+ (#Apply Text List)
(#Product ## inner
Nat
(#Product ## locals
- (#App (#App Bindings Text) (#Product Type Nat))
+ (#Apply (#Product Type Nat) (#Apply Text Bindings))
## captured
- (#App (#App Bindings Text) (#Product Type Ref))))))
+ (#Apply (#Product Type Ref) (#Apply Text Bindings))))))
(#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "name")
(#Cons (#TextA "inner")
(#Cons (#TextA "locals")
@@ -402,11 +402,11 @@
## (#Record (List [(w (Code' w)) (w (Code' w))])))
(_lux_def Code'
(#Named ["lux" "Code'"]
- (_lux_case (#App (#Bound +1)
- (#App (#Bound +0)
- (#Bound +1)))
+ (_lux_case (#Apply (#Apply (#Bound +1)
+ (#Bound +0))
+ (#Bound +1))
Code
- (_lux_case (#App [List Code])
+ (_lux_case (#Apply Code List)
Code-List
(#UnivQ #Nil
(#Sum ## "lux;Bool"
@@ -432,7 +432,7 @@
(#Sum ## "lux;Tuple"
Code-List
## "lux;Record"
- (#App List (#Product Code Code))
+ (#Apply (#Product Code Code) List)
)))))))))))
))))
(#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "Bool")
@@ -455,14 +455,14 @@
## (Meta Cursor (Code' (Meta Cursor))))
(_lux_def Code
(#Named ["lux" "Code"]
- (_lux_case (#App Meta Cursor)
+ (_lux_case (#Apply Cursor Meta)
w
- (#App w (#App Code' w))))
+ (#Apply (#Apply w Code') w)))
(#Cons [["lux" "doc"] (#TextA "The type of Code nodes for Lux syntax.")]
default-def-meta-exported))
(_lux_def Code-List
- (#App List Code)
+ (#Apply Code List)
default-def-meta-unexported)
## (type: (Either l r)
@@ -524,25 +524,24 @@
(#Product ## "lux;module-hash"
Nat
(#Product ## "lux;module-aliases"
- (#App List (#Product Text Text))
+ (#Apply (#Product Text Text) List)
(#Product ## "lux;defs"
- (#App List (#Product Text
- Def))
+ (#Apply (#Product Text Def) List)
(#Product ## "lux;imports"
- (#App List Text)
+ (#Apply Text List)
(#Product ## "lux;tags"
- (#App List
- (#Product Text
- (#Product Nat
- (#Product (#App List Ident)
- (#Product Bool
- Type)))))
+ (#Apply (#Product Text
+ (#Product Nat
+ (#Product (#Apply Ident List)
+ (#Product Bool
+ Type))))
+ List)
(#Product ## "lux;types"
- (#App List
- (#Product Text
- (#Product (#App List Ident)
- (#Product Bool
- Type))))
+ (#Apply (#Product Text
+ (#Product (#Apply Ident List)
+ (#Product Bool
+ Type)))
+ List)
(#Product ## "lux;module-anns"
Anns
Module-State))
@@ -570,9 +569,8 @@
(#Product ## var-counter
Nat
## var-bindings
- (#App List
- (#Product Nat
- (#App Maybe Type))))))
+ (#Apply (#Product Nat (#Apply Type Maybe))
+ List))))
(#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "ex-counter")
(#Cons (#TextA "var-counter")
(#Cons (#TextA "var-bindings")
@@ -633,18 +631,17 @@
(#Product ## "lux;cursor"
Cursor
(#Product ## "lux;modules"
- (#App List (#Product Text
- Module))
+ (#Apply (#Product Text Module) List)
(#Product ## "lux;scopes"
- (#App List Scope)
+ (#Apply Scope List)
(#Product ## "lux;type-context"
Type-Context
(#Product ## "lux;expected"
- (#App Maybe Type)
+ (#Apply Type Maybe)
(#Product ## "lux;seed"
Nat
(#Product ## scope-type-vars
- (#App List Nat)
+ (#Apply Nat List)
## "lux;host"
Void))))))))))
(#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "info")
@@ -671,8 +668,8 @@
(#Named ["lux" "Lux"]
(#UnivQ #Nil
(#Function Compiler
- (#App (#App Either Text)
- (#Product Compiler (#Bound +1))))))
+ (#Apply (#Product Compiler (#Bound +1))
+ (#Apply Text Either)))))
(#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.")]
@@ -683,7 +680,7 @@
## (-> (List Code) (Lux (List Code))))
(_lux_def Macro
(#Named ["lux" "Macro"]
- (#Function Code-List (#App Lux Code-List)))
+ (#Function Code-List (#Apply Code-List Lux)))
(#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))
@@ -694,8 +691,8 @@
#Nil))
(_lux_def _meta
- (_lux_: (#Function (#App Code'
- (#App Meta Cursor))
+ (_lux_: (#Function (#Apply (#Apply Cursor Meta)
+ Code')
Code)
(_lux_function _ data
[dummy-cursor data]))
@@ -705,9 +702,9 @@
(_lux_: (#UnivQ #Nil
(#Function (#Bound +1)
(#Function Compiler
- (#App (#App Either Text)
- (#Product Compiler
- (#Bound +1))))))
+ (#Apply (#Product Compiler
+ (#Bound +1))
+ (#Apply Text Either)))))
(_lux_function _ val
(_lux_function _ state
(#Right state val))))
@@ -717,9 +714,9 @@
(_lux_: (#UnivQ #Nil
(#Function Text
(#Function Compiler
- (#App (#App Either Text)
- (#Product Compiler
- (#Bound +1))))))
+ (#Apply (#Product Compiler
+ (#Bound +1))
+ (#Apply Text Either)))))
(_lux_function _ msg
(_lux_function _ state
(#Left msg))))
@@ -771,17 +768,17 @@
#Nil)
(_lux_def form$
- (_lux_: (#Function (#App List Code) Code)
+ (_lux_: (#Function (#Apply Code List) Code)
(_lux_function _ tokens (_meta (#Form tokens))))
#Nil)
(_lux_def tuple$
- (_lux_: (#Function (#App List Code) Code)
+ (_lux_: (#Function (#Apply Code List) Code)
(_lux_function _ tokens (_meta (#Tuple tokens))))
#Nil)
(_lux_def record$
- (_lux_: (#Function (#App List (#Product Code Code)) Code)
+ (_lux_: (#Function (#Apply (#Product Code Code) List) Code)
(_lux_function _ tokens (_meta (#Record tokens))))
#Nil)
@@ -1004,8 +1001,8 @@
(#Cons x (#Cons y xs))
(return (#Cons (form$ (#Cons (symbol$ ["lux" "$'"])
- (#Cons (form$ (#Cons (tag$ ["lux" "App"])
- (#Cons x (#Cons y #Nil))))
+ (#Cons (form$ (#Cons (tag$ ["lux" "Apply"])
+ (#Cons y (#Cons x #Nil))))
xs)))
#Nil))
@@ -1118,8 +1115,8 @@
#Nil
## (-> (List Code) (-> (List Text) (Lux (List Code))) (Lux (List Code)))
(#Function ($' List Code)
- (#Function (#Function ($' List Text) (#App Lux ($' List Code)))
- (#App Lux ($' List Code))
+ (#Function (#Function ($' List Text) (#Apply ($' List Code) Lux))
+ (#Apply ($' List Code) Lux)
))
(_lux_case args
#Nil
@@ -1763,7 +1760,7 @@
(do Monad<Lux>
[=elem (untemplate elem)]
(wrap (form$ (list (symbol$ ["" "_lux_:"])
- (form$ (list (tag$ ["lux" "App"]) (tuple$ (list (symbol$ ["lux" "List"]) (symbol$ ["lux" "Code"])))))
+ (form$ (list (tag$ ["lux" "Apply"]) (tuple$ (list (symbol$ ["lux" "Code"]) (symbol$ ["lux" "List"])))))
(form$ (list (tag$ ["lux" "Cons"]) (tuple$ (list =elem (tag$ ["lux" "Nil"]))))))))))))
elems))]
(wrap (wrap-meta (form$ (list tag
@@ -2495,7 +2492,7 @@
[_ (#Form (#Cons type-fn args))]
(fold (_lux_: (-> Code Code Code)
- (function' [arg type-fn] (` (#;App (~ type-fn) (~ arg)))))
+ (function' [arg type-fn] (` (#;Apply (~ arg) (~ type-fn)))))
(walk-type type-fn)
(map walk-type args))
@@ -2632,9 +2629,9 @@
[Int (List Self)])")])
(_lux_case tokens
(#Cons [_ (#Symbol "" name)] (#Cons body #Nil))
- (let' [body' (replace-syntax (list [name (` (#App (~ (make-bound +0)) (~ (make-bound +1))))])
+ (let' [body' (replace-syntax (list [name (` (#Apply (~ (make-bound +1)) (~ (make-bound +0))))])
(update-bounds body))]
- (return (list (` (#App (#UnivQ #Nil (~ body')) Void)))))
+ (return (list (` (#Apply Void (#UnivQ #Nil (~ body')))))))
_
(fail "Wrong syntax for Rec")))
@@ -3382,8 +3379,8 @@
(#Product left right)
(#Product (beta-reduce env left) (beta-reduce env right))
- (#App ?type-fn ?type-arg)
- (#App (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
+ (#Apply arg func)
+ (#Apply (beta-reduce env arg) (beta-reduce env func))
(#UnivQ ?local-env ?local-def)
(case ?local-env
@@ -3428,7 +3425,7 @@
(#ExQ env body)
(#Some (beta-reduce (list& type-fn param env) body))
- (#App F A)
+ (#Apply A F)
(do Monad<Maybe>
[type-fn* (apply-type F A)]
(apply-type type-fn* param))
@@ -3452,18 +3449,27 @@
[flatten-variant #;Sum]
[flatten-tuple #;Product]
[flatten-lambda #;Function]
- [flatten-app #;App]
)
+(def: (flatten-app type)
+ (-> Type [Type (List Type)])
+ (case type
+ (#;Apply head func')
+ (let [[func tail] (flatten-app func')]
+ [func (#;Cons head tail)])
+
+ _
+ [type (list)]))
+
(def: (resolve-struct-type type)
(-> Type (Maybe (List Type)))
(case type
(#Product _)
(#Some (flatten-tuple type))
- (#App fun arg)
+ (#Apply arg func)
(do Monad<Maybe>
- [output (apply-type fun arg)]
+ [output (apply-type func arg)]
(resolve-struct-type output))
(#UnivQ _ body)
@@ -3516,8 +3522,8 @@
(def: (resolve-type-tags type)
(-> Type (Lux (Maybe [(List Ident) (List Type)])))
(case type
- (#App fun arg)
- (resolve-type-tags fun)
+ (#Apply arg func)
+ (resolve-type-tags func)
(#UnivQ env body)
(resolve-type-tags body)
@@ -3668,7 +3674,7 @@
(struct (~@ defs)))))))
#;None
- (fail "Struct must have a name other than \"_\"!"))
+ (fail "Cannot infer name, so struct must have a name other than \"_\"!"))
#None
(fail "Wrong syntax for struct:"))))
@@ -4265,8 +4271,12 @@
(#ExQ env body)
($_ Text/append "(Ex " (Type/show body) ")")
- (#App _)
- ($_ Text/append "(" (|> (flatten-app type) (map Type/show) (interpose " ") reverse (fold Text/append "")) ")")
+ (#Apply _)
+ (let [[func args] (flatten-app type)]
+ ($_ Text/append
+ "(" (Type/show func) " "
+ (|> args (map Type/show) (interpose " ") reverse (fold Text/append ""))
+ ")"))
(#Named [prefix name] _)
($_ Text/append prefix ";" name)
@@ -4858,7 +4868,7 @@
(<tag> left right)
(<tag> (beta-reduce env left) (beta-reduce env right)))
([#;Function]
- [#;App])
+ [#;Apply])
(^template [<tag>]
(<tag> old-env def)
@@ -5151,8 +5161,8 @@
(let [env' (untemplate-list (map type-to-ast env))]
(` (#ExQ (~ env') (~ (type-to-ast type)))))
- (#App fun arg)
- (` (#App (~ (type-to-ast fun)) (~ (type-to-ast arg))))
+ (#Apply arg fun)
+ (` (#Apply (~ (type-to-ast arg)) (~ (type-to-ast fun))))
(#Named [module name] type)
(` (#Named [(~ (text$ module)) (~ (text$ name))] (~ (type-to-ast type))))
@@ -5486,7 +5496,7 @@
expected get-expected-type
g!temp (gensym "temp")]
(let [output (list g!temp
- (` (;_lux_case (;_lux_: (#;App Maybe (~ (type-to-ast expected)))
+ (` (;_lux_case (;_lux_: (#;Apply (~ (type-to-ast expected)) Maybe)
(case (~ g!temp)
(~@ (multi-level-case$ g!temp [mlc body]))
diff --git a/stdlib/source/lux/control/effect.lux b/stdlib/source/lux/control/effect.lux
index 457519442..6c6feee06 100644
--- a/stdlib/source/lux/control/effect.lux
+++ b/stdlib/source/lux/control/effect.lux
@@ -229,7 +229,7 @@
(def: (un-apply type-app)
(-> Type Type)
(case type-app
- (#;App effect value)
+ (#;Apply value effect)
effect
_
@@ -269,17 +269,17 @@
(List/append (flatten-effect-stack left)
(flatten-effect-stack right))
- (^ (#;App branches (#;Var _)))
+ (^ (#;Apply (#;Var _) branches))
(flatten-effect-stack branches)
- (^ (#;App (#;App (#;Named (ident-for ;;|@) _)
- left)
- right))
+ (^ (#;Apply right
+ (#;Apply left
+ (#;Named (ident-for ;;|@) _))))
(#;Cons left (flatten-effect-stack right))
- (^ (#;App (#;App (#;Named (ident-for M;Free) _)
- effect)
- param))
+ (^ (#;Apply param
+ (#;Apply effect
+ (#;Named (ident-for M;Free) _))))
(list effect)
_
@@ -321,10 +321,10 @@
[input (macro;find-type var)
output macro;expected-type]
(case [input output]
- (^multi [(#;App eff0 _) (#;App stackT0 recT0)]
+ (^multi [(#;Apply _ eff0) (#;Apply recT0 stackT0)]
[(type;apply-type stackT0 recT0) (#;Some unfoldT0)]
- [stackT0 (^ (#;App (#;Named (ident-for M;Free) _)
- stackT1))]
+ [stackT0 (^ (#;Apply stackT1
+ (#;Named (ident-for M;Free) _)))]
[(type;apply-type stackT1 recT0) (#;Some unfoldT1)]
[(flatten-effect-stack unfoldT1) stack]
[(|> stack list;enumerate
diff --git a/stdlib/source/lux/host.jvm.lux b/stdlib/source/lux/host.jvm.lux
index 05f8313fc..77b77c219 100644
--- a/stdlib/source/lux/host.jvm.lux
+++ b/stdlib/source/lux/host.jvm.lux
@@ -2006,7 +2006,7 @@
(#;Host name params)
(:: Monad<Lux> wrap name)
- (#;App F A)
+ (#;Apply A F)
(case (type;apply-type F A)
#;None
(macro;fail (format "Cannot apply type: " (type;to-text F) " to " (type;to-text A)))
diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux
index 7f1c7bc8c..22812023a 100644
--- a/stdlib/source/lux/macro/poly.lux
+++ b/stdlib/source/lux/macro/poly.lux
@@ -200,7 +200,7 @@
(do macro;Monad<Lux>
[#let [[:func: :args:] (loop [:type: (type;un-name :type:)]
(case :type:
- (#;App :func: :arg:)
+ (#;Apply :arg: :func:)
(let [[:func:' :args:] (recur :func:)]
[:func:' (list& :arg: :args:)])
@@ -217,7 +217,7 @@
(-> Ident (Matcher Type))
(;function [:type:]
(case (type;un-name :type:)
- (^multi (#;App :quant: :arg:)
+ (^multi (#;Apply :arg: :quant:)
[(type;un-alias :quant:) (#;Named actual _)]
(Ident/= name actual))
(:: macro;Monad<Lux> wrap :arg:)
@@ -229,7 +229,7 @@
(-> Ident (Matcher [Type Type]))
(;function [:type:]
(case (type;un-name :type:)
- (^multi (#;App (#;App :quant: :arg0:) :arg1:)
+ (^multi (#;Apply :arg1: (#;Apply :arg0: :quant:))
[(type;un-alias :quant:) (#;Named actual _)]
(Ident/= name actual))
(:: macro;Monad<Lux> wrap [:arg0: :arg1:])
@@ -308,7 +308,7 @@
(|> env
(dict;put current-size [funcT funcA])
(dict;put (n.inc current-size) [varT varA])
- (extend-env [(#;App funcT varT) (` (#;App (~ funcA) (~ varA)))]
+ (extend-env [(#;Apply varT funcT) (` (#;Apply (~ varA) (~ funcA)))]
type-vars')
))))
@@ -402,7 +402,7 @@
(<tag> left right)
(` (<tag> (~ (to-ast env left))
(~ (to-ast env right)))))
- ([#;Function] [#;App])
+ ([#;Function] [#;Apply])
(^template [<tag> <macro> <flattener>]
(<tag> left right)
diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux
index 76620ea40..fa55ca41b 100644
--- a/stdlib/source/lux/type.lux
+++ b/stdlib/source/lux/type.lux
@@ -20,8 +20,8 @@
(^template [<tag>]
(<tag> left right)
(<tag> (beta-reduce env left) (beta-reduce env right)))
- ([#;Sum] [#;Product]
- [#;Function] [#;App])
+ ([#;Sum] [#;Product]
+ [#;Function] [#;Apply])
(^template [<tag>]
(<tag> old-env def)
@@ -64,7 +64,7 @@
([#;Var] [#;Ex] [#;Bound])
(^or [(#;Function xleft xright) (#;Function yleft yright)]
- [(#;App xleft xright) (#;App yleft yright)])
+ [(#;Apply xleft xright) (#;Apply yleft yright)])
(and (= xleft yleft)
(= xright yright))
@@ -119,9 +119,9 @@
(def: #export (flatten-application type)
(-> Type [Type (List Type)])
(case type
- (#;App left' right)
- (let [[left rights] (flatten-application left')]
- [left (List/append rights (list right))])
+ (#;Apply arg func')
+ (let [[func args] (flatten-application func')]
+ [func (List/append args (list arg))])
_
[type (list)]))
@@ -148,7 +148,7 @@
(#;Some (beta-reduce (list& type-func param env) body)))
([#;UnivQ] [#;ExQ])
- (#;App F A)
+ (#;Apply A F)
(do Monad<Maybe>
[type-fn* (apply-type F A)]
(apply-type type-fn* param))
@@ -180,7 +180,7 @@
(<tag> left right)
(` (<tag> (~ (to-ast left))
(~ (to-ast right)))))
- ([#;Function] [#;App])
+ ([#;Function] [#;Apply])
(^template [<tag> <macro> <flattener>]
(<tag> left right)
@@ -246,7 +246,7 @@
(#;Ex id)
($_ Text/append "⟨e:" (Nat/encode id) "⟩")
- (#;App fun param)
+ (#;Apply param fun)
(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 "")) ")"))
@@ -304,14 +304,14 @@
(#;Cons input inputs')
(#;Function input (function inputs' output))))
-(def: #export (application quant params)
- (-> Type (List Type) Type)
+(def: #export (application params quant)
+ (-> (List Type) Type Type)
(case params
#;Nil
quant
(#;Cons param params')
- (application (#;App quant param) params')))
+ (application params' (#;Apply param quant))))
(do-template [<name> <tag>]
[(def: #export (<name> size body)
@@ -330,7 +330,7 @@
(#;Named [module name] _type)
(quantified? _type)
- (#;App F A)
+ (#;Apply A F)
(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 8fd88da82..b0018525b 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -54,7 +54,7 @@
(#;Named _ sig-type')
(find-member-type idx sig-type')
- (#;App func arg)
+ (#;Apply arg func)
(case (type;apply-type func arg)
#;None
(tc;fail (format "Cannot apply type " (%type func) " to type " (%type arg)))
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index e8f24102c..1779f62bd 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -253,7 +253,7 @@
=right (clean t-id right)]
(wrap (<tag> =left =right))))
([#;Function]
- [#;App]
+ [#;Apply]
[#;Product]
[#;Sum])
@@ -293,36 +293,9 @@
(def: #export (delete-var id)
(-> Nat (Check Unit))
- (do Monad<Check>
- [? (bound? id)
- _ (if ?
- (wrap [])
- (do Monad<Check>
- [[ex-id ex] existential]
- (write-var id ex)))
- bindings get-bindings
- bindings' (mapM @
- (function [(^@ binding [b-id b-type])]
- (if (n.= id b-id)
- (wrap binding)
- (case b-type
- #;None
- (wrap binding)
-
- (#;Some b-type')
- (case b-type'
- (#;Var t-id)
- (if (n.= id t-id)
- (wrap [b-id #;None])
- (wrap binding))
-
- _
- (do Monad<Check>
- [b-type'' (clean id b-type')]
- (wrap [b-id (#;Some b-type'')])))
- )))
- bindings)]
- (set-bindings (var::remove id bindings'))))
+ (function [context]
+ (#R;Success [(update@ #;var-bindings (var::remove id) context)
+ []])))
(def: #export (with-var k)
(All [a] (-> (-> [Nat Type] (Check a)) (Check a)))
@@ -429,32 +402,32 @@
(function [bound]
(check' expected bound fixed)))
- [(#;App (#;Ex eid) eA) (#;App (#;Ex aid) aA)]
+ [(#;Apply eA (#;Ex eid)) (#;Apply aA (#;Ex aid))]
(if (n.= eid aid)
(check' eA aA fixed)
(fail-check expected actual))
- [(#;App (#;Var id) A1) (#;App F2 A2)]
+ [(#;Apply A1 (#;Var id)) (#;Apply A2 F2)]
(either (do Monad<Check>
[F1 (read-var id)]
- (check' (#;App F1 A1) actual fixed))
+ (check' (#;Apply A1 F1) actual fixed))
(do Monad<Check>
[fixed (check' (#;Var id) F2 fixed)
e' (apply-type! F2 A1)
a' (apply-type! F2 A2)]
(check' e' a' fixed)))
- [(#;App F1 A1) (#;App (#;Var id) A2)]
+ [(#;Apply A1 F1) (#;Apply A2 (#;Var id))]
(either (do Monad<Check>
[F2 (read-var id)]
- (check' expected (#;App F2 A2) fixed))
+ (check' expected (#;Apply A2 F2) fixed))
(do Monad<Check>
[fixed (check' F1 (#;Var id) fixed)
e' (apply-type! F1 A1)
a' (apply-type! F1 A2)]
(check' e' a' fixed)))
- [(#;App F A) _]
+ [(#;Apply A F) _]
(let [fx-pair [expected actual]]
(case (fx-get fx-pair fixed)
(#;Some ?)
@@ -467,7 +440,7 @@
[expected' (apply-type! F A)]
(check' expected' actual (fx-put fx-pair true fixed)))))
- [_ (#;App F A)]
+ [_ (#;Apply A F)]
(do Monad<Check>
[actual' (apply-type! F A)]
(check' expected actual' fixed))
diff --git a/stdlib/test/test/lux/type.lux b/stdlib/test/test/lux/type.lux
index 8adc9384e..a4c1019f3 100644
--- a/stdlib/test/test/lux/type.lux
+++ b/stdlib/test/test/lux/type.lux
@@ -113,7 +113,7 @@
extra (|> gen-type
(R;filter (function [type]
(case type
- (^or (#;Function _) (#;App _))
+ (^or (#;Function _) (#;Apply _))
false
_
@@ -127,7 +127,7 @@
(&/= extra output))))
(test "Can build and tear-down application types."
- (let [[tfunc tparams] (|> members (&;application extra) &;flatten-application)]
+ (let [[tfunc tparams] (|> extra (&;application members) &;flatten-application)]
(n.= (list;size members) (list;size tparams))))
))
diff --git a/stdlib/test/test/lux/type/check.lux b/stdlib/test/test/lux/type/check.lux
index 1c4767a15..703d89d11 100644
--- a/stdlib/test/test/lux/type/check.lux
+++ b/stdlib/test/test/lux/type/check.lux
@@ -123,10 +123,10 @@
[meta gen-type
data gen-type]
(test "Can type-check type application."
- (and (&;checks? (#;App (#;App Meta meta) data)
+ (and (&;checks? (#;Apply data (#;Apply meta Meta))
(type;tuple (list meta data)))
(&;checks? (type;tuple (list meta data))
- (#;App (#;App Meta meta) data)))))
+ (#;Apply data (#;Apply meta Meta))))))
(context: "Host types"
[nameL gen-name
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-06 14:33:32 +0000