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". --- stdlib/source/spec/compositor/generation/case.lux | 288 ---------------------- 1 file changed, 288 deletions(-) delete mode 100644 stdlib/source/spec/compositor/generation/case.lux (limited to 'stdlib/source/spec/compositor/generation/case.lux') diff --git a/stdlib/source/spec/compositor/generation/case.lux b/stdlib/source/spec/compositor/generation/case.lux deleted file mode 100644 index 2424aa330..000000000 --- a/stdlib/source/spec/compositor/generation/case.lux +++ /dev/null @@ -1,288 +0,0 @@ -(.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