(.using [library [lux {"-" symbol} ["_" test {"+" Test}] [abstract ["[0]" monad {"+" do}] [\\specification ["$[0]" equivalence]]] [control ["[0]" pipe] ["[0]" maybe]] [data ["[0]" bit ("[1]#[0]" equivalence)] ["[0]" text ("[1]#[0]" equivalence)] [collection ["[0]" list] ["[0]" array]]] [macro ["^" pattern] ["[0]" code ("[1]#[0]" equivalence)]] [math ["[0]" random {"+" Random} ("[1]#[0]" monad)] [number ["n" nat]]]]] [\\library ["[0]" / ("[1]#[0]" equivalence)]] ["[0]" / "_" ["[1][0]" abstract] ["[1][0]" check] ["[1][0]" dynamic] ["[1][0]" implicit] ["[1][0]" poly] ["[1][0]" quotient] ["[1][0]" refinement] ["[1][0]" resource] ["[1][0]" unit] ["[1][0]" variance]]) (def: short (Random Text) (do [! random.monad] [size (|> random.nat (# ! each (n.% 10)))] (random.unicode size))) (def: symbol (Random Symbol) (random.and ..short ..short)) (def: (random' parameters) (-> Nat (Random Type)) (random.rec (function (_ again) (let [pairG (random.and again again) un_parameterized (is (Random Type) ($_ random.either (random#each (|>> {.#Primitive}) (random.and ..short (random.list 0 again))) (random#each (|>> {.#Primitive}) (random.and ..short (random.list 1 again))) (random#each (|>> {.#Primitive}) (random.and ..short (random.list 2 again))) (random#each (|>> {.#Sum}) pairG) (random#each (|>> {.#Product}) pairG) (random#each (|>> {.#Function}) pairG) ))] (case parameters 0 un_parameterized _ (|> random.nat (random#each (|>> (n.% parameters) {.#Parameter})) (random.either un_parameterized))))))) (def: .public (random parameters) (-> Nat (Random Type)) ($_ random.either (random#each (/.univ_q parameters) (random' parameters)) (random#each (/.ex_q parameters) (random' parameters)) )) (def: .public test Test (<| (_.covering /._) ($_ _.and (_.for [/.equivalence] ($equivalence.spec /.equivalence (..random 0))) (do [! random.monad] [anonymousT (random.only (|>> (pipe.case {.#Named _ _} false _ true)) (..random 0)) symbol/0 ..symbol symbol/1 ..symbol .let [namedT {.#Named symbol/0 anonymousT} aliasedT {.#Named symbol/1 namedT}]] ($_ _.and (_.cover [/.de_aliased] (# /.equivalence = namedT (/.de_aliased aliasedT))) (_.cover [/.anonymous] (# /.equivalence = anonymousT (/.anonymous aliasedT))))) (do [! random.monad] [size (|> random.nat (# ! each (n.% 3))) members (|> (..random 0) (random.only (function (_ type) (case type (^.or {.#Sum _} {.#Product _}) #0 _ #1))) (list.repeated size) (monad.all !)) .let [(open "/#[0]") /.equivalence (open "list#[0]") (list.equivalence /.equivalence)]] (`` ($_ _.and (~~ (template [ ] [(_.cover [ ] (let [flat (|> members )] (or (list#= members flat) (and (list#= (list) members) (list#= (list ) flat)))))] [/.variant /.flat_variant Nothing] [/.tuple /.flat_tuple Any] )) ))) (_.cover [/.applied] (and (<| (maybe.else #0) (do maybe.monad [partial (/.applied (list Bit) Ann) full (/.applied (list Int) partial)] (in (# /.equivalence = full {.#Product Bit Int})))) (|> (/.applied (list Bit) Text) (pipe.case {.#None} #1 _ #0)))) (do [! random.monad] [size (|> random.nat (# ! each (n.% 3))) members (monad.all ! (list.repeated size (..random 0))) extra (|> (..random 0) (random.only (function (_ type) (case type (^.or {.#Function _} {.#Apply _}) #0 _ #1)))) .let [(open "/#[0]") /.equivalence (open "list#[0]") (list.equivalence /.equivalence)]] ($_ _.and (_.cover [/.function /.flat_function] (let [[inputs output] (|> (/.function members extra) /.flat_function)] (and (list#= members inputs) (/#= extra output)))) (_.cover [/.application /.flat_application] (let [[tfunc tparams] (|> extra (/.application members) /.flat_application)] (n.= (list.size members) (list.size tparams)))) )) (do [! random.monad] [size (|> random.nat (# ! each (|>> (n.% 3) ++))) body_type (|> (..random 0) (random.only (function (_ type) (case type (^.or {.#UnivQ _} {.#ExQ _}) #0 _ #1)))) .let [(open "/#[0]") /.equivalence]] (`` ($_ _.and (~~ (template [ ] [(_.cover [ ] (let [[flat_size flat_body] (|> body_type ( size) )] (and (n.= size flat_size) (/#= body_type flat_body))))] [/.univ_q /.flat_univ_q] [/.ex_q /.flat_ex_q] )) (_.cover [/.quantified?] (and (not (/.quantified? body_type)) (|> body_type (/.univ_q size) /.quantified?) (|> body_type (/.ex_q size) /.quantified?))) ))) (do [! random.monad] [depth (|> random.nat (# ! each (|>> (n.% 3) ++))) element_type (|> (..random 0) (random.only (function (_ type) (case type (pattern {.#Primitive name (list element_type)}) (not (text#= array.type_name name)) _ #1)))) .let [(open "/#[0]") /.equivalence]] ($_ _.and (_.cover [/.array /.flat_array] (let [[flat_depth flat_element] (|> element_type (/.array depth) /.flat_array)] (and (n.= depth flat_depth) (/#= element_type flat_element)))) (_.cover [/.array?] (and (not (/.array? element_type)) (/.array? (/.array depth element_type)))) )) (_.cover [/.by_example] (let [example (is (Maybe Nat) {.#None})] (/#= (.type (List Nat)) (/.by_example [a] (Maybe a) example (List a))))) (do random.monad [sample random.nat] (_.cover [/.log!] (exec (/.log! sample) true))) (do random.monad [left random.nat right (random.ascii/lower 1) .let [left,right [left right]]] (_.cover [/.as] (|> left,right (/.as [l r] (And l r) (Or l r)) (/.as [l r] (Or l r) (And l r)) (same? left,right)))) (do random.monad [expected random.nat] (_.cover [/.sharing] (n.= expected (/.sharing [a] (I64 a) expected (I64 a) (.i64 expected))))) (do random.monad [expected_left random.nat expected_right random.nat] (_.cover [/.let] (let [[actual_left actual_right] (is (/.let [side /.Nat] [side side]) [expected_left expected_right])] (and (same? expected_left actual_left) (same? expected_right actual_right))))) (do random.monad [.let [(open "/#[0]") /.equivalence] left (..random 0) right (..random 0)] ($_ _.and (_.cover [/.code] (bit#= (/#= left right) (code#= (/.code left) (/.code right)))) (_.cover [/.format] (bit#= (/#= left right) (text#= (/.format left) (/.format right)))) )) /abstract.test /check.test /dynamic.test /implicit.test /poly.test /quotient.test /refinement.test /resource.test /unit.test /variance.test )))