aboutsummaryrefslogtreecommitdiff
path: root/source
diff options
context:
space:
mode:
authorEduardo Julian2015-08-28 22:46:12 -0400
committerEduardo Julian2015-08-28 22:46:12 -0400
commit8de225f98aaed212bf3b683208bff5c6ab85a835 (patch)
treef9a3e197c7bf62cffa411f5a9e768cbca6a76d9b /source
parenta10d922283a9256f0f0015d9d00a0c549b1891cb (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.lux882
-rw-r--r--source/lux/codata/stream.lux8
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)