aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2019-04-17 23:18:18 -0400
committerEduardo Julian2019-04-17 23:18:18 -0400
commita2e790c57c49104c63c26a306158141980791da8 (patch)
treef8db56f793d6f0804ddf4069eaae5d6d1f0e6386
parent319f5d120a88eb9e9a75e5ca0c03f5fd555cab14 (diff)
- Improved error messaging when trying to access an unbound type-parameter during beta-reduction.
- Removed the (unused) "var::remove" function.
-rw-r--r--stdlib/source/lux/type.lux225
-rw-r--r--stdlib/source/lux/type/check.lux21
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)