From b1d166bcf88c24c2a1847866d1cf4e944fb80788 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 29 Apr 2015 23:58:19 -0400 Subject: - Made a slight correction to the Syntax type when it comes to records (slot-names are no longer Text, but Syntax). - lux/type;bound? no longer does further derefs to check for bound-ness? - Improved the way 2 type-vars are type-checked. - When cleaning type-vars, the dereffed typed is no longer cleaned again. --- source/lux.lux | 400 ++++++++++++++++++++++++++----------------------------- src/lux/type.clj | 50 ++++--- 2 files changed, 225 insertions(+), 225 deletions(-) diff --git a/source/lux.lux b/source/lux.lux index 973d5727b..e9b4484c5 100644 --- a/source/lux.lux +++ b/source/lux.lux @@ -168,9 +168,9 @@ (case' (#AppT [(#BoundT "w") (#AppT [(#BoundT "Syntax'") (#BoundT "w")])]) - Syntax' - (case' (#AppT [List Syntax']) - Syntax'List + Syntax + (case' (#AppT [List Syntax]) + SyntaxList (case' (#TupleT (#Cons [Text (#Cons [Text #Nil])])) Ident (#AllT [#None "Syntax'" "w" @@ -181,9 +181,9 @@ (#Cons [["lux;Text" Text] (#Cons [["lux;Symbol" Ident] (#Cons [["lux;Tag" Ident] - (#Cons [["lux;Form" Syntax'List] - (#Cons [["lux;Tuple" Syntax'List] - (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax' #Nil])]))])] + (#Cons [["lux;Form" SyntaxList] + (#Cons [["lux;Tuple" SyntaxList] + (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Syntax (#Cons [Syntax #Nil])]))])] #Nil]) ])])])])])])])])]) )]) @@ -308,8 +308,8 @@ (case' tokens (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])]) (return (:' SyntaxList - (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"])) - (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])]))) + (#Cons [($form (#Cons [($symbol ["" "case'"]) + (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])) #Nil]))) _ @@ -657,7 +657,7 @@ (->' ($' List (B' a)) ($' List (#TupleT (list (B' a) (B' a)))))) (case' xs (#Cons [x (#Cons [y xs'])]) - (list& [x y] (as-pairs xs')) + (#Cons [[x y] (as-pairs xs')]) _ #Nil)) @@ -730,46 +730,31 @@ (_meta (#Form (list (_meta (#Tag ["lux" "Cons"])) (_meta (#Tuple (list token (untemplate-list tokens'))))))))) -## (def (untemplate token) -## (->' Syntax Syntax) -## (case' token -## (#Meta [_ (#Bool value)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Bool"])) (_meta (#Bool value))))) - -## (#Meta [_ (#Int value)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Int"])) (_meta (#Int value))))) - -## (#Meta [_ (#Real value)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Real"])) (_meta (#Real value))))) - -## (#Meta [_ (#Char value)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Char"])) (_meta (#Char value))))) - -## (#Meta [_ (#Text value)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Text"])) (_meta (#Text value))))) - -## (#Meta [_ (#Tag [module name])]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Tag"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name)))))))) - -## (#Meta [_ (#Symbol [module name])]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Symbol"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name)))))))) - -## (#Meta [_ (#Tuple elems)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Tuple"])) (untemplate-list (map untemplate elems))))) +(defmacro #export ($ tokens) + (case' tokens + (#Cons [op (#Cons [init args])]) + (return (:' SyntaxList + (list (fold (:' (->' Syntax Syntax Syntax) + (lambda [a1 a2] + ($form (list op a1 a2)))) + init + args)))) + + _ + (fail "Wrong syntax for $"))) -## (#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol ["" "~"])]) (#Cons [(#Meta [_ unquoted]) #Nil])]))]) -## (_meta unquoted) +(def (list:++ xs ys) + (All' [a] (->' ($' List (B' a)) ($' List (B' a)) ($' List (B' a)))) + (case' xs + (#Cons [x xs']) + (#Cons [x (list:++ xs' ys)]) -## (#Meta [_ (#Form elems)]) -## (wrap-meta (#Form (list (_meta (#Tag ["lux" "Form"])) (untemplate-list (map untemplate elems))))) + #Nil + ys)) -## (#Meta [_ (#Record fields)]) -## (wrap-meta (#Record (map (:' (->' (#TupleT (list Text Syntax)) (#TupleT (list Text Syntax))) -## (lambda [kv] -## (let [[k v] kv] -## [k (untemplate v)]))) -## fields))) -## )) +## (: (All [a b] +## (-> (-> a b) (List a) (List b))) +## map) (def (splice untemplate tag elems) (->' (->' Syntax Syntax) Syntax ($' List Syntax) Syntax) @@ -782,39 +767,64 @@ spliced _ - (_meta (#Form (list ($symbol ["lux" "list"]) elem)))))) + ($form (list ($symbol ["" ":'"]) + ($symbol ["lux" "SyntaxList"]) + ($form (list ($symbol ["lux" "list"]) (untemplate elem)))))))) elems)] (wrap-meta ($form (list tag - (wrap-meta ($form (list& ($tag ["lux" "$"]) - ($tag ["lux" "list:++"]) - elems'))))))) + ($form (list& ($symbol ["lux" "$"]) + ($symbol ["lux" "list:++"]) + elems')))))) false (wrap-meta ($form (list tag (untemplate-list (map untemplate elems))))))) +## (def (splice untemplate tag elems) +## (->' (->' Syntax Syntax) Syntax ($' List Syntax) Syntax) +## (case' (any? spliced? elems) +## true +## (let [elems' (map (:' (->' Syntax Syntax) +## (lambda [elem] +## (case' elem +## (#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol ["" "~@"])]) (#Cons [spliced #Nil])]))]) +## spliced + +## _ +## ($form (list ($symbol ["" ":'"]) +## ($symbol ["lux" "SyntaxList"]) +## ($form (list ($symbol ["lux" "list"]) (untemplate elem)))))))) +## elems)] +## (wrap-meta ($form (list tag +## ($form (list& ($symbol ["lux" "$"]) +## ($symbol ["lux" "list:++"]) +## elems')))))) + +## false +## (wrap-meta ($form (list tag (untemplate-list (map untemplate elems))))))) + (def (untemplate token) (->' Syntax Syntax) (case' token (#Meta [_ (#Bool value)]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Bool"])) (_meta (#Bool value))))) + (wrap-meta ($form (list ($tag ["lux" "Bool"]) (_meta (#Bool value))))) (#Meta [_ (#Int value)]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Int"])) (_meta (#Int value))))) + (wrap-meta ($form (list ($tag ["lux" "Int"]) (_meta (#Int value))))) (#Meta [_ (#Real value)]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Real"])) (_meta (#Real value))))) + (wrap-meta ($form (list ($tag ["lux" "Real"]) (_meta (#Real value))))) (#Meta [_ (#Char value)]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Char"])) (_meta (#Char value))))) + (wrap-meta ($form (list ($tag ["lux" "Char"]) (_meta (#Char value))))) (#Meta [_ (#Text value)]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Text"])) (_meta (#Text value))))) + (wrap-meta ($form (list ($tag ["lux" "Text"]) (_meta (#Text value))))) (#Meta [_ (#Tag [module name])]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Tag"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name)))))))) + (wrap-meta ($form (list ($tag ["lux" "Tag"]) ($tuple (list (_meta (#Text module)) (_meta (#Text name))))))) (#Meta [_ (#Symbol [module name])]) - (wrap-meta ($form (list (_meta (#Tag ["lux" "Symbol"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name)))))))) + (wrap-meta ($form (list ($tag ["lux" "Symbol"]) ($tuple (list (_meta (#Text module)) (_meta (#Text name))))))) (#Meta [_ (#Tuple elems)]) (splice untemplate ($tag ["lux" "Tuple"]) elems) @@ -826,11 +836,12 @@ (splice untemplate ($tag ["lux" "Form"]) elems) (#Meta [_ (#Record fields)]) - (wrap-meta (_meta (#Record (map (:' (->' (#TupleT (list Text Syntax)) (#TupleT (list Text Syntax))) - (lambda [kv] - (let [[k v] kv] - [k (untemplate v)]))) - fields)))) + (wrap-meta ($form (list ($tag ["lux" "Record"]) + (untemplate-list (map (:' (->' (#TupleT (list Syntax Syntax)) Syntax) + (lambda [kv] + (let [[k v] kv] + ($tuple (list (untemplate k) (untemplate v)))))) + fields))))) )) (defmacro #export (` tokens) @@ -865,7 +876,8 @@ ## return) ## (: (All [a b] (-> (-> a (m b)) (m a) (m b))) ## bind)) -(def' Monad +(def Monad + Type (All' [m] (#RecordT (list ["lux;return" (All' [a] (->' (B' a) ($' (B' m) (B' a))))] ["lux;bind" (All' [a b] (->' (->' (B' a) ($' (B' m) (B' b))) @@ -901,62 +913,114 @@ (#Right [state' a]) (f a state'))))}) -## (defmacro #export (^ tokens) -## (case' tokens -## (#Cons [(#Meta [_ (#Symbol ["" class-name])]) #Nil]) -## (return (:' SyntaxList -## (list (` (#DataT (~ (_meta (#Text class-name)))))))) - -## _ -## (fail "Wrong syntax for ^"))) - -## (defmacro #export (-> tokens) -## (case' (reverse tokens) -## (#Cons [output inputs]) -## (return (:' SyntaxList -## (list (fold (:' (->' Syntax Syntax Syntax) -## (lambda [o i] -## (` (#;LambdaT [(~ i) (~ o)])))) -## output -## inputs)))) +(defmacro #export (^ tokens) + (case' tokens + (#Cons [(#Meta [_ (#Symbol ["" class-name])]) #Nil]) + (return (:' SyntaxList + (list (` (#DataT (~ (_meta (#Text class-name)))))))) + + _ + (fail "Wrong syntax for ^"))) + +(defmacro #export (-> tokens) + (case' (reverse tokens) + (#Cons [output inputs]) + (return (:' SyntaxList + (list (fold (:' (->' Syntax Syntax Syntax) + (lambda [o i] + (` (#;LambdaT [(~ i) (~ o)])))) + output + inputs)))) -## _ -## (fail "Wrong syntax for ->"))) - -## (defmacro #export (, tokens) -## (return (:' SyntaxList -## (list (` (#TupleT (list (~@ tokens)))))))) - -## (defmacro #export (| tokens) -## (do Lux:Monad -## [pairs (map% Lux:Monad -## (lambda [token] -## (case' token -## (#Tag ident) -## (;return (` [(~ ($text (ident->text ident))) (,)])) - -## (#Form (#Cons [(#Tag ident) (#Cons [value #Nil])])) -## (;return (` [(~ ($text (ident->text ident))) (~ value)])) + _ + (fail "Wrong syntax for ->"))) + +(defmacro #export (, tokens) + (return (:' SyntaxList + (list (` (#TupleT (list (~@ tokens)))))))) + +## (: (All [a b] +## (-> (-> a b a) a (List b) a)) +## fold) + +## (: (All [a] +## (-> (List a) (List a))) +## reverse) + +## (: (All [a] +## (-> (List a) (List (, a a)))) +## as-pairs) + +(defmacro (do tokens) + (case' tokens + (#Cons [monad (#Cons [(#Meta [_ (#Tuple bindings)]) (#Cons [body #Nil])])]) + (let [body' (fold (:' (-> Syntax (, Syntax Syntax) Syntax) + (lambda [body' binding] + (let [[var value] binding] + (` (;bind (lambda' (~ ($symbol ["" ""])) + (~ var) + (~ body')) + (~ value)))))) + body + (reverse (as-pairs bindings)))] + (return (:' SyntaxList + (list (` (case' (~ monad) + {#;return ;return #;bind ;bind} + (~ body'))))))) + + _ + (fail "Wrong syntax for do"))) + +(def (map% m f xs) + ## (All [m a b] + ## (-> (Monad m) (-> a (m b)) (List a) (m (List b)))) + (All' [m a b] + (-> ($' Monad (B' m)) + (-> (B' a) ($' (B' m) (B' b))) + ($' List (B' a)) + ($' (B' m) ($' List (B' b))))) + (let [{#;return ;return #;bind ;bind} m] + (case' xs + #Nil + (;return #Nil) + + (#Cons [x xs']) + (do m + [y (f x) + ys (map% m f xs')] + (;return (#Cons [y ys]))) + ))) + +(defmacro #export (| tokens) + (do Lux:Monad + [pairs (map% Lux:Monad + (lambda [token] + (case' token + (#Tag ident) + (;return (` [(~ ($text (ident->text ident))) (,)])) + + (#Form (#Cons [(#Tag ident) (#Cons [value #Nil])])) + (;return (` [(~ ($text (ident->text ident))) (~ value)])) -## _ -## (fail "Wrong syntax for |"))) -## tokens)] -## (` (#VariantT (list (~@ pairs)))))) - -## (defmacro #export (& tokens) -## (if (not (int:= 2 (length tokens))) -## (fail "& expects an even number of arguments.") -## (do Lux:Monad -## [pairs (map% Lux:Monad -## (lambda [pair] -## (case' pair -## [(#Tag ident) value] -## (;return (` [(~ ($text (ident->text ident))) (~ value)])) + _ + (fail "Wrong syntax for |"))) + tokens)] + (` (#VariantT (list (~@ pairs)))))) + +(defmacro #export (& tokens) + (if (not (int:= 2 (length tokens))) + (fail "& expects an even number of arguments.") + (do Lux:Monad + [pairs (map% Lux:Monad + (lambda [pair] + (case' pair + [(#Tag ident) value] + (;return (` [(~ ($text (ident->text ident))) (~ value)])) -## _ -## (fail "Wrong syntax for &"))) -## (as-pairs tokens))] -## (` (#RecordT (list (~@ pairs))))))) + _ + (fail "Wrong syntax for &"))) + (as-pairs tokens))] + (` (#RecordT (list (~@ pairs))))))) ## (defmacro #export (All tokens) ## (case' (:' (, Ident SyntaxList) @@ -1002,38 +1066,6 @@ ## (let [[module name] ident] ## ($ text:++ module ";" name))) -## (def (map% monad f xs) -## (All' [m a b] -## (->' ($' Monad (B' m)) -## (->' (B' a) ($' (B' m) (B' b))) -## ($' (B' m) ($' List (B' b))))) -## (let [{#;return ;return #;bind ;bind} monad] -## (case' xs -## #Nil -## (;return #Nil) - -## (#Cons [x xs']) -## (do monad -## [x' (f x) -## xs'' (map% monad f xs')] -## (;return (#Cons [x' xs''])))))) - -## (defmacro (do tokens) -## (case' tokens -## (#Cons [monad (#Cons [(#Meta [_ (#Tuple bindings)]) (#Cons [body #Nil])])]) -## (return (:' SyntaxList -## (list (` (case' (~ monad) -## {#;return ;return #;bind ;bind} -## (~ (fold (:' (-> Syntax (, Syntax Syntax) Syntax) -## (lambda [body' binding] -## (let [[lhs rhs] binding] -## (` (;bind (lambda [(~ lhs)] (~ body')) (~ rhs)))))) -## body -## (reverse (as-pairs bindings))))))))) - -## _ -## (fail "Wrong syntax for do"))) - ## (def #export (find-macro ident state) ## (->' Ident ($' Lux Macro)) ## (let [[module name] ident] @@ -1066,10 +1098,6 @@ ## ## (jvm-invokevirtual java.lang.Object "equals" [java.lang.Object] ## ## x [y])) -## ## (def #export (int:+ x y) -## ## (-> Int Int Int) -## ## (jvm-ladd x y)) - ## ## (def (replace-ident ident value syntax) ## ## (-> (, Text Text) Syntax Syntax Syntax) ## ## (let [[module name] ident] @@ -1201,8 +1229,6 @@ ## ## _ ## ## (fail "Wrong syntax for :!"))) - - ## ## (def (print x) ## ## (-> (^ java.lang.Object) []) ## ## (jvm-invokevirtual java.io.PrintStream "print" [java.lang.Object] @@ -1227,16 +1253,6 @@ ## ## (lambda [x] ## ## (f (g x)))) -## ## (def (++ xs ys) -## ## (All [a] -## ## (-> (List a) (List a) (List a))) -## ## (case' xs -## ## #Nil -## ## ys - -## ## (#Cons [x xs']) -## ## (#Cons [x (++ xs' ys)]))) - ## ## (def concat ## ## (All [a] ## ## (-> (List (List a)) (List a))) @@ -1314,26 +1330,18 @@ ## ## true false ## ## false true)) -## ## (defmacro (|> tokens) -## ## (case' tokens -## ## (#Cons [init apps]) -## ## (return (list (fold (lambda [acc app] -## ## (case' app -## ## (#Form parts) -## ## (#Form (++ parts (list acc))) - -## ## _ -## ## (` ((~ app) (~ acc))))) -## ## init -## ## apps))))) - -## ## (defmacro ($ tokens) -## ## (case' tokens -## ## (#Cons [op (#Cons [init args])]) -## ## (return (list (fold (lambda [acc elem] -## ## (` ((~ op) (~ acc) (~ elem)))) -## ## init -## ## args))))) +## (defmacro (|> tokens) +## (case' tokens +## (#Cons [init apps]) +## (return (list (fold (lambda [acc app] +## (case' app +## (#Form parts) +## (#Form (++ parts (list acc))) + +## _ +## (` ((~ app) (~ acc))))) +## init +## apps))))) ## ## (def (const x) ## ## (All [a b] @@ -1666,30 +1674,6 @@ ## ## ($ text-++ "(" (fold text-++ "" (interpose " " (map show-syntax members))) ")") ## ## )) -## ## (defmacro (do tokens) -## ## (case' tokens -## ## (#Cons [(#Meta [_ monad]) (#Cons [(#Meta [_ (#Tuple bindings)]) (#Cons [body #Nil])])]) -## ## (let [output (fold (lambda [body binding] -## ## (case' binding -## ## [lhs rhs] -## ## (` (lux;bind (lambda [(~ lhs)] (~ body)) -## ## (~ rhs))))) -## ## body -## ## (reverse (as-pairs bindings)))] -## ## (return (list (` (using (~ monad) (~ output)))))))) - -## ## (def (map% f xs) -## ## (All [m a b] -## ## (-> (-> a (m b)) (List a) (m (List b)))) -## ## (case' xs -## ## #Nil -## ## (return xs) - -## ## (#Cons [x xs']) -## ## (do [y (f x) -## ## ys (map% f xs')] -## ## (return (#Cons [y ys]))))) - ## ## ## (defmacro ($keys tokens) ## ## ## (case' tokens ## ## ## (#Cons [(#Meta [_ (#Tuple fields)]) #Nil]) diff --git a/src/lux/type.clj b/src/lux/type.clj index 73b244569..684ff374d 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -114,7 +114,7 @@ (&/T "lux;Tag" Ident) (&/T "lux;Form" Syntax*List) (&/T "lux;Tuple" Syntax*List) - (&/T "lux;Record" (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Syntax*)))))) + (&/T "lux;Record" (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Syntax* Syntax*)))))) )))) (def Syntax @@ -141,14 +141,7 @@ (if-let [type (->> state (&/get$ &/$TYPES) (&/get$ &/$MAPPINGS) (&/|get id))] (matchv ::M/objects [type] [["lux;Some" type*]] - (matchv ::M/objects [type*] - [["lux;VarT" ?id]] - (&/run-state (&/try-all% (&/|list (bound? ?id) - (return false))) - state) - - [_] - (return* state true)) + (return* state true) [["lux;None" _]] (return* state false)) @@ -222,8 +215,7 @@ (matchv ::M/objects [type] [["lux;VarT" ?id]] (if (= ?tid ?id) - (|do [=type (deref ?id)] - (clean* ?tid =type)) + (deref ?id) (return type)) [["lux;LambdaT" [?arg ?return]]] @@ -514,12 +506,36 @@ [["lux;VarT" ?eid] ["lux;VarT" ?aid]] (if (= ?eid ?aid) (return (&/T fixpoints nil)) - (&/try-all% (&/|list (|do [ebound (deref ?eid)] - (check* fixpoints ebound actual)) - (|do [abound (deref ?aid)] - (check* fixpoints expected abound)) - (|do [_ (set-var ?eid actual)] - (return (&/T fixpoints nil)))))) + ;; (&/try-all% (&/|list (|do [ebound (deref ?eid)] + ;; (check* fixpoints ebound actual)) + ;; (|do [abound (deref ?aid)] + ;; (check* fixpoints expected abound)) + ;; (|do [_ (set-var ?eid actual)] + ;; (return (&/T fixpoints nil))))) + (|do [ebound (&/try-all% (&/|list (|do [ebound (deref ?eid)] + (return (&/V "lux;Some" ebound))) + (return (&/V "lux;None" nil)))) + abound (&/try-all% (&/|list (|do [abound (deref ?aid)] + (return (&/V "lux;Some" abound))) + (return (&/V "lux;None" nil))))] + (matchv ::M/objects [ebound abound] + [["lux;None" _] ["lux;None" _]] + (|do [_ (set-var ?eid actual)] + (return (&/T fixpoints nil))) + + [["lux;Some" etype] ["lux;None" _]] + (check* fixpoints etype actual) + ;; (|do [_ (set-var ?aid etype)] + ;; (return (&/T fixpoints nil))) + + [["lux;None" _] ["lux;Some" atype]] + (check* fixpoints expected atype) + ;; (|do [_ (set-var ?eid atype)] + ;; (return (&/T fixpoints nil))) + + [["lux;Some" etype] ["lux;Some" atype]] + (check* fixpoints etype atype))) + ) [["lux;VarT" ?id] _] (&/try-all% (&/|list (|do [_ (set-var ?id actual)] -- cgit v1.2.3