aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/spec/compositor/generation/case.lux
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/spec/compositor/generation/case.lux')
-rw-r--r--stdlib/source/spec/compositor/generation/case.lux288
1 files changed, 0 insertions, 288 deletions
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 [<gen> <synth> <path>]
- [(do r.monad
- [value <gen>]
- (wrap [(<synth> value)
- (<path> 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 <head> <tail>)
- (<| 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)
- ))
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-29 05:53:52 +0000