From fd8ea1e1b9cae781abe42aeadda2e0ef149994d6 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sat, 5 Nov 2022 21:23:20 -0400 Subject: Property-based testing can now log/print successful seeds from run. --- stdlib/source/specification/lux/abstract/apply.lux | 101 +++++++++------------ .../source/specification/lux/abstract/comonad.lux | 77 +++++++--------- 2 files changed, 79 insertions(+), 99 deletions(-) (limited to 'stdlib/source/specification') diff --git a/stdlib/source/specification/lux/abstract/apply.lux b/stdlib/source/specification/lux/abstract/apply.lux index 607024f11..eaf4d741c 100644 --- a/stdlib/source/specification/lux/abstract/apply.lux +++ b/stdlib/source/specification/lux/abstract/apply.lux @@ -16,64 +16,53 @@ [\\library ["[0]" / (.only Apply)]] [// - [functor (.only Injection Comparison)]]) + ["[0]S" functor (.only Injection Comparison)]]) -(def (identity injection comparison (open "/#[0]")) +(def .public (spec injection comparison it) (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) - (do [! random.monad] - [sample (at ! each injection random.nat)] - (_.test "Identity." - ((comparison n.=) - (/#on sample (injection function.identity)) - sample)))) + (<| (_.for [/.Apply]) + (type.let [:$/1: (-> Nat Nat)]) + (do [! random.monad] + [sample random.nat + increase (is (Random :$/1:) + (at ! each n.+ random.nat)) + decrease (is (Random :$/1:) + (at ! each n.- random.nat))]) + (all _.and + (_.for [/.functor] + (functorS.spec injection comparison (the /.functor it))) -(def (homomorphism injection comparison (open "/#[0]")) - (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) - (do [! random.monad] - [sample random.nat - increase (at ! each n.+ random.nat)] - (_.test "Homomorphism." - ((comparison n.=) - (/#on (injection sample) (injection increase)) - (injection (increase sample)))))) + (_.coverage [/.on] + (let [(open "/#[0]") it -(def (interchange injection comparison (open "/#[0]")) - (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) - (do [! random.monad] - [sample random.nat - increase (at ! each n.+ random.nat)] - (_.test "Interchange." - ((comparison n.=) - (/#on (injection sample) (injection increase)) - (/#on (injection increase) (injection (is (-> (-> Nat Nat) Nat) - (function (_ f) (f sample))))))))) + identity! + ((comparison n.=) + (/#on (injection sample) + (injection function.identity)) + (injection sample)) -(def (composition injection comparison (open "/#[0]")) - (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) - (type.let [:$/1: (-> Nat Nat)] - (do [! random.monad] - [sample random.nat - increase (is (Random :$/1:) - (at ! each n.+ random.nat)) - decrease (is (Random :$/1:) - (at ! each n.- random.nat))] - (_.test "Composition." - ((comparison n.=) - (|> (injection (is (-> :$/1: :$/1: :$/1:) - function.composite)) - (/#on (injection increase)) - (/#on (injection decrease)) - (/#on (injection sample))) - (/#on (/#on (injection sample) - (injection increase)) - (injection decrease))))))) - -(def .public (spec injection comparison apply) - (All (_ f) (-> (Injection f) (Comparison f) (Apply f) Test)) - (_.for [/.Apply] - (all _.and - (..identity injection comparison apply) - (..homomorphism injection comparison apply) - (..interchange injection comparison apply) - (..composition injection comparison apply) - ))) + homomorphism! + ((comparison n.=) + (/#on (injection sample) (injection increase)) + (injection (increase sample))) + + interchange! + ((comparison n.=) (/#on (injection sample) (injection increase)) + (/#on (injection increase) (injection (is (-> (-> Nat Nat) Nat) + (function (_ f) (f sample)))))) + + composition! + ((comparison n.=) + (|> (injection (is (-> :$/1: :$/1: :$/1:) + function.composite)) + (/#on (injection increase)) + (/#on (injection decrease)) + (/#on (injection sample))) + (/#on (/#on (injection sample) + (injection increase)) + (injection decrease)))] + (and identity! + homomorphism! + interchange! + composition!))) + ))) diff --git a/stdlib/source/specification/lux/abstract/comonad.lux b/stdlib/source/specification/lux/abstract/comonad.lux index 2583715f2..9763f136b 100644 --- a/stdlib/source/specification/lux/abstract/comonad.lux +++ b/stdlib/source/specification/lux/abstract/comonad.lux @@ -12,51 +12,42 @@ [\\library ["[0]" / (.only CoMonad)]] [// - [functor (.only Injection Comparison)]]) + ["[0]S" functor (.only Injection Comparison)]]) -(def (left_identity injection (open "_//[0]")) - (All (_ f) (-> (Injection f) (CoMonad f) Test)) - (do [! random.monad] - [sample random.nat - morphism (at ! each (function (_ diff) - (|>> _//out (n.+ diff))) - random.nat) - .let [start (injection sample)]] - (_.test "Left identity." - (n.= (morphism start) - (|> start _//disjoint (_//each morphism) _//out))))) - -(def (right_identity injection comparison (open "_//[0]")) - (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test)) - (do random.monad - [sample random.nat - .let [start (injection sample) - == (comparison n.=)]] - (_.test "Right identity." - (== start - (|> start _//disjoint (_//each _//out)))))) - -(def (associativity injection comparison (open "_//[0]")) - (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test)) - (do [! random.monad] - [sample random.nat - increase (at ! each (function (_ diff) - (|>> _//out (n.+ diff))) - random.nat) - decrease (at ! each (function (_ diff) - (|>> _//out(n.- diff))) - random.nat) - .let [start (injection sample) - == (comparison n.=)]] - (_.test "Associativity." - (== (|> start _//disjoint (_//each (|>> _//disjoint (_//each increase) decrease))) - (|> start _//disjoint (_//each increase) _//disjoint (_//each decrease)))))) - -(def .public (spec injection comparison subject) +(def .public (spec injection comparison it) (All (_ f) (-> (Injection f) (Comparison f) (CoMonad f) Test)) (<| (_.for [/.CoMonad]) + (do [! random.monad] + [.let [(open "/#[0]") it] + sample random.nat + increase (at ! each (function (_ diff) + (|>> /#out (n.+ diff))) + random.nat) + decrease (at ! each (function (_ diff) + (|>> /#out (n.- diff))) + random.nat) + morphism (at ! each (function (_ diff) + (|>> /#out (n.+ diff))) + random.nat) + .let [start (injection sample) + == (comparison n.=)]]) (all _.and - (..left_identity injection subject) - (..right_identity injection comparison subject) - (..associativity injection comparison subject) + (_.for [/.functor] + (functorS.spec injection comparison (the /.functor it))) + + (_.coverage [/.disjoint /.out] + (let [left_identity! + (n.= (morphism start) + (|> start /#disjoint (/#each morphism) /#out)) + + right_identity! + (== start + (|> start /#disjoint (/#each /#out))) + + associativity! + (== (|> start /#disjoint (/#each (|>> /#disjoint (/#each increase) decrease))) + (|> start /#disjoint (/#each increase) /#disjoint (/#each decrease)))] + (and left_identity! + right_identity! + associativity!))) ))) -- cgit v1.2.3