aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--source/lux/meta/type.lux157
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))