From 1a7aa7e3ed6fae612d2b22eacc5805bd786efdd9 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 21 Jun 2017 23:33:01 -0400 Subject: - Renamed "App" to "Apply" and swapped the order of the arguments to it. - Also did argument swapping for lux/type;application. --- stdlib/source/lux.lux | 224 ++++++++++++++++++----------------- stdlib/source/lux/control/effect.lux | 22 ++-- stdlib/source/lux/host.jvm.lux | 2 +- stdlib/source/lux/macro/poly.lux | 10 +- stdlib/source/lux/type.lux | 26 ++-- stdlib/source/lux/type/auto.lux | 2 +- stdlib/source/lux/type/check.lux | 49 ++------ 7 files changed, 159 insertions(+), 176 deletions(-) (limited to 'stdlib/source') 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 [=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 [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 - [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 @@ ( left right) ( (beta-reduce env left) (beta-reduce env right))) ([#;Function] - [#;App]) + [#;Apply]) (^template [] ( 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 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 [#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 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 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 @@ ( left right) (` ( (~ (to-ast env left)) (~ (to-ast env right))))) - ([#;Function] [#;App]) + ([#;Function] [#;Apply]) (^template [ ] ( 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 [] ( left right) ( (beta-reduce env left) (beta-reduce env right))) - ([#;Sum] [#;Product] - [#;Function] [#;App]) + ([#;Sum] [#;Product] + [#;Function] [#;Apply]) (^template [] ( 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 [type-fn* (apply-type F A)] (apply-type type-fn* param)) @@ -180,7 +180,7 @@ ( left right) (` ( (~ (to-ast left)) (~ (to-ast right))))) - ([#;Function] [#;App]) + ([#;Function] [#;Apply]) (^template [ ] ( 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 [ ] [(def: #export ( size body) @@ -330,7 +330,7 @@ (#;Named [module name] _type) (quantified? _type) - (#;App F A) + (#;Apply A F) (default false (do Monad [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 ( =left =right)))) ([#;Function] - [#;App] + [#;Apply] [#;Product] [#;Sum]) @@ -293,36 +293,9 @@ (def: #export (delete-var id) (-> Nat (Check Unit)) - (do Monad - [? (bound? id) - _ (if ? - (wrap []) - (do Monad - [[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 - [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 [F1 (read-var id)] - (check' (#;App F1 A1) actual fixed)) + (check' (#;Apply A1 F1) actual fixed)) (do Monad [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 [F2 (read-var id)] - (check' expected (#;App F2 A2) fixed)) + (check' expected (#;Apply A2 F2) fixed)) (do Monad [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 [actual' (apply-type! F A)] (check' expected actual' fixed)) -- cgit v1.2.3