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 | |
| 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.
| -rw-r--r-- | source/lux.lux | 882 | ||||
| -rw-r--r-- | source/lux/codata/stream.lux | 8 | ||||
| -rw-r--r-- | src/lux/analyser/case.clj | 44 | ||||
| -rw-r--r-- | src/lux/analyser/env.clj | 4 | ||||
| -rw-r--r-- | src/lux/analyser/host.clj | 2 | ||||
| -rw-r--r-- | src/lux/analyser/lux.clj | 63 | ||||
| -rw-r--r-- | src/lux/analyser/module.clj | 2 | ||||
| -rw-r--r-- | src/lux/base.clj | 37 | ||||
| -rw-r--r-- | src/lux/compiler/type.clj | 19 | ||||
| -rw-r--r-- | src/lux/reader.clj | 4 | ||||
| -rw-r--r-- | src/lux/type.clj | 445 |
11 files changed, 750 insertions, 760 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) diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj index 5987cbdf7..829b5b6d8 100644 --- a/src/lux/analyser/case.clj +++ b/src/lux/analyser/case.clj @@ -48,7 +48,7 @@ (fail "##9##")))] (resolve-type type*)) - (&/$AllT _aenv _aname _aarg _abody) + (&/$UnivQ _) ;; (&type/actual-type _abody) (|do [$var &type/existential =type (&type/apply-type type $var)] @@ -61,42 +61,46 @@ _ (&type/actual-type type))) +(defn update-up-frame [frame] + (|let [[_env _idx _var] frame] + (&/T _env (+ 2 _idx) _var))) + (defn adjust-type* [up type] - "(-> (List (, (Maybe (Env Text Type)) Text Text Type)) Type (Lux Type))" + "(-> (List (, (Maybe (List Type)) Int Type)) Type (Lux Type))" ;; (prn 'adjust-type* (&type/show-type type)) (|case type - (&/$AllT _aenv _aname _aarg _abody) + (&/$UnivQ _aenv _abody) (&type/with-var (fn [$var] (|do [=type (&type/apply-type type $var)] - (adjust-type* (&/|cons (&/T _aenv _aname _aarg $var) up) =type)))) + (adjust-type* (&/Cons$ (&/T _aenv 1 $var) (&/|map update-up-frame up)) =type)))) (&/$TupleT ?members) (|do [(&/$TupleT ?members*) (&/fold% (fn [_abody ena] - (|let [[_aenv _aname _aarg (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/V &/$BoundT _aarg))] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))] (&type/clean* _avar _abody)))) type up)] (return (&type/Tuple$ (&/|map (fn [v] (&/fold (fn [_abody ena] - (|let [[_aenv _aname _aarg _avar] ena] - (&/V &/$AllT (&/T _aenv _aname _aarg _abody)))) + (|let [[_aenv _aidx _avar] ena] + (&/V &/$UnivQ (&/T _aenv _abody)))) v up)) ?members*)))) (&/$VariantT ?members) (|do [(&/$VariantT ?members*) (&/fold% (fn [_abody ena] - (|let [[_aenv _aname _aarg (&/$VarT _avar)] ena] - (|do [_ (&type/set-var _avar (&/V &/$BoundT _aarg))] + (|let [[_aenv _aidx (&/$VarT _avar)] ena] + (|do [_ (&type/set-var _avar (&/V &/$BoundT _aidx))] (&type/clean* _avar _abody)))) type up)] (return (&/V &/$VariantT (&/|map (fn [v] (&/fold (fn [_abody ena] - (|let [[_aenv _aname _aarg _avar] ena] - (&/V &/$AllT (&/T _aenv _aname _aarg _abody)))) + (|let [[_aenv _aidx _avar] ena] + (&/V &/$UnivQ (&/T _aenv _abody)))) v up)) ?members*)))) @@ -169,7 +173,7 @@ (|do [[=tests =kont] (&/fold (fn [kont* vm] (|let [[v m] vm] (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)] - (return (&/T (&/|cons =test =tests) =kont))))) + (return (&/T (&/Cons$ =test =tests) =kont))))) (|do [=kont kont] (return (&/T (&/|list) =kont))) (&/|reverse (&/zip2 ?member-types ?members)))] @@ -192,7 +196,7 @@ (|do [[=tests =kont] (&/fold (fn [kont* vm] (|let [[v m] vm] (|do [[=test [=tests =kont]] (analyse-pattern v m kont*)] - (return (&/T (&/|cons =test =tests) =kont))))) + (return (&/T (&/Cons$ =test =tests) =kont))))) (|do [=kont kont] (return (&/T (&/|list) =kont))) (&/|reverse (&/zip2 ?member-types ?members)))] @@ -242,7 +246,7 @@ (defn ^:private analyse-branch [analyse exo-type value-type pattern body patterns] (|do [pattern+body (analyse-pattern value-type pattern (&&/analyse-1 analyse exo-type body))] - (return (&/|cons pattern+body patterns)))) + (return (&/Cons$ pattern+body patterns)))) (let [compare-kv #(.compareTo ^String (aget ^objects %1 0) ^String (aget ^objects %2 0))] (defn ^:private merge-total [struct test+body] @@ -258,31 +262,31 @@ (return (&/V $BoolTotal (&/T total? (&/|list ?value)))) [($BoolTotal total? ?values) ($BoolTestAC ?value)] - (return (&/V $BoolTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $BoolTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($IntTestAC ?value)] (return (&/V $IntTotal (&/T total? (&/|list ?value)))) [($IntTotal total? ?values) ($IntTestAC ?value)] - (return (&/V $IntTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $IntTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($RealTestAC ?value)] (return (&/V $RealTotal (&/T total? (&/|list ?value)))) [($RealTotal total? ?values) ($RealTestAC ?value)] - (return (&/V $RealTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $RealTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($CharTestAC ?value)] (return (&/V $CharTotal (&/T total? (&/|list ?value)))) [($CharTotal total? ?values) ($CharTestAC ?value)] - (return (&/V $CharTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $CharTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($TextTestAC ?value)] (return (&/V $TextTotal (&/T total? (&/|list ?value)))) [($TextTotal total? ?values) ($TextTestAC ?value)] - (return (&/V $TextTotal (&/T total? (&/|cons ?value ?values)))) + (return (&/V $TextTotal (&/T total? (&/Cons$ ?value ?values)))) [($DefaultTotal total?) ($TupleTestAC ?tests)] (|do [structs (&/map% (fn [t] diff --git a/src/lux/analyser/env.clj b/src/lux/analyser/env.clj index 666807586..66478eecc 100644 --- a/src/lux/analyser/env.clj +++ b/src/lux/analyser/env.clj @@ -22,7 +22,7 @@ =return (body (&/update$ &/$envs (fn [stack] (let [bound-unit (&/V &&/$var (&/V &/$Local (->> (&/|head stack) (&/get$ &/$locals) (&/get$ &/$counter))))] - (&/|cons (&/update$ &/$locals #(->> % + (&/Cons$ (&/update$ &/$locals #(->> % (&/update$ &/$counter inc) (&/update$ &/$mappings (fn [m] (&/|put name (&/T bound-unit type) m)))) (&/|head stack)) @@ -31,7 +31,7 @@ (|case =return (&/$Right ?state ?value) (return* (&/update$ &/$envs (fn [stack*] - (&/|cons (&/update$ &/$locals #(->> % + (&/Cons$ (&/update$ &/$locals #(->> % (&/update$ &/$counter dec) (&/set$ &/$mappings old-mappings)) (&/|head stack*)) diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj index 8ccfc5ace..098dc89df 100644 --- a/src/lux/analyser/host.clj +++ b/src/lux/analyser/host.clj @@ -313,7 +313,7 @@ (&&/analyse-1 analyse (&/V &/$DataT (as-otype ?method-output)) ?method-body)) (&/|reverse (if (:static? =method-modifiers) =method-inputs - (&/|cons (&/T ";this" ?super-class) + (&/Cons$ (&/T ";this" ?super-class) =method-inputs)))))] (return {:name ?method-name :modifiers =method-modifiers diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj index 634769839..c3f7622b8 100644 --- a/src/lux/analyser/lux.clj +++ b/src/lux/analyser/lux.clj @@ -42,7 +42,7 @@ (return (&/|list (&/T (&/V &&/$tuple =elems) exo-type)))) - (&/$AllT _) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type** (&type/apply-type exo-type* $var)] @@ -90,7 +90,7 @@ (&/$None) (fail (str "[Analyser Error] There is no case " idx " for variant type " (&type/show-type exo-type*)))) - (&/$AllT _) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type** (&type/apply-type exo-type* $var)] @@ -98,41 +98,20 @@ _ (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))) -;; (defn analyse-variant [analyse exo-type ident ?values] -;; (|do [exo-type* (|case exo-type -;; (&/$VarT ?id) -;; (&/try-all% (&/|list (|do [exo-type* (&type/deref ?id)] -;; (&type/actual-type exo-type*)) -;; (|do [_ (&type/set-var ?id &type/Type)] -;; (&type/actual-type &type/Type)))) - -;; _ -;; (&type/actual-type exo-type))] -;; (|case exo-type* -;; (&/$VariantT ?cases) -;; (|do [?tag (&&/resolved-ident ident)] -;; (if-let [vtype (&/|get ?tag ?cases)] -;; (|do [=value (analyse-variant-body analyse vtype ?values)] -;; (return (&/|list (&/T (&/V &&/$variant (&/T ?tag =value)) -;; exo-type)))) -;; (fail (str "[Analyser Error] There is no case " ?tag " for variant type " (&type/show-type exo-type*))))) - -;; (&/$AllT _) -;; (&type/with-var -;; (fn [$var] -;; (|do [exo-type** (&type/apply-type exo-type* $var)] -;; (analyse-variant analyse exo-type** ident ?values)))) - -;; _ -;; (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))) (defn analyse-record [analyse exo-type ?elems] + ;; (when @&type/!flag + ;; (prn 'analyse-record (&type/show-type exo-type) + ;; (&/->seq (&/|map (fn [pair] + ;; (|let [[k v] pair] + ;; (str (&/show-ast k) " " (&/show-ast v)))) + ;; ?elems)))) (|do [exo-type* (|case exo-type (&/$VarT ?id) (|do [exo-type* (&type/deref ?id)] (&type/actual-type exo-type*)) - (&/$AllT _) + (&/$UnivQ _) (|do [$var &type/existential =type (&type/apply-type exo-type $var)] (&type/actual-type =type)) @@ -148,7 +127,7 @@ (return ?table) _ - (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*)))) + (fail (str "[Analyser Error] The type of a record must be a record-type:\n" (&type/show-type exo-type*) "\n" (&type/show-type exo-type)))) _ (&/assert! (= (&/|length types) (&/|length ?elems)) (str "[Analyser Error] Record length mismatch. Expected: " (&/|length types) "; actual: " (&/|length ?elems))) members (&&record/order-record ?elems) @@ -221,13 +200,13 @@ (&/$Cons top-outer _) (do ;; (prn 'analyse-symbol/_3 ?module name) - (|let [scopes (&/|tail (&/folds #(&/|cons (&/get$ &/$name %2) %1) + (|let [scopes (&/|tail (&/folds #(&/Cons$ (&/get$ &/$name %2) %1) (&/|map #(&/get$ &/$name %) outer) (&/|reverse inner))) [=local inner*] (&/fold2 (fn [register+new-inner frame in-scope] (|let [[register new-inner] register+new-inner [register* frame*] (&&lambda/close-over (&/|reverse in-scope) name register frame)] - (&/T register* (&/|cons frame* new-inner)))) + (&/T register* (&/Cons$ frame* new-inner)))) (&/T (or (->> top-outer (&/get$ &/$locals) (&/get$ &/$mappings) (&/|get name)) (->> top-outer (&/get$ &/$closure) (&/get$ &/$mappings) (&/|get name))) (&/|list)) @@ -255,7 +234,7 @@ (&/$Cons ?arg ?args*) (|do [?fun-type* (&type/actual-type fun-type)] (|case ?fun-type* - (&/$AllT _aenv _aname _aarg _abody) + (&/$UnivQ _) ;; (|do [$var &type/existential ;; type* (&type/apply-type ?fun-type* $var)] ;; (analyse-apply* analyse exo-type type* ?args)) @@ -268,7 +247,7 @@ (|do [? (&type/bound? ?id) type** (if ? (&type/clean $var =output-t) - (|do [_ (&type/set-var ?id (&/V &/$BoundT _aarg))] + (|do [_ (&type/set-var ?id (&/V &/$BoundT 1))] (&type/clean $var =output-t)))] (return (&/T type** =args))) )))) @@ -276,7 +255,7 @@ (&/$LambdaT ?input-t ?output-t) (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*) =arg (&&/analyse-1 analyse ?input-t ?arg)] - (return (&/T =output-t (&/|cons =arg =args)))) + (return (&/T =output-t (&/Cons$ =arg =args)))) ;; [[&/$VarT ?id-t]] ;; (|do [ (&type/deref ?id-t)]) @@ -332,7 +311,7 @@ (defn analyse-lambda* [analyse exo-type ?self ?arg ?body] (|do [exo-type* (&type/actual-type exo-type)] (|case exo-type - (&/$AllT _) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type** (&type/apply-type exo-type* $var)] @@ -353,7 +332,7 @@ (defn analyse-lambda** [analyse exo-type ?self ?arg ?body] (|case exo-type - (&/$AllT _env _self _arg _body) + (&/$UnivQ _) (&type/with-var (fn [$var] (|do [exo-type* (&type/apply-type exo-type $var) @@ -376,12 +355,12 @@ (|do [?? (&type/bound? ?_id)] ;; (return (&/T _expr exo-type)) (if ?? - (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id ":" _arg " " (&type/show-type dtype))) + (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))) (return (&/T _expr exo-type))) ) _ - (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id ":" _arg " " (&type/show-type dtype))))) + (fail (str "[Analyser Error] Can't use type-var in any type-specific way inside polymorphic functions: " ?id " " (&type/show-type dtype))))) (return (&/T _expr exo-type)))))))) _ @@ -395,8 +374,8 @@ (defn analyse-def [analyse compile-token ?name ?value] ;; (prn 'analyse-def/BEGIN ?name) - ;; (when (= "PList/Dict" ?name) - ;; (prn 'DEF ?name (&/show-ast ?value))) + ;; (when (= "monoid$" ?name) + ;; (reset! &type/!flag true)) (|do [module-name &/get-module-name ;; :let [_ (println 'DEF/PRE (str module-name ";" ?name))] ? (&&module/defined? module-name ?name)] diff --git a/src/lux/analyser/module.clj b/src/lux/analyser/module.clj index 77630bafe..6eca13b44 100644 --- a/src/lux/analyser/module.clj +++ b/src/lux/analyser/module.clj @@ -41,7 +41,7 @@ (return* (&/update$ &/$modules (fn [ms] (&/|update current-module - (fn [m] (&/update$ $imports (partial &/|cons module) m)) + (fn [m] (&/update$ $imports (partial &/Cons$ module) m)) ms)) state) nil)))) diff --git a/src/lux/base.clj b/src/lux/base.clj index 44459beb4..5444c6c81 100644 --- a/src/lux/base.clj +++ b/src/lux/base.clj @@ -54,7 +54,7 @@ "BoundT" "VarT" "ExT" - "AllT" + "UnivQ" "AppT" "NamedT") @@ -285,9 +285,6 @@ (reverse (partition 2 steps)))) ;; [Resources/Combinators] -(defn |cons [head tail] - (V $Cons (T head tail))) - (defn |++ [xs ys] (|case xs ($Nil) @@ -348,7 +345,7 @@ ($Cons x xs*) (if (p x) (|let [[pre post] (|split-with p xs*)] - (T (|cons x pre) post)) + (T (Cons$ x pre) post)) (T (V $Nil nil) xs)))) (defn |contains? [k table] @@ -383,7 +380,7 @@ (|list init) ($Cons x xs*) - (|cons init (folds f (f init x) xs*)))) + (Cons$ init (folds f (f init x) xs*)))) (defn |length [xs] (fold (fn [acc _] (inc acc)) 0 xs)) @@ -417,7 +414,7 @@ (|list) ($Cons [k v] plist*) - (|cons k (|keys plist*)))) + (Cons$ k (|keys plist*)))) (defn |vals [plist] (|case plist @@ -425,7 +422,7 @@ (|list) ($Cons [k v] plist*) - (|cons v (|vals plist*)))) + (Cons$ v (|vals plist*)))) (defn |interpose [sep xs] (|case xs @@ -449,7 +446,7 @@ ys (<name> f xs*)] (return (<joiner> y ys))))) - map% |cons + map% Cons$ flat-map% |++) (defn list-join [xss] @@ -465,7 +462,7 @@ (defn |reverse [xs] (fold (fn [tail head] - (|cons head tail)) + (Cons$ head tail)) (|list) xs)) @@ -501,7 +498,7 @@ (defn repeat% [monad] (try-all% (|list (|do [head monad tail (repeat% monad)] - (return (|cons head tail))) + (return (Cons$ head tail))) (return (|list))))) (defn exhaust% [step] @@ -677,11 +674,11 @@ (defn ->list [seq] (if (empty? seq) (|list) - (|cons (first seq) (->list (rest seq))))) + (Cons$ (first seq) (->list (rest seq))))) (defn |repeat [n x] (if (> n 0) - (|cons x (|repeat (dec n) x)) + (Cons$ x (|repeat (dec n) x)) (|list))) (def get-module-name @@ -707,7 +704,7 @@ (defn with-scope [name body] (fn [state] - (let [output (body (update$ $envs #(|cons (env name) %) state))] + (let [output (body (update$ $envs #(Cons$ (env name) %) state))] (|case output ($Right state* datum) (return* (update$ $envs |tail state*) datum) @@ -723,7 +720,7 @@ (return (->> top (get$ $inner-closures) str)))] (fn [state] (let [body* (with-scope closure-name body)] - (run-state body* (update$ $envs #(|cons (update$ $inner-closures inc (|head %)) + (run-state body* (update$ $envs #(Cons$ (update$ $inner-closures inc (|head %)) (|tail %)) state)))))) @@ -789,10 +786,10 @@ ($Meta _ ($TagS ?module ?tag)) (str "#" ?module ";" ?tag) - ($Meta _ ($SymbolS ?module ?ident)) + ($Meta _ ($SymbolS ?module ?name)) (if (.equals "" ?module) - ?ident - (str ?module ";" ?ident)) + ?name + (str ?module ";" ?name)) ($Meta _ ($TupleS ?elems)) (str "[" (->> ?elems (|map show-ast) (|interpose " ") (fold str "")) "]") @@ -832,7 +829,7 @@ [($Cons x xs*) ($Cons y ys*)] (|do [z (f x y) zs (map2% f xs* ys*)] - (return (|cons z zs))) + (return (Cons$ z zs))) [($Nil) ($Nil)] (return (V $Nil nil)) @@ -843,7 +840,7 @@ (defn map2 [f xs ys] (|case [xs ys] [($Cons x xs*) ($Cons y ys*)] - (|cons (f x y) (map2 f xs* ys*)) + (Cons$ (f x y) (map2 f xs* ys*)) [_ _] (V $Nil nil))) diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj index 54a7c5e0c..0d0300844 100644 --- a/src/lux/compiler/type.clj +++ b/src/lux/compiler/type.clj @@ -21,6 +21,11 @@ (&/T (&/V &a/$tuple members) &type/$Void)) +(defn ^:private int$ [value] + "(-> Int Analysis)" + (&/T (&/V &a/$int value) + &type/$Void)) + (defn ^:private text$ [text] "(-> Text Analysis)" (&/T (&/V &a/$text text) @@ -58,20 +63,16 @@ (&/$LambdaT ?input ?output) (variant$ &/$LambdaT (tuple$ (&/|list (->analysis ?input) (->analysis ?output)))) - (&/$AllT ?env ?name ?arg ?body) - (variant$ &/$AllT + (&/$UnivQ ?env ?body) + (variant$ &/$UnivQ (tuple$ (&/|list (&/fold (fn [tail head] - (|let [[hlabel htype] head] - (Cons$ (tuple$ (&/|list (text$ hlabel) (->analysis htype))) - tail))) + (Cons$ (->analysis head) tail)) $Nil (&/|reverse ?env)) - (text$ ?name) - (text$ ?arg) (->analysis ?body)))) - (&/$BoundT ?name) - (variant$ &/$BoundT (text$ ?name)) + (&/$BoundT ?idx) + (variant$ &/$BoundT (int$ ?idx)) (&/$AppT ?fun ?arg) (variant$ &/$AppT (tuple$ (&/|list (->analysis ?fun) (->analysis ?arg)))) diff --git a/src/lux/reader.clj b/src/lux/reader.clj index aa845c09d..0fcb5097b 100644 --- a/src/lux/reader.clj +++ b/src/lux/reader.clj @@ -33,7 +33,7 @@ output) ($Yes output line*) - (return* (&/set$ &/$source (&/|cons line* more) state) + (return* (&/set$ &/$source (&/Cons$ line* more) state) output)) ))) @@ -117,7 +117,7 @@ column-num* (+ column-num match-length)] (if (= column-num* (.length line)) (recur (str prefix match "\n") reader**) - (&/V &/$Right (&/T (&/|cons (&/T (&/T file-name line-num column-num*) line) + (&/V &/$Right (&/T (&/Cons$ (&/T (&/T file-name line-num column-num*) line) reader**) (&/T (&/T file-name line-num column-num) (str prefix match)))))) (&/V &/$Left (str "[Reader Error] Pattern failed: " regex)))))))) diff --git a/src/lux/type.clj b/src/lux/type.clj index bcef74475..2b06553c3 100644 --- a/src/lux/type.clj +++ b/src/lux/type.clj @@ -40,8 +40,8 @@ (defn Variant$ [members] ;; (assert (|list? members)) (&/V &/$VariantT members)) -(defn All$ [env name arg body] - (&/V &/$AllT (&/T env name arg body))) +(defn Univ$ [env body] + (&/V &/$UnivQ (&/T env body))) (defn Named$ [name type] (&/V &/$NamedT (&/T name type))) @@ -57,91 +57,90 @@ (def IO (Named$ (&/T "lux/data" "IO") - (All$ empty-env "IO" "a" - (Lambda$ Unit (Bound$ "a"))))) + (Univ$ empty-env + (Lambda$ Unit (Bound$ 1))))) (def List (Named$ (&/T "lux" "List") - (All$ empty-env "lux;List" "a" - (Variant$ (&/|list - ;; lux;Nil - Unit - ;; lux;Cons - (Tuple$ (&/|list (Bound$ "a") - (App$ (Bound$ "lux;List") - (Bound$ "a")))) - ))))) + (Univ$ empty-env + (Variant$ (&/|list + ;; lux;Nil + Unit + ;; lux;Cons + (Tuple$ (&/|list (Bound$ 1) + (App$ (Bound$ 0) + (Bound$ 1)))) + ))))) (def Maybe (Named$ (&/T "lux" "Maybe") - (All$ empty-env "lux;Maybe" "a" - (Variant$ (&/|list - ;; lux;None - Unit - ;; lux;Some - (Bound$ "a") - ))))) + (Univ$ empty-env + (Variant$ (&/|list + ;; lux;None + Unit + ;; lux;Some + (Bound$ 1) + ))))) (def Type (Named$ (&/T "lux" "Type") - (let [Type (App$ (Bound$ "Type") (Bound$ "_")) + (let [Type (App$ (Bound$ 0) (Bound$ 1)) TypeList (App$ List Type) - TypeEnv (App$ List (Tuple$ (&/|list Text Type))) TypePair (Tuple$ (&/|list Type Type))] - (App$ (All$ empty-env "Type" "_" - (Variant$ (&/|list - ;; DataT - Text - ;; VariantT - TypeList - ;; TupleT - TypeList - ;; LambdaT - TypePair - ;; BoundT - Text - ;; VarT - Int - ;; ExT - Int - ;; AllT - (Tuple$ (&/|list TypeEnv Text Text Type)) - ;; AppT - TypePair - ;; NamedT - (Tuple$ (&/|list Ident Type)) - ))) + (App$ (Univ$ empty-env + (Variant$ (&/|list + ;; DataT + Text + ;; VariantT + TypeList + ;; TupleT + TypeList + ;; LambdaT + TypePair + ;; BoundT + Int + ;; VarT + Int + ;; ExT + Int + ;; UnivQ + (Tuple$ (&/|list TypeList Type)) + ;; AppT + TypePair + ;; NamedT + (Tuple$ (&/|list Ident Type)) + ))) $Void)))) (def Bindings (Named$ (&/T "lux" "Bindings") - (All$ empty-env "lux;Bindings" "k" - (All$ empty-env "" "v" - (Tuple$ (&/|list - ;; "lux;counter" - Int - ;; "lux;mappings" - (App$ List - (Tuple$ (&/|list (Bound$ "k") - (Bound$ "v")))))))))) + (Univ$ empty-env + (Univ$ empty-env + (Tuple$ (&/|list + ;; "lux;counter" + Int + ;; "lux;mappings" + (App$ List + (Tuple$ (&/|list (Bound$ 3) + (Bound$ 1)))))))))) (def Env (Named$ (&/T "lux" "Env") - (let [bindings (App$ (App$ Bindings (Bound$ "k")) - (Bound$ "v"))] - (All$ empty-env "lux;Env" "k" - (All$ empty-env "" "v" - (Tuple$ - (&/|list - ;; "lux;name" - Text - ;; "lux;inner-closures" - Int - ;; "lux;locals" - bindings - ;; "lux;closure" - bindings - ))))))) + (let [bindings (App$ (App$ Bindings (Bound$ 3)) + (Bound$ 1))] + (Univ$ empty-env + (Univ$ empty-env + (Tuple$ + (&/|list + ;; "lux;name" + Text + ;; "lux;inner-closures" + Int + ;; "lux;locals" + bindings + ;; "lux;closure" + bindings + ))))))) (def Cursor (Named$ (&/T "lux" "Cursor") @@ -149,42 +148,42 @@ (def Meta (Named$ (&/T "lux" "Meta") - (All$ empty-env "lux;Meta" "m" - (All$ empty-env "" "v" - (Variant$ (&/|list - ;; &/$Meta - (Tuple$ (&/|list (Bound$ "m") - (Bound$ "v"))))))))) + (Univ$ empty-env + (Univ$ empty-env + (Variant$ (&/|list + ;; &/$Meta + (Tuple$ (&/|list (Bound$ 3) + (Bound$ 1))))))))) (def AST* (Named$ (&/T "lux" "AST'") - (let [AST* (App$ (Bound$ "w") - (App$ (Bound$ "lux;AST'") - (Bound$ "w"))) + (let [AST* (App$ (Bound$ 1) + (App$ (Bound$ 0) + (Bound$ 1))) AST*List (App$ List AST*)] - (All$ empty-env "lux;AST'" "w" - (Variant$ (&/|list - ;; &/$BoolS - Bool - ;; &/$IntS - Int - ;; &/$RealS - Real - ;; &/$CharS - Char - ;; &/$TextS - Text - ;; &/$SymbolS - Ident - ;; &/$TagS - Ident - ;; &/$FormS - AST*List - ;; &/$TupleS - AST*List - ;; &/$RecordS - (App$ List (Tuple$ (&/|list AST* AST*)))) - ))))) + (Univ$ empty-env + (Variant$ (&/|list + ;; &/$BoolS + Bool + ;; &/$IntS + Int + ;; &/$RealS + Real + ;; &/$CharS + Char + ;; &/$TextS + Text + ;; &/$SymbolS + Ident + ;; &/$TagS + Ident + ;; &/$FormS + AST*List + ;; &/$TupleS + AST*List + ;; &/$RecordS + (App$ List (Tuple$ (&/|list AST* AST*)))) + ))))) (def AST (Named$ (&/T "lux" "AST") @@ -195,21 +194,21 @@ (def Either (Named$ (&/T "lux" "Either") - (All$ empty-env "lux;Either" "l" - (All$ empty-env "" "r" - (Variant$ (&/|list - ;; &/$Left - (Bound$ "l") - ;; &/$Right - (Bound$ "r"))))))) + (Univ$ empty-env + (Univ$ empty-env + (Variant$ (&/|list + ;; &/$Left + (Bound$ 3) + ;; &/$Right + (Bound$ 1))))))) (def StateE - (All$ empty-env "lux;StateE" "s" - (All$ empty-env "" "a" - (Lambda$ (Bound$ "s") - (App$ (App$ Either Text) - (Tuple$ (&/|list (Bound$ "s") - (Bound$ "a")))))))) + (Univ$ empty-env + (Univ$ empty-env + (Lambda$ (Bound$ 3) + (App$ (App$ Either Text) + (Tuple$ (&/|list (Bound$ 3) + (Bound$ 1)))))))) (def Source (Named$ (&/T "lux" "Source") @@ -229,17 +228,17 @@ (Data$ "clojure.lang.Atom"))))) (def DefData* - (All$ empty-env "lux;DefData'" "" - (Variant$ (&/|list - ;; "lux;ValueD" - (Tuple$ (&/|list Type Unit)) - ;; "lux;TypeD" - Type - ;; "lux;MacroD" - (Bound$ "") - ;; "lux;AliasD" - Ident - )))) + (Univ$ empty-env + (Variant$ (&/|list + ;; "lux;ValueD" + (Tuple$ (&/|list Type Unit)) + ;; "lux;TypeD" + Type + ;; "lux;MacroD" + (Bound$ 1) + ;; "lux;AliasD" + Ident + )))) (def LuxVar (Named$ (&/T "lux" "LuxVar") @@ -250,63 +249,63 @@ Ident)))) (def $Module - (All$ empty-env "lux;$Module" "Compiler" - (Tuple$ - (&/|list - ;; "lux;module-aliases" - (App$ List (Tuple$ (&/|list Text Text))) - ;; "lux;defs" - (App$ List - (Tuple$ (&/|list Text - (Tuple$ (&/|list Bool - (App$ DefData* - (Lambda$ ASTList - (App$ (App$ StateE (Bound$ "Compiler")) - ASTList)))))))) - ;; "lux;imports" - (App$ List Text) - ;; "lux;tags" - ;; (List (, Text (, Int (List Ident) Type))) - (App$ List - (Tuple$ (&/|list Text - (Tuple$ (&/|list Int - (App$ List Ident) - Type))))) - ;; "lux;types" - ;; (List (, Text (, (List Ident) Type))) - (App$ List - (Tuple$ (&/|list Text - (Tuple$ (&/|list (App$ List Ident) - Type))))) - )))) + (Univ$ empty-env + (Tuple$ + (&/|list + ;; "lux;module-aliases" + (App$ List (Tuple$ (&/|list Text Text))) + ;; "lux;defs" + (App$ List + (Tuple$ (&/|list Text + (Tuple$ (&/|list Bool + (App$ DefData* + (Lambda$ ASTList + (App$ (App$ StateE (Bound$ 1)) + ASTList)))))))) + ;; "lux;imports" + (App$ List Text) + ;; "lux;tags" + ;; (List (, Text (, Int (List Ident) Type))) + (App$ List + (Tuple$ (&/|list Text + (Tuple$ (&/|list Int + (App$ List Ident) + Type))))) + ;; "lux;types" + ;; (List (, Text (, (List Ident) Type))) + (App$ List + (Tuple$ (&/|list Text + (Tuple$ (&/|list (App$ List Ident) + Type))))) + )))) (def $Compiler (Named$ (&/T "lux" "Compiler") - (App$ (All$ empty-env "lux;Compiler" "" - (Tuple$ - (&/|list - ;; "lux;source" - Source - ;; "lux;cursor" - Cursor - ;; "lux;modules" - (App$ List (Tuple$ (&/|list Text - (App$ $Module (App$ (Bound$ "lux;Compiler") (Bound$ "")))))) - ;; "lux;envs" - (App$ List - (App$ (App$ Env Text) - (Tuple$ (&/|list LuxVar Type)))) - ;; "lux;types" - (App$ (App$ Bindings Int) Type) - ;; "lux;expected" - Type - ;; "lux;seed" - Int - ;; "lux;eval?" - Bool - ;; "lux;host" - Host - ))) + (App$ (Univ$ empty-env + (Tuple$ + (&/|list + ;; "lux;source" + Source + ;; "lux;cursor" + Cursor + ;; "lux;modules" + (App$ List (Tuple$ (&/|list Text + (App$ $Module (App$ (Bound$ 0) (Bound$ 1)))))) + ;; "lux;envs" + (App$ List + (App$ (App$ Env Text) + (Tuple$ (&/|list LuxVar Type)))) + ;; "lux;types" + (App$ (App$ Bindings Int) Type) + ;; "lux;expected" + Type + ;; "lux;seed" + Int + ;; "lux;eval?" + Bool + ;; "lux;host" + Host + ))) $Void))) (def Macro @@ -439,13 +438,10 @@ (|do [=members (&/map% (partial clean* ?tid) ?members)] (return (Variant$ =members))) - (&/$AllT ?env ?name ?arg ?body) - (|do [=env (&/map% (fn [[k v]] - (|do [=v (clean* ?tid v)] - (return (&/T k =v)))) - ?env) + (&/$UnivQ ?env ?body) + (|do [=env (&/map% (partial clean* ?tid) ?env) body* (clean* ?tid ?body)] - (return (All$ =env ?name ?arg body*))) + (return (Univ$ =env body*))) _ (return type) @@ -463,7 +459,7 @@ (|case type (&/$LambdaT ?in ?out) (|let [[??out ?args] (unravel-fun ?out)] - (&/T ??out (&/|cons ?in ?args))) + (&/T ??out (&/Cons$ ?in ?args))) _ (&/T type (&/|list)))) @@ -505,26 +501,16 @@ (&/$ExT ?id) (str "⟨" ?id "⟩") - (&/$BoundT name) - name + (&/$BoundT idx) + (str idx) (&/$AppT _ _) (|let [[?call-fun ?call-args] (unravel-app type)] (str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")) - (&/$AllT ?env ?name ?arg ?body) - (if (= "" ?name) - (let [[args body] (loop [args (list ?arg) - body* ?body] - (|case body* - (&/$AllT ?env* ?name* ?arg* ?body*) - (recur (cons ?arg* args) ?body*) - - _ - [args body*]))] - (str "(All " ?name " [" (->> args reverse (interpose " ") (reduce str "")) "] " (show-type body) ")")) - ?name) - + (&/$UnivQ ?env ?body) + (str "(All " (show-type ?body) ")") + (&/$NamedT ?name ?type) (&/ident->text ?name) @@ -554,8 +540,8 @@ [(&/$VarT xid) (&/$VarT yid)] (.equals ^Object xid yid) - [(&/$BoundT xname) (&/$BoundT yname)] - (.equals ^Object xname yname) + [(&/$BoundT xidx) (&/$BoundT yidx)] + (= xidx yidx) [(&/$ExT xid) (&/$ExT yid)] (.equals ^Object xid yid) @@ -563,24 +549,8 @@ [(&/$AppT xlambda xparam) (&/$AppT ylambda yparam)] (and (type= xlambda ylambda) (type= xparam yparam)) - [(&/$AllT xenv xname xarg xbody) (&/$AllT yenv yname yarg ybody)] - (and (.equals ^Object xname yname) - (.equals ^Object xarg yarg) - ;; (matchv ::M/objects [xenv yenv] - ;; [[&/$None _] [&/$None _]] - ;; true - - ;; [[&/$Some xenv*] [&/$Some yenv*]] - ;; (&/fold (fn [old bname] - ;; (and old - ;; (type= (&/|get bname xenv*) (&/|get bname yenv*)))) - ;; (= (&/|length xenv*) (&/|length yenv*)) - ;; (&/|keys xenv*)) - - ;; [_ _] - ;; false) - (type= xbody ybody) - ) + [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)] + (type= xbody ybody) [(&/$NamedT ?xname ?xtype) _] (type= ?xtype y) @@ -607,14 +577,18 @@ ))) (defn ^:private fp-put [k v fixpoints] - (&/|cons (&/T k v) fixpoints)) + (&/Cons$ (&/T k v) fixpoints)) (defn ^:private check-error [expected actual] (str "[Type Checker]\nExpected: " (show-type expected) "\n\nActual: " (show-type actual) "\n")) +;; (def !flag (atom false)) + (defn beta-reduce [env type] + ;; (when @!flag + ;; (prn 'beta-reduce (show-type type))) (|case type (&/$VariantT ?members) (Variant$ (&/|map (partial beta-reduce env) ?members)) @@ -625,10 +599,10 @@ (&/$AppT ?type-fn ?type-arg) (App$ (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) - (All$ env ?local-name ?local-arg ?local-def) + (Univ$ env ?local-def) _ type) @@ -636,21 +610,26 @@ (&/$LambdaT ?input ?output) (Lambda$ (beta-reduce env ?input) (beta-reduce env ?output)) - (&/$BoundT ?name) - (if-let [bound (&/|get ?name env)] + (&/$BoundT ?idx) + (|case (&/|at ?idx env) + (&/$Some bound) (beta-reduce env bound) - type) + + _ + (assert false (str "[Type Error] Unknown var: " ?idx " | " (&/->seq (&/|map show-type env))))) _ type )) (defn apply-type [type-fn param] + ;; (when @!flag + ;; (prn 'apply-type (show-type type-fn) (show-type param))) (|case type-fn - (&/$AllT local-env local-name local-arg local-def) + (&/$UnivQ local-env local-def) (return (beta-reduce (->> local-env - (&/|put local-name type-fn) - (&/|put local-arg param)) + (&/Cons$ param) + (&/Cons$ type-fn)) local-def)) (&/$AppT F A) @@ -839,13 +818,13 @@ (|do [actual* (apply-type F A)] (check* class-loader fixpoints expected actual*)) - [(&/$AllT _) _] + [(&/$UnivQ _) _] (with-var (fn [$arg] (|do [expected* (apply-type expected $arg)] (check* class-loader fixpoints expected* actual)))) - [_ (&/$AllT _)] + [_ (&/$UnivQ _)] (with-var (fn [$arg] (|do [actual* (apply-type actual $arg)] @@ -910,7 +889,7 @@ (|do [_ (check* init-fixpoints input param)] (return output)) - (&/$AllT _) + (&/$UnivQ _) (with-var (fn [$var] (|do [func* (apply-type func $var) |