From e085c8c685b1e22827443a43d6f20b5ab6e72d6a Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Tue, 1 Sep 2015 16:48:54 -0400 Subject: - Fixed the implementation of the Rec macro, which forgot to do application on Void to achieve "recursion". - Introduced ExQ types into the type-system (still pending work on inference). --- source/lux.lux | 171 +++++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 111 insertions(+), 60 deletions(-) (limited to 'source/lux.lux') diff --git a/source/lux.lux b/source/lux.lux index 722369131..5f5c6925b 100644 --- a/source/lux.lux +++ b/source/lux.lux @@ -8,51 +8,51 @@ ("apply" ["java.lang.Object"] "java.lang.Object" ["public" "abstract"])) ## Basic types -(_lux_def Bool (9 ["lux" "Bool"] - (0 "java.lang.Boolean"))) +(_lux_def Bool (10 ["lux" "Bool"] + (0 "java.lang.Boolean"))) (_lux_export Bool) -(_lux_def Int (9 ["lux" "Int"] - (0 "java.lang.Long"))) +(_lux_def Int (10 ["lux" "Int"] + (0 "java.lang.Long"))) (_lux_export Int) -(_lux_def Real (9 ["lux" "Real"] - (0 "java.lang.Double"))) +(_lux_def Real (10 ["lux" "Real"] + (0 "java.lang.Double"))) (_lux_export Real) -(_lux_def Char (9 ["lux" "Char"] - (0 "java.lang.Character"))) +(_lux_def Char (10 ["lux" "Char"] + (0 "java.lang.Character"))) (_lux_export Char) -(_lux_def Text (9 ["lux" "Text"] - (0 "java.lang.String"))) +(_lux_def Text (10 ["lux" "Text"] + (0 "java.lang.String"))) (_lux_export Text) -(_lux_def Unit (9 ["lux" "Unit"] - (2 (0)))) +(_lux_def Unit (10 ["lux" "Unit"] + (2 (0)))) (_lux_export Unit) -(_lux_def Void (9 ["lux" "Void"] - (1 (0)))) +(_lux_def Void (10 ["lux" "Void"] + (1 (0)))) (_lux_export Void) -(_lux_def Ident (9 ["lux" "Ident"] - (2 (1 Text (1 Text (0)))))) +(_lux_def Ident (10 ["lux" "Ident"] + (2 (1 Text (1 Text (0)))))) (_lux_export Ident) ## (deftype (List a) ## (| #Nil ## (#Cons a (List a)))) (_lux_def List - (9 ["lux" "List"] - (7 (0) - (1 (1 ## "lux;Nil" - (2 (0)) - (1 ## "lux;Cons" - (2 (1 (4 1) - (1 (8 (4 0) (4 1)) - (0)))) - (0))))))) + (10 ["lux" "List"] + (7 (0) + (1 (1 ## "lux;Nil" + (2 (0)) + (1 ## "lux;Cons" + (2 (1 (4 1) + (1 (9 (4 0) (4 1)) + (0)))) + (0))))))) (_lux_export List) (_lux_declare-tags [#Nil #Cons] List) @@ -60,13 +60,13 @@ ## (| #None ## (1 a))) (_lux_def Maybe - (9 ["lux" "Maybe"] - (7 (0) - (1 (1 ## "lux;None" - (2 (0)) - (1 ## "lux;Some" - (4 1) - (0))))))) + (10 ["lux" "Maybe"] + (7 (0) + (1 (1 ## "lux;None" + (2 (0)) + (1 ## "lux;Some" + (4 1) + (0))))))) (_lux_export Maybe) (_lux_declare-tags [#None #Some] Maybe) @@ -78,40 +78,43 @@ ## (#BoundT Int) ## (#VarT Int) ## (#UnivQ (List Type) Type) +## (#ExQ (List Type) Type) ## (#AppT Type Type) ## (#NamedT Ident Type) ## )) (_lux_def Type - (9 ["lux" "Type"] - (_lux_case (8 (4 0) (4 1)) - Type - (_lux_case (8 List Type) - TypeList - (8 (7 (0) - (1 (1 ## "lux;DataT" - Text - (1 ## "lux;VariantT" - TypeList - (1 ## "lux;TupleT" + (10 ["lux" "Type"] + (_lux_case (9 (4 0) (4 1)) + Type + (_lux_case (9 List Type) + TypeList + (9 (7 (0) + (1 (1 ## "lux;DataT" + Text + (1 ## "lux;VariantT" TypeList - (1 ## "lux;LambdaT" - (2 (1 Type (1 Type (0)))) - (1 ## "lux;BoundT" - Int - (1 ## "lux;VarT" + (1 ## "lux;TupleT" + TypeList + (1 ## "lux;LambdaT" + (2 (1 Type (1 Type (0)))) + (1 ## "lux;BoundT" Int - (1 ## "lux;ExT" + (1 ## "lux;VarT" Int - (1 ## "lux;UnivQ" - (2 (1 TypeList (1 Type (0)))) - (1 ## "lux;AppT" - (2 (1 Type (1 Type (0)))) - (1 ## "lux;NamedT" - (2 (1 Ident (1 Type (0)))) - (0))))))))))))) - Void))))) + (1 ## "lux;ExT" + Int + (1 ## "lux;UnivQ" + (2 (1 TypeList (1 Type (0)))) + (1 ## "lux;ExQ" + (2 (1 TypeList (1 Type (0)))) + (1 ## "lux;AppT" + (2 (1 Type (1 Type (0)))) + (1 ## "lux;NamedT" + (2 (1 Ident (1 Type (0)))) + (0)))))))))))))) + Void))))) (_lux_export Type) -(_lux_declare-tags [#DataT #VariantT #TupleT #LambdaT #BoundT #VarT #ExT #UnivQ #AppT #NamedT] Type) +(_lux_declare-tags [#DataT #VariantT #TupleT #LambdaT #BoundT #VarT #ExT #UnivQ #ExQ #AppT #NamedT] Type) ## (deftype (Bindings k v) ## (& #counter Int @@ -841,6 +844,33 @@ (fail "Wrong syntax for All")) )) +(defmacro #export (Ex tokens) + (let'' [self-name tokens] (_lux_: (#TupleT (#Cons Text (#Cons ASTList #Nil))) + (_lux_case tokens + (#Cons [_ (#SymbolS "" self-name)] tokens) + [self-name tokens] + + _ + ["" tokens])) + (_lux_case tokens + (#Cons [_ (#TupleS args)] (#Cons body #Nil)) + (parse-univq-args args + (lambda'' [names] + (let'' body' (foldL (_lux_: (#LambdaT AST (#LambdaT Text AST)) + (lambda'' [body' name'] + (form$ (#Cons (tag$ ["lux" "ExQ"]) + (#Cons (tag$ ["lux" "Nil"]) + (#Cons (replace-syntax (#Cons [name' (make-bound 1)] #Nil) + (update-bounds body')) #Nil)))))) + (replace-syntax (#Cons [self-name (make-bound -2)] #Nil) + body) + names) + (return (#Cons body' #Nil))))) + + _ + (fail "Wrong syntax for Ex")) + )) + (def'' (reverse list) (All [a] (#LambdaT ($' List a) ($' List a))) (foldL (lambda'' [tail head] (#Cons head tail)) @@ -1765,7 +1795,7 @@ (_lux_case tokens (#Cons [_ (#SymbolS "" name)] (#Cons body #Nil)) (let' [body' (replace-syntax (@list [name (` (#AppT (~ (make-bound 0)) (~ (make-bound 1))))]) body)] - (return (@list (` (#UnivQ #Nil (~ body')))))) + (return (@list (` (#AppT (#UnivQ #Nil (~ body')) Void))))) _ (fail "Wrong syntax for Rec"))) @@ -2056,7 +2086,7 @@ (if (symbol? arg) (` (;_lux_lambda (~ g!blank) (~ arg) (~ body'))) (` (;_lux_lambda (~ g!blank) (~ g!blank) - (case (~ g!blank) (~ arg) (~ body'))))))) + (case (~ g!blank) (~ arg) (~ body'))))))) body (reverse tail)))] (return (@list (if (symbol? head) @@ -2266,6 +2296,9 @@ (#UnivQ ?env ?body) ($ text:++ "(All " (type:show ?body) ")") + (#ExQ ?env ?body) + ($ text:++ "(Ex " (type:show ?body) ")") + (#NamedT name type) (ident->text name) )) @@ -2303,6 +2336,14 @@ _ type) + (#ExQ ?local-env ?local-def) + (case ?local-env + #Nil + (#ExQ env ?local-def) + + _ + type) + (#LambdaT ?input ?output) (#LambdaT (beta-reduce env ?input) (beta-reduce env ?output)) @@ -2352,6 +2393,9 @@ (#UnivQ _ body) (resolve-struct-type body) + (#ExQ _ body) + (resolve-struct-type body) + (#NamedT name type) (resolve-struct-type type) @@ -2398,6 +2442,9 @@ (#UnivQ env body) (resolve-type-tags body) + + (#ExQ env body) + (resolve-type-tags body) (#NamedT [module name] _) (do Lux/Monad @@ -3257,6 +3304,10 @@ (#UnivQ env type) (let [env' (untemplate-list (map type->syntax env))] (` (#UnivQ (~ env') (~ (type->syntax type))))) + + (#ExQ env type) + (let [env' (untemplate-list (map type->syntax env))] + (` (#ExQ (~ env') (~ (type->syntax type))))) (#AppT fun arg) (` (#AppT (~ (type->syntax fun)) (~ (type->syntax arg)))) -- cgit v1.2.3