aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--source/lux.lux323
-rw-r--r--src/lux.clj6
-rw-r--r--src/lux/analyser.clj15
-rw-r--r--src/lux/analyser/base.clj18
-rw-r--r--src/lux/analyser/case.clj236
-rw-r--r--src/lux/analyser/lambda.clj2
-rw-r--r--src/lux/analyser/lux.clj104
-rw-r--r--src/lux/base.clj12
-rw-r--r--src/lux/type.clj413
9 files changed, 634 insertions, 495 deletions
diff --git a/source/lux.lux b/source/lux.lux
index 357366d58..ca6a1925c 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -74,173 +74,170 @@
#Nil])])])])])])])])])])]))])
#NothingT]))))
-## ## (deftype (Maybe a)
-## ## (| #None
-## ## (#Some a)))
-## (def' Maybe
-## (#AllT [#Nil "Maybe" "a"
-## (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
-## (#Cons [["lux;Some" (#BoundT "a")]
-## #Nil])]))]))
-
-## ## (deftype (Bindings k v)
-## ## (& #counter Int
-## ## #mappings (List (, k v))))
-## (def' Bindings
-## (#AllT [#Nil "Bindings" "k"
-## (#AllT [#Nil "" "v"
-## (#RecordT (#Cons [["lux;counter" Int]
-## (#Cons [["lux;mappings" (#AppT [List
-## (#TupleT (#Cons [(#BoundT "k")
-## (#Cons [(#BoundT "v")
-## #Nil])]))])]
-## #Nil])]))])]))
-
-## ## (deftype (Env k v)
-## ## (& #name Text
-## ## #inner-closures Int
-## ## #locals (Bindings k v)
-## ## #closure (Bindings k v)))
-## (def' Env
-## (#AllT [#Nil "Env" "k"
-## (#AllT [#Nil "" "v"
-## (#RecordT (#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])])])]))])]))
-
-## ## (deftype Cursor
-## ## (, Text Int Int))
-## (def' Cursor
-## (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])])))
-
-## ## (deftype (Meta m v)
-## ## (| (#Meta (, m v))))
-## (def' Meta
-## (#AllT [#Nil "Meta" "m"
-## (#AllT [#Nil "" "v"
-## (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
-## (#Cons [(#BoundT "v")
-## #Nil])]))]
-## #Nil]))])]))
-
-## ## (def' Reader
-## ## (List (Meta Cursor Text)))
-## (def' Reader
-## (#AppT [List
-## (#AppT [(#AppT [Meta Cursor])
-## Text])]))
-
-## ## (deftype Compiler_State
-## ## (& #source (Maybe Reader)
-## ## #modules (List Any)
-## ## #module-aliases (List Any)
-## ## #global-env (Maybe (Env Text Any))
-## ## #local-envs (List (Env Text Any))
-## ## #types (Bindings Int Type)
-## ## #writer (^ org.objectweb.asm.ClassWriter)
-## ## #loader (^ java.net.URLClassLoader)
-## ## #eval-ctor Int))
-## (def' Compiler_State
-## (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])]
-## (#Cons [["lux;modules" (#AppT [List Any])]
-## (#Cons [["lux;module-aliases" (#AppT [List Any])]
-## (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])]
-## (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])]
-## (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])]
-## (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")]
-## (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")]
-## (#Cons [["lux;eval-ctor" Int]
-## #Nil])])])])])])])])])))
+## (deftype (Maybe a)
+## (| #None
+## (#Some a)))
+(def' Maybe
+ (#AllT [#Nil "Maybe" "a"
+ (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
+ (#Cons [["lux;Some" (#BoundT "a")]
+ #Nil])]))]))
-## ## (deftype #rec Syntax
-## ## (Meta Cursor (| (#Bool Bool)
-## ## (#Int Int)
-## ## (#Real Real)
-## ## (#Char Char)
-## ## (#Text Text)
-## ## (#Form (List Syntax))
-## ## (#Tuple (List Syntax))
-## ## (#Record (List (, Text Syntax))))))
-## (def' Syntax
-## (case' (#AppT [(#BoundT "Syntax") (#BoundT "")])
-## Syntax
-## (case' (#AppT [List Syntax])
-## SyntaxList
-## (#AppT [(#AllT [#Nil "Syntax" ""
-## (#VariantT (#Cons [["lux;Bool" Bool]
-## (#Cons [["lux;Int" Int]
-## (#Cons [["lux;Real" Real]
-## (#Cons [["lux;Char" Char]
-## (#Cons [["lux;Text" Text]
-## (#Cons [["lux;Form" SyntaxList]
-## (#Cons [["lux;Tuple" SyntaxList]
-## (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])]
-## #Nil])])])])])])])]))])
-## #NothingT]))))
+## (deftype (Bindings k v)
+## (& #counter Int
+## #mappings (List (, k v))))
+(def' Bindings
+ (#AllT [#Nil "Bindings" "k"
+ (#AllT [#Nil "" "v"
+ (#RecordT (#Cons [["lux;counter" Int]
+ (#Cons [["lux;mappings" (#AppT [List
+ (#TupleT (#Cons [(#BoundT "k")
+ (#Cons [(#BoundT "v")
+ #Nil])]))])]
+ #Nil])]))])]))
+
+## (deftype (Env k v)
+## (& #name Text
+## #inner-closures Int
+## #locals (Bindings k v)
+## #closure (Bindings k v)))
+(def' Env
+ (#AllT [#Nil "Env" "k"
+ (#AllT [#Nil "" "v"
+ (#RecordT (#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])])])]))])]))
+
+## (deftype Cursor
+## (, Text Int Int))
+(def' Cursor
+ (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])])))
+
+## (deftype (Meta m v)
+## (| (#Meta (, m v))))
+(def' Meta
+ (#AllT [#Nil "Meta" "m"
+ (#AllT [#Nil "" "v"
+ (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
+ (#Cons [(#BoundT "v")
+ #Nil])]))]
+ #Nil]))])]))
-## ## (deftype (Either l r)
-## ## (| (#Left l)
-## ## (#Right r)))
-## (def' Either
-## (#AllT [#Nil "_" "l"
-## (#AllT [#Nil "" "r"
-## (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
-## (#Cons [["lux;Right" (#BoundT "r")]
-## #Nil])]))])]))
+## (def' Reader
+## (List (Meta Cursor Text)))
+(def' Reader
+ (#AppT [List
+ (#AppT [(#AppT [Meta Cursor])
+ Text])]))
+
+## (deftype Compiler_State
+## (& #source (Maybe Reader)
+## #modules (List Any)
+## #module-aliases (List Any)
+## #global-env (Maybe (Env Text Any))
+## #local-envs (List (Env Text Any))
+## #types (Bindings Int Type)
+## #writer (^ org.objectweb.asm.ClassWriter)
+## #loader (^ java.net.URLClassLoader)
+## #eval-ctor Int))
+(def' Compiler_State
+ (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])]
+ (#Cons [["lux;modules" (#AppT [List Any])]
+ (#Cons [["lux;module-aliases" (#AppT [List Any])]
+ (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])]
+ (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])]
+ (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])]
+ (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")]
+ (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")]
+ (#Cons [["lux;eval-ctor" Int]
+ #Nil])])])])])])])])])))
+
+## (deftype #rec Syntax
+## (Meta Cursor (| (#Bool Bool)
+## (#Int Int)
+## (#Real Real)
+## (#Char Char)
+## (#Text Text)
+## (#Form (List Syntax))
+## (#Tuple (List Syntax))
+## (#Record (List (, Text Syntax))))))
+(def' Syntax
+ (case' (#AppT [(#BoundT "Syntax") (#BoundT "")])
+ Syntax
+ (case' (#AppT [List Syntax])
+ SyntaxList
+ (#AppT [(#AllT [#Nil "Syntax" ""
+ (#AppT [(#AppT [Meta Cursor])
+ (#VariantT (#Cons [["lux;Bool" Bool]
+ (#Cons [["lux;Int" Int]
+ (#Cons [["lux;Real" Real]
+ (#Cons [["lux;Char" Char]
+ (#Cons [["lux;Text" Text]
+ (#Cons [["lux;Form" SyntaxList]
+ (#Cons [["lux;Tuple" SyntaxList]
+ (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])]
+ #Nil])])])])])])])]))])])
+ #NothingT]))))
+
+## (deftype (Either l r)
+## (| (#Left l)
+## (#Right r)))
+(def' Either
+ (#AllT [#Nil "_" "l"
+ (#AllT [#Nil "" "r"
+ (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
+ (#Cons [["lux;Right" (#BoundT "r")]
+ #Nil])]))])]))
+
+## (deftype Macro
+## (-> (List Syntax) Compiler_State
+## (Either Text [Compiler_State (List Syntax)])))
+(def' Macro
+ (case' (#AppT [List Syntax])
+ SyntaxList
+ (#LambdaT [SyntaxList
+ (#LambdaT [Compiler_State
+ (#AppT [(#AppT [Either Text])
+ (#TupleT (#Cons [Compiler_State
+ (#Cons [SyntaxList #Nil])]))])])])))
+
+## Base functions & macros
+## (def (_meta data)
+## (All [a] (-> a (Meta Cursor a)))
+## (#Meta [["" -1 -1] data]))
+(def' _meta
+ (check' (#AllT [#Nil "_" "a"
+ (#LambdaT [(#BoundT "a")
+ (#AppT [(#AppT [Meta Cursor])
+ (#BoundT "a")])])])
+ (lambda' _ data
+ (#Meta [["" -1 -1] data]))))
+
+(def' let'
+ (check' Macro
+ (lambda' _ tokens
+ (lambda' _ state
+ (case' tokens
+ (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
+ (#Right [state
+ (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
+ (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
+ #Nil])])
+
+ _
+ (#Left "Wrong syntax for let'"))
+ ))))
-## ## (deftype Macro
-## ## (-> (List Syntax) Compiler_State
-## ## (Either Text [Compiler_State (List Syntax)])))
-## (def' Macro
-## (case' (#AppT [List Syntax])
-## SyntaxList
-## (#LambdaT [SyntaxList
-## (#LambdaT [CompilerState
-## (#AppT [(#AppT [Either Text])
-## (#TupleT (#Cons [CompilerState
-## (#Cons [SyntaxList #Nil])]))])])])))
-
-## ## Base functions & macros
-## ## (def (_meta data)
-## ## (All [a] (-> a (Meta Cursor a)))
-## ## (#Meta [["" -1 -1] data]))
-## (def' _meta
-## (check' (#AllT [#Nil "_" "a"
-## (#LambdaT [(#BoundT "a")
-## (#AppT [(#AppT [Meta Cursor])
-## (#BoundT "a")])])])
-## (lambda' _ data
-## (#Meta [["" -1 -1] data]))))
-
-## ## (def' let'
-## ## (check' Macro
-## ## (lambda' _ tokens
-## ## (lambda' _ state
-## ## (case' tokens
-## ## (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
-## ## (#Right [state
-## ## (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
-## ## (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
-## ## #Nil])])
-
-## ## _
-## ## (#Left "Wrong syntax for let'"))
-## ## ))))
-## ## (def' let'
-## ## (check' Macro
-## ## (lambda' _ tokens
-## ## (lambda' _ state
-## ## (#Left "Wrong syntax for let'")
-## ## ))))
## (def' let'
-## (check' (#AppT [(#AppT [Either Text])
-## (#TupleT (#Cons [CompilerState
-## (#Cons [(#AppT [List Syntax]) #Nil])]))])
-## (#Left "Wrong syntax for let'")))
+## (check' Macro
+## (lambda' _ tokens
+## (lambda' _ state
+## (#Left "Wrong syntax for let'")
+## ))))
## (def' let'
## (lambda' _ tokens
diff --git a/src/lux.clj b/src/lux.clj
index 7bee8df16..e035e92c8 100644
--- a/src/lux.clj
+++ b/src/lux.clj
@@ -11,8 +11,12 @@
;; TODO: All optimizations
;; TODO: Anonymous classes
;; TODO:
-
+
;; Finish total-locals
+
+ ;; TODO: Change &type/check to it returns a tuple with the new expected & actual types
+ ;; TODO: Stop passing-along the exo-types and instead pass-along endo-types where possible
+ ;; TODO: Optimize analyser to avoid redundant checks when dealing with type-checking (making sure check* is being handed a type)
(time (&compiler/compile-all (&/|list "lux")))
(System/gc)
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 39eaf9e16..14d5599e4 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -38,19 +38,24 @@
(matchv ::M/objects [token]
;; Standard special forms
[["lux;Meta" [meta ["lux;Bool" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) &type/Bool))))
+ (|do [_ (&type/check exo-type &type/Bool)]
+ (return (&/|list (&/V "Expression" (&/T (&/V "bool" ?value) exo-type)))))
[["lux;Meta" [meta ["lux;Int" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) &type/Int))))
+ (|do [_ (&type/check exo-type &type/Int)]
+ (return (&/|list (&/V "Expression" (&/T (&/V "int" ?value) exo-type)))))
[["lux;Meta" [meta ["lux;Real" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) &type/Real))))
+ (|do [_ (&type/check exo-type &type/Real)]
+ (return (&/|list (&/V "Expression" (&/T (&/V "real" ?value) exo-type)))))
[["lux;Meta" [meta ["lux;Char" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) &type/Char))))
+ (|do [_ (&type/check exo-type &type/Char)]
+ (return (&/|list (&/V "Expression" (&/T (&/V "char" ?value) exo-type)))))
[["lux;Meta" [meta ["lux;Text" ?value]]]]
- (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) &type/Text))))
+ (|do [_ (&type/check exo-type &type/Text)]
+ (return (&/|list (&/V "Expression" (&/T (&/V "text" ?value) exo-type)))))
[["lux;Meta" [meta ["lux;Tuple" ?elems]]]]
(&&lux/analyse-tuple analyse exo-type ?elems)
diff --git a/src/lux/analyser/base.clj b/src/lux/analyser/base.clj
index 0d2d8304a..35c12c3e0 100644
--- a/src/lux/analyser/base.clj
+++ b/src/lux/analyser/base.clj
@@ -37,9 +37,21 @@
(fail "[Analyser Error] Can't expand to other than 2 elements.")))))
(defn with-var [k]
- (|do [=var &type/fresh-var
+ (|do [=var &type/create-var
=ret (k =var)]
(matchv ::M/objects [=ret]
[["Expression" [?expr ?type]]]
- (|do [=type (&type/clean =var ?type)]
- (return (&/V "Expression" (&/T ?expr =type)))))))
+ (|do [id (&type/var-id =var)
+ =type (&type/clean id ?type)
+ :let [_ (prn 'with-var/CLEANING id)]
+ _ (&type/delete-var id)]
+ (return (&/V "Expression" (&/T ?expr =type))))
+
+ [_]
+ (assert false (pr-str '&&/with-var (aget =ret 0))))))
+
+(defmacro with-vars [vars body]
+ (reduce (fn [b v]
+ `(with-var (fn [~v] ~b)))
+ body
+ (reverse vars)))
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 6b2fe7a03..74d5ea5a3 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -8,93 +8,116 @@
[env :as &env])))
;; [Utils]
+(defn ^:private resolve-type [type]
+ (matchv ::M/objects [type]
+ [["lux;VarT" ?idx]]
+ (|do [type* (&type/deref ?idx)]
+ (resolve-type type*))
+
+ [_]
+ (&type/actual-type type)))
+
+(defn ^:private variant-case [case type]
+ (matchv ::M/objects [type]
+ [["lux;VariantT" ?cases]]
+ (if-let [case-type (&/|get case ?cases)]
+ (return case-type)
+ (fail (str "[Pattern-maching error] Variant lacks case: " case)))
+
+ [_]
+ (fail "[Pattern-maching error] Type is not a variant.")))
+
(defn ^:private analyse-variant [analyse-pattern idx value-type tag value]
(|do [[idx* test] (analyse-pattern idx value-type value)]
(return (&/T idx* (&/V "VariantTestAC" (&/T tag test))))))
(defn ^:private analyse-pattern [idx value-type pattern]
- (prn 'analyse-pattern/pattern (aget pattern 0) (aget pattern 1) (alength (aget pattern 1)))
+ ;; (prn 'analyse-pattern/pattern (aget pattern 0) (aget pattern 1) (alength (aget pattern 1)))
(matchv ::M/objects [pattern]
[["lux;Meta" [_ pattern*]]]
;; (assert false)
(do ;; (prn 'analyse-pattern/pattern* (aget pattern* 0))
- ;; (when (= "lux;Form" (aget pattern* 0))
- ;; (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons"
- ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta"
- ;; (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1)))
- ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag"
- ;; (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"]
- ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons"
- ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b>
- ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil"
- ;; )
- ;; ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
- ;; ["lux;Cons" [?value
- ;; ["lux;Nil" _]]]]]]
- (matchv ::M/objects [pattern*]
- [["lux;Symbol" [?module ?name]]]
- (return (&/T (inc idx) (&/V "StoreTestAC" (&/T idx (str ?module ";" ?name) value-type))))
-
- [["lux;Bool" ?value]]
- (|do [_ (&type/check value-type &type/Bool)]
- (return (&/T idx (&/V "BoolTestAC" ?value))))
-
- [["lux;Int" ?value]]
- (|do [_ (&type/check value-type &type/Int)]
- (return (&/T idx (&/V "IntTestAC" ?value))))
-
- [["lux;Real" ?value]]
- (|do [_ (&type/check value-type &type/Real)]
- (return (&/T idx (&/V "RealTestAC" ?value))))
-
- [["lux;Char" ?value]]
- (|do [_ (&type/check value-type &type/Char)]
- (return (&/T idx (&/V "CharTestAC" ?value))))
-
- [["lux;Text" ?value]]
- (|do [_ (&type/check value-type &type/Text)]
- (return (&/T idx (&/V "TextTestAC" ?value))))
-
- [["lux;Tuple" ?members]]
- (|do [=vars (&/map% (fn [_] &type/fresh-var)
- (&/|range (&/|length ?members)))
- _ (&type/check value-type (&/V "lux;TupleT" =vars))
- [idx* tests] (&/fold% (fn [idx+subs mv]
- (|let [[_idx subs] idx+subs
- [?member ?var] mv]
- (|do [[idx* test] (analyse-pattern _idx ?var ?member)]
- (return (&/T idx* (&/|cons test subs))))))
- (&/T idx (&/|list))
- (&/zip2 ?members =vars))]
- (return (&/T idx* (&/V "TupleTestAC" (&/|reverse tests)))))
-
- [["lux;Record" ?fields]]
- (|do [=vars (&/map% (fn [_] &type/fresh-var)
- (&/|range (&/|length ?fields)))
- _ (&type/check value-type (&/V "lux;RecordT" (&/zip2 (&/|keys ?fields) =vars)))
- tests (&/fold% (fn [idx+subs mv]
- (|let [[_idx subs] idx+subs
- [[slot value] ?var] mv]
- (|do [[idx* test] (analyse-pattern _idx ?var value)]
- (return (&/T idx* (&/|cons (&/T slot test) subs))))))
- (&/T idx (&/|list)) (&/zip2 ?fields =vars))]
- (return (&/V "RecordTestAC" tests)))
-
- [["lux;Tag" [?module ?name]]]
- (|do [module* (if (= "" ?module)
- &/get-module-name
- (return ?module))]
- (analyse-variant analyse-pattern idx value-type (str module* ";" ?name) (&/V "lux;Meta" (&/T (&/T "" -1 -1)
- (&/V "lux;Tuple" (&/|list))))))
-
- [["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
- ["lux;Cons" [?value
- ["lux;Nil" _]]]]]]]
- (|do [module* (if (= "" ?module)
- &/get-module-name
- (return ?module))]
- (analyse-variant analyse-pattern idx value-type (str module* ";" ?name) ?value))
- ))
+ ;; (when (= "lux;Form" (aget pattern* 0))
+ ;; (prn 'analyse-pattern/_2 (aget pattern* 1 0)) ;; "lux;Cons"
+ ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 0)) ;; "lux;Meta"
+ ;; (prn 'analyse-pattern/_2 (alength (aget pattern* 1 1 0 1)))
+ ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 0 1 1 0)) ;; "lux;Tag"
+ ;; (prn 'analyse-pattern/_2 [(aget pattern* 1 1 0 1 1 1 0) (aget pattern* 1 1 0 1 1 1 1)]) ;; ["" "Cons"]
+ ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 0)) ;; "lux;Cons"
+ ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 0)) ;; #<Object[] [Ljava.lang.Object;@63c7c38b>
+ ;; (prn 'analyse-pattern/_2 (aget pattern* 1 1 1 1 1 0)) ;; "lux;Nil"
+ ;; )
+ ;; ["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
+ ;; ["lux;Cons" [?value
+ ;; ["lux;Nil" _]]]]]]
+ (matchv ::M/objects [pattern*]
+ [["lux;Symbol" [?module ?name]]]
+ (return (&/T (inc idx) (&/V "StoreTestAC" (&/T idx (str ?module ";" ?name) value-type))))
+
+ [["lux;Bool" ?value]]
+ (|do [_ (&type/check value-type &type/Bool)]
+ (return (&/T idx (&/V "BoolTestAC" ?value))))
+
+ [["lux;Int" ?value]]
+ (|do [_ (&type/check value-type &type/Int)]
+ (return (&/T idx (&/V "IntTestAC" ?value))))
+
+ [["lux;Real" ?value]]
+ (|do [_ (&type/check value-type &type/Real)]
+ (return (&/T idx (&/V "RealTestAC" ?value))))
+
+ [["lux;Char" ?value]]
+ (|do [_ (&type/check value-type &type/Char)]
+ (return (&/T idx (&/V "CharTestAC" ?value))))
+
+ [["lux;Text" ?value]]
+ (|do [_ (&type/check value-type &type/Text)]
+ (return (&/T idx (&/V "TextTestAC" ?value))))
+
+ [["lux;Tuple" ?members]]
+ (|do [=vars (&/map% (constantly &type/create-var) ?members)
+ _ (&type/check value-type (&/V "lux;TupleT" =vars))
+ [idx* tests] (&/fold% (fn [idx+subs mv]
+ (|let [[_idx subs] idx+subs
+ [?member ?var] mv]
+ (|do [[idx* test] (analyse-pattern _idx ?var ?member)]
+ (return (&/T idx* (&/|cons test subs))))))
+ (&/T idx (&/|list))
+ (&/zip2 ?members =vars))]
+ (return (&/T idx* (&/V "TupleTestAC" (&/|reverse tests)))))
+
+ [["lux;Record" ?fields]]
+ (|do [=vars (&/map% (constantly &type/create-var) ?fields)
+ _ (&type/check value-type (&/V "lux;RecordT" (&/zip2 (&/|keys ?fields) =vars)))
+ tests (&/fold% (fn [idx+subs mv]
+ (|let [[_idx subs] idx+subs
+ [[slot value] ?var] mv]
+ (|do [[idx* test] (analyse-pattern _idx ?var value)]
+ (return (&/T idx* (&/|cons (&/T slot test) subs))))))
+ (&/T idx (&/|list)) (&/zip2 ?fields =vars))]
+ (return (&/V "RecordTestAC" tests)))
+
+ [["lux;Tag" [?module ?name]]]
+ (|do [module* (if (= "" ?module)
+ &/get-module-name
+ (return ?module))
+ :let [=tag (str module* ";" ?name)]
+ value-type* (resolve-type value-type)
+ case-type (variant-case =tag value-type*)]
+ (analyse-variant analyse-pattern idx case-type =tag (&/V "lux;Meta" (&/T (&/T "" -1 -1)
+ (&/V "lux;Tuple" (&/|list))))))
+
+ [["lux;Form" ["lux;Cons" [["lux;Meta" [_ ["lux;Tag" [?module ?name]]]]
+ ["lux;Cons" [?value
+ ["lux;Nil" _]]]]]]]
+ (|do [module* (if (= "" ?module)
+ &/get-module-name
+ (return ?module))
+ :let [=tag (str module* ";" ?name)]
+ value-type* (resolve-type value-type)
+ case-type (variant-case =tag value-type*)]
+ (analyse-variant analyse-pattern idx case-type =tag ?value))
+ ))
))
(defn ^:private with-test [test body]
@@ -127,9 +150,9 @@
(let [compare-kv #(compare (aget %1 0) (aget %2 0))]
(defn ^:private merge-total [struct test+body]
- (prn 'merge-total (aget struct 0) (class test+body))
- (prn 'merge-total (aget struct 0) (aget test+body 0))
- (prn 'merge-total (aget struct 0) (aget test+body 0 0))
+ ;; (prn 'merge-total (aget struct 0) (class test+body))
+ ;; (prn 'merge-total (aget struct 0) (aget test+body 0))
+ ;; (prn 'merge-total (aget struct 0) (aget test+body 0 0))
(matchv ::M/objects [test+body]
[[test ?body]]
(matchv ::M/objects [struct test]
@@ -222,49 +245,41 @@
[["MatchAC" ?tests]]
(&/fold% merge-total (&/V "DefaultTotal" false) ?tests))))
-(defn ^:private resolve-type [type]
- (matchv ::M/objects [type]
- [["lux;VarT" ?idx]]
- (&type/deref ?idx)
-
- [_]
- (return type)))
-
(defn ^:private check-totality [value-type struct]
(prn 'check-totality (aget value-type 0) (aget struct 0) (&type/show-type value-type))
- (matchv ::M/objects [value-type struct]
- [_ ["BoolTotal" [?total _]]]
+ (matchv ::M/objects [struct]
+ [["BoolTotal" [?total _]]]
(|do [_ (&type/check value-type &type/Bool)]
(return ?total))
- [_ ["IntTotal" [?total _]]]
+ [["IntTotal" [?total _]]]
(|do [_ (&type/check value-type &type/Int)]
(return ?total))
- [_ ["RealTotal" [?total _]]]
+ [["RealTotal" [?total _]]]
(|do [_ (&type/check value-type &type/Real)]
(return ?total))
- [_ ["CharTotal" [?total _]]]
+ [["CharTotal" [?total _]]]
(|do [_ (&type/check value-type &type/Char)]
(return ?total))
- [_ ["TextTotal" [?total _]]]
+ [["TextTotal" [?total _]]]
(|do [_ (&type/check value-type &type/Text)]
(return ?total))
- [_ ["TupleTotal" [?total ?structs]]]
- (|do [elems-vars (&/map% (constantly &type/fresh-var) (&/|range (&/|length ?structs)))
+ [["TupleTotal" [?total ?structs]]]
+ (|do [elems-vars (&/map% (constantly &type/create-var) ?structs)
_ (&type/check value-type (&/V "lux;TupleT" elems-vars))
totals (&/map% (fn [sv]
- (|let [[struct tvar] sv]
- (check-totality tvar struct)))
+ (|let [[sub-struct tvar] sv]
+ (check-totality tvar sub-struct)))
(&/zip2 ?structs elems-vars))]
(return (or ?total
(every? true? totals))))
- [_ ["RecordTotal" [?total ?structs]]]
- (|do [elems-vars (&/map% (constantly &type/fresh-var) (&/|range (&/|length ?structs)))
+ [["RecordTotal" [?total ?structs]]]
+ (|do [elems-vars (&/map% (constantly &type/create-var) ?structs)
:let [structs+vars (&/zip2 ?structs elems-vars)
record-type (&/V "lux;RecordT" (&/|map (fn [sv]
(|let [[[k v] tvar] sv]
@@ -278,13 +293,24 @@
(return (or ?total
(every? true? totals))))
- [_ ["VariantTotal" [?total ?structs]]]
+ [["VariantTotal" [?total ?structs]]]
(&/try-all% (&/|list (|do [real-type (resolve-type value-type)
- :let [_ (prn 'real-type (&type/show-type real-type))]]
- (assert false))
+ :let [_ (prn 'real-type/_1 (&type/show-type real-type))]
+ veredicts (matchv ::M/objects [real-type]
+ [["lux;VariantT" ?cases]]
+ (&/map% (fn [case]
+ (|let [[ctag ctype] case]
+ (if-let [sub-struct (&/|get ctag ?structs)]
+ (check-totality ctype sub-struct)
+ (return ?total))))
+ ?cases)
+
+ [_]
+ (fail "[Pattern-maching error] Value is not a variant."))]
+ (return (&/fold #(and %1 %2) ?total veredicts)))
(fail "[Pattern-maching error] Can't pattern-match on an unknown variant type.")))
- [_ ["DefaultTotal" true]]
+ [["DefaultTotal" true]]
(return true)
))
diff --git a/src/lux/analyser/lambda.clj b/src/lux/analyser/lambda.clj
index 619c39766..ae049f50f 100644
--- a/src/lux/analyser/lambda.clj
+++ b/src/lux/analyser/lambda.clj
@@ -8,7 +8,7 @@
;; [Resource]
(defn with-lambda [self self-type arg arg-type body]
;; (prn 'with-lambda (&/|length self) (&/|length arg))
- (prn 'with-lambda [(aget self 0) (aget self 1)] [(aget arg 0) (aget arg 1)] (alength self) (alength arg))
+ ;; (prn 'with-lambda [(aget self 0) (aget self 1)] [(aget arg 0) (aget arg 1)] (alength self) (alength arg))
(|let [[?module1 ?name1] self
[?module2 ?name2] arg]
(&/with-closure
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index a9a42ffe3..32f65320a 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -19,9 +19,9 @@
;; [Exports]
(defn analyse-tuple [analyse exo-type ?elems]
- (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")
- (&type/show-type exo-type))
- (|do [members-vars (&/map% (constantly &type/fresh-var) ?elems)
+ ;; (prn 'analyse-tuple (str "[" (->> ?elems (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")) "]")
+ ;; (&type/show-type exo-type))
+ (|do [members-vars (&/map% (constantly &type/create-var) ?elems)
_ (&type/check exo-type (&/V "lux;TupleT" members-vars))
=elems (&/map% (fn [ve]
(|let [[=var elem] ve]
@@ -36,8 +36,8 @@
(defn analyse-variant [analyse exo-type ident ?value]
(|let [[?module ?name] ident]
- (do (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value))
- (|do [:let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
+ (do ;; (prn 'analyse-variant (str ?module ";" ?name) (&/show-ast ?value))
+ (|do [;; :let [_ (prn 'analyse-variant/exo-type (&type/show-type exo-type))]
module (if (= "" ?module)
&/get-module-name
(return ?module))
@@ -53,13 +53,15 @@
[_]
(&type/actual-type exo-type))
- :let [_ (prn 'exo-type* (&type/show-type exo-type*))]]
+ ;; :let [_ (prn 'analyse-variant/exo-type* (&type/show-type exo-type*))]
+ ]
(matchv ::M/objects [exo-type*]
[["lux;VariantT" ?cases]]
(if-let [vtype (&/|get ?tag ?cases)]
- (|do [:let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
+ (|do [;; :let [_ (prn 'VARIANT_BODY ?tag (&/show-ast ?value) (&type/show-type vtype))]
=value (&&/analyse-1 analyse vtype ?value)
- :let [_ (prn 'GOT_VALUE =value)]]
+ ;; :let [_ (prn 'GOT_VALUE =value)]
+ ]
(return (&/|list (&/V "Expression" (&/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*))))
@@ -178,47 +180,79 @@
_ (&/assert! (> num-branches 0) "[Analyser Error] Can't have empty branches in \"case'\" expression.")
_ (&/assert! (even? num-branches) "[Analyser Error] Unbalanced branches in \"case'\" expression.")
=value ((analyse-1+ analyse) ?value)
+ :let [_ (prn 'analyse-case/GOT_VALUE)]
=value-type (&&/expr-type =value)
- =match (&&case/analyse-branches analyse exo-type =value-type (&/|as-pairs ?branches))]
+ =match (&&case/analyse-branches analyse exo-type =value-type (&/|as-pairs ?branches))
+ :let [_ (prn 'analyse-case/GOT_MATCH)]]
(return (&/|list (&/V "Expression" (&/T (&/V "case" (&/T =value =match))
exo-type))))))
-(defn analyse-lambda [analyse exo-type ?self ?arg ?body]
+(defn analyse-lambda* [analyse exo-type ?self ?arg ?body]
;; (prn 'analyse-lambda ?self ?arg ?body)
- (|do [=lambda-type* &type/fresh-lambda
- _ (&type/check exo-type =lambda-type*)]
- (matchv ::M/objects [=lambda-type*]
- [["lux;LambdaT" [=arg =return]]]
- (|do [[=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
- ?arg =arg
- (&&/analyse-1 analyse =return ?body))
- =lambda-type** (&type/clean =return =lambda-type*)
- =lambda-type (matchv ::M/objects [=arg]
- [["lux;VarT" ?id]]
- (&/try-all% (&/|list (|do [bound (&type/deref ?id)]
- (&type/clean =arg =lambda-type**))
- (let [var-name (str (gensym ""))]
- (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))
- lambda-type (&type/clean =arg =lambda-type**)]
- (return (&/V "lux;AllT" (&/T (&/|list) "" var-name lambda-type)))))))
+ (|do [lambda-expr (&&/with-vars [=arg =return]
+ (|do [:let [_ (prn 'analyse-lambda/_-1 (&type/show-type =arg) (&type/show-type =return))]
+ :let [=lambda-type* (&/V "lux;LambdaT" (&/T =arg =return))]
+ :let [_ (prn 'analyse-lambda/_0)]
+ _ (&type/check exo-type =lambda-type*)
+ :let [_ (prn 'analyse-lambda/_0.5 (&type/show-type exo-type))]
+ :let [_ (prn 'analyse-lambda/_1 (&type/show-type =lambda-type*))]
+ _ (|do [aid (&type/var-id =arg)
+ atype (&type/deref aid)
+ rid (&type/var-id =return)
+ rtype (&type/deref rid)
+ :let [_ (prn 'analyse-lambda/_1.5 (&type/show-type atype) (&type/show-type rtype))]]
+ (return nil))
+ [=scope =captured =body] (&&lambda/with-lambda ?self =lambda-type*
+ ?arg =arg
+ (&&/analyse-1 analyse =return ?body))
+ :let [_ (prn 'analyse-lambda/_2)]
+ =lambda-type (matchv ::M/objects [=arg]
+ [["lux;VarT" ?id]]
+ (|do [? (&type/bound? ?id)]
+ (if ?
+ (return =lambda-type*)
+ (let [var-name (str (gensym ""))]
+ (|do [_ (&type/set-var ?id (&/V "lux;BoundT" var-name))]
+ (return (&/V "lux;AllT" (&/T (&/|list) "" var-name =lambda-type*)))))))
+
+ [_]
+ (fail ""))
+ :let [_ (prn 'analyse-lambda/_3 (&type/show-type =lambda-type))]]
+ (return (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type)))))
+ :let [_ (prn 'analyse-lambda/_4)]]
+ (return lambda-expr)))
- [_]
- (fail ""))]
- (return (&/|list (&/V "Expression" (&/T (&/V "lambda" (&/T =scope =captured =body)) =lambda-type))))))))
+(defn analyse-lambda [analyse exo-type ?self ?arg ?body]
+ (prn 'analyse-lambda/&& (aget exo-type 0))
+ (|do [output (matchv ::M/objects [exo-type]
+ [["lux;AllT" _]]
+ (&&/with-var
+ (fn [$arg]
+ (|do [exo-type* (&type/apply-type exo-type $arg)
+ outputs (analyse-lambda analyse exo-type* ?self ?arg ?body)]
+ (return (&/|head outputs)))))
+
+ [_]
+ (analyse-lambda* analyse exo-type ?self ?arg ?body))]
+ (return (&/|list output))))
(defn analyse-def [analyse exo-type ?name ?value]
- (prn 'analyse-def ?name (&/show-ast ?value))
+ ;; (prn 'analyse-def/CODE ?name (&/show-ast ?value))
(|do [_ (&type/check exo-type &type/Nothing)
module-name &/get-module-name
? (&&def/defined? module-name ?name)]
(if ?
(fail (str "[Analyser Error] Can't redefine " ?name))
- (|do [=value (&/with-scope ?name
+ (|do [:let [_ (prn 'analyse-def/_0)]
+ =value (&/with-scope ?name
(&&/with-var
#(&&/analyse-1 analyse % ?value)))
+ :let [_ (prn 'analyse-def/_1)]
=value-type (&&/expr-type =value)
- :let [_ (prn 'analyse-def ?name (&type/show-type =value-type))]
- _ (&&def/define module-name ?name =value-type)]
+ :let [_ (prn 'analyse-def/_2)]
+ ;; :let [_ (prn 'analyse-def/TYPE ?name (&type/show-type =value-type))]
+ _ (&&def/define module-name ?name =value-type)
+ :let [_ (prn 'analyse-def/_3)]]
(return (&/|list (&/V "Statement" (&/V "def" (&/T ?name =value)))))))))
(defn analyse-declare-macro [exo-type ident]
@@ -241,12 +275,12 @@
==type (eval! =type)
_ (&type/check exo-type ==type)
:let [_ (println "analyse-check#4" (&type/show-type ==type))]
- =value (&&/analyse-1 analyse exo-type ?value)
+ =value (&&/analyse-1 analyse ==type ?value)
:let [_ (println "analyse-check#5")]]
(matchv ::M/objects [=value]
[["Expression" [?expr ?expr-type]]]
(|do [:let [_ (println "analyse-check#6" (&type/show-type ?expr-type))]
- _ (&type/check ==type ?expr-type)
+ ;; _ (&type/check ==type ?expr-type)
:let [_ (println "analyse-check#7")]]
(return (&/|list (&/V "Expression" (&/T ?expr ==type))))))))
diff --git a/src/lux/base.clj b/src/lux/base.clj
index 91519eb0c..f9d3c9c23 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -87,6 +87,16 @@
(V "lux;Cons" (T (T slot value) table*))
(V "lux;Cons" (T (T k v) (|put slot value table*))))))
+(defn |remove [slot table]
+ (matchv ::M/objects [table]
+ [["lux;Nil" _]]
+ table
+
+ [["lux;Cons" [[k v] table*]]]
+ (if (= k slot)
+ table*
+ (V "lux;Cons" (T (T k v) (|remove slot table*))))))
+
(defn |merge [table1 table2]
;; (prn '|merge (aget table1 0) (aget table2 0))
(matchv ::M/objects [table2]
@@ -125,7 +135,7 @@
;; [Resources/Monads]
(defn fail [message]
(fn [_]
- (prn 'FAIL message)
+ ;; (prn 'FAIL message)
(V "lux;Left" message)))
(defn return [value]
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 0cd839cf2..4eeea30aa 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -7,6 +7,42 @@
(declare show-type)
;; [Util]
+(def Any (&/V "lux;AnyT" nil))
+(def Nothing (&/V "lux;NothingT" nil))
+(def Bool (&/V "lux;DataT" "java.lang.Boolean"))
+(def Int (&/V "lux;DataT" "java.lang.Long"))
+(def Real (&/V "lux;DataT" "java.lang.Double"))
+(def Char (&/V "lux;DataT" "java.lang.Character"))
+(def Text (&/V "lux;DataT" "java.lang.String"))
+(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)))
+ (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
+ (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
+ (&/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;VariantT" (&/|list (&/T "lux;AnyT" Unit)
+ (&/T "lux;NothingT" Unit)
+ (&/T "lux;DataT" Text)
+ (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type)))
+ (&/T "lux;VariantT" TypeEnv)
+ (&/T "lux;RecordT" TypeEnv)
+ (&/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;AppT" TypePair)
+ ))))
+ (&/V "lux;NothingT" nil)))))
+
(defn bound? [id]
(fn [state]
(if-let [type* (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
@@ -16,21 +52,21 @@
[["lux;None" _]]
(return* state false))
- (fail* (str "Unknown type-var: " id)))))
+ (fail* (str "[Type Error] Unknown type-var: " id)))))
(defn deref [id]
(fn [state]
(let [mappings (->> state (&/get$ "lux;types") (&/get$ "lux;mappings"))]
(do (prn 'deref/mappings (&/->seq (&/|keys mappings)))
(if-let [type* (->> mappings (&/|get id))]
- (do (prn 'deref/type* (aget type* 0))
+ (do ;; (prn 'deref/type* (aget type* 0))
(matchv ::M/objects [type*]
[["lux;Some" type]]
(return* state type)
[["lux;None" _]]
- (fail* (str "Unbound type-var: " id))))
- (fail* (str "Unknown type-var: " id)))))))
+ (fail* (str "[Type Error] Unbound type-var: " id))))
+ (fail* (str "[Type Error] Unknown type-var: " id)))))))
(defn set-var [id type]
(fn [state]
@@ -38,17 +74,17 @@
(do ;; (prn 'set-var (aget tvar 0))
(matchv ::M/objects [tvar]
[["lux;Some" bound]]
- (fail* (str "Can't rebind type var: " id " | Current type: " (show-type bound)))
+ (fail* (str "[Type Error] Can't rebind type var: " id " | Current type: " (show-type bound)))
[["lux;None" _]]
(return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|put id (&/V "lux;Some" type) %)
ts))
state)
nil)))
- (fail* (str "Unknown type-var: " id)))))
+ (fail* (str "[Type Error] Unknown type-var: " id)))))
;; [Exports]
-(def fresh-var
+(def create-var
(fn [state]
(let [id (->> state (&/get$ "lux;types") (&/get$ "lux;counter"))]
(return* (&/update$ "lux;types" #(->> %
@@ -57,59 +93,79 @@
state)
(&/V "lux;VarT" id)))))
-(def fresh-lambda
- (|do [=arg fresh-var
- =return fresh-var]
- (return (&/V "lux;LambdaT" (&/T =arg =return)))))
-
-(defn clean [tvar type]
- (matchv ::M/objects [tvar]
- [["lux;VarT" ?tid]]
- (matchv ::M/objects [type]
- [["lux;VarT" ?id]]
- (if (= ?tid ?id)
- (|do [=type (deref ?id)]
- (clean tvar =type))
- (return type))
-
- [["lux;LambdaT" [?arg ?return]]]
- (|do [=arg (clean tvar ?arg)
- =return (clean tvar ?return)]
- (return (&/V "lux;LambdaT" (&/T =arg =return))))
-
- [["lux;AppT" [?lambda ?param]]]
- (|do [=lambda (clean tvar ?lambda)
- =param (clean tvar ?param)]
- (return (&/V "lux;AppT" (&/T =lambda =param))))
-
- [["lux;TupleT" ?members]]
- (|do [=members (&/map% (partial clean tvar) ?members)]
- (return (&/V "lux;TupleT" =members)))
-
- [["lux;VariantT" ?members]]
- (|do [=members (&/map% (fn [[k v]]
- (|do [=v (clean tvar v)]
- (return (&/T k =v))))
- ?members)]
- (return (&/V "lux;VariantT" =members)))
-
- [["lux;RecordT" ?members]]
- (|do [=members (&/map% (fn [[k v]]
- (|do [=v (clean tvar v)]
- (return (&/T k =v))))
- ?members)]
- (return (&/V "lux;RecordT" =members)))
-
- [["lux;AllT" [?env ?name ?arg ?body]]]
- (|do [=env (&/map% (fn [[k v]]
- (|do [=v (clean tvar v)]
- (return (&/T k =v))))
- ?env)]
- (return (&/V "lux;AllT" (&/T =env ?name ?arg ?body))))
-
- [_]
- (return type)
- )))
+(defn delete-var [id]
+ (fn [state]
+ (prn 'delete-var id)
+ (if-let [tvar (->> state (&/get$ "lux;types") (&/get$ "lux;mappings") (&/|get id))]
+ (return* (&/update$ "lux;types" (fn [ts] (&/update$ "lux;mappings" #(&/|remove id %)
+ ts))
+ state)
+ nil)
+ (fail* (str "[Type Error] Unknown type-var: " id)))))
+
+(defn var-id [type]
+ (matchv ::M/objects [type]
+ [["lux;VarT" ?id]]
+ (return ?id)
+
+ [_]
+ (fail (str "[Type Error] Not type-var: " (show-type type)))))
+
+(defn clean [?tid type]
+ (matchv ::M/objects [type]
+ [["lux;VarT" ?id]]
+ (if (= ?tid ?id)
+ (|do [=type (deref ?id)]
+ (clean ?tid =type))
+ (return type))
+
+ [["lux;LambdaT" [?arg ?return]]]
+ (|do [=arg (clean ?tid ?arg)
+ =return (clean ?tid ?return)]
+ (return (&/V "lux;LambdaT" (&/T =arg =return))))
+
+ [["lux;AppT" [?lambda ?param]]]
+ (|do [=lambda (clean ?tid ?lambda)
+ =param (clean ?tid ?param)]
+ (return (&/V "lux;AppT" (&/T =lambda =param))))
+
+ [["lux;TupleT" ?members]]
+ (|do [=members (&/map% (partial clean ?tid) ?members)]
+ (return (&/V "lux;TupleT" =members)))
+
+ [["lux;VariantT" ?members]]
+ (|do [=members (&/map% (fn [[k v]]
+ (|do [=v (clean ?tid v)]
+ (return (&/T k =v))))
+ ?members)]
+ (return (&/V "lux;VariantT" =members)))
+
+ [["lux;RecordT" ?members]]
+ (|do [=members (&/map% (fn [[k v]]
+ (|do [=v (clean ?tid v)]
+ (return (&/T k =v))))
+ ?members)]
+ (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)
+ body* (clean ?tid ?body)]
+ (return (&/V "lux;AllT" (&/T =env ?name ?arg body*))))
+
+ [_]
+ (return type)
+ ))
+
+(defn with-var [k]
+ (|do [=var create-var
+ id (var-id =var)
+ type (k =var)]
+ (|do [type* (clean id type)
+ _ (delete-var id)]
+ (return type*))))
(defn show-type [type]
;; (prn 'show-type (aget type 0))
@@ -167,80 +223,88 @@
))
(defn type= [x y]
- (matchv ::M/objects [x y]
- [["lux;AnyT" _] ["lux;AnyT" _]]
- true
-
- [["lux;NothingT" _] ["lux;NothingT" _]]
- true
-
- [["lux;DataT" xname] ["lux;DataT" yname]]
- (= xname yname)
-
- [["lux;TupleT" xelems] ["lux;TupleT" yelems]]
- (&/fold (fn [old xy] (and old (type= (aget xy 0) (aget xy 1))))
- true
- (&/zip2 xelems yelems))
-
- [["lux;VariantT" xcases] ["lux;VariantT" ycases]]
- (&/fold (fn [old cases]
- (matchv ::M/objects [cases]
- [[[xtag xtype] [ytag ytype]]]
- (and (= xtag ytag)
- (type= xtype ytype))))
- true (&/zip2 xcases ycases))
-
-
- [["lux;RecordT" xfields] ["lux;RecordT" yfields]]
- (&/fold (fn [old cases]
- (matchv ::M/objects [cases]
- [[[xtag xtype] [ytag ytype]]]
- (and (= xtag ytag)
- (type= xtype ytype))))
- true (&/zip2 xfields yfields))
-
- [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]]
- (and (type= xinput yinput)
- (type= xoutput youtput))
-
- [["lux;VarT" xid] ["lux;VarT" yid]]
- (= xid yid)
-
- [["lux;BoundT" xname] ["lux;BoundT" yname]]
- (= xname yname)
-
- [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]]
- (and (type= xlambda ylambda)
- (type= xparam yparam))
-
- [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]]
- (and (&/fold (fn [old cases]
- (matchv ::M/objects [cases]
- [[[xtag xtype] [ytag ytype]]]
- (and (= xtag ytag)
- (type= xtype ytype))))
- true (&/zip2 xenv yenv))
- (= xname yname)
- (= xarg yarg)
- (type= xbody ybody))
-
- [_ _]
- (do ;; (prn 'type= (show-type x) (show-type y))
- false)
- ))
-
-(defn ^:private fp-get [k xs]
- (matchv ::M/objects [k]
- [[e a]]
- (matchv ::M/objects [xs]
+ (let [output (matchv ::M/objects [x y]
+ [["lux;AnyT" _] ["lux;AnyT" _]]
+ true
+
+ [["lux;NothingT" _] ["lux;NothingT" _]]
+ true
+
+ [["lux;DataT" xname] ["lux;DataT" yname]]
+ (= xname yname)
+
+ [["lux;TupleT" xelems] ["lux;TupleT" yelems]]
+ (&/fold (fn [old xy]
+ (|let [[x* y*] xy]
+ (and old
+ (type= x* y*))))
+ true
+ (&/zip2 xelems yelems))
+
+ [["lux;VariantT" xcases] ["lux;VariantT" ycases]]
+ (and (= (&/|length xcases) (&/|length ycases))
+ (&/fold (fn [old case]
+ (and old
+ (type= (&/|get case xcases) (&/|get case ycases))))
+ true
+ (&/|keys xcases)))
+
+ [["lux;RecordT" xfields] ["lux;RecordT" yfields]]
+ (and (= (&/|length xfields) (&/|length yfields))
+ (&/fold (fn [old field]
+ (and old
+ (type= (&/|get field xfields) (&/|get field yfields))))
+ true
+ (&/|keys xfields)))
+
+ [["lux;LambdaT" [xinput xoutput]] ["lux;LambdaT" [yinput youtput]]]
+ (and (type= xinput yinput)
+ (type= xoutput youtput))
+
+ [["lux;VarT" xid] ["lux;VarT" yid]]
+ (= xid yid)
+
+ [["lux;BoundT" xname] ["lux;BoundT" yname]]
+ (= xname yname)
+
+ [["lux;AppT" [xlambda xparam]] ["lux;AppT" [ylambda yparam]]]
+ (and (type= xlambda ylambda)
+ (type= xparam yparam))
+
+ [["lux;AllT" [xenv xname xarg xbody]] ["lux;AllT" [yenv yname yarg ybody]]]
+ (do ;; (prn 'TESTING_ALLT
+ ;; '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))
+ ))
+
+ [_ _]
+ (do (prn 'type= (show-type x) (show-type y))
+ false)
+ )]
+ ;; (prn 'type= output (show-type x) (show-type y))
+ output))
+
+(defn ^:private fp-get [k fixpoints]
+ (|let [[e a] k]
+ (matchv ::M/objects [fixpoints]
[["lux;Nil" _]]
(&/V "lux;None" nil)
- [["lux;Cons" [[[e* a*] v*] xs*]]]
+ [["lux;Cons" [[[e* a*] v*] fixpoints*]]]
(if (and (type= e e*)
(type= a a*))
(&/V "lux;Some" v*)
- (fp-get k xs*))
+ (fp-get k fixpoints*))
)))
(defn ^:private fp-put [k v fixpoints]
@@ -315,7 +379,7 @@
(def init-fixpoints (&/|list))
(defn ^:private check* [fixpoints expected actual]
- (prn 'check* (aget expected 0) (aget actual 0))
+ ;; (prn 'check* (aget expected 0) (aget actual 0))
;; (prn 'check* (show-type expected) (show-type actual))
(matchv ::M/objects [expected actual]
[["lux;AnyT" _] _]
@@ -347,8 +411,17 @@
(check* fixpoints expected bound))))
[["lux;AppT" [F A]] _]
- (|do [expected* (apply-type F A)
- :let [fp-pair (&/T expected actual)]]
+ (let [fp-pair (&/T expected actual)
+ _ (prn 'LEFT_APP (&/|length fixpoints))
+ _ (when (> (&/|length fixpoints) 10)
+ (println 'FIXPOINTS (->> (&/|keys fixpoints)
+ (&/|map (fn [pair]
+ (|let [[e a] pair]
+ (str (show-type e) ":+:"
+ (show-type a)))))
+ (&/|interpose "\n\n")
+ (&/fold str "")))
+ (assert false))]
(matchv ::M/objects [(fp-get fp-pair fixpoints)]
[["lux;Some" ?]]
(if ?
@@ -356,21 +429,34 @@
(fail (check-error expected actual)))
[["lux;None" _]]
- (check* (fp-put fp-pair true fixpoints) expected* actual)))
+ (|do [expected* (apply-type F A)]
+ (check* (fp-put fp-pair true fixpoints) expected* actual))))
[_ ["lux;AppT" [F A]]]
(|do [actual* (apply-type F A)]
(check* fixpoints expected actual*))
[["lux;AllT" _] _]
- (|do [$var fresh-var
- expected* (apply-type expected $var)]
- (check* fixpoints expected* actual))
+ (with-var
+ (fn [$arg]
+ (|do [expected* (apply-type expected $arg)]
+ (check* fixpoints expected* actual))))
[_ ["lux;AllT" _]]
- (|do [$var fresh-var
- actual* (apply-type actual $var)]
- (check* fixpoints expected actual*))
+ (with-var
+ (fn [$arg]
+ (|do [actual* (apply-type actual $arg)]
+ (check* fixpoints expected actual*))))
+
+ ;; [["lux;AllT" _] _]
+ ;; (|do [$arg create-var
+ ;; expected* (apply-type expected $arg)]
+ ;; (check* fixpoints expected* actual))
+
+ ;; [_ ["lux;AllT" _]]
+ ;; (|do [$arg create-var
+ ;; actual* (apply-type actual $arg)]
+ ;; (check* fixpoints expected actual*))
[["lux;DataT" e!name] ["lux;DataT" a!name]]
(if (= e!name a!name)
@@ -382,8 +468,8 @@
(check* fixpoints* eO aO))
[["lux;TupleT" e!members] ["lux;TupleT" a!members]]
- (do (do (prn 'e!members (&/|length e!members))
- (prn 'a!members (&/|length a!members)))
+ (do ;; (do (prn 'e!members (&/|length e!members))
+ ;; (prn 'a!members (&/|length a!members)))
(if (= (&/|length e!members) (&/|length a!members))
(|do [fixpoints* (&/fold% (fn [fixp ea]
(|let [[e a] ea]
@@ -405,7 +491,7 @@
[["lux;VariantT" e!cases] ["lux;VariantT" a!cases]]
(if (= (&/|length e!cases) (&/|length a!cases))
(|do [fixpoints* (&/fold% (fn [fixp slot]
- (prn "lux;VariantT" slot)
+ (prn 'VARIANT_CASE slot)
(if-let [e!type (&/|get slot e!cases)]
(if-let [a!type (&/|get slot a!cases)]
(|do [[fixp* _] (check* fixp e!type a!type)]
@@ -420,7 +506,7 @@
[["lux;RecordT" e!fields] ["lux;RecordT" a!fields]]
(if (= (&/|length e!fields) (&/|length a!fields))
(|do [fixpoints* (&/fold% (fn [fixp slot]
- (prn "lux;RecordT" slot)
+ (prn 'RECORD_FIELD slot)
(if-let [e!type (&/|get slot e!fields)]
(if-let [a!type (&/|get slot a!fields)]
(|do [[fixp* _] (check* fixp e!type a!type)]
@@ -456,9 +542,10 @@
(return output))
[["lux;AllT" [local-env local-name local-arg local-def]]]
- (|do [$var fresh-var
- func* (apply-type func $var)]
- (apply-lambda func* param))
+ (with-var
+ (fn [$arg]
+ (|do [func* (apply-type func $arg)]
+ (apply-lambda func* param))))
[_]
(fail (str "[Type System] Can't apply type " (show-type func) " to type " (show-type param)))
@@ -473,39 +560,3 @@
[_]
(return type)
))
-
-(def Any (&/V "lux;AnyT" nil))
-(def Nothing (&/V "lux;NothingT" nil))
-(def Bool (&/V "lux;DataT" "java.lang.Boolean"))
-(def Int (&/V "lux;DataT" "java.lang.Long"))
-(def Real (&/V "lux;DataT" "java.lang.Double"))
-(def Char (&/V "lux;DataT" "java.lang.Character"))
-(def Text (&/V "lux;DataT" "java.lang.String"))
-(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)))
- (&/T "lux;Cons" (&/V "lux;TupleT" (&/|list (&/V "lux;BoundT" "a")
- (&/V "lux;AppT" (&/T (&/V "lux;BoundT" "List")
- (&/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;VariantT" (&/|list (&/T "lux;AnyT" Unit)
- (&/T "lux;NothingT" Unit)
- (&/T "lux;DataT" Text)
- (&/T "lux;TupleT" (&/V "lux;AppT" (&/T List Type)))
- (&/T "lux;VariantT" TypeEnv)
- (&/T "lux;RecordT" TypeEnv)
- (&/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;AppT" TypePair)
- ))))
- (&/V "lux;NothingT" nil)))))