- Added the lux/meta/type module (still missing equality due to an issue with type-inference & Type/Show needs some pending corrections).

1 files changed, 157 insertions, 0 deletions

diff --git a/source/lux/meta/type.lux b/source/lux/meta/type.lux
new file mode 100644
index 000000000..d32ea993b
--- /dev/null
+++ b/source/lux/meta/type.lux
@@ -0,0 +1,157 @@
+##  Copyright (c) Eduardo Julian. All rights reserved.
+##  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+##  If a copy of the MPL was not distributed with this file,
+##  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(;import lux
+         (lux (control show
+                       eq
+                       monad)
+              (data (text #open ("text:" Text/Monoid Text/Eq))
+                    (number/int #open ("int:" Int/Eq Int/Show))
+                    maybe
+                    (list #refer #all #open ("list:" List/Monad)))
+              ))
+
+## [Structures]
+(defstruct #export Type/Show (Show Type)
+  (def (show type)
+    (case type
+      (#;DataT name)
+      ($ text:++ "(^ " name ")")
+
+      (#;TupleT members)
+      (case members
+        #;Nil
+        "(,)"
+
+        _
+        ($ text:++ "(, " (|> members (list:map show) (interpose " ") (foldL text:++ "")) ")"))
+
+      (#;VariantT members)
+      (case members
+        #;Nil
+        "(|)"
+
+        _
+        ($ text:++ "(| " (|> members (list:map show) (interpose " ") (foldL text:++ "")) ")"))
+
+      (#;LambdaT input output)
+      ($ text:++ "(-> " (show input) " " (show output) ")")
+
+      (#;VarT id)
+      ($ text:++ "⌈" (int:show id) "⌋")
+
+      (#;BoundT idx)
+      (int:show idx)
+
+      (#;ExT id)
+      ($ text:++ "⟨" (int:show id) "⟩")
+
+      (#;AppT fun param)
+      ($ text:++ "(" (show fun) " " (show param) ")")
+
+      (#;UnivQ env body)
+      ($ text:++ "(All " (show body) ")")
+
+      (#;ExQ env body)
+      ($ text:++ "(Ex " (show body) ")")
+
+      (#;NamedT [module name] type)
+      ($ text:++ module ";" name)
+      )))
+
+## (defstruct #export Type/Eq (Eq Type)
+##   (def (= x y)
+##     (case [x y]
+##       [(#;DataT xname) (#;DataT yname)]
+##       (text:= xname yname)
+
+##       (\or [(#;VarT xid) (#;VarT yid)]
+##        [(#;ExT xid) (#;ExT yid)]
+##        [(#;BoundT xid) (#;BoundT yid)])
+##       (int:= xid yid)
+
+##       (\or [(#;LambdaT xleft xright) (#;LambdaT yleft yright)]
+##        [(#;AppT xleft xright) (#;AppT yleft yright)])
+##       (and (= xleft yleft)
+##            (= xright yright))
+
+##       [(#;NamedT [xmodule xname] xtype) (#;NamedT [ymodule yname] ytype)]
+##       (and (text:= xmodule ymodule)
+##            (text:= xname yname)
+##            (= xtype ytype))
+
+##       (\or [(#;TupleT xmembers) (#;TupleT ymembers)]
+##        [(#;VariantT xmembers) (#;VariantT ymembers)])
+##       (and (int:= (size xmembers) (size ymembers))
+##            (foldL (lambda [prev [x y]]
+##                     (and prev (= v y)))
+##                   true
+##                   (zip2 xmembers ymembers)))
+
+##       (\or [(#;UnivQ yenv ybody) (#;UnivQ yenv ybody)]
+##        [(#;ExQ yenv ybody) (#;ExQ yenv ybody)])
+##       (and (int:= (size xenv) (size yenv))
+##            (foldL (lambda [prev [x y]]
+##                     (and prev (= v y)))
+##                   (= xbody ybody)
+##                   (zip2 xenv yenv)))
+
+##       _
+##       false
+##       )))
+
+## [Functions]
+(def #export (beta-reduce env type)
+  (-> (List Type) Type Type)
+  (case type
+    (\template [<tag>]
+     [(<tag> members)
+      (<tag> (list:map (beta-reduce env) members))])
+    [[#;VariantT]
+     [#;TupleT]]
+
+    (\template [<tag>]
+     [(<tag> left right)
+      (<tag> (beta-reduce env left) (beta-reduce env right))])
+    [[#;LambdaT]
+     [#;AppT]]
+
+    (\template [<tag>]
+     [(<tag> env def)
+      (case env
+        #;Nil
+        (<tag> env def)
+
+        _
+        type)])
+    [[#;UnivQ]
+     [#;ExQ]]
+    
+    (#;BoundT idx)
+    (? type (@ idx env))
+    
+    (#;NamedT name type)
+    (beta-reduce env type)
+
+    _
+    type
+    ))
+
+(def #export (apply-type type-fun param)
+  (-> Type Type (Maybe Type))
+  (case type-fun
+    (#;UnivQ env body)
+    (#;Some (beta-reduce (@list& type-fun param env) body))
+
+    (#;AppT F A)
+    (do Maybe/Monad
+      [type-fn* (apply-type F A)]
+      (apply-type type-fn* param))
+
+    (#;NamedT name type)
+    (apply-type type param)
+    
+    _
+    #;None))