aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2015-04-25 17:30:54 -0400
committerEduardo Julian2015-04-25 17:30:54 -0400
commitcc8f12a30f0f7144e9ce0a2846b30d4d9c36d0eb (patch)
tree8212f3e71a7e2ce0f672cce118ba703153bfe3de
parentd366abe19aaf9b688312d2f845f6771b8478cc0c (diff)
- More accurate AllT environment management by using (Maybe TypeEnv) instead of TypeEnv. The performance of the type-checker also improved thanks to that.
Diffstat (limited to '')
-rw-r--r--source/lux.lux58
-rw-r--r--src/lux/type.clj85
2 files changed, 86 insertions, 57 deletions
diff --git a/source/lux.lux b/source/lux.lux
index a005da3da..aab80ed7e 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -22,11 +22,14 @@
(def' Text (#DataT "java.lang.String"))
(export' Text)
+(def' Void (#VariantT #Nil))
+(export' Void)
+
## (deftype (List a)
## (| #Nil
## (#Cons (, a (List a)))))
(def' List
- (#AllT [#Nil "List" "a"
+ (#AllT [#None "List" "a"
(#VariantT (#Cons [["lux;Nil" (#TupleT #Nil)]
(#Cons [["lux;Cons" (#TupleT (#Cons [(#BoundT "a")
(#Cons [(#AppT [(#BoundT "List") (#BoundT "a")])
@@ -34,6 +37,16 @@
#Nil])]))]))
(export' List)
+## (deftype (Maybe a)
+## (| #None
+## (#Some a)))
+(def' Maybe
+ (#AllT [#None "Maybe" "a"
+ (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
+ (#Cons [["lux;Some" (#BoundT "a")]
+ #Nil])]))]))
+(export' Maybe)
+
## (deftype #rec Type
## (| #AnyT
## #NothingT
@@ -44,47 +57,36 @@
## (#LambdaT (, Type Type))
## (#BoundT Text)
## (#VarT Int)
-## (#AllT (, (List (, Text Type)) Text Text Type))
+## (#AllT (, (Maybe (List (, Text Type))) Text Text Type))
## (#AppT (, Type Type))))
(def' Type
(case' (#AppT [(#BoundT "Type") (#BoundT "")])
Type
(case' (#AppT [List (#TupleT (#Cons [Text (#Cons [Type #Nil])]))])
TypeEnv
- (#AppT [(#AllT [#Nil "Type" ""
+ (#AppT [(#AllT [#None "Type" ""
(#VariantT (#Cons [["lux;AnyT" (#TupleT #Nil)]
(#Cons [["lux;NothingT" (#TupleT #Nil)]
(#Cons [["lux;DataT" Text]
- (#Cons [["lux;TupleT" (#AppT [List (#AppT [(#BoundT "Type") (#BoundT "")])])]
+ (#Cons [["lux;TupleT" (#AppT [List Type])]
(#Cons [["lux;VariantT" TypeEnv]
(#Cons [["lux;RecordT" TypeEnv]
(#Cons [["lux;LambdaT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))]
(#Cons [["lux;BoundT" Text]
(#Cons [["lux;VarT" Int]
- (#Cons [["lux;AllT" (#TupleT (#Cons [TypeEnv (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))]
+ (#Cons [["lux;AllT" (#TupleT (#Cons [(#AppT [Maybe TypeEnv]) (#Cons [Text (#Cons [Text (#Cons [Type #Nil])])])]))]
(#Cons [["lux;AppT" (#TupleT (#Cons [Type (#Cons [Type #Nil])]))]
#Nil])])])])])])])])])])]))])
#NothingT]))))
(export' Type)
-## (deftype (Maybe a)
-## (| #None
-## (#Some a)))
-(def' Maybe
- (:' Type
- (#AllT [#Nil "Maybe" "a"
- (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
- (#Cons [["lux;Some" (#BoundT "a")]
- #Nil])]))])))
-(export' Maybe)
-
## (deftype (Bindings k v)
## (& #counter Int
## #mappings (List (, k v))))
(def' Bindings
(:' Type
- (#AllT [#Nil "Bindings" "k"
- (#AllT [#Nil "" "v"
+ (#AllT [#None "Bindings" "k"
+ (#AllT [#None "" "v"
(#RecordT (#Cons [["lux;counter" Int]
(#Cons [["lux;mappings" (#AppT [List
(#TupleT (#Cons [(#BoundT "k")
@@ -99,8 +101,8 @@
## #closure (Bindings k v)))
(def' Env
(:' Type
- (#AllT [#Nil "Env" "k"
- (#AllT [#Nil "" "v"
+ (#AllT [#None "Env" "k"
+ (#AllT [#None "" "v"
(#RecordT (#Cons [["lux;name" Text]
(#Cons [["lux;inner-closures" Int]
(#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")])
@@ -119,8 +121,8 @@
## (| (#Meta (, m v))))
(def' Meta
(:' Type
- (#AllT [#Nil "Meta" "m"
- (#AllT [#Nil "" "v"
+ (#AllT [#None "Meta" "m"
+ (#AllT [#None "" "v"
(#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
(#Cons [(#BoundT "v")
#Nil])]))]
@@ -186,7 +188,7 @@
Syntax'List
(case' (#TupleT (#Cons [Text (#Cons [Text #Nil])]))
Ident
- (#AllT [#Nil "Syntax'" "w"
+ (#AllT [#None "Syntax'" "w"
(#VariantT (#Cons [["lux;Bool" Bool]
(#Cons [["lux;Int" Int]
(#Cons [["lux;Real" Real]
@@ -217,8 +219,8 @@
## (#Right r)))
(def' Either
(:' Type
- (#AllT [#Nil "_" "l"
- (#AllT [#Nil "" "r"
+ (#AllT [#None "_" "l"
+ (#AllT [#None "" "r"
(#VariantT (#Cons [["lux;Left" (#BoundT "l")]
(#Cons [["lux;Right" (#BoundT "r")]
#Nil])]))])])))
@@ -452,7 +454,7 @@
(#Cons [(#Meta [_ (#Tuple (#Cons [(#Meta [_ (#Symbol ["" arg-name])]) other-args]))])
(#Cons [body #Nil])])
(return' (#Cons [(_meta (#Form (#Cons [(_meta (#Tag ["lux" "AllT"]))
- (#Cons [(_meta (#Tuple (#Cons [(_meta (#Tag ["lux" "Nil"]))
+ (#Cons [(_meta (#Tuple (#Cons [(_meta (#Tag ["lux" "None"]))
(#Cons [(_meta (#Text ""))
(#Cons [(_meta (#Text arg-name))
(#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "All'"]))
@@ -760,7 +762,7 @@
## (lambda [body arg]
## (case' arg
## (#Meta [_ (#Symbol [arg-module arg-name])])
-## (` (#AllT (list) "" (~ (_meta (#Text arg-name))) (~ (replace-ident [arg-module arg-name]
+## (` (#AllT #None "" (~ (_meta (#Text arg-name))) (~ (replace-ident [arg-module arg-name]
## (` (#BoundT (~ (#Text ($ text:++ arg-module ";" arg-name)))))
## body)))))))
## body
@@ -1596,7 +1598,7 @@
## (#Symbol ["" arg]))
## args)
## body' (replace-syntax arg-replacements body)]
-## (return (list (` (#AllT [#Nil (~ name') (#Tuple (list (~@ args')))
+## (return (list (` (#AllT [#None (~ name') (#Tuple (list (~@ args')))
## (~ body')]))))))
## (def (walk-syntax type)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 35190da27..17db11b43 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -17,18 +17,22 @@
(def Unit (&/V "lux;TupleT" (&/|list)))
(def List
- (&/V "lux;AllT" (&/T (&/|table) "List" "a"
- (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" (&/V "lux;TupleT" (&/|list)))
+ (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "List" "a"
+ (&/V "lux;VariantT" (&/|list (&/T "lux;Nil" Unit)
(&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
(&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
(&/V "lux;BoundT" "a")))))))))))
+(def Maybe
+ (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "Maybe" "a"
+ (&/V "lux;VariantT" (&/|list (&/T "lux;None" Unit)
+ (&/T "lux;Some" (&/V "lux;BoundT" "a")))))))
+
(def Type
(let [Type (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "Type") (&/V "lux;BoundT" "_")))
TypeEnv (&/V "lux;AppT" (&/T List (&/V "lux;TupleT" (&/|list Text Type))))
- Unit (&/V "lux;TupleT" (&/|list))
TypePair (&/V "lux;TupleT" (&/|list Type Type))]
- (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/|list) "Type" "_"
+ (&/V "lux;AppT" (&/T (&/V "lux;AllT" (&/T (&/V "lux;None" nil) "Type" "_"
(&/V "lux;VariantT" (&/|list (&/T "lux;AnyT" Unit)
(&/T "lux;NothingT" Unit)
(&/T "lux;DataT" Text)
@@ -38,7 +42,7 @@
(&/T "lux;LambdaT" TypePair)
(&/T "lux;BoundT" Text)
(&/T "lux;VarT" Int)
- (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list TypeEnv Text Text Type)))
+ (&/T "lux;AllT" (&/V "lux;TupleT" (&/|list (&/V "lux;AppT" (&/T Maybe TypeEnv)) Text Text Type)))
(&/T "lux;AppT" TypePair)
))))
(&/V "lux;NothingT" nil)))))
@@ -154,10 +158,16 @@
(return (&/V "lux;RecordT" =members)))
[["lux;AllT" [?env ?name ?arg ?body]]]
- (|do [=env (&/map% (fn [[k v]]
- (|do [=v (clean* ?tid v)]
- (return (&/T k =v))))
- ?env)
+ (|do [=env (matchv ::M/objects [?env]
+ [["lux;None" _]]
+ (return ?env)
+
+ [["lux;Some" ?env*]]
+ (|do [clean-env (&/map% (fn [[k v]]
+ (|do [=v (clean* ?tid v)]
+ (return (&/T k =v))))
+ ?env*)]
+ (return (&/V "lux;Some" clean-env))))
body* (clean* ?tid ?body)]
(return (&/V "lux;AllT" (&/T =env ?name ?arg body*))))
@@ -284,20 +294,27 @@
;; 'NAME [xname yname] (= xname yname)
;; 'ARG (= xarg yarg)
;; 'LENGTH [(&/|length xenv) (&/|length yenv)] (= (&/|length xenv) (&/|length yenv)))
- (and (= xname yname)
- (= xarg yarg)
- (type= xbody ybody)
- ;; (= (&/|length xenv) (&/|length yenv))
- ;; (&/fold (fn [old bname]
- ;; (and old
- ;; (type= (&/|get bname xenv) (&/|get bname yenv))))
- ;; true
- ;; (&/|keys xenv))
- ))
+ (and (= xname yname)
+ (= xarg yarg)
+ ;; (matchv ::M/objects [xenv yenv]
+ ;; [["lux;None" _] ["lux;None" _]]
+ ;; true
+
+ ;; [["lux;Some" xenv*] ["lux;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)
+ ))
[_ _]
(do ;; (prn 'type= (show-type x) (show-type y))
- false)
+ false)
)]
;; (prn 'type= output (show-type x) (show-type y))
output))
@@ -343,16 +360,19 @@
(&/V "lux;AppT" (&/T (beta-reduce env ?type-fn) (beta-reduce env ?type-arg)))
[["lux;AllT" [?local-env ?local-name ?local-arg ?local-def]]]
- (&/V "lux;AllT" (&/T (&/|merge ?local-env env) ?local-name ?local-arg ?local-def))
+ (matchv ::M/objects [?local-env]
+ [["lux;None" _]]
+ (&/V "lux;AllT" (&/T (&/V "lux;Some" env) ?local-name ?local-arg ?local-def))
+
+ [["lux;Some" _]]
+ type)
[["lux;LambdaT" [?input ?output]]]
(&/V "lux;LambdaT" (&/T (beta-reduce env ?input) (beta-reduce env ?output)))
[["lux;BoundT" ?name]]
(if-let [bound (&/|get ?name env)]
- (do ;; (prn 'beta-reduce "lux;BoundT" ?name (->> (&/|keys env) (&/|interpose " ") (&/fold str ""))
- ;; (show-type bound))
- (beta-reduce env bound))
+ (beta-reduce env bound)
type)
[_]
@@ -372,10 +392,17 @@
;; (prn 'apply-type (aget type-fn 0) (aget param 0))
(matchv ::M/objects [type-fn]
[["lux;AllT" [local-env local-name local-arg local-def]]]
- (return (beta-reduce (->> local-env
- (&/|put local-name type-fn)
- (&/|put local-arg param))
- local-def))
+ (let [;; _ (prn 'apply-type/local-env (aget local-env 0) (show-type type-fn))
+ local-env* (matchv ::M/objects [local-env]
+ [["lux;None" _]]
+ (&/|table)
+
+ [["lux;Some" local-env*]]
+ local-env*)]
+ (return (beta-reduce (->> local-env*
+ (&/|put local-name type-fn)
+ (&/|put local-arg param))
+ local-def)))
[["lux;AppT" [F A]]]
(|do [type-fn* (apply-type F A)]
@@ -552,7 +579,7 @@
(|do [_ (check* init-fixpoints input param)]
(return output))
- [["lux;AllT" [local-env local-name local-arg local-def]]]
+ [["lux;AllT" _]]
(with-var
(fn [$var]
(|do [func* (apply-type func $var)