(.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 (:coerce 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 "lux")
                                           (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__ "lux")
                                                                         (__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)
      ))