From 0abd5bd3c0e38e352e9ba38268e04e1c858ab01e Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 15 Jul 2021 00:45:15 -0400 Subject: Re-named "spec" hierarchy to "specification". --- .../specification/compositor/generation/case.lux | 288 +++++++++++++++++++++ 1 file changed, 288 insertions(+) create mode 100644 stdlib/source/specification/compositor/generation/case.lux (limited to 'stdlib/source/specification/compositor/generation/case.lux') diff --git a/stdlib/source/specification/compositor/generation/case.lux b/stdlib/source/specification/compositor/generation/case.lux new file mode 100644 index 000000000..2424aa330 --- /dev/null +++ b/stdlib/source/specification/compositor/generation/case.lux @@ -0,0 +1,288 @@ +(.module: + [lux (#- case) + ["_" test (#+ Test)] + [abstract + [monad (#+ do)]] + [control + [pipe (#+ case>)] + ["." try (#+ Try)]] + [data + ["." text ("#\." equivalence) + ["%" format (#+ format)]] + [number + ["n" nat] + ["f" frac]] + [collection + ["." list ("#\." fold)]]] + [math + ["r" random (#+ Random)]] + [tool + [compiler + ["." reference] + ["." analysis] + ["." synthesis (#+ Path Synthesis)] + ["." phase + ["#/." synthesis + ["." case]] + ["." extension/synthesis]]]]] + [/// + [common (#+ Runner)]]) + +(def: limit Nat 10) + +(def: size + (Random Nat) + (|> r.nat (\ r.monad map (|>> (n.% ..limit) (n.max 2))))) + +(def: (tail? size idx) + (-> Nat Nat Bit) + (n.= (dec size) idx)) + +(def: #export (verify expected) + (-> Frac (Try Any) Bit) + (|>> (case> (#try.Success actual) + (f.= expected (:as Frac actual)) + + (#try.Failure _) + false))) + +(def: case + (Random [Synthesis Path]) + (<| r.rec (function (_ case)) + (`` ($_ r.either + (do r.monad + [value r.i64] + (wrap [(synthesis.i64 value) + synthesis.path/pop])) + (~~ (template [ ] + [(do r.monad + [value ] + (wrap [( value) + ( value)]))] + + [r.bit synthesis.bit synthesis.path/bit] + [r.i64 synthesis.i64 synthesis.path/i64] + [r.frac synthesis.f64 synthesis.path/f64] + [(r.unicode 5) synthesis.text synthesis.path/text])) + (do {! r.monad} + [size ..size + idx (|> r.nat (\ ! map (n.% size))) + [subS subP] case + #let [unitS (synthesis.text synthesis.unit) + caseS (synthesis.tuple + (list.concat (list (list.repeat idx unitS) + (list subS) + (list.repeat (|> size dec (n.- idx)) unitS)))) + caseP ($_ synthesis.path/seq + (if (tail? size idx) + (synthesis.member/right idx) + (synthesis.member/left idx)) + subP)]] + (wrap [caseS caseP])) + (do {! r.monad} + [size ..size + idx (|> r.nat (\ ! map (n.% size))) + [subS subP] case + #let [right? (tail? size idx) + caseS (synthesis.variant + {#analysis.lefts idx + #analysis.right? right? + #analysis.value subS}) + caseP ($_ synthesis.path/seq + (if right? + (synthesis.side/right idx) + (synthesis.side/left idx)) + subP)]] + (wrap [caseS caseP])) + )))) + +(def: (let-spec run) + (-> Runner Test) + (do r.monad + [value r.safe-frac] + (_.test (%.name (name-of synthesis.branch/let)) + (|> (synthesis.branch/let [(synthesis.f64 value) + 0 + (synthesis.variable/local 0)]) + (run "let-spec") + (verify value))))) + +(def: (if-spec run) + (-> Runner Test) + (do r.monad + [on-true r.safe-frac + on-false (|> r.safe-frac (r.filter (|>> (f.= on-true) not))) + verdict r.bit] + (_.test (%.name (name-of synthesis.branch/if)) + (|> (synthesis.branch/if [(synthesis.bit verdict) + (synthesis.f64 on-true) + (synthesis.f64 on-false)]) + (run "if-spec") + (verify (if verdict on-true on-false)))))) + +(def: (case-spec run) + (-> Runner Test) + (do r.monad + [[inputS pathS] ..case + on-success r.safe-frac + on-failure (|> r.safe-frac (r.filter (|>> (f.= on-success) not)))] + (_.test (%.name (name-of synthesis.branch/case)) + (|> (synthesis.branch/case + [inputS + ($_ synthesis.path/alt + ($_ synthesis.path/seq + pathS + (synthesis.path/then (synthesis.f64 on-success))) + (synthesis.path/then (synthesis.f64 on-failure)))]) + (run "case-spec") + (verify on-success))))) + +(def: special-input + Synthesis + (let [_cursor_ (: Synthesis + (synthesis.tuple (list (synthesis.text .prelude_module) + (synthesis.i64 +901) + (synthesis.i64 +13)))) + _code_ (: (-> Synthesis Synthesis) + (function (_ content) + (synthesis.tuple (list _cursor_ content)))) + _nil_ (: Synthesis + (synthesis.variant [0 #0 (synthesis.text "")])) + _cons_ (: (-> Synthesis Synthesis Synthesis) + (function (_ head tail) + (synthesis.variant [0 #1 (synthesis.tuple (list head tail))]))) + _list_ (: (-> (List Synthesis) Synthesis) + (list\fold _cons_ _nil_))] + (let [__tuple__ (: (-> (List Synthesis) Synthesis) + (|>> list.reverse _list_ [9 #0] synthesis.variant _code_)) + __form__ (: (-> (List Synthesis) Synthesis) + (|>> list.reverse _list_ [8 #0] synthesis.variant _code_)) + __text__ (: (-> Text Synthesis) + (function (_ value) + (_code_ (synthesis.variant [5 #0 (synthesis.text value)])))) + __identifier__ (: (-> Name Synthesis) + (function (_ [module short]) + (_code_ (synthesis.variant [6 #0 (synthesis.tuple (list (synthesis.text module) + (synthesis.text short)))])))) + __tag__ (: (-> Name Synthesis) + (function (_ [module short]) + (_code_ (synthesis.variant [7 #0 (synthesis.tuple (list (synthesis.text module) + (synthesis.text short)))])))) + __list__ (: (-> (List Synthesis) Synthesis) + (list\fold (function (_ head tail) + (__form__ (list (__tag__ ["" "Cons"]) head tail))) + (__tag__ ["" "Nil"]))) + __apply__ (: (-> Synthesis Synthesis Synthesis) + (function (_ func arg) + (__form__ (list func arg))))] + (|> _nil_ + (_cons_ (__apply__ (__identifier__ ["" "form$"]) + (__list__ (list (__apply__ (__identifier__ ["" "tag$"]) + (__tuple__ (list (__text__ .prelude_module) + (__text__ "Cons")))) + (__identifier__ ["" "export?-meta"]) + (__identifier__ ["" "tail"]))))) + (_cons_ (__tuple__ (list (__identifier__ ["" "tail"])))) + )))) + +(def: special-path + Path + (let [_nil_ (synthesis.path/side (#.Left 0)) + _cons_ (synthesis.path/side (#.Right 0)) + _head_ (synthesis.path/member (#.Left 0)) + _tail_ (synthesis.path/member (#.Right 0)) + _tuple_ (synthesis.path/side (#.Left 9))] + ($_ synthesis.path/alt + ($_ synthesis.path/seq + _cons_ + _head_ + _head_ (synthesis.path/bind 2) synthesis.path/pop + _tail_ _tuple_ _cons_ + _head_ (synthesis.path/bind 3) synthesis.path/pop + _tail_ (synthesis.path/bind 4) synthesis.path/pop + synthesis.path/pop synthesis.path/pop synthesis.path/pop synthesis.path/pop + _tail_ _cons_ + _head_ (synthesis.path/bind 5) synthesis.path/pop + _tail_ _nil_ + ## THEN + (synthesis.path/then (synthesis.bit #1))) + ($_ synthesis.path/seq + (synthesis.path/bind 2) + ## THEN + (synthesis.path/then (synthesis.bit #0)))))) + +(def: special-pattern + analysis.Pattern + (let [## [_ (#Tuple (#Cons arg args'))] + head (<| analysis.pattern/tuple (list (analysis.pattern/bind 2)) + analysis.pattern/variant [9 #0] + analysis.pattern/variant [0 #1] + analysis.pattern/tuple (list (analysis.pattern/bind 3) + (analysis.pattern/bind 4))) + ## (#Cons body #Nil) + tail (<| analysis.pattern/variant [0 #1] + analysis.pattern/tuple (list (analysis.pattern/bind 5)) + analysis.pattern/variant [0 #0] + (analysis.pattern/unit))] + ## (#Cons ) + (<| analysis.pattern/variant [0 #1] + (analysis.pattern/tuple (list head tail))))) + +(def: special-pattern-path + Path + ($_ synthesis.path/alt + (<| try.assume + (phase.run [extension/synthesis.bundle + synthesis.init]) + (case.path phase/synthesis.phase + special-pattern) + (analysis.bit #1)) + ($_ synthesis.path/seq + (synthesis.path/bind 2) + ## THEN + (synthesis.path/then (synthesis.bit #0))))) + +## TODO: Get rid of this ASAP +(def: (special-spec run) + (-> Runner Test) + ($_ _.and + (_.test "===" + (and (text\= (synthesis.%path special-path) + (synthesis.%path special-pattern-path)) + (\ synthesis.path-equivalence = special-path special-pattern-path))) + (_.test "CODE" + (|> special-input + (run "special-input") + (case> (#try.Success output) + true + + (#try.Failure _) + false))) + (_.test "PATTERN-MATCHING 0" + (|> (synthesis.branch/case [special-input + special-path]) + (run "special-path") + (case> (#try.Success output) + true + + (#try.Failure _) + false))) + (_.test "PATTERN-MATCHING 1" + (|> (synthesis.branch/case [special-input + special-pattern-path]) + (run "special-pattern-path") + (case> (#try.Success output) + true + + (#try.Failure _) + false))) + )) + +(def: #export (spec run) + (-> Runner Test) + ($_ _.and + (..special-spec run) + (..let-spec run) + (..if-spec run) + (..case-spec run) + )) -- cgit v1.2.3