aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/lux/type.clj14
-rw-r--r--test/test/lux/lexer.clj60
-rw-r--r--test/test/lux/parser.clj53
-rw-r--r--test/test/lux/reader.clj29
-rw-r--r--test/test/lux/type.clj473
5 files changed, 546 insertions, 83 deletions
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 70a2f69fa..295d7bfdb 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -756,21 +756,15 @@
[(&/$ExQ e!env e!def) _]
(with-var
(fn [$arg]
- (|do [:let [expected* (beta-reduce (->> e!env
- (&/$Cons $arg)
- (&/$Cons expected))
- e!def)]
+ (|do [expected* (apply-type expected $arg)
=output (check* class-loader fixpoints invariant?? expected* actual)
_ (clean $arg actual)]
(return =output))))
[_ (&/$ExQ a!env a!def)]
- (|do [$arg existential]
- (|let [actual* (beta-reduce (->> a!env
- (&/$Cons $arg)
- (&/$Cons expected))
- a!def)]
- (check* class-loader fixpoints invariant?? expected actual*)))
+ (|do [$arg existential
+ actual* (apply-type actual $arg)]
+ (check* class-loader fixpoints invariant?? expected actual*))
[(&/$HostT e!data) (&/$HostT a!data)]
(&&host/check-host-types (partial check* class-loader fixpoints true)
diff --git a/test/test/lux/lexer.clj b/test/test/lux/lexer.clj
index dc00c1d51..3bd45cb5f 100644
--- a/test/test/lux/lexer.clj
+++ b/test/test/lux/lexer.clj
@@ -5,11 +5,12 @@
(ns test.lux.lexer
(:use clojure.test)
- (:require (lux [base :as & :refer [deftags |do return* return fail fail* |let |case]]
+ (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
[reader :as &reader]
[lexer :as &lexer])
[lux.analyser.module :as &a-module]
- :reload-all))
+ :reload-all
+ ))
;; [Utils]
(def ^:private module-name "test")
@@ -37,7 +38,7 @@
(|case (&/run-state (|do [[_ single-line] &lexer/lex
[_ multi-line] &lexer/lex
[_ multi-line-embedded] &lexer/lex]
- (return (&/T single-line multi-line multi-line-embedded)))
+ (return (&/T [single-line multi-line multi-line-embedded])))
(make-state (str "##" input1 "\n" "#(" input2 ")#" "\n" "#(" input3 ")#")))
(&/$Right state [(&lexer/$Comment output1)
(&lexer/$Comment output2)
@@ -56,7 +57,7 @@
input2 "false"]
(|case (&/run-state (|do [[_ output1] &lexer/lex
[_ output2] &lexer/lex]
- (return (&/T output1 output2)))
+ (return (&/T [output1 output2])))
(make-state (str input1 "\n" input2)))
(&/$Right state [(&lexer/$Bool output1)
(&lexer/$Bool output2)])
@@ -75,7 +76,7 @@
(|case (&/run-state (|do [[_ output1] &lexer/lex
[_ output2] &lexer/lex
[_ output3] &lexer/lex]
- (return (&/T output1 output2 output3)))
+ (return (&/T [output1 output2 output3])))
(make-state (str input1 "\n" input2 "\n" input3)))
(&/$Right state [(&lexer/$Int output1)
(&lexer/$Int output2)
@@ -96,7 +97,7 @@
(|case (&/run-state (|do [[_ output1] &lexer/lex
[_ output2] &lexer/lex
[_ output3] &lexer/lex]
- (return (&/T output1 output2 output3)))
+ (return (&/T [output1 output2 output3])))
(make-state (str input1 "\n" input2 "\n" input3)))
(&/$Right state [(&lexer/$Real output1)
(&lexer/$Real output2)
@@ -129,7 +130,7 @@
[_ output7] &lexer/lex
[_ output8] &lexer/lex
[_ output9] &lexer/lex]
- (return (&/T output1 output2 output3 output4 output5 output6 output7 output8 output9)))
+ (return (&/T [output1 output2 output3 output4 output5 output6 output7 output8 output9])))
(make-state (str "#\"" input1 "\"" "\n" "#\"" input2 "\"" "\n" "#\"" input3 "\""
"\n" "#\"" input4 "\"" "\n" "#\"" input5 "\"" "\n" "#\"" input6 "\""
"\n" "#\"" input7 "\"" "\n" "#\"" input8 "\"" "\n" "#\"" input9 "\"")))
@@ -161,16 +162,13 @@
(let [input1 ""
input2 "abc"
input3 "yolo\\nlol\\tmeme"
- input4 "This is a test \\
- \\ of multi-line text. \\
-
- \\ I just wanna make sure it works alright..."]
+ input4 "This is a test\\nof multi-line text.\\n\\nI just wanna make sure it works alright..."]
(|case (&/run-state (|do [[_ output1] &lexer/lex
[_ output2] &lexer/lex
[_ output3] &lexer/lex
[_ output4] &lexer/lex]
- (return (&/T output1 output2 output3 output4)))
- (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"")))
+ (return (&/T [output1 output2 output3 output4])))
+ (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"" "\n" "\"" input4 "\"")))
(&/$Right state [(&lexer/$Text output1)
(&lexer/$Text output2)
(&lexer/$Text output3)
@@ -197,22 +195,22 @@
[_ output3] &lexer/lex
[_ output4] &lexer/lex
[_ output5] &lexer/lex]
- (return (&/T output1 output2 output3 output4 output5)))
- (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5)))
+ (return (&/T [output1 output2 output3 output4 output5])))
+ (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5 " ")))
(&/$Right state [(&lexer/$Symbol output1)
(&lexer/$Symbol output2)
(&lexer/$Symbol output3)
(&lexer/$Symbol output4)
(&lexer/$Symbol output5)])
(are [input output] (&/ident= input output)
- (&/T "" "foo") output1
- (&/T "test" "bar0123456789") output2
- (&/T "lux" "b1a2z3") output3
- (&/T "test" "quux") output4
- (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+ (&/T ["" "foo"]) output1
+ (&/T ["test" "bar0123456789"]) output2
+ (&/T ["lux" "b1a2z3"]) output3
+ (&/T ["test" "quux"]) output4
+ (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
_
- (is false "Couldn't read.")
+ (is false "Couldn't read")
)))
(deftest lex-tag
@@ -227,19 +225,19 @@
[_ output3] &lexer/lex
[_ output4] &lexer/lex
[_ output5] &lexer/lex]
- (return (&/T output1 output2 output3 output4 output5)))
- (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5)))
+ (return (&/T [output1 output2 output3 output4 output5])))
+ (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5 " ")))
(&/$Right state [(&lexer/$Tag output1)
(&lexer/$Tag output2)
(&lexer/$Tag output3)
(&lexer/$Tag output4)
(&lexer/$Tag output5)])
(are [input output] (&/ident= input output)
- (&/T "" "foo") output1
- (&/T "test" "bar0123456789") output2
- (&/T "lux" "b1a2z3") output3
- (&/T "test" "quux") output4
- (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+ (&/T ["" "foo"]) output1
+ (&/T ["test" "bar0123456789"]) output2
+ (&/T ["lux" "b1a2z3"]) output3
+ (&/T ["test" "quux"]) output4
+ (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
_
(is false "Couldn't read.")
@@ -259,7 +257,7 @@
[_ output4] &lexer/lex
[_ output5] &lexer/lex
[_ output6] &lexer/lex]
- (return (&/T output1 output2 output3 output4 output5 output6)))
+ (return (&/T [output1 output2 output3 output4 output5 output6])))
(make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5 "\n" input6)))
(&/$Right state [(&lexer/$Open_Paren)
(&lexer/$Close_Paren)
@@ -273,4 +271,6 @@
(is false "Couldn't read.")
)))
-;; (run-all-tests)
+(comment
+ (run-all-tests)
+ )
diff --git a/test/test/lux/parser.clj b/test/test/lux/parser.clj
index 13bd3500c..29e916b74 100644
--- a/test/test/lux/parser.clj
+++ b/test/test/lux/parser.clj
@@ -6,7 +6,7 @@
(ns test.lux.parser
(:use (clojure test
template))
- (:require (lux [base :as & :refer [deftags |do return* return fail fail* |let |case]]
+ (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
[reader :as &reader]
[parser :as &parser])
[lux.analyser.module :as &a-module]
@@ -147,17 +147,20 @@
(deftest parse-text
(let [input1 ""
input2 "abc"
- input3 "yolo\\nlol\\tmeme"]
+ input3 "yolo\\nlol\\tmeme"
+ input4 "This is a test\\nof multi-line text.\\n\\nI just wanna make sure it works alright..."]
(|case (&/run-state (|do [output1 &parser/parse
output2 &parser/parse
- output3 &parser/parse]
- (return (&/|++ output1 (&/|++ output2 output3))))
- (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"")))
- (&/$Right state (&/$Cons [_ (&/$TextS output1)] (&/$Cons [_ (&/$TextS output2)] (&/$Cons [_ (&/$TextS output3)] (&/$Nil)))))
+ output3 &parser/parse
+ output4 &parser/parse]
+ (return (&/|++ output1 (&/|++ output2 (&/|++ output3 output4)))))
+ (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"" "\n" "\"" input4 "\"")))
+ (&/$Right state (&/$Cons [_ (&/$TextS output1)] (&/$Cons [_ (&/$TextS output2)] (&/$Cons [_ (&/$TextS output3)] (&/$Cons [_ (&/$TextS output4)] (&/$Nil))))))
(are [input output] (= input output)
input1 output1
input2 output2
- "yolo\nlol\tmeme" output3)
+ "yolo\nlol\tmeme" output3
+ "This is a test\nof multi-line text.\n\nI just wanna make sure it works alright..." output4)
_
(is false "Couldn't read.")
@@ -176,7 +179,7 @@
output4 &parser/parse
output5 &parser/parse]
(return (&/|++ output1 (&/|++ output2 (&/|++ output3 (&/|++ output4 output5))))))
- (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5)))
+ (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5 " ")))
(&/$Right state (&/$Cons [_ (&/$SymbolS output1)]
(&/$Cons [_ (&/$SymbolS output2)]
(&/$Cons [_ (&/$SymbolS output3)]
@@ -184,11 +187,11 @@
(&/$Cons [_ (&/$SymbolS output5)]
(&/$Nil)))))))
(are [input output] (&/ident= input output)
- (&/T "" "foo") output1
- (&/T "test" "bar0123456789") output2
- (&/T "lux" "b1a2z3") output3
- (&/T "test" "quux") output4
- (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+ (&/T ["" "foo"]) output1
+ (&/T ["test" "bar0123456789"]) output2
+ (&/T ["lux" "b1a2z3"]) output3
+ (&/T ["test" "quux"]) output4
+ (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
_
(is false "Couldn't read.")
@@ -207,7 +210,7 @@
output4 &parser/parse
output5 &parser/parse]
(return (&/|++ output1 (&/|++ output2 (&/|++ output3 (&/|++ output4 output5))))))
- (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5)))
+ (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5 " ")))
(&/$Right state (&/$Cons [_ (&/$TagS output1)]
(&/$Cons [_ (&/$TagS output2)]
(&/$Cons [_ (&/$TagS output3)]
@@ -215,11 +218,11 @@
(&/$Cons [_ (&/$TagS output5)]
(&/$Nil)))))))
(are [input output] (&/ident= input output)
- (&/T "" "foo") output1
- (&/T "test" "bar0123456789") output2
- (&/T "lux" "b1a2z3") output3
- (&/T "test" "quux") output4
- (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+ (&/T ["" "foo"]) output1
+ (&/T ["test" "bar0123456789"]) output2
+ (&/T ["lux" "b1a2z3"]) output3
+ (&/T ["test" "quux"]) output4
+ (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
_
(is false "Couldn't read.")
@@ -236,10 +239,10 @@
(&/$Cons [_ (&/$TagS tagv)]
(&/$Nil))))))]
(&/$Nil)))
- (do (is (&/ident= (&/T "" "yolo") symv))
+ (do (is (&/ident= (&/T ["" "yolo"]) symv))
(is (= 123 intv))
(is (= "lol" textv))
- (is (&/ident= (&/T "" "meme") tagv)))
+ (is (&/ident= (&/T ["" "meme"]) tagv)))
_
(is false "Couldn't read.")
@@ -257,13 +260,15 @@
(&/$Cons [[_ (&/$TextS textv)] [_ (&/$TagS tagv)]]
(&/$Nil))))]
(&/$Nil)))
- (do (is (&/ident= (&/T "" "yolo") symv))
+ (do (is (&/ident= (&/T ["" "yolo"]) symv))
(is (= 123 intv))
(is (= "lol" textv))
- (is (&/ident= (&/T "" "meme") tagv)))
+ (is (&/ident= (&/T ["" "meme"]) tagv)))
_
(is false "Couldn't read.")
)))
-(run-all-tests)
+(comment
+ (run-all-tests)
+ )
diff --git a/test/test/lux/reader.clj b/test/test/lux/reader.clj
index ca4797f10..ee9cb4c35 100644
--- a/test/test/lux/reader.clj
+++ b/test/test/lux/reader.clj
@@ -5,7 +5,7 @@
(ns test.lux.reader
(:use clojure.test)
- (:require (lux [base :as & :refer [deftags |do return* return fail fail* |let |case]]
+ (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
[reader :as &reader])
:reload-all))
@@ -15,13 +15,13 @@
;; [Tests]
(deftest test-source-code-reading
- (is (= 4 (&/|length source))))
+ (is (= 5 (&/|length source))))
(deftest test-text-reading
;; Should be capable of recognizing literal texts.
(let [input "lo"]
(|case (&/run-state (&reader/read-text input) init-state)
- (&/$Right state [cursor output])
+ (&/$Right state [cursor end-line? output])
(is (= input output))
_
@@ -31,19 +31,8 @@
(deftest test-regex-reading
;; Should be capable of matching simple, grouping regex-patterns.
(|case (&/run-state (&reader/read-regex #"l(.)l") init-state)
- (&/$Right state [cursor output])
- (is (= "lol" "lol"))
-
- _
- (is false "Couldn't read.")
- ))
-
-(deftest test-regex2-reading
- ;; Should be capable of matching double, grouping regex-patterns.
- (|case (&/run-state (&reader/read-regex2 #"(.)(..)") init-state)
- (&/$Right state [cursor [left right]])
- (is (and (= "l" left)
- (= "ol" right)))
+ (&/$Right state [cursor end-line? output])
+ (is (= "lol" output))
_
(is false "Couldn't read.")
@@ -51,12 +40,14 @@
(deftest test-regex+-reading
;; Should be capable of matching multi-line regex-patterns.
- (|case (&/run-state (&reader/read-regex+ #"(?is)^(.*?)(cat|$)") init-state)
+ (|case (&/run-state (&reader/read-regex+ #"(?is)^((?!cat).)*") init-state)
(&/$Right state [cursor output])
- (is (= "lol\nmeme\nnyan " output))
+ (is (= "\nlol\nmeme\nnyan " output))
_
(is false "Couldn't read.")
))
-;; (run-all-tests)
+(comment
+ (run-all-tests)
+ )
diff --git a/test/test/lux/type.clj b/test/test/lux/type.clj
new file mode 100644
index 000000000..1a43f7cc4
--- /dev/null
+++ b/test/test/lux/type.clj
@@ -0,0 +1,473 @@
+;; Copyright (c) Eduardo Julian. All rights reserved.
+;; This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+;; If a copy of the MPL was not distributed with this file,
+;; You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(ns test.lux.type
+ (:use clojure.test)
+ (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
+ [type :as &type])
+ :reload-all
+ ))
+
+;; [Tests]
+(deftest check-base-types
+ (|case (&/run-state (|do [_ (&type/check &/$UnitT &/$UnitT)
+
+ _ (&type/check &/$VoidT &/$VoidT)]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-simple-host-types
+ (|case (&/run-state (|do [_ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+
+ _ (&type/check (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-complex-host-types
+ (|case (&/run-state (|do [_ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Object" &/$Nil)))
+ (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$HostT "java.util.ArrayList" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil))))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-named-types
+ (|case (&/run-state (|do [_ (&type/check (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+
+ _ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil)))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-sum-types
+ (|case (&/run-state (|do [_ (&type/check (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Object" &/$Nil))
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Object" &/$Nil)))
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-prod-types
+ (|case (&/run-state (|do [_ (&type/check (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Object" &/$Nil))
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Object" &/$Nil)))
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-lambda-types
+ (|case (&/run-state (|do [_ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Object" &/$Nil))
+ (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+
+ _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Object" &/$Nil)))
+ (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
+ (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
+ (&/$HostT "java.lang.Boolean" &/$Nil))))
+ ]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-ex-types
+ (|case (&/run-state (|do [_ (&type/check (&/$ExT 0) (&/$ExT 0))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-univ-quantification
+ (|case (&/run-state (|do [_ (&type/check (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1))))
+
+ _ (&type/check (&/$UnivQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1)))
+ (&/$UnivQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1))))
+
+ _ (&type/check (&/$UnivQ (&/|list)
+ (&/$SumT
+ ;; lux;Nil
+ &/$UnitT
+ ;; lux;Cons
+ (&/$ProdT (&/$BoundT 1)
+ (&/$AppT (&/$BoundT 0)
+ (&/$BoundT 1)))))
+ (&/$UnivQ (&/|list)
+ (&/$SumT
+ ;; lux;Nil
+ &/$UnitT
+ ;; lux;Cons
+ (&/$ProdT (&/$BoundT 1)
+ (&/$AppT (&/$BoundT 0)
+ (&/$BoundT 1))))))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-ex-quantification
+ (|case (&/run-state (|do [_ (&type/check (&/$ExQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$ExQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1))))
+
+ _ (&type/check (&/$ExQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1)))
+ (&/$ExQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1))))
+
+ _ (&type/check (&/$ExQ (&/|list)
+ (&/$SumT
+ ;; lux;Nil
+ &/$UnitT
+ ;; lux;Cons
+ (&/$ProdT (&/$BoundT 1)
+ (&/$AppT (&/$BoundT 0)
+ (&/$BoundT 1)))))
+ (&/$ExQ (&/|list)
+ (&/$SumT
+ ;; lux;Nil
+ &/$UnitT
+ ;; lux;Cons
+ (&/$ProdT (&/$BoundT 1)
+ (&/$AppT (&/$BoundT 0)
+ (&/$BoundT 1))))))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-app-type
+ (|case (&/run-state (|do [_ (&type/check (&/$AppT (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$AppT (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$AppT (&/$UnivQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1)))
+ (&/$HostT "java.lang.Object" &/$Nil))
+ (&/$AppT (&/$UnivQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$AppT (&/$ExQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$AppT (&/$ExQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+
+ _ (&type/check (&/$AppT (&/$ExQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1)))
+ (&/$HostT "java.lang.Object" &/$Nil))
+ (&/$AppT (&/$ExQ (&/|list)
+ (&/$SumT
+ ;; lux;None
+ &/$UnitT
+ ;; lux;Some
+ (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil)))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(deftest check-var-type
+ (|case (&/run-state (|do [_ (&type/with-var
+ (fn [$var]
+ (|do [_ (&type/check $var (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+ (return nil))))
+
+ _ (&type/with-var
+ (fn [$var]
+ (|do [_ (&type/check (&/$AppT (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ $var)
+ (&/$AppT (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil)))
+ (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+ (return nil))))
+
+ _ (&type/with-var
+ (fn [$var]
+ (|do [_ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil) $var)
+ (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+ (return nil))))
+
+ _ (&type/with-var
+ (fn [$var]
+ (|do [_ (&type/check (&/$AppT (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ (&/$HostT "java.lang.Boolean" &/$Nil))
+ (&/$AppT (&/$UnivQ (&/|list)
+ (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+ $var))
+ (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+ (return nil))))
+
+ _ (&type/with-var
+ (fn [$var1]
+ (&type/with-var
+ (fn [$var2]
+ (|do [_ (&type/check $var1 $var2)]
+ (return nil))))))
+
+ _ (&type/with-var
+ (fn [$var1]
+ (&type/with-var
+ (fn [$var2]
+ (|do [_ (&type/check $var2 $var1)]
+ (return nil))))))
+
+ _ (&type/with-var
+ (fn [$var1]
+ (&type/with-var
+ (fn [$var2]
+ (|do [_ (&type/check $var1 $var2)
+ _ (&type/check $var1 (&/$HostT "java.lang.Boolean" (&/|list)))
+ =var1 (&type/deref+ $var1)
+ _ (&/assert! (&type/type= =var1 $var2) "")
+ =var2 (&type/deref+ $var2)
+ _ (&/assert! (&type/type= =var2 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+ (return nil))))))
+
+ _ (&type/with-var
+ (fn [$var1]
+ (&type/with-var
+ (fn [$var2]
+ (|do [_ (&type/check $var2 $var1)
+ _ (&type/check $var1 (&/$HostT "java.lang.Boolean" (&/|list)))
+ =var2 (&type/deref+ $var2)
+ _ (&/assert! (&type/type= =var2 $var1) "")
+ =var1 (&type/deref+ $var1)
+ _ (&/assert! (&type/type= =var1 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+ (return nil))))))
+
+ _ (&type/with-var
+ (fn [$var1]
+ (&type/with-var
+ (fn [$var2]
+ (|do [_ (&type/check $var1 $var2)
+ _ (&type/check $var2 (&/$HostT "java.lang.Boolean" (&/|list)))
+ =var1 (&type/deref+ $var1)
+ _ (&/assert! (&type/type= =var1 $var2) "")
+ =var2 (&type/deref+ $var2)
+ _ (&/assert! (&type/type= =var2 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+ (return nil))))))
+
+ _ (&type/with-var
+ (fn [$var1]
+ (&type/with-var
+ (fn [$var2]
+ (|do [_ (&type/check $var2 $var1)
+ _ (&type/check $var2 (&/$HostT "java.lang.Boolean" (&/|list)))
+ =var2 (&type/deref+ $var2)
+ _ (&/assert! (&type/type= =var2 $var1) "")
+ =var1 (&type/deref+ $var1)
+ _ (&/assert! (&type/type= =var1 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+ (return nil))))))]
+ (return nil))
+ (&/init-state nil))
+ (&/$Right state nil)
+ (is true)
+
+ (&/$Left error)
+ (is false error)
+ ))
+
+(comment
+ (run-all-tests)
+ )
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 14:43:06 +0000