diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/test/aedifex.lux | 12 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/auto.lux | 43 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/build.lux | 12 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/clean.lux | 54 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/deploy.lux | 4 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/deps.lux | 7 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/install.lux | 4 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/pom.lux | 4 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/command/test.lux | 2 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/package.lux | 64 | ||||
| -rw-r--r-- | stdlib/source/test/aedifex/profile.lux | 2 | ||||
| -rw-r--r-- | stdlib/source/test/lux/type/check.lux | 835 |
12 files changed, 758 insertions, 285 deletions
diff --git a/stdlib/source/test/aedifex.lux b/stdlib/source/test/aedifex.lux index b7d0d29d9..8757242c5 100644 --- a/stdlib/source/test/aedifex.lux +++ b/stdlib/source/test/aedifex.lux @@ -15,9 +15,9 @@ ["#." input] ["#." local] ["#." metadata] - ## ["#." package] - ## ["#." profile] - ## ["#." project] + ["#." package] + ["#." profile] + ["#." project] ## ["#." parser] ## ["#." pom] ## ["#." repository] @@ -43,10 +43,10 @@ /input.test /local.test /metadata.test + /package.test + /profile.test + /project.test - ## /package.test - ## /profile.test - ## /project.test ## /parser.test ## /pom.test ## /repository.test diff --git a/stdlib/source/test/aedifex/command/auto.lux b/stdlib/source/test/aedifex/command/auto.lux index c23519bcc..7ef74d2c0 100644 --- a/stdlib/source/test/aedifex/command/auto.lux +++ b/stdlib/source/test/aedifex/command/auto.lux @@ -14,7 +14,9 @@ ["!" capability]]] [data ["." text - ["%" format (#+ format)]] + ["%" format (#+ format)] + [encoding + ["." utf8]]] [collection ["." dictionary] ["." set] @@ -27,7 +29,7 @@ [console (#+ Console)] ["." shell (#+ Shell)] ["." program (#+ Program)] - ["." file (#+ Path) + ["." file (#+ Path File) ["." watch]]]] ["." // #_ ["@." version] @@ -47,28 +49,22 @@ ["#." dependency ["#/." resolution (#+ Resolution)]]]]]}) -(def: (command end_signal dummy_files) - (-> Text (List Path) - [(Atom [Nat (List Path)]) +(def: (command expected_runs end_signal dummy_file) + (-> Nat Text (File Promise) + [(Atom Nat) (-> (Console Promise) (Program Promise) (file.System Promise) (Shell Promise) Resolution (Command Any))]) - (let [@runs (: (Atom [Nat (List Path)]) - (atom.atom [0 dummy_files]))] + (let [@runs (: (Atom Nat) + (atom.atom 0))] [@runs (function (_ console program fs shell resolution profile) (do {! promise.monad} - [[_ [runs remaining_files]] (promise.future - (atom.update (function (_ [runs remaining_files]) - [(inc runs) remaining_files]) - @runs))] - (case remaining_files - #.Nil + [[_ actual_runs] (promise.future (atom.update inc @runs))] + (if (n.= expected_runs actual_runs) (wrap (#try.Failure end_signal)) - - (#.Cons head tail) (do (try.with !) - [_ (!.use (\ fs create_file) [head])] + [_ (!.use (\ dummy_file over_write) (\ utf8.codec encode (%.nat actual_runs)))] (do ! - [_ (promise.future (atom.write [runs tail] @runs))] + [_ (promise.future (atom.write actual_runs @runs))] (wrap (#try.Success [])))))))])) (def: #export test @@ -85,7 +81,7 @@ #let [empty_profile (: Profile (\ ///.monoid identity)) with_target (: (-> Profile Profile) - (set@ #///.target (#.Some target))) + (set@ #///.target target)) with_program (: (-> Profile Profile) (set@ #///.program (#.Some program))) @@ -98,15 +94,14 @@ working_directory (random.ascii/alpha 5) expected_runs (\ ! map (|>> (n.% 10) (n.max 2)) random.nat) - dummy_files (|> (random.ascii/alpha 5) - (random.set text.hash (dec expected_runs)) - (\ ! map (|>> set.to_list (list\map (|>> (format source /)))))) + dummy_path (\ ! map (|>> (format source /)) (random.ascii/alpha 5)) resolution @build.resolution] ($_ _.and (wrap (do promise.monad [verdict (do ///action.monad - [#let [[@runs command] (..command end_signal dummy_files)] - _ (!.use (\ fs create_directory) [source]) + [_ (!.use (\ fs create_directory) [source]) + dummy_file (!.use (\ fs create_file) [dummy_path]) + #let [[@runs command] (..command expected_runs end_signal dummy_file)] _ (\ watcher poll [])] (do promise.monad [outcome ((/.do! 1 watcher command) @@ -116,7 +111,7 @@ (shell.async (@build.good_shell [])) resolution profile) - [actual_runs _] (promise.future (atom.read @runs))] + actual_runs (promise.future (atom.read @runs))] (wrap (#try.Success (and (n.= expected_runs actual_runs) (case outcome (#try.Failure error) diff --git a/stdlib/source/test/aedifex/command/build.lux b/stdlib/source/test/aedifex/command/build.lux index 234343fea..7fd8c3eb3 100644 --- a/stdlib/source/test/aedifex/command/build.lux +++ b/stdlib/source/test/aedifex/command/build.lux @@ -109,7 +109,7 @@ #let [empty_profile (: Profile (\ ///.monoid identity)) with_target (: (-> Profile Profile) - (set@ #///.target (#.Some target))) + (set@ #///.target target)) with_program (: (-> Profile Profile) (set@ #///.program (#.Some program))) @@ -128,16 +128,6 @@ (#try.Failure error) (exception.match? /.no_specified_program error))))) (wrap (do promise.monad - [outcome (/.do! (@version.echo "") (program.async (program.mock environment.empty home working_directory)) fs shell ///dependency/resolution.empty - (with_program empty_profile))] - (_.cover' [/.no_specified_target] - (case outcome - (#try.Success _) - false - - (#try.Failure error) - (exception.match? /.no_specified_target error))))) - (wrap (do promise.monad [outcome (/.do! (@version.echo "") (program.async (program.mock environment.empty home working_directory)) fs shell ///dependency/resolution.empty profile)] (_.cover' [/.Compiler /.no_available_compiler] (case outcome diff --git a/stdlib/source/test/aedifex/command/clean.lux b/stdlib/source/test/aedifex/command/clean.lux index d98473259..705cca7f2 100644 --- a/stdlib/source/test/aedifex/command/clean.lux +++ b/stdlib/source/test/aedifex/command/clean.lux @@ -99,35 +99,25 @@ sub_files (..files (format sub_path /)) dummy @profile.random] - ($_ _.and - (wrap (do promise.monad - [#let [console (@version.echo "")] - verdict (do {! (try.with promise.monad)} - [_ (/.do! console fs (set@ #///.target #.None dummy))] - (\ ! map (text\= /.failure) - (!.use (\ console read_line) [])))] - (_.cover' [/.failure] - (try.default false verdict)))) - (wrap (do promise.monad - [#let [console (@version.echo "")] - verdict (do {! (try.with promise.monad)} - [_ (..create_directory! fs target_path direct_files) - _ (..create_directory! fs sub_path sub_files) - context_exists!/pre (..directory_exists? fs context) - target_exists!/pre (..assets_exist? fs target_path direct_files) - sub_exists!/pre (..assets_exist? fs sub_path sub_files) - _ (/.do! console fs (set@ #///.target (#.Some target_path) dummy)) - context_exists!/post (..directory_exists? fs context) - target_exists!/post (..assets_exist? fs target_path direct_files) - sub_exists!/post (..assets_exist? fs sub_path sub_files) - logging (!.use (\ console read_line) [])] - (wrap (and (and context_exists!/pre - context_exists!/post) - (and target_exists!/pre - (not target_exists!/post)) - (and sub_exists!/pre - (not sub_exists!/post)) - (text\= /.success logging))))] - (_.cover' [/.do! /.success] - (try.default false verdict)))) - )))) + (wrap (do promise.monad + [#let [console (@version.echo "")] + verdict (do {! (try.with promise.monad)} + [_ (..create_directory! fs target_path direct_files) + _ (..create_directory! fs sub_path sub_files) + context_exists!/pre (..directory_exists? fs context) + target_exists!/pre (..assets_exist? fs target_path direct_files) + sub_exists!/pre (..assets_exist? fs sub_path sub_files) + _ (/.do! console fs (set@ #///.target target_path dummy)) + context_exists!/post (..directory_exists? fs context) + target_exists!/post (..assets_exist? fs target_path direct_files) + sub_exists!/post (..assets_exist? fs sub_path sub_files) + logging (!.use (\ console read_line) [])] + (wrap (and (and context_exists!/pre + context_exists!/post) + (and target_exists!/pre + (not target_exists!/post)) + (and sub_exists!/pre + (not sub_exists!/post)) + (text\= (/.success target_path) logging))))] + (_.cover' [/.do! /.success] + (try.default false verdict))))))) diff --git a/stdlib/source/test/aedifex/command/deploy.lux b/stdlib/source/test/aedifex/command/deploy.lux index cc99f2e48..7e1bf166e 100644 --- a/stdlib/source/test/aedifex/command/deploy.lux +++ b/stdlib/source/test/aedifex/command/deploy.lux @@ -123,7 +123,7 @@ (\ ///hash.md5_codec decode actual_md5))) #let [succeeded! - (text\= //clean.success logging) + (text\= /.success logging) deployed_library! (\ binary.equivalence = @@ -149,5 +149,5 @@ deployed_pom! deployed_sha-1! deployed_md5!)))] - (_.cover' [/.do!] + (_.cover' [/.do! /.success] (try.default false verdict))))))) diff --git a/stdlib/source/test/aedifex/command/deps.lux b/stdlib/source/test/aedifex/command/deps.lux index 8b5e3820e..2b4898dd3 100644 --- a/stdlib/source/test/aedifex/command/deps.lux +++ b/stdlib/source/test/aedifex/command/deps.lux @@ -107,9 +107,6 @@ (set@ #///.dependencies (set.from_list ///dependency.hash (list dependee depender))) (/.do! console local (list (///repository.mock ($///dependency/resolution.single depender_artifact depender_package) [])))) - logging! (\ ///action.monad map - (text\= //clean.success) - (!.use (\ console read_line) [])) #let [had_dependee_before! (set.member? pre dependee_artifact) @@ -122,9 +119,7 @@ had_depender_after! (dictionary.key? post depender)]] - (wrap (and logging! - - had_dependee_before! + (wrap (and had_dependee_before! lacked_depender_before! had_dependee_after! diff --git a/stdlib/source/test/aedifex/command/install.lux b/stdlib/source/test/aedifex/command/install.lux index 33ee7192d..8096fc2b2 100644 --- a/stdlib/source/test/aedifex/command/install.lux +++ b/stdlib/source/test/aedifex/command/install.lux @@ -92,7 +92,7 @@ library_path (format artifact_path ///artifact/extension.lux_library) pom_path (format artifact_path ///artifact/extension.pom)] - #let [succeeded! (text\= //clean.success logging)] + #let [succeeded! (text\= /.success logging)] library_exists! (\ promise.monad map exception.return (file.file_exists? promise.monad fs library_path)) @@ -102,7 +102,7 @@ (wrap (and succeeded! library_exists! pom_exists!)))] - (_.cover' [/.do!] + (_.cover' [/.do! /.success] (try.default false verdict)))) (wrap (do {! promise.monad} [#let [fs (file.mock (\ file.default separator)) diff --git a/stdlib/source/test/aedifex/command/pom.lux b/stdlib/source/test/aedifex/command/pom.lux index c368d5f84..f7f182225 100644 --- a/stdlib/source/test/aedifex/command/pom.lux +++ b/stdlib/source/test/aedifex/command/pom.lux @@ -54,7 +54,7 @@ actual (!.use (\ file content) []) logging! (\ ///action.monad map - (text\= //clean.success) + (text\= /.success) (!.use (\ console read_line) [])) #let [expected_path! @@ -65,7 +65,7 @@ (wrap (and logging! expected_path! expected_content!)))] - (_.cover' [/.do!] + (_.cover' [/.do! /.success] (try.default false verdict))) (#try.Failure error) diff --git a/stdlib/source/test/aedifex/command/test.lux b/stdlib/source/test/aedifex/command/test.lux index 6b7ba9324..291b31863 100644 --- a/stdlib/source/test/aedifex/command/test.lux +++ b/stdlib/source/test/aedifex/command/test.lux @@ -51,7 +51,7 @@ #let [empty_profile (: Profile (\ ///.monoid identity)) with_target (: (-> Profile Profile) - (set@ #///.target (#.Some target))) + (set@ #///.target target)) with_test (: (-> Profile Profile) (set@ #///.test (#.Some test))) diff --git a/stdlib/source/test/aedifex/package.lux b/stdlib/source/test/aedifex/package.lux index 960a75f21..132c51b38 100644 --- a/stdlib/source/test/aedifex/package.lux +++ b/stdlib/source/test/aedifex/package.lux @@ -2,13 +2,21 @@ [lux #* ["_" test (#+ Test)] [abstract - [monad (#+ do)]] + [monad (#+ do)] + {[0 #spec] + [/ + ["$." equivalence]]}] [control ["." try] [concurrency [promise (#+ Promise)]]] [data - ["." text] + ["." product] + ["." text + [encoding + ["." utf8]]] + [format + ["." xml (#+ XML)]] [collection ["." set (#+ Set)]]] [math @@ -27,9 +35,11 @@ ["." / ["/#" // #_ ["#" profile] - ["#." dependency (#+ Dependency)] ["#." pom] - ["#." hash]]]}) + [dependency + ["#." status]] + [repository + ["#." origin]]]]}) (def: #export random (Random [//.Profile /.Package]) @@ -51,15 +61,37 @@ (do {! random.monad} [[profile package] ..random] ($_ _.and + (_.for [/.equivalence] + ($equivalence.spec /.equivalence (\ ! map product.right ..random))) + + (_.cover [/.local?] + (/.local? (set@ #/.origin (#//origin.Local "~/yolo") package))) + (_.cover [/.remote?] + (/.remote? (set@ #/.origin (#//origin.Remote "https://example.com") package))) (_.cover [/.local] - false - ## (and (\ //hash.equivalence = - ## (//hash.sha-1 (get@ #/.library package)) - ## (get@ #/.sha-1 package)) - ## (\ //hash.equivalence = - ## (//hash.md5 (get@ #/.library package)) - ## (get@ #/.md5 package))) - ) + (let [expected_pom (|> package (get@ #/.pom) product.left) + expected_library (|> package (get@ #/.library) product.left) + + local (/.local expected_pom expected_library) + + [actual_pom binary_pom pom_status] (get@ #/.pom local) + [actual_library library_status] (get@ #/.library local)] + (and (case (get@ #/.origin local) + (#//origin.Local "") true + _ false) + (and (is? expected_library actual_library) + (case library_status + #//status.Unverified true + _ false)) + (and (is? expected_pom actual_pom) + (|> (do try.monad + [xml_pom (\ utf8.codec decode binary_pom) + decoded_pom (\ xml.codec decode xml_pom)] + (wrap (\ xml.equivalence = actual_pom decoded_pom))) + (try.default false)) + (case pom_status + #//status.Unverified true + _ false))))) (_.cover [/.dependencies] (let [expected (get@ #//.dependencies profile)] (case (/.dependencies package) @@ -68,4 +100,12 @@ (#try.Failure error) false))) + (_.cover [/.repositories] + (let [expected (get@ #//.repositories profile)] + (case (/.repositories package) + (#try.Success actual) + (\ set.equivalence = expected actual) + + (#try.Failure error) + false))) )))) diff --git a/stdlib/source/test/aedifex/profile.lux b/stdlib/source/test/aedifex/profile.lux index ea03a1e92..3410255f5 100644 --- a/stdlib/source/test/aedifex/profile.lux +++ b/stdlib/source/test/aedifex/profile.lux @@ -125,7 +125,7 @@ (..set_of text.hash ..repository) (..set_of //dependency.hash @dependency.random) (..set_of text.hash ..source) - (random.maybe ..target) + ..target (random.maybe (random.ascii/alpha 1)) (random.maybe (random.ascii/alpha 1)) (..dictionary_of text.hash (random.ascii/alpha 1) ..repository) diff --git a/stdlib/source/test/lux/type/check.lux b/stdlib/source/test/lux/type/check.lux index 45e648b9c..e6e0f4b16 100644 --- a/stdlib/source/test/lux/type/check.lux +++ b/stdlib/source/test/lux/type/check.lux @@ -1,20 +1,29 @@ (.module: [lux (#- type) - ["%" data/text/format (#+ format)] ["_" test (#+ Test)] [abstract - ["." monad (#+ do)]] + ["." monad (#+ do)] + {[0 #spec] + [/ + ["$." functor (#+ Injection Comparison)] + ["$." apply] + ["$." monad]]}] [control - [pipe (#+ case>)]] + [pipe (#+ case>)] + ["." function] + ["." try] + ["." exception (#+ exception:)]] [data + ["." bit ("#\." equivalence)] ["." product] ["." maybe] - ["." text ("#\." equivalence)] + ["." text ("#\." equivalence) + ["%" format (#+ format)]] [collection - ["." list ("#\." functor)] + ["." list ("#\." functor monoid)] ["." set]]] [math - ["." random (#+ Random)] + ["." random (#+ Random) ("#\." monad)] [number ["n" nat]]] ["." type ("#\." equivalence)]] @@ -34,27 +43,26 @@ (-> Nat (Random Type)) (random.rec (function (_ recur) - (let [(^open "R\.") random.monad - pairG (random.and recur recur) - quantifiedG (random.and (R\wrap (list)) (type' (inc num_vars))) - random_pair (random.either (random.either (R\map (|>> #.Sum) pairG) - (R\map (|>> #.Product) pairG)) - (random.either (R\map (|>> #.Function) pairG) - (R\map (|>> #.Apply) pairG))) - random_id (let [random_id (random.either (R\map (|>> #.Var) random.nat) - (R\map (|>> #.Ex) random.nat))] + (let [pairG (random.and recur recur) + quantifiedG (random.and (random\wrap (list)) (type' (inc num_vars))) + random_pair (random.either (random.either (random\map (|>> #.Sum) pairG) + (random\map (|>> #.Product) pairG)) + (random.either (random\map (|>> #.Function) pairG) + (random\map (|>> #.Apply) pairG))) + random_id (let [random_id (random.either (random\map (|>> #.Var) random.nat) + (random\map (|>> #.Ex) random.nat))] (case num_vars 0 random_id - _ (random.either (R\map (|>> (n.% num_vars) (n.* 2) inc #.Parameter) random.nat) + _ (random.either (random\map (|>> (n.% num_vars) (n.* 2) inc #.Parameter) random.nat) random_id))) - random_quantified (random.either (R\map (|>> #.UnivQ) quantifiedG) - (R\map (|>> #.ExQ) quantifiedG))] + random_quantified (random.either (random\map (|>> #.UnivQ) quantifiedG) + (random\map (|>> #.ExQ) quantifiedG))] ($_ random.either - (R\map (|>> #.Primitive) (random.and ..short (R\wrap (list)))) + (random\map (|>> #.Primitive) (random.and ..short (random\wrap (list)))) random_pair random_id random_quantified - (R\map (|>> #.Named) (random.and ..name (type' 0))) + (random\map (|>> #.Named) (random.and ..name (type' 0))) ))))) (def: type @@ -81,178 +89,633 @@ _ #0)) -(def: (type_checks? input) - (-> (/.Check []) Bit) - (case (/.run /.fresh_context input) - (#.Right []) - #1 +(def: injection + (Injection (All [a] (/.Check a))) + (\ /.monad wrap)) - (#.Left error) - #0)) +(def: comparison + (Comparison (All [a] (/.Check a))) + (function (_ == left right) + (case [(/.run /.fresh_context left) (/.run /.fresh_context right)] + [(#try.Success left) (#try.Success right)] + (== left right) -(def: (build_ring num_connections) - (-> Nat (/.Check [[Nat Type] (List [Nat Type]) [Nat Type]])) - (do {! /.monad} - [[head_id head_type] /.var - ids+types (monad.seq ! (list.repeat num_connections /.var)) - [tail_id tail_type] (monad.fold ! (function (_ [tail_id tail_type] [_head_id _head_type]) - (do ! - [_ (/.check head_type tail_type)] - (wrap [tail_id tail_type]))) - [head_id head_type] - ids+types)] - (wrap [[head_id head_type] ids+types [tail_id tail_type]]))) + _ + false))) -(def: #export test +(def: polymorphism + Test + ($_ _.and + (_.for [/.functor] + ($functor.spec ..injection ..comparison /.functor)) + (_.for [/.apply] + ($apply.spec ..injection ..comparison /.apply)) + (_.for [/.monad] + ($monad.spec ..injection ..comparison /.monad)) + )) + +(exception: yolo) + +(def: error_handling Test - (<| (_.context (%.name (name_of /._))) + ($_ _.and + (do random.monad + [expected (random.ascii/upper 10)] + (_.cover [/.fail] + (case (/.run /.fresh_context + (: (/.Check Any) + (/.fail expected))) + (#try.Success _) false + (#try.Failure actual) (is? expected actual)))) + (do random.monad + [expected (random.ascii/upper 10)] + (_.cover [/.assert] + (and (case (/.run /.fresh_context + (: (/.Check Any) + (/.assert expected true))) + (#try.Success _) true + (#try.Failure actual) false) + (case (/.run /.fresh_context (/.assert expected false)) + (#try.Success _) false + (#try.Failure actual) (is? expected actual))))) + (_.cover [/.throw] + (case (/.run /.fresh_context + (: (/.Check Any) + (/.throw ..yolo []))) + (#try.Success _) false + (#try.Failure error) (exception.match? ..yolo error))) + )) + +(def: var + Test + (<| (_.for [/.Var]) ($_ _.and + (_.cover [/.var] + (case (/.run /.fresh_context + (do /.monad + [[var_id var_type] /.var] + (wrap (type\= var_type (#.Var var_id))))) + (#try.Success verdict) verdict + (#try.Failure error) false)) + (do random.monad + [nominal (random.ascii/upper 10)] + (_.cover [/.bind] + (case (/.run /.fresh_context + (do /.monad + [[var_id var_type] /.var + _ (/.bind (#.Primitive nominal (list)) + var_id)] + (wrap true))) + (#try.Success _) true + (#try.Failure error) false))) (do random.monad - [sample (random.filter ..valid_type? ..type)] - ($_ _.and - (_.test "Any is the super-type of everything." - (/.checks? Any sample)) - (_.test "Nothing is the sub-type of everything." - (/.checks? sample Nothing)) - )) - ($_ _.and - (_.test "Any and Nothing match themselves." - (and (/.checks? Nothing Nothing) - (/.checks? Any Any))) - (_.test "Existential types only match with themselves." - (and (type_checks? (do /.monad - [[_ exT] /.existential] - (/.check exT exT))) - (not (type_checks? (do /.monad - [[_ exTL] /.existential - [_ exTR] /.existential] - (/.check exTL exTR)))))) - (_.test "Names do not affect type-checking." - (and (type_checks? (do /.monad - [[_ exT] /.existential] - (/.check (#.Named ["module" "name"] exT) - exT))) - (type_checks? (do /.monad - [[_ exT] /.existential] - (/.check exT - (#.Named ["module" "name"] exT)))) - (type_checks? (do /.monad - [[_ exT] /.existential] - (/.check (#.Named ["module" "name"] exT) - (#.Named ["module" "name"] exT)))))) - (_.test "Functions are covariant on inputs and contravariant on outputs." - (and (/.checks? (#.Function Nothing Any) - (#.Function Any Nothing)) - (not (/.checks? (#.Function Any Nothing) - (#.Function Nothing Any))))) - ) + [nominal (random.ascii/upper 10)] + (_.cover [/.bound?] + (and (|> (do /.monad + [[var_id var_type] /.var + pre (/.bound? var_id) + _ (/.bind (#.Primitive nominal (list)) + var_id) + post (/.bound? var_id)] + (wrap (and (not pre) + post))) + (/.run /.fresh_context) + (try.default false)) + (|> (do /.monad + [[var_id var/0] /.var + pre (/.bound? var_id) + [_ var/1] /.var + _ (/.check var/0 var/1) + post (/.bound? var_id)] + (wrap (and (not pre) + (not post)))) + (/.run /.fresh_context) + (try.default false))))) (do random.monad - [meta ..type - data ..type] - (_.test "Can type-check type application." - (and (/.checks? (|> Ann (#.Apply meta) (#.Apply data)) - (type.tuple (list meta data))) - (/.checks? (type.tuple (list meta data)) - (|> Ann (#.Apply meta) (#.Apply data)))))) + [nominal (random.ascii/upper 10)] + (_.cover [/.cannot_rebind_var] + (case (/.run /.fresh_context + (do /.monad + [[var_id var_type] /.var + _ (/.bind (#.Primitive nominal (list)) + var_id)] + (/.bind (#.Primitive nominal (list)) + var_id))) + (#try.Success _) + false + + (#try.Failure error) + (exception.match? /.cannot_rebind_var error)))) + (do random.monad + [nominal (random.ascii/upper 10) + var_id random.nat] + (_.cover [/.unknown_type_var] + (case (/.run /.fresh_context + (/.bind (#.Primitive nominal (list)) + var_id)) + (#try.Success _) + false + + (#try.Failure error) + (exception.match? /.unknown_type_var error)))) + (do random.monad + [nominal (random.ascii/upper 10) + #let [expected (#.Primitive nominal (list))]] + (_.cover [/.read] + (and (|> (do /.monad + [[var_id var_type] /.var] + (/.read var_id)) + (/.run /.fresh_context) + (case> (#try.Success #.None) true + _ false)) + (|> (do /.monad + [[var_id var/0] /.var + [_ var/1] /.var + _ (/.check var/0 var/1)] + (/.read var_id)) + (/.run /.fresh_context) + (case> (#try.Success #.None) true + _ false)) + (|> (do /.monad + [[var_id var_type] /.var + _ (/.bind expected var_id)] + (/.read var_id)) + (/.run /.fresh_context) + (case> (#try.Success (#.Some actual)) + (is? expected actual) + + _ + false))))) + (do random.monad + [nominal (random.ascii/upper 10) + #let [expected (#.Primitive nominal (list))]] + (_.cover [/.read!] + (case (/.run /.fresh_context + (do /.monad + [[var_id var_type] /.var + _ (/.bind expected var_id)] + (/.read! var_id))) + (#try.Success actual) + (is? expected actual) + + _ + false))) + (do random.monad + [nominal (random.ascii/upper 10) + #let [expected (#.Primitive nominal (list))]] + (_.cover [/.unbound_type_var] + (case (/.run /.fresh_context + (do /.monad + [[var_id var_type] /.var] + (/.read! var_id))) + (#try.Failure error) + (exception.match? /.unbound_type_var error) + + _ + false))) + ))) + +(def: context + Test + ($_ _.and + (_.cover [/.fresh_context] + (and (n.= 0 (get@ #.var_counter /.fresh_context)) + (n.= 0 (get@ #.ex_counter /.fresh_context)) + (list.empty? (get@ #.var_bindings /.fresh_context)))) + (_.cover [/.context] + (and (case (/.run /.fresh_context /.context) + (#try.Success actual) + (is? /.fresh_context actual) + + (#try.Failure error) + false) + (case (/.run /.fresh_context + (do /.monad + [_ /.var] + /.context)) + (#try.Success actual) + (and (n.= 1 (get@ #.var_counter actual)) + (n.= 0 (get@ #.ex_counter actual)) + (n.= 1 (list.size (get@ #.var_bindings actual)))) + + (#try.Failure error) + false))) + (_.cover [/.existential] + (case (/.run /.fresh_context + (do /.monad + [_ /.existential] + /.context)) + (#try.Success actual) + (and (n.= 0 (get@ #.var_counter actual)) + (n.= 1 (get@ #.ex_counter actual)) + (n.= 0 (list.size (get@ #.var_bindings actual)))) + + (#try.Failure error) + false)) + )) + +(def: succeeds? + (All [a] (-> (/.Check a) Bit)) + (|>> (/.run /.fresh_context) + (case> (#try.Success _) + true + + (#try.Failure error) + false))) + +(def: fails? + (All [a] (-> (/.Check a) Bit)) + (|>> ..succeeds? + not)) + +(def: nominal + (Random Type) + (do random.monad + [name (random.ascii/upper 10)] + (wrap (#.Primitive name (list))))) + +(def: (non_twins = random) + (All [a] (-> (-> a a Bit) (Random a) (Random [a a]))) + (do random.monad + [left random + right (random.filter (|>> (= left) not) random)] + (wrap [left right]))) + +(type: Super + (Ex [sub] [Text sub])) + +(type: Sub + (Super Bit)) + +(def: (handles_nominal_types! name/0 name/1 parameter/0 parameter/1) + (-> Text Text Type Type Bit) + (let [names_matter! + (and (..succeeds? (/.check (#.Primitive name/0 (list)) + (#.Primitive name/0 (list)))) + (..fails? (/.check (#.Primitive name/0 (list)) + (#.Primitive name/1 (list))))) + + parameters_matter! + (and (..succeeds? (/.check (#.Primitive name/0 (list parameter/0)) + (#.Primitive name/0 (list parameter/0)))) + (..fails? (/.check (#.Primitive name/0 (list parameter/0)) + (#.Primitive name/0 (list parameter/1))))) + + covariant_parameters! + (and (..succeeds? (/.check (#.Primitive name/0 (list Super)) + (#.Primitive name/0 (list Sub)))) + (..fails? (/.check (#.Primitive name/0 (list Sub)) + (#.Primitive name/0 (list Super)))))] + (and names_matter! + parameters_matter! + covariant_parameters!))) + +(template [<assertion> <combinator>] + [(def: (<assertion> name/0 name/1) + (-> Text Text Bit) + (let [pair/0 (<combinator> (#.Primitive name/0 (list)) (#.Primitive name/0 (list))) + pair/1 (<combinator> (#.Primitive name/1 (list)) (#.Primitive name/1 (list))) + + invariant! + (and (..succeeds? (/.check pair/0 pair/0)) + (..fails? (/.check pair/0 pair/1))) + + super_pair (<combinator> Super Super) + sub_pair (<combinator> Sub Sub) + + covariant! + (and (..succeeds? (/.check super_pair sub_pair)) + (..fails? (/.check sub_pair super_pair)))] + (and invariant! + covariant!)))] + + [handles_products! #.Product] + [handles_sums! #.Sum] + ) + +(def: (handles_function_variance! nominal) + (-> Type Bit) + (let [functions_have_contravariant_inputs! + (..succeeds? (/.check (#.Function Sub nominal) (#.Function Super nominal))) + + functions_have_covariant_outputs! + (..succeeds? (/.check (#.Function nominal Super) (#.Function nominal Sub)))] + (and functions_have_contravariant_inputs! + functions_have_covariant_outputs!))) + +(def: (verdict check) + (All [_] (-> (/.Check _) (/.Check Bit))) + (function (_ context) + (#try.Success [context (case (check context) + (#try.Success _) + true + + (#try.Failure _) + false)]))) + +(def: (build_ring tail_size) + (-> Nat (/.Check [Type (List Type) Type])) + (do {! /.monad} + [[id/head var/head] /.var + var/tail+ (monad.map ! (function (_ _) + (do ! + [[id/T var/tail] /.var] + (wrap var/tail))) + (list.repeat tail_size /.var)) + var/last (monad.fold ! (function (_ var/next var/prev) + (do ! + [_ (/.check var/prev var/next)] + (wrap var/next))) + var/head + var/tail+) + _ (/.check var/last var/head)] + (wrap [var/head var/tail+ var/last]))) + +(def: (handles_var_rings! tail_size nominal/0 nominal/1) + (-> Nat Type Type Bit) + (let [can_create_rings_of_variables! + (succeeds? (..build_ring tail_size)) + + can_bind_rings_of_variables! + (succeeds? (do {! /.monad} + [[var/head var/tail+ var/last] (..build_ring tail_size) + _ (/.check var/head nominal/0) + failures (monad.map ! (|>> (/.check nominal/1) ..verdict) (list& var/head var/tail+)) + successes (monad.map ! (|>> (/.check nominal/0) ..verdict) (list& var/head var/tail+))] + (/.assert "" (and (list.every? (bit\= false) failures) + (list.every? (bit\= true) successes))))) + + can_merge_multiple_rings_of_variables! + (succeeds? (do {! /.monad} + [[var/head/0 var/tail+/0 var/last/0] (..build_ring tail_size) + [var/head/1 var/tail+/1 var/last/1] (..build_ring tail_size) + _ (/.check var/head/0 var/head/1) + _ (/.check var/head/0 nominal/0) + #let [all_variables (list\compose (list& var/head/0 var/tail+/0) + (list& var/head/1 var/tail+/1))] + failures (monad.map ! (|>> (/.check nominal/1) ..verdict) all_variables) + successes (monad.map ! (|>> (/.check nominal/0) ..verdict) all_variables)] + (/.assert "" (and (list.every? (bit\= false) failures) + (list.every? (bit\= true) successes)))))] + (and can_create_rings_of_variables! + can_bind_rings_of_variables! + can_merge_multiple_rings_of_variables!))) + +(def: (handles_vars! nominal) + (-> Type Bit) + (let [vars_check_against_themselves! + (succeeds? (do /.monad + [[id var] /.var] + (/.check var var))) + + can_bind_vars_by_checking_against_them! + (and (succeeds? (do /.monad + [[id var] /.var] + (/.check var nominal))) + (succeeds? (do /.monad + [[id var] /.var] + (/.check nominal var)))) + + cannot_rebind! + (fails? (do /.monad + [[id var] /.var + _ (/.check var nominal)] + (/.check var ..Sub))) + + bound_vars_check_against_their_bound_types! + (and (succeeds? (do /.monad + [[id var] /.var + _ (/.check var nominal)] + (/.check nominal var))) + (succeeds? (do /.monad + [[id var] /.var + _ (/.check var ..Super)] + (/.check var ..Sub))) + (succeeds? (do /.monad + [[id var] /.var + _ (/.check var ..Sub)] + (/.check ..Super var))) + + (fails? (do /.monad + [[id var] /.var + _ (/.check var ..Super)] + (/.check ..Sub var))) + (fails? (do /.monad + [[id var] /.var + _ (/.check var ..Sub)] + (/.check var ..Super))))] + (and vars_check_against_themselves! + can_bind_vars_by_checking_against_them! + cannot_rebind! + bound_vars_check_against_their_bound_types!))) + +(def: handles_existentials! + Bit + (let [existentials_always_match_themselves! + (..succeeds? (do /.monad + [[_ single] /.existential] + (/.check single single))) + + existentials_never_match_each_other! + (..fails? (do /.monad + [[_ left] /.existential + [_ right] /.existential] + (/.check left right)))] + (and existentials_always_match_themselves! + existentials_never_match_each_other!))) + +(def: (handles_quantification! nominal) + (-> Type Bit) + (let [universals_satisfy_themselves! + (..succeeds? (/.check (.type (All [a] (Maybe a))) + (.type (All [a] (Maybe a))))) + + existentials_satisfy_themselves! + (..succeeds? (/.check (.type (Ex [a] (Maybe a))) + (.type (Ex [a] (Maybe a))))) + + universals_satisfy_particulars! + (..succeeds? (/.check (.type (Maybe nominal)) + (.type (All [a] (Maybe a))))) + + particulars_do_not_satisfy_universals! + (..fails? (/.check (.type (All [a] (Maybe a))) + (.type (Maybe nominal)))) + + particulars_satisfy_existentials! + (..succeeds? (/.check (.type (Ex [a] (Maybe a))) + (.type (Maybe nominal)))) + + existentials_do_not_satisfy_particulars! + (..fails? (/.check (.type (Maybe nominal)) + (.type (Ex [a] (Maybe a)))))] + (and universals_satisfy_themselves! + existentials_satisfy_themselves! + + universals_satisfy_particulars! + particulars_do_not_satisfy_universals! + + particulars_satisfy_existentials! + existentials_do_not_satisfy_particulars! + ))) + +(def: (handles_ultimates! nominal) + (-> Type Bit) + (let [any_is_the_ultimate_super_type! + (and (..succeeds? (/.check Any nominal)) + (..fails? (/.check nominal Any))) + + nothing_is_the_ultimate_sub_type! + (and (..succeeds? (/.check nominal Nothing)) + (..fails? (/.check Nothing nominal))) + + ultimates_check_themselves! + (and (..succeeds? (/.check Any Any)) + (..succeeds? (/.check Nothing Nothing)))] + (and any_is_the_ultimate_super_type! + nothing_is_the_ultimate_sub_type! + ultimates_check_themselves!))) + +(def: (names_do_not_affect_types! left_name right_name nominal) + (-> Name Name Type Bit) + (and (..succeeds? (/.check (#.Named left_name Any) nominal)) + (..succeeds? (/.check Any (#.Named right_name nominal))) + (..succeeds? (/.check (#.Named left_name Any) (#.Named right_name nominal))))) + +## TODO: Test all the crazy corner cases from /.check_apply +(def: (handles_application! nominal/0 nominal/1) + (-> Type Type Bit) + (let [types_flow_through! + (and (..succeeds? (/.check (.type ((All [a] a) nominal/0)) + nominal/0)) + (..succeeds? (/.check nominal/0 + (.type ((All [a] a) nominal/0)))) + + (..succeeds? (/.check (.type ((Ex [a] a) nominal/0)) + nominal/0)) + (..succeeds? (/.check nominal/0 + (.type ((Ex [a] a) nominal/0))))) + + multiple_parameters! + (and (..succeeds? (/.check (.type ((All [a b] [a b]) nominal/0 nominal/1)) + (.type [nominal/0 nominal/1]))) + (..succeeds? (/.check (.type [nominal/0 nominal/1]) + (.type ((All [a b] [a b]) nominal/0 nominal/1)))) + + (..succeeds? (/.check (.type ((Ex [a b] [a b]) nominal/0 nominal/1)) + (.type [nominal/0 nominal/1]))) + (..succeeds? (/.check (.type [nominal/0 nominal/1]) + (.type ((Ex [a b] [a b]) nominal/0 nominal/1)))))] + (and types_flow_through! + multiple_parameters!))) + +(def: check + Test + (do {! random.monad} + [nominal ..nominal + [name/0 name/1] (..non_twins text\= (random.ascii/upper 10)) + [parameter/0 parameter/1] (..non_twins type\= ..nominal) + left_name ..name + right_name ..name + ring_tail_size (\ ! map (n.% 10) random.nat)] + (_.cover [/.check] + (and (..handles_nominal_types! name/0 name/1 parameter/0 parameter/1) + (..handles_products! name/0 name/1) + (..handles_sums! name/0 name/1) + (..handles_function_variance! nominal) + (..handles_vars! nominal) + (..handles_var_rings! ring_tail_size parameter/0 parameter/1) + ..handles_existentials! + (..handles_quantification! nominal) + (..handles_ultimates! nominal) + (..handles_application! parameter/0 parameter/1) + (..names_do_not_affect_types! left_name right_name nominal) + )))) + +(def: dirty_type + (Random (-> Type Type)) + (random.rec + (function (_ dirty_type) + (`` ($_ random.either + (random\map (function (_ id) + (function.constant (#.Ex id))) + random.nat) + (do random.monad + [module (random.ascii/upper 10) + short (random.ascii/upper 10) + anonymousT dirty_type] + (wrap (function (_ holeT) + (#.Named [module short] (anonymousT holeT))))) + (~~ (template [<tag>] + [(do random.monad + [leftT dirty_type + rightT dirty_type] + (wrap (function (_ holeT) + (<tag> (leftT holeT) (rightT holeT)))))] + + [#.Sum] + [#.Product] + [#.Function] + [#.Apply] + )) + (do {! random.monad} + [name (random.ascii/upper 10) + parameterT dirty_type] + (wrap (function (_ holeT) + (#.Primitive name (list (parameterT holeT)))))) + (~~ (template [<tag>] + [(do {! random.monad} + [funcT dirty_type + argT dirty_type + body random.nat] + (wrap (function (_ holeT) + (<tag> (list (funcT holeT) (argT holeT)) + (#.Parameter body)))))] + + [#.UnivQ] + [#.ExQ] + )) + ))))) + +(def: clean + Test + (do random.monad + [type_shape ..dirty_type] + (_.cover [/.clean] + (and (|> (do /.monad + [[var_id varT] /.var + cleanedT (/.clean (type_shape varT))] + (wrap (type\= (type_shape varT) + cleanedT))) + (/.run /.fresh_context) + (try.default false)) + (|> (do /.monad + [[var_id varT] /.var + [_ replacementT] /.existential + _ (/.check varT replacementT) + cleanedT (/.clean (type_shape varT))] + (wrap (type\= (type_shape replacementT) + cleanedT))) + (/.run /.fresh_context) + (try.default false)) + )))) + +(def: #export test + Test + (<| (_.covering /._) + (_.for [/.Check]) + ($_ _.and + ..polymorphism (do random.monad - [#let [gen_short (random.ascii 10)] - nameL gen_short - nameR (|> gen_short (random.filter (|>> (text\= nameL) not))) - paramL ..type - paramR (random.filter (|>> (/.checks? paramL) not) ..type)] - ($_ _.and - (_.test "Primitive types match when they have the same name and the same parameters." - (/.checks? (#.Primitive nameL (list paramL)) - (#.Primitive nameL (list paramL)))) - (_.test "Names matter to primitive types." - (not (/.checks? (#.Primitive nameL (list paramL)) - (#.Primitive nameR (list paramL))))) - (_.test "Parameters matter to primitive types." - (not (/.checks? (#.Primitive nameL (list paramL)) - (#.Primitive nameL (list paramR))))) - )) - ($_ _.and - (_.test "Type-vars check against themselves." - (type_checks? (do /.monad - [[id var] /.var] - (/.check var var)))) - (_.test "Can bind unbound type-vars by type-checking against them." - (and (type_checks? (do /.monad - [[id var] /.var] - (/.check var .Any))) - (type_checks? (do /.monad - [[id var] /.var] - (/.check .Any var))))) - (_.test "Cannot rebind already bound type-vars." - (not (type_checks? (do /.monad - [[id var] /.var - _ (/.check var .Bit)] - (/.check var .Nat))))) - (_.test "If the type bound to a var is a super-type to another, then the var is also a super-type." - (type_checks? (do /.monad - [[id var] /.var - _ (/.check var Any)] - (/.check var .Bit)))) - (_.test "If the type bound to a var is a sub-type of another, then the var is also a sub-type." - (type_checks? (do /.monad - [[id var] /.var - _ (/.check var Nothing)] - (/.check .Bit var)))) - ) - (do {! random.monad} - [num_connections (|> random.nat (\ ! map (n.% 100))) - boundT (|> ..type (random.filter (|>> (case> (#.Var _) #0 _ #1)))) - pick_pcg (random.and random.nat random.nat)] - ($_ _.and - (_.test "Can create rings of variables." - (type_checks? (do /.monad - [[[head_id head_type] ids+types [tail_id tail_type]] (build_ring num_connections) - #let [ids (list\map product.left ids+types)] - headR (/.ring head_id) - tailR (/.ring tail_id)] - (/.assert "" - (let [same_rings? (\ set.equivalence = headR tailR) - expected_size? (n.= (inc num_connections) (set.size headR)) - same_vars? (|> (set.to_list headR) - (list.sort n.<) - (\ (list.equivalence n.equivalence) = (list.sort n.< (#.Cons head_id ids))))] - (and same_rings? - expected_size? - same_vars?)))))) - (_.test "When a var in a ring is bound, all the ring is bound." - (type_checks? (do {! /.monad} - [[[head_id headT] ids+types tailT] (build_ring num_connections) - #let [ids (list\map product.left ids+types)] - _ (/.check headT boundT) - head_bound (/.read head_id) - tail_bound (monad.map ! /.read ids) - headR (/.ring head_id) - tailR+ (monad.map ! /.ring ids)] - (let [rings_were_erased? (and (set.empty? headR) - (list.every? set.empty? tailR+)) - same_types? (list.every? (type\= boundT) (list& (maybe.default headT head_bound) - (list\map (function (_ [tail_id ?tailT]) - (maybe.default (#.Var tail_id) ?tailT)) - (list.zip/2 ids tail_bound))))] - (/.assert "" - (and rings_were_erased? - same_types?)))))) - (_.test "Can merge multiple rings of variables." - (type_checks? (do /.monad - [[[head_idL headTL] ids+typesL [tail_idL tailTL]] (build_ring num_connections) - [[head_idR headTR] ids+typesR [tail_idR tailTR]] (build_ring num_connections) - headRL_pre (/.ring head_idL) - headRR_pre (/.ring head_idR) - _ (/.check headTL headTR) - headRL_post (/.ring head_idL) - headRR_post (/.ring head_idR)] - (/.assert "" - (let [same_rings? (\ set.equivalence = headRL_post headRR_post) - expected_size? (n.= (n.* 2 (inc num_connections)) - (set.size headRL_post)) - union? (\ set.equivalence = headRL_post (set.union headRL_pre headRR_pre))] - (and same_rings? - expected_size? - union?)))))) - )) + [expected random.nat] + (_.cover [/.run] + (case (/.run /.fresh_context + (\ /.monad wrap expected)) + (#try.Success actual) (is? expected actual) + (#try.Failure error) false))) + ..error_handling + ..var + ..context + ..check + ..clean ))) |