From 512598de80963203cf162d2f353d43b47273ffaf Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Fri, 1 Jul 2016 19:06:04 -0400 Subject: - Small fixes to reader & type-system. - Test suites for reader, lexer and parser got updated. - Added unit-tests for type-system. --- src/lux/type.clj | 14 +- test/test/lux/lexer.clj | 60 +++--- test/test/lux/parser.clj | 53 +++--- test/test/lux/reader.clj | 29 +-- test/test/lux/type.clj | 473 +++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 546 insertions(+), 83 deletions(-) create mode 100644 test/test/lux/type.clj 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) + ) -- cgit v1.2.3