diff options
| -rw-r--r-- | source/lux/meta/type.lux | 157 |
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)) |