diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/lux/type.lux | 225 | ||||
| -rw-r--r-- | stdlib/source/lux/type/check.lux | 21 |
2 files changed, 121 insertions, 125 deletions
diff --git a/stdlib/source/lux/type.lux b/stdlib/source/lux/type.lux index 31de534eb..d8288314c 100644 --- a/stdlib/source/lux/type.lux +++ b/stdlib/source/lux/type.lux @@ -19,6 +19,113 @@ ["." code] ["s" syntax (#+ Syntax syntax:)]]]) +(template [<name> <tag>] + [(def: #export (<name> type) + (-> Type [Nat Type]) + (loop [num-args 0 + type type] + (case type + (<tag> env sub-type) + (recur (inc num-args) sub-type) + + _ + [num-args type])))] + + [flatten-univ-q #.UnivQ] + [flatten-ex-q #.ExQ] + ) + +(def: #export (flatten-function type) + (-> Type [(List Type) Type]) + (case type + (#.Function in out') + (let [[ins out] (flatten-function out')] + [(list& in ins) out]) + + _ + [(list) type])) + +(def: #export (flatten-application type) + (-> Type [Type (List Type)]) + (case type + (#.Apply arg func') + (let [[func args] (flatten-application func')] + [func (list@compose args (list arg))]) + + _ + [type (list)])) + +(template [<name> <tag>] + [(def: #export (<name> type) + (-> Type (List Type)) + (case type + (<tag> left right) + (list& left (<name> right)) + + _ + (list type)))] + + [flatten-variant #.Sum] + [flatten-tuple #.Product] + ) + +(def: #export (to-text type) + (-> Type Text) + (case type + (#.Primitive name params) + ($_ text@compose + "(primitive " + (text.enclose' text.double-quote name) + (|> params + (list@map (|>> to-text (text@compose " "))) + (list@fold (function.flip text@compose) "")) + ")") + + (^template [<tag> <open> <close> <flatten>] + (<tag> _) + ($_ text@compose <open> + (|> (<flatten> type) + (list@map to-text) + list.reverse + (list.interpose " ") + (list@fold text@compose "")) + <close>)) + ([#.Sum "(| " ")" flatten-variant] + [#.Product "[" "]" flatten-tuple]) + + (#.Function input output) + (let [[ins out] (flatten-function type)] + ($_ text@compose "(-> " + (|> ins + (list@map to-text) + list.reverse + (list.interpose " ") + (list@fold text@compose "")) + " " (to-text out) ")")) + + (#.Parameter idx) + (nat@encode idx) + + (#.Var id) + ($_ text@compose "⌈v:" (nat@encode id) "⌋") + + (#.Ex id) + ($_ text@compose "⟨e:" (nat@encode id) "⟩") + + (#.Apply param fun) + (let [[type-func type-args] (flatten-application type)] + ($_ text@compose "(" (to-text type-func) " " (|> type-args (list@map to-text) list.reverse (list.interpose " ") (list@fold text@compose "")) ")")) + + (^template [<tag> <desc>] + (<tag> env body) + ($_ text@compose "(" <desc> " {" (|> env (list@map to-text) (text.join-with " ")) "} " (to-text body) ")")) + ([#.UnivQ "All"] + [#.ExQ "Ex"]) + + (#.Named [module name] type) + ($_ text@compose module "." name) + )) + (def: (beta-reduce env type) (-> (List Type) Type Type) (case type @@ -43,7 +150,16 @@ [#.ExQ]) (#.Parameter idx) - (maybe.default (error! (text@compose "Unknown type var: " (nat@encode idx))) + (maybe.default (error! ($_ text@compose + "Unknown type parameter" text.new-line + " Index: " (nat@encode idx) text.new-line + "Environment: " (|> env + list.enumerate + (list@map (.function (_ [index type]) + ($_ text@compose + (nat@encode index) + " " (..to-text type)))) + (text.join-with (text@compose text.new-line " "))))) (list.nth idx env)) _ @@ -91,56 +207,6 @@ #0 ))) -(template [<name> <tag>] - [(def: #export (<name> type) - (-> Type [Nat Type]) - (loop [num-args 0 - type type] - (case type - (<tag> env sub-type) - (recur (inc num-args) sub-type) - - _ - [num-args type])))] - - [flatten-univ-q #.UnivQ] - [flatten-ex-q #.ExQ] - ) - -(def: #export (flatten-function type) - (-> Type [(List Type) Type]) - (case type - (#.Function in out') - (let [[ins out] (flatten-function out')] - [(list& in ins) out]) - - _ - [(list) type])) - -(def: #export (flatten-application type) - (-> Type [Type (List Type)]) - (case type - (#.Apply arg func') - (let [[func args] (flatten-application func')] - [func (list@compose args (list arg))]) - - _ - [type (list)])) - -(template [<name> <tag>] - [(def: #export (<name> type) - (-> Type (List Type)) - (case type - (<tag> left right) - (list& left (<name> right)) - - _ - (list type)))] - - [flatten-variant #.Sum] - [flatten-tuple #.Product] - ) - (def: #export (apply params func) (-> (List Type) Type (Maybe Type)) (case params @@ -193,63 +259,6 @@ ([#.UnivQ] [#.ExQ]) )) -(def: #export (to-text type) - (-> Type Text) - (case type - (#.Primitive name params) - ($_ text@compose - "(primitive " - (text.enclose' text.double-quote name) - (|> params - (list@map (|>> to-text (text@compose " "))) - (list@fold (function.flip text@compose) "")) - ")") - - (^template [<tag> <open> <close> <flatten>] - (<tag> _) - ($_ text@compose <open> - (|> (<flatten> type) - (list@map to-text) - list.reverse - (list.interpose " ") - (list@fold text@compose "")) - <close>)) - ([#.Sum "(| " ")" flatten-variant] - [#.Product "[" "]" flatten-tuple]) - - (#.Function input output) - (let [[ins out] (flatten-function type)] - ($_ text@compose "(-> " - (|> ins - (list@map to-text) - list.reverse - (list.interpose " ") - (list@fold text@compose "")) - " " (to-text out) ")")) - - (#.Parameter idx) - (nat@encode idx) - - (#.Var id) - ($_ text@compose "⌈v:" (nat@encode id) "⌋") - - (#.Ex id) - ($_ text@compose "⟨e:" (nat@encode id) "⟩") - - (#.Apply param fun) - (let [[type-func type-args] (flatten-application type)] - ($_ text@compose "(" (to-text type-func) " " (|> type-args (list@map to-text) list.reverse (list.interpose " ") (list@fold text@compose "")) ")")) - - (^template [<tag> <desc>] - (<tag> env body) - ($_ text@compose "(" <desc> " {" (|> env (list@map to-text) (text.join-with " ")) "} " (to-text body) ")")) - ([#.UnivQ "All"] - [#.ExQ "Ex"]) - - (#.Named [module name] type) - ($_ text@compose module "." name) - )) - (def: #export (un-alias type) (-> Type Type) (case type diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux index ee45875d5..3eed928f9 100644 --- a/stdlib/source/lux/type/check.lux +++ b/stdlib/source/lux/type/check.lux @@ -115,6 +115,10 @@ (open: "check@." ..monad) +(def: (var::new id plist) + (-> Var Type-Vars Type-Vars) + (#.Cons [id #.None] plist)) + (def: (var::get id plist) (-> Var Type-Vars (Maybe (Maybe Type))) (case plist @@ -127,10 +131,6 @@ #.Nil #.None)) -(def: (var::new id plist) - (-> Var Type-Vars Type-Vars) - (#.Cons [id #.None] plist)) - (def: (var::put id value plist) (-> Var (Maybe Type) Type-Vars Type-Vars) (case plist @@ -145,19 +145,6 @@ (#.Cons [var-id var-type] (var::put id value plist'))))) -(def: (var::remove id plist) - (-> Var Type-Vars Type-Vars) - (case plist - (#.Cons [var-id var-type] - plist') - (if (!n/= id var-id) - plist' - (#.Cons [var-id var-type] - (var::remove id plist'))) - - #.Nil - #.Nil)) - (def: #export (run context proc) (All [a] (-> Type-Context (Check a) (Error a))) (case (proc context) |