From a2e790c57c49104c63c26a306158141980791da8 Mon Sep 17 00:00:00 2001
From: Eduardo Julian
Date: Wed, 17 Apr 2019 23:18:18 -0400
Subject: - Improved error messaging when trying to access an unbound
 type-parameter during beta-reduction. - Removed the (unused) "var::remove"
 function.

---
 stdlib/source/lux/type.lux       | 225 ++++++++++++++++++++-------------------
 stdlib/source/lux/type/check.lux |  21 +---
 2 files changed, 121 insertions(+), 125 deletions(-)

(limited to 'stdlib')

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)
-- 
cgit v1.2.3