diff options
author | Eduardo Julian | 2015-08-28 22:46:12 -0400 |
---|---|---|
committer | Eduardo Julian | 2015-08-28 22:46:12 -0400 |
commit | 8de225f98aaed212bf3b683208bff5c6ab85a835 (patch) | |
tree | f9a3e197c7bf62cffa411f5a9e768cbca6a76d9b /source | |
parent | a10d922283a9256f0f0015d9d00a0c549b1891cb (diff) |
- Changed the name of AllT (for-all type) to UnivQ (universal quantification).
- UnivQ no longer stores the environment as key-val pairs with Text names, but instead stores it as type-lists with variables accessed via an index through a (updated) BoundT.
- UnivQ no longer stores the name of the type-fun, not the name of the type-arg.
Diffstat (limited to '')
-rw-r--r-- | source/lux.lux | 882 | ||||
-rw-r--r-- | source/lux/codata/stream.lux | 8 |
2 files changed, 460 insertions, 430 deletions
diff --git a/source/lux.lux b/source/lux.lux index 815f95c69..d96b18fcb 100644 --- a/source/lux.lux +++ b/source/lux.lux @@ -45,12 +45,12 @@ ## (#Cons a (List a)))) (_lux_def List (9 ["lux" "List"] - (7 (0) "lux;List" "a" + (7 (0) (1 (1 ## "lux;Nil" (2 (0)) (1 ## "lux;Cons" - (2 (1 (4 "a") - (1 (8 (4 "lux;List") (4 "a")) + (2 (1 (4 1) + (1 (8 (4 0) (4 1)) (0)))) (0))))))) (_lux_export List) @@ -61,11 +61,11 @@ ## (1 a))) (_lux_def Maybe (9 ["lux" "Maybe"] - (7 (0) "lux;Maybe" "a" + (7 (0) (1 (1 ## "lux;None" (2 (0)) (1 ## "lux;Some" - (4 "a") + (4 1) (0))))))) (_lux_export Maybe) (_lux_declare-tags [#None #Some] Maybe) @@ -75,61 +75,59 @@ ## (#VariantT (List Type)) ## (#TupleT (List Type)) ## (#LambdaT Type Type) -## (#BoundT Text) +## (#BoundT Int) ## (#VarT Int) -## (#AllT (List (, Text Type)) Text Text Type) +## (#UnivQ (List Type) Type) ## (#AppT Type Type) ## (#NamedT Ident Type) ## )) (_lux_def Type (9 ["lux" "Type"] - (_lux_case (8 (4 "Type") (4 "_")) + (_lux_case (8 (4 0) (4 1)) Type - (_lux_case (8 List (2 (1 Text (1 Type (0))))) - TypeEnv - (_lux_case (8 List Type) - TypeList - (8 (7 (0) "Type" "_" - (1 (1 ## "lux;DataT" - Text - (1 ## "lux;VariantT" - TypeList - (1 ## "lux;TupleT" - TypeList - (1 ## "lux;LambdaT" - (2 (1 Type (1 Type (0)))) - (1 ## "lux;BoundT" - Text - (1 ## "lux;VarT" - Int - (1 ## "lux;ExT" - Int - (1 ## "lux;AllT" - (2 (1 TypeEnv (1 Text (1 Text (1 Type (0)))))) - (1 ## "lux;AppT" - (2 (1 Type (1 Type (0)))) - (1 ## "lux;NamedT" - (2 (1 Ident (1 Type (0)))) - (0))))))))))))) - Void)))))) + (_lux_case (8 List Type) + TypeList + (8 (7 (0) + (1 (1 ## "lux;DataT" + Text + (1 ## "lux;VariantT" + TypeList + (1 ## "lux;TupleT" + TypeList + (1 ## "lux;LambdaT" + (2 (1 Type (1 Type (0)))) + (1 ## "lux;BoundT" + Int + (1 ## "lux;VarT" + Int + (1 ## "lux;ExT" + 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))))) (_lux_export Type) -(_lux_declare-tags [#DataT #VariantT #TupleT #LambdaT #BoundT #VarT #ExT #AllT #AppT #NamedT] Type) +(_lux_declare-tags [#DataT #VariantT #TupleT #LambdaT #BoundT #VarT #ExT #UnivQ #AppT #NamedT] Type) ## (deftype (Bindings k v) ## (& #counter Int ## #mappings (List (, k v)))) (_lux_def Bindings (#NamedT ["lux" "Bindings"] - (#AllT [#Nil "lux;Bindings" "k" - (#AllT [#None "" "v" + (#UnivQ #Nil + (#UnivQ #Nil (#TupleT (#Cons ## "lux;counter" Int (#Cons ## "lux;mappings" - (#AppT [List - (#TupleT (#Cons [(#BoundT "k") - (#Cons [(#BoundT "v") - #Nil])]))]) - #Nil)))])]))) + (#AppT List + (#TupleT (#Cons (#BoundT 3) + (#Cons (#BoundT 1) + #Nil)))) + #Nil))))))) (_lux_export Bindings) (_lux_declare-tags [#counter #mappings] Bindings) @@ -140,19 +138,19 @@ ## #closure (Bindings k v))) (_lux_def Env (#NamedT ["lux" "Env"] - (#AllT #Nil "lux;Env" "k" - (#AllT #None "" "v" - (#TupleT (#Cons ## "lux;name" - Text - (#Cons ## "lux;inner-closures" - Int - (#Cons ## "lux;locals" - (#AppT (#AppT Bindings (#BoundT "k")) - (#BoundT "v")) - (#Cons ## "lux;closure" - (#AppT (#AppT Bindings (#BoundT "k")) - (#BoundT "v")) - #Nil))))))))) + (#UnivQ #Nil + (#UnivQ #Nil + (#TupleT (#Cons ## "lux;name" + Text + (#Cons ## "lux;inner-closures" + Int + (#Cons ## "lux;locals" + (#AppT (#AppT Bindings (#BoundT 3)) + (#BoundT 1)) + (#Cons ## "lux;closure" + (#AppT (#AppT Bindings (#BoundT 3)) + (#BoundT 1)) + #Nil))))))))) (_lux_export Env) (_lux_declare-tags [#name #inner-closures #locals #closure] Env) @@ -167,13 +165,13 @@ ## (| (#Meta m v))) (_lux_def Meta (#NamedT ["lux" "Meta"] - (#AllT #Nil "lux;Meta" "m" - (#AllT #None "" "v" - (#VariantT (#Cons ## "lux;Meta" - (#TupleT (#Cons (#BoundT "m") - (#Cons (#BoundT "v") - #Nil))) - #Nil)))))) + (#UnivQ #Nil + (#UnivQ #Nil + (#VariantT (#Cons ## "lux;Meta" + (#TupleT (#Cons (#BoundT 3) + (#Cons (#BoundT 1) + #Nil))) + #Nil)))))) (_lux_export Meta) (_lux_declare-tags [#Meta] Meta) @@ -190,36 +188,36 @@ ## (#RecordS (List (, (w (AST' w)) (w (AST' w))))))) (_lux_def AST' (#NamedT ["lux" "AST'"] - (_lux_case (#AppT (#BoundT "w") - (#AppT (#BoundT "lux;AST'") - (#BoundT "w"))) + (_lux_case (#AppT (#BoundT 1) + (#AppT (#BoundT 0) + (#BoundT 1))) AST (_lux_case (#AppT [List AST]) ASTList - (#AllT #Nil "lux;AST'" "w" - (#VariantT (#Cons ## "lux;BoolS" - Bool - (#Cons ## "lux;IntS" - Int - (#Cons ## "lux;RealS" - Real - (#Cons ## "lux;CharS" - Char - (#Cons ## "lux;TextS" - Text - (#Cons ## "lux;SymbolS" - Ident - (#Cons ## "lux;TagS" + (#UnivQ #Nil + (#VariantT (#Cons ## "lux;BoolS" + Bool + (#Cons ## "lux;IntS" + Int + (#Cons ## "lux;RealS" + Real + (#Cons ## "lux;CharS" + Char + (#Cons ## "lux;TextS" + Text + (#Cons ## "lux;SymbolS" Ident - (#Cons ## "lux;FormS" - ASTList - (#Cons ## "lux;TupleS" + (#Cons ## "lux;TagS" + Ident + (#Cons ## "lux;FormS" ASTList - (#Cons ## "lux;RecordS" - (#AppT List (#TupleT (#Cons AST (#Cons AST #Nil)))) - #Nil) - ))))))))) - )))))) + (#Cons ## "lux;TupleS" + ASTList + (#Cons ## "lux;RecordS" + (#AppT List (#TupleT (#Cons AST (#Cons AST #Nil)))) + #Nil) + ))))))))) + )))))) (_lux_export AST') (_lux_declare-tags [#BoolS #IntS #RealS #CharS #TextS #SymbolS #TagS #FormS #TupleS #RecordS] AST') @@ -239,26 +237,26 @@ ## (#Right r))) (_lux_def Either (#NamedT ["lux" "Either"] - (#AllT #Nil "lux;Either" "l" - (#AllT #None "" "r" - (#VariantT (#Cons ## "lux;Left" - (#BoundT "l") - (#Cons ## "lux;Right" - (#BoundT "r") - #Nil))))))) + (#UnivQ #Nil + (#UnivQ #Nil + (#VariantT (#Cons ## "lux;Left" + (#BoundT 3) + (#Cons ## "lux;Right" + (#BoundT 1) + #Nil))))))) (_lux_export Either) (_lux_declare-tags [#Left #Right] Either) ## (deftype (StateE s a) ## (-> s (Either Text (, s a)))) (_lux_def StateE - (#AllT [#Nil "lux;StateE" "s" - (#AllT [#None "" "a" - (#LambdaT [(#BoundT "s") - (#AppT [(#AppT [Either Text]) - (#TupleT (#Cons [(#BoundT "s") - (#Cons [(#BoundT "a") - #Nil])]))])])])])) + (#UnivQ #Nil + (#UnivQ #Nil + (#LambdaT (#BoundT 3) + (#AppT (#AppT Either Text) + (#TupleT (#Cons (#BoundT 3) + (#Cons (#BoundT 1) + #Nil)))))))) ## (deftype Source ## (List (Meta Cursor Text))) @@ -291,18 +289,16 @@ ## (#AliasD Ident))) (_lux_def DefData' (#NamedT ["lux" "DefData'"] - (#AllT [#Nil "lux;DefData'" "" - (#VariantT (#Cons [## "lux;ValueD" - (#TupleT (#Cons [Type - (#Cons [Unit - #Nil])])) - (#Cons [## "lux;TypeD" - Type - (#Cons [## "lux;MacroD" - (#BoundT "") - (#Cons [## "lux;AliasD" - Ident - #Nil])])])]))]))) + (#UnivQ #Nil + (#VariantT (#Cons ## "lux;ValueD" + (#TupleT (#Cons Type (#Cons Unit #Nil))) + (#Cons ## "lux;TypeD" + Type + (#Cons ## "lux;MacroD" + (#BoundT 1) + (#Cons ## "lux;AliasD" + Ident + #Nil)))))))) (_lux_export DefData') (_lux_declare-tags [#ValueD #TypeD #MacroD #AliasD] DefData') @@ -328,34 +324,34 @@ ## )) (_lux_def Module (#NamedT ["lux" "Module"] - (#AllT [#Nil "lux;Module" "Compiler" - (#TupleT (#Cons [## "lux;module-aliases" - (#AppT [List (#TupleT (#Cons [Text (#Cons [Text #Nil])]))]) - (#Cons [## "lux;defs" - (#AppT [List (#TupleT (#Cons [Text - (#Cons [(#TupleT (#Cons [Bool (#Cons [(#AppT [DefData' (#LambdaT [ASTList - (#AppT [(#AppT [StateE (#BoundT "Compiler")]) - ASTList])])]) - #Nil])])) - #Nil])]))]) - (#Cons [## "lux;imports" - (#AppT [List Text]) - (#Cons [## "lux;tags" - (#AppT [List - (#TupleT (#Cons Text - (#Cons (#TupleT (#Cons Int - (#Cons (#AppT [List Ident]) - (#Cons Type - #Nil)))) - #Nil)))]) - (#Cons [## "lux;types" - (#AppT [List - (#TupleT (#Cons Text - (#Cons (#TupleT (#Cons (#AppT [List Ident]) - (#Cons Type - #Nil))) - #Nil)))]) - #Nil])])])])]))]))) + (#UnivQ #Nil + (#TupleT (#Cons ## "lux;module-aliases" + (#AppT List (#TupleT (#Cons Text (#Cons Text #Nil)))) + (#Cons ## "lux;defs" + (#AppT List (#TupleT (#Cons Text + (#Cons (#TupleT (#Cons Bool (#Cons (#AppT DefData' (#LambdaT ASTList + (#AppT (#AppT StateE (#BoundT 1)) + ASTList))) + #Nil))) + #Nil)))) + (#Cons ## "lux;imports" + (#AppT List Text) + (#Cons ## "lux;tags" + (#AppT List + (#TupleT (#Cons Text + (#Cons (#TupleT (#Cons Int + (#Cons (#AppT List Ident) + (#Cons Type + #Nil)))) + #Nil)))) + (#Cons ## "lux;types" + (#AppT List + (#TupleT (#Cons Text + (#Cons (#TupleT (#Cons (#AppT List Ident) + (#Cons Type + #Nil))) + #Nil)))) + #Nil))))))))) (_lux_export Module) (_lux_declare-tags [#module-aliases #defs #imports #tags #types] Module) @@ -372,30 +368,30 @@ ## )) (_lux_def Compiler (#NamedT ["lux" "Compiler"] - (#AppT [(#AllT [#Nil "lux;Compiler" "" - (#TupleT (#Cons [## "lux;source" - Source - (#Cons [## "lux;cursor" - Cursor - (#Cons [## "lux;modules" - (#AppT [List (#TupleT (#Cons [Text - (#Cons [(#AppT [Module (#AppT [(#BoundT "lux;Compiler") (#BoundT "")])]) - #Nil])]))]) - (#Cons [## "lux;envs" - (#AppT [List (#AppT [(#AppT [Env Text]) - (#TupleT (#Cons [LuxVar (#Cons [Type #Nil])]))])]) - (#Cons [## "lux;type-vars" - (#AppT [(#AppT [Bindings Int]) Type]) - (#Cons [## "lux;expected" - Type - (#Cons [## "lux;seed" - Int - (#Cons [## "lux;eval?" - Bool - (#Cons [## "lux;host" - Host - #Nil])])])])])])])])]))]) - Void]))) + (#AppT (#UnivQ #Nil + (#TupleT (#Cons ## "lux;source" + Source + (#Cons ## "lux;cursor" + Cursor + (#Cons ## "lux;modules" + (#AppT List (#TupleT (#Cons Text + (#Cons (#AppT Module (#AppT (#BoundT 0) (#BoundT 1))) + #Nil)))) + (#Cons ## "lux;envs" + (#AppT List (#AppT (#AppT Env Text) + (#TupleT (#Cons LuxVar (#Cons Type #Nil))))) + (#Cons ## "lux;type-vars" + (#AppT (#AppT Bindings Int) Type) + (#Cons ## "lux;expected" + Type + (#Cons ## "lux;seed" + Int + (#Cons ## "lux;eval?" + Bool + (#Cons ## "lux;host" + Host + #Nil))))))))))) + Void))) (_lux_export Compiler) (_lux_declare-tags [#source #cursor #modules #envs #type-vars #expected #seed #eval? #host] Compiler) @@ -431,13 +427,13 @@ ## (Either Text (, Compiler a)))) ## ...) (_lux_def return - (_lux_: (#AllT #Nil "" "a" - (#LambdaT (#BoundT "a") - (#LambdaT Compiler - (#AppT (#AppT Either Text) - (#TupleT (#Cons Compiler - (#Cons (#BoundT "a") - #Nil))))))) + (_lux_: (#UnivQ #Nil + (#LambdaT (#BoundT 1) + (#LambdaT Compiler + (#AppT (#AppT Either Text) + (#TupleT (#Cons Compiler + (#Cons (#BoundT 1) + #Nil))))))) (_lux_lambda _ val (_lux_lambda _ state (#Right state val))))) @@ -448,27 +444,42 @@ ## (Either Text (, Compiler a)))) ## ...) (_lux_def fail - (_lux_: (#AllT #Nil "" "a" - (#LambdaT Text - (#LambdaT Compiler - (#AppT (#AppT Either Text) - (#TupleT (#Cons Compiler - (#Cons (#BoundT "a") - #Nil))))))) + (_lux_: (#UnivQ #Nil + (#LambdaT Text + (#LambdaT Compiler + (#AppT (#AppT Either Text) + (#TupleT (#Cons Compiler + (#Cons (#BoundT 1) + #Nil))))))) (_lux_lambda _ msg (_lux_lambda _ state (#Left msg))))) -(_lux_def text$ - (_lux_: (#LambdaT Text AST) - (_lux_lambda _ text - (_meta (#TextS text))))) +(_lux_def bool$ + (_lux_: (#LambdaT Bool AST) + (_lux_lambda _ value + (_meta (#BoolS value))))) (_lux_def int$ (_lux_: (#LambdaT Int AST) (_lux_lambda _ value (_meta (#IntS value))))) +(_lux_def real$ + (_lux_: (#LambdaT Real AST) + (_lux_lambda _ value + (_meta (#RealS value))))) + +(_lux_def char$ + (_lux_: (#LambdaT Char AST) + (_lux_lambda _ value + (_meta (#CharS value))))) + +(_lux_def text$ + (_lux_: (#LambdaT Text AST) + (_lux_lambda _ text + (_meta (#TextS text))))) + (_lux_def symbol$ (_lux_: (#LambdaT Ident AST) (_lux_lambda _ ident @@ -542,7 +553,7 @@ #Nil)) _ - (fail "Wrong syntax for lambda"))))) + (fail "Wrong syntax for lambda''"))))) (_lux_declare-macro lambda'') (_lux_def def'' @@ -601,7 +612,7 @@ #Nil])) _ - (fail "Wrong syntax for def")) + (fail "Wrong syntax for def''")) ))) (_lux_declare-macro def'') @@ -638,82 +649,179 @@ (defmacro (->' tokens) (_lux_case tokens - (#Cons [input (#Cons [output #Nil])]) - (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "LambdaT"])) - (#Cons [(_meta (#TupleS (#Cons [input (#Cons [output #Nil])]))) - #Nil])]))) - #Nil])) - - (#Cons [input (#Cons [output others])]) - (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "LambdaT"])) - (#Cons [(_meta (#TupleS (#Cons [input - (#Cons [(_meta (#FormS (#Cons [(_meta (#SymbolS ["lux" "->'"])) - (#Cons [output others])]))) - #Nil])]))) - #Nil])]))) - #Nil])) + (#Cons input (#Cons output #Nil)) + (return (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "LambdaT"]) + (#Cons (_meta (#TupleS (#Cons input (#Cons output #Nil)))) + #Nil)))) + #Nil)) + + (#Cons input (#Cons output others)) + (return (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "LambdaT"]) + (#Cons (_meta (#TupleS (#Cons input + (#Cons (_meta (#FormS (#Cons (symbol$ ["lux" "->'"]) + (#Cons output others)))) + #Nil)))) + #Nil)))) + #Nil)) _ (fail "Wrong syntax for ->'"))) -(defmacro (All' tokens) +(defmacro ($' tokens) (_lux_case tokens - (#Cons [(#Meta [_ (#TupleS #Nil)]) - (#Cons [body #Nil])]) - (return (#Cons [body - #Nil])) - - (#Cons [(#Meta [_ (#TupleS (#Cons [(#Meta [_ (#SymbolS ["" arg-name])]) other-args]))]) - (#Cons [body #Nil])]) - (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "AllT"])) - (#Cons [(_meta (#TupleS (#Cons [(_meta (#TagS ["lux" "None"])) - (#Cons [(_meta (#TextS "")) - (#Cons [(_meta (#TextS arg-name)) - (#Cons [(_meta (#FormS (#Cons [(_meta (#SymbolS ["lux" "All'"])) - (#Cons [(_meta (#TupleS other-args)) - (#Cons [body - #Nil])])]))) - #Nil])])])]))) - #Nil])]))) - #Nil])) + (#Cons x #Nil) + (return tokens) + + (#Cons x (#Cons y xs)) + (return (#Cons (_meta (#FormS (#Cons (symbol$ ["lux" "$'"]) + (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "AppT"]) + (#Cons x (#Cons y #Nil))))) + xs)))) + #Nil)) _ - (fail "Wrong syntax for All'"))) + (fail "Wrong syntax for $'"))) -(defmacro (B' tokens) - (_lux_case tokens - (#Cons [(#Meta [_ (#SymbolS ["" bound-name])]) - #Nil]) - (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "BoundT"])) - (#Cons [(_meta (#TextS bound-name)) - #Nil])]))) - #Nil])) +(def'' (map f xs) + (#UnivQ #Nil + (#UnivQ #Nil + (->' (->' (#BoundT 3) (#BoundT 1)) ($' List (#BoundT 3)) ($' List (#BoundT 1))))) + (_lux_case xs + #Nil + #Nil + + (#Cons x xs') + (#Cons (f x) (map f xs')))) + +(def'' RepEnv + Type + ($' List (#TupleT (#Cons Text (#Cons AST #Nil))))) + +(def'' (make-env xs ys) + (->' ($' List Text) ($' List AST) RepEnv) + (_lux_case (_lux_: (#TupleT (#Cons ($' List Text) (#Cons ($' List AST) #Nil))) + [xs ys]) + [(#Cons x xs') (#Cons y ys')] + (#Cons [x y] (make-env xs' ys')) _ - (fail "Wrong syntax for B'"))) + #Nil)) -(defmacro ($' tokens) - (_lux_case tokens - (#Cons [x #Nil]) - (return tokens) +(def'' (text:= x y) + (->' Text Text Bool) + (_jvm_invokevirtual "java.lang.Object" "equals" ["java.lang.Object"] + x [y])) + +(def'' (get-rep key env) + (->' Text RepEnv ($' Maybe AST)) + (_lux_case env + #Nil + #None + + (#Cons [k v] env') + (_lux_case (text:= k key) + true + (#Some v) + + false + (get-rep key env')))) + +(def'' (replace-syntax reps syntax) + (->' RepEnv AST AST) + (_lux_case syntax + (#Meta _ (#SymbolS "" name)) + (_lux_case (get-rep name reps) + (#Some replacement) + replacement + + #None + syntax) + + (#Meta _ (#FormS parts)) + (#Meta _ (#FormS (map (replace-syntax reps) parts))) - (#Cons [x (#Cons [y xs])]) - (return (#Cons [(_meta (#FormS (#Cons [(_meta (#SymbolS ["lux" "$'"])) - (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "AppT"])) - (#Cons [(_meta (#TupleS (#Cons [x (#Cons [y #Nil])]))) - #Nil])]))) - xs])]))) - #Nil])) + (#Meta _ (#TupleS members)) + (#Meta _ (#TupleS (map (replace-syntax reps) members))) + (#Meta _ (#RecordS slots)) + (#Meta _ (#RecordS (map (_lux_: (->' (#TupleT (#Cons AST (#Cons AST #Nil))) (#TupleT (#Cons AST (#Cons AST #Nil)))) + (lambda'' [slot] + (_lux_case slot + [k v] + [(replace-syntax reps k) (replace-syntax reps v)]))) + slots))) + _ - (fail "Wrong syntax for $'"))) + syntax) + ) + +(def'' (update-bounds ast) + (->' AST AST) + (_lux_case ast + (#Meta _ (#BoolS value)) + (bool$ value) + + (#Meta _ (#IntS value)) + (int$ value) + + (#Meta _ (#RealS value)) + (real$ value) + + (#Meta _ (#CharS value)) + (char$ value) + + (#Meta _ (#TextS value)) + (text$ value) + + (#Meta _ (#SymbolS value)) + (symbol$ value) + + (#Meta _ (#TagS value)) + (tag$ value) + + (#Meta _ (#TupleS members)) + (tuple$ (map update-bounds members)) + + (#Meta _ (#RecordS pairs)) + (record$ (map (_lux_: (->' (#TupleT (#Cons AST (#Cons AST #Nil))) (#TupleT (#Cons AST (#Cons AST #Nil)))) + (lambda'' [pair] + (let'' [name val] pair + [name (update-bounds val)]))) + pairs)) + + (#Meta _ (#FormS (#Cons (#Meta _ (#TagS "lux" "BoundT")) (#Cons (#Meta _ (#IntS idx)) #Nil)))) + (form$ (#Cons (tag$ ["lux" "BoundT"]) (#Cons (int$ (_jvm_ladd 2 idx)) #Nil))) + + (#Meta _ (#FormS members)) + (form$ (map update-bounds members))) + ) + +(defmacro (All' tokens) + (_lux_case tokens + (#Cons (#Meta _ (#TupleS (#Cons (#Meta _ (#SymbolS "" arg-name)) other-args))) + (#Cons body #Nil)) + (let'' bound-var (_meta (#FormS (#Cons (tag$ ["lux" "BoundT"]) (#Cons (int$ 1) #Nil)))) + (let'' body' (replace-syntax (#Cons [arg-name bound-var] #Nil) + (update-bounds body)) + (return (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "UnivQ"]) + (#Cons (tag$ ["lux" "Nil"]) + (#Cons (_lux_case other-args + #Nil + body' + + _ + (_meta (#FormS (#Cons (symbol$ ["lux" "All'"]) + (#Cons (_meta (#TupleS other-args)) + (#Cons body' + #Nil)))))) + #Nil))))) + #Nil)))) + + _ + (fail "Wrong syntax for All'"))) (def'' (foldL f init xs) - (All' [a b] - (->' (->' (B' a) (B' b) (B' a)) - (B' a) - ($' List (B' b)) - (B' a))) + (All' [a b] (->' (->' a b a) a ($' List b) a)) (_lux_case xs #Nil init @@ -722,8 +830,7 @@ (foldL f (f init x) xs'))) (def'' (reverse list) - (All' [a] - (->' ($' List (B' a)) ($' List (B' a)))) + (All' [a] (->' ($' List a) ($' List a))) (foldL (lambda'' [tail head] (#Cons head tail)) #Nil list)) @@ -822,8 +929,7 @@ )) (def''' (as-pairs xs) - (All' [a] - (->' ($' List (B' a)) ($' List (#TupleT (list (B' a) (B' a)))))) + (All' [a] (->' ($' List a) ($' List (#TupleT (list a a))))) (_lux_case xs (#Cons [x (#Cons [y xs'])]) (#Cons [[x y] (as-pairs xs')]) @@ -846,24 +952,14 @@ _ (fail "Wrong syntax for let'"))) -(def''' (map f xs) - (All' [a b] - (->' (->' (B' a) (B' b)) ($' List (B' a)) ($' List (B' b)))) - (_lux_case xs - #Nil - #Nil - - (#Cons [x xs']) - (#Cons [(f x) (map f xs')]))) - (def''' (any? p xs) (All' [a] - (->' (->' (B' a) Bool) ($' List (B' a)) Bool)) + (->' (->' a Bool) ($' List a) Bool)) (_lux_case xs #Nil false - (#Cons [x xs']) + (#Cons x xs') (_lux_case (p x) true true false (any? p xs')))) @@ -894,17 +990,17 @@ (_meta (#TupleS (list token (untemplate-list tokens'))))))))) (def''' #export (list:++ xs ys) - (All' [a] (->' ($' List (B' a)) ($' List (B' a)) ($' List (B' a)))) + (All' [a] (->' ($' List a) ($' List a) ($' List a))) (_lux_case xs - (#Cons [x xs']) - (#Cons [x (list:++ xs' ys)]) + (#Cons x xs') + (#Cons x (list:++ xs' ys)) #Nil ys)) (defmacro #export ($ tokens) (_lux_case tokens - (#Cons [op (#Cons [init args])]) + (#Cons op (#Cons init args)) (return (list (foldL (lambda' [a1 a2] (form$ (list op a1 a2))) init args))) @@ -1044,7 +1140,7 @@ (def''' #export Lux Type (All' [a] - (->' Compiler ($' Either Text (#TupleT (list Compiler (B' a))))))) + (->' Compiler ($' Either Text (#TupleT (list Compiler a)))))) ## (defsig (Monad m) ## (: (All [a] (-> a (m a))) @@ -1055,40 +1151,40 @@ Type (#NamedT ["lux" "Monad"] (All' [m] - (#TupleT (list (All' [a] (->' (B' a) ($' (B' m) (B' a)))) - (All' [a b] (->' (->' (B' a) ($' (B' m) (B' b))) - ($' (B' m) (B' a)) - ($' (B' m) (B' b))))))))) + (#TupleT (list (All' [a] (->' a ($' m a))) + (All' [a b] (->' (->' a ($' m b)) + ($' m a) + ($' m b)))))))) (_lux_declare-tags [#return #bind] Monad) (def''' Maybe/Monad ($' Monad Maybe) {#return (lambda' return [x] - (#Some x)) + (#Some x)) #bind (lambda' [f ma] - (_lux_case ma - #None #None - (#Some a) (f a)))}) + (_lux_case ma + #None #None + (#Some a) (f a)))}) (def''' Lux/Monad ($' Monad Lux) {#return (lambda' [x] - (lambda' [state] - (#Right state x))) + (lambda' [state] + (#Right state x))) #bind (lambda' [f ma] - (lambda' [state] - (_lux_case (ma state) - (#Left msg) - (#Left msg) + (lambda' [state] + (_lux_case (ma state) + (#Left msg) + (#Left msg) - (#Right state' a) - (f a state'))))}) + (#Right state' a) + (f a state'))))}) (defmacro #export (^ tokens) (_lux_case tokens @@ -1116,16 +1212,16 @@ (#Cons monad (#Cons (#Meta _ (#TupleS bindings)) (#Cons body #Nil))) (let' [body' (foldL (_lux_: (-> AST (, AST AST) AST) (lambda' [body' binding] - (let' [[var value] binding] - (_lux_case var - (#Meta _ (#TagS "" "let")) - (`' (;let' (~ value) (~ body'))) - - _ - (`' (bind (_lux_lambda (~ (symbol$ ["" ""])) - (~ var) - (~ body')) - (~ value))))))) + (let' [[var value] binding] + (_lux_case var + (#Meta _ (#TagS "" "let")) + (`' (;let' (~ value) (~ body'))) + + _ + (`' (bind (_lux_lambda (~ (symbol$ ["" ""])) + (~ var) + (~ body')) + (~ value))))))) body (reverse (as-pairs bindings)))] (return (list (`' (_lux_case (~ monad) @@ -1139,10 +1235,10 @@ ## (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))))) + (-> ($' Monad m) + (-> a ($' m b)) + ($' List a) + ($' m ($' List b)))) (let' [{#;return wrap #;bind _} m] (_lux_case xs #Nil @@ -1157,14 +1253,14 @@ (def''' (. f g) (All' [a b c] - (-> (-> (B' b) (B' c)) (-> (B' a) (B' b)) (-> (B' a) (B' c)))) + (-> (-> b c) (-> a b) (-> a c))) (lambda' [x] (f (g x)))) (def''' (get-ident x) (-> AST ($' Maybe Ident)) (_lux_case x - (#Meta [_ (#SymbolS sname)]) + (#Meta _ (#SymbolS sname)) (#Some sname) _ @@ -1173,7 +1269,7 @@ (def''' (get-name x) (-> AST ($' Maybe Text)) (_lux_case x - (#Meta [_ (#SymbolS ["" sname])]) + (#Meta _ (#SymbolS "" sname)) (#Some sname) _ @@ -1182,46 +1278,16 @@ (def''' (tuple->list tuple) (-> AST ($' Maybe ($' List AST))) (_lux_case tuple - (#Meta [_ (#TupleS members)]) + (#Meta _ (#TupleS members)) (#Some members) _ #None)) -(def''' RepEnv - Type - ($' List (, Text AST))) - -(def''' (make-env xs ys) - (-> ($' List Text) ($' List AST) RepEnv) - (_lux_case (_lux_: (, ($' List Text) ($' List AST)) - [xs ys]) - [(#Cons [x xs']) (#Cons [y ys'])] - (#Cons [[x y] (make-env xs' ys')]) - - _ - #Nil)) - -(def''' (text:= x y) - (-> Text Text Bool) - (_jvm_invokevirtual "java.lang.Object" "equals" ["java.lang.Object"] - x [y])) - -(def''' (get-rep key env) - (-> Text RepEnv ($' Maybe AST)) - (_lux_case env - #Nil - #None - - (#Cons [[k v] env']) - (if (text:= k key) - (#Some v) - (get-rep key env')))) - (def''' (apply-template env template) (-> RepEnv AST AST) (_lux_case template - (#Meta [_ (#SymbolS ["" sname])]) + (#Meta _ (#SymbolS "" sname)) (_lux_case (get-rep sname env) (#Some subst) subst @@ -1229,13 +1295,13 @@ _ template) - (#Meta [_ (#TupleS elems)]) + (#Meta _ (#TupleS elems)) (tuple$ (map (apply-template env) elems)) - (#Meta [_ (#FormS elems)]) + (#Meta _ (#FormS elems)) (form$ (map (apply-template env) elems)) - (#Meta [_ (#RecordS members)]) + (#Meta _ (#RecordS members)) (record$ (map (_lux_: (-> (, AST AST) (, AST AST)) (lambda' [kv] (let' [[slot value] kv] @@ -1247,7 +1313,7 @@ (def''' (join-map f xs) (All' [a b] - (-> (-> (B' a) ($' List (B' b))) ($' List (B' a)) ($' List (B' b)))) + (-> (-> a ($' List b)) ($' List a) ($' List b))) (_lux_case xs #Nil #Nil @@ -1339,63 +1405,33 @@ (let' [[module name] ident] ($ text:++ module ";" name))) -(def''' (replace-syntax reps syntax) - (-> RepEnv AST AST) - (_lux_case syntax - (#Meta [_ (#SymbolS ["" name])]) - (_lux_case (get-rep name reps) - (#Some replacement) - replacement - - #None - syntax) - - (#Meta [_ (#FormS parts)]) - (#Meta [_ (#FormS (map (replace-syntax reps) parts))]) - - (#Meta [_ (#TupleS members)]) - (#Meta [_ (#TupleS (map (replace-syntax reps) members))]) - - (#Meta [_ (#RecordS slots)]) - (#Meta [_ (#RecordS (map (_lux_: (-> (, AST AST) (, AST AST)) - (lambda' [slot] - (let' [[k v] slot] - [(replace-syntax reps k) (replace-syntax reps v)]))) - slots))]) - - _ - syntax) - ) +(def''' (make-bound idx) + (-> Int AST) + (`' (#;BoundT (~ (int$ idx))))) (defmacro #export (All tokens) - (let' [[self-ident tokens'] (_lux_: (, Text ASTList) - (_lux_case tokens - (#Cons [(#Meta [_ (#SymbolS ["" self-ident])]) tokens']) - [self-ident tokens'] - - _ - ["" tokens]))] - (_lux_case tokens' - (#Cons [(#Meta [_ (#TupleS args)]) (#Cons [body #Nil])]) - (_lux_case (map% Maybe/Monad get-name args) - (#Some idents) - (_lux_case idents - #Nil - (return (list body)) - - (#Cons [harg targs]) - (let' [replacements (map (_lux_: (-> Text (, Text AST)) - (lambda' [ident] [ident (`' (#;BoundT (~ (text$ ident))))])) - (list& self-ident idents)) - body' (foldL (lambda' [body' arg'] - (`' (#;AllT [#;None "" (~ (text$ arg')) (~ body')]))) - (replace-syntax replacements body) - (reverse targs))] - ## (#;Some #;Nil) - (return (list (`' (#;AllT [#;None (~ (text$ self-ident)) (~ (text$ harg)) (~ body')])))))) + (let' [[self-name tokens] (_lux_: (, Text ASTList) + (_lux_case tokens + (#Cons (#Meta _ (#SymbolS "" self-name)) tokens) + [self-name tokens] + + _ + ["" tokens]))] + (_lux_case tokens + (#Cons (#Meta _ (#TupleS (#Cons harg targs))) (#Cons body #Nil)) + (_lux_case (map% Maybe/Monad get-name (#Cons harg targs)) + (#Some names) + (let' [body' (foldL (lambda' [body' name'] + (`' (#;UnivQ #;Nil (~ (|> body' + (update-bounds) + (replace-syntax (list [name' (make-bound 1)]))))))) + (replace-syntax (list [self-name (make-bound -2)]) + body) + names)] + (return (list body'))) #None - (fail "'All' arguments must be symbols.")) + (fail "\"All\" arguments must be symbols.")) _ (fail "Wrong syntax for All")) @@ -2162,8 +2198,8 @@ (#VarT id) ($ text:++ "⌈" (->text id) "⌋") - (#BoundT name) - name + (#BoundT idx) + (->text idx) (#ExT ?id) ($ text:++ "⟨" (->text ?id) "⟩") @@ -2171,15 +2207,28 @@ (#AppT ?lambda ?param) ($ text:++ "(" (type:show ?lambda) " " (type:show ?param) ")") - (#AllT ?env ?name ?arg ?body) - ($ text:++ "(All " ?name " [" ?arg "] " (type:show ?body) ")") + (#UnivQ ?env ?body) + ($ text:++ "(All " (type:show ?body) ")") (#NamedT name type) (ident->text name) )) +(def (@ idx xs) + (All [a] + (-> Int (List a) (Maybe a))) + (case xs + #Nil + #None + + (#Cons x xs') + (if (i= idx 0) + (#Some x) + (@ (i- idx 1) xs') + ))) + (def (beta-reduce env type) - (-> (List (, Text Type)) Type Type) + (-> (List Type) Type Type) (case type (#VariantT ?cases) (#VariantT (map (beta-reduce env) ?cases)) @@ -2190,10 +2239,10 @@ (#AppT ?type-fn ?type-arg) (#AppT (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)) - (#AllT ?local-env ?local-name ?local-arg ?local-def) + (#UnivQ ?local-env ?local-def) (case ?local-env #Nil - (#AllT env ?local-name ?local-arg ?local-def) + (#UnivQ env ?local-def) _ type) @@ -2201,8 +2250,8 @@ (#LambdaT ?input ?output) (#LambdaT (beta-reduce env ?input) (beta-reduce env ?output)) - (#BoundT ?name) - (case (get ?name env) + (#BoundT idx) + (case (@ idx env) (#Some bound) bound @@ -2219,11 +2268,8 @@ (def (apply-type type-fn param) (-> Type Type (Maybe Type)) (case type-fn - (#AllT env name arg body) - (#Some (beta-reduce (|> env - (put name type-fn) - (put arg param)) - body)) + (#UnivQ env body) + (#Some (beta-reduce (list& type-fn param env) body)) (#AppT F A) (do Maybe/Monad @@ -2247,7 +2293,7 @@ [output (apply-type fun arg)] (resolve-struct-type output)) - (#AllT _ _ _ body) + (#UnivQ _ body) (resolve-struct-type body) (#NamedT name type) @@ -2294,7 +2340,7 @@ (#AppT fun arg) (resolve-type-tags fun) - (#AllT env name arg body) + (#UnivQ env body) (resolve-type-tags body) (#NamedT [module name] _) @@ -2556,19 +2602,6 @@ (#Left ($ text:++ "Unknown module: " module))) )) -(def (@ idx xs) - (All [a] - (-> Int (List a) (Maybe a))) - (case xs - #Nil - #None - - (#Cons x xs') - (if (i= idx 0) - (#Some x) - (@ (i- idx 1) xs') - ))) - (def (split-with' p ys xs) (All [a] (-> (-> a Bool) (List a) (List a) (, (List a) (List a)))) @@ -3139,8 +3172,8 @@ (#LambdaT in out) (` (#;LambdaT (~ (type->syntax in)) (~ (type->syntax out)))) - (#BoundT name) - (` (#;BoundT (~ (text$ name)))) + (#BoundT idx) + (` (#;BoundT (~ (int$ idx)))) (#VarT id) (` (#;VarT (~ (int$ id)))) @@ -3148,12 +3181,9 @@ (#ExT id) (` (#;ExT (~ (int$ id)))) - (#AllT env name arg type) - (let [env' (untemplate-list (map (: (-> (, Text Type) AST) - (lambda [[label type]] - (tuple$ (list (text$ label) (type->syntax type))))) - env))] - (` (#;AllT (~ env') (~ (text$ name)) (~ (text$ arg)) (~ (type->syntax type))))) + (#UnivQ env type) + (let [env' (untemplate-list (map type->syntax env))] + (` (#;UnivQ (~ env') (~ (type->syntax type))))) (#AppT fun arg) (` (#;AppT (~ (type->syntax fun)) (~ (type->syntax arg)))) diff --git a/source/lux/codata/stream.lux b/source/lux/codata/stream.lux index 956bc6994..b4c0e0239 100644 --- a/source/lux/codata/stream.lux +++ b/source/lux/codata/stream.lux @@ -24,8 +24,8 @@ (All [a] (-> a (List a) a (List a) (Stream a))) (case xs - #;Nil (cycle' init full init full) - (#;Cons [y xs']) (... [x (cycle' y xs' init full)]))) + #;Nil (cycle' init full init full) + (#;Cons x' xs') (... [x (cycle' x' xs' init full)]))) ## [Functions] (def #export (iterate f x) @@ -42,8 +42,8 @@ (All [a] (-> (List a) (Maybe (Stream a)))) (case xs - #;Nil #;None - (#;Cons [x xs']) (#;Some (cycle' x xs' x xs')))) + #;Nil #;None + (#;Cons x xs') (#;Some (cycle' x xs' x xs')))) (do-template [<name> <return> <part>] [(def #export (<name> s) |