(.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 ("#\." mix)]]]
   [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.= (-- size) idx))

(def: .public (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]
                (in [(synthesis.i64 value)
                     synthesis.path/pop]))
              (~~ (template [<gen> <synth> <path>]
                    [(do r.monad
                       [value <gen>]
                       (in [(<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.together (list (list.repeated idx unitS)
                                                   (list subS)
                                                   (list.repeated (|> size -- (n.- idx)) unitS))))
                       caseP ($_ synthesis.path/seq
                                 (if (tail? size idx)
                                   (synthesis.member/right idx)
                                   (synthesis.member/left idx))
                                 subP)]]
                (in [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)]]
                (in [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.only (|>> (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.only (|>> (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))))
        _end_ (: Synthesis
                 (synthesis.variant [0 #0 (synthesis.text "")]))
        _item_ (: (-> Synthesis Synthesis Synthesis)
                  (function (_ head tail)
                    (synthesis.variant [0 #1 (synthesis.tuple (list head tail))])))
        _list_ (: (-> (List Synthesis) Synthesis)
                  (list\mix _item_ _end_))]
    (let [__tuple__ (: (-> (List Synthesis) Synthesis)
                       (|>> list.reversed _list_ [9 #0] synthesis.variant _code_))
          __form__ (: (-> (List Synthesis) Synthesis)
                      (|>> list.reversed _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\mix (function (_ head tail)
                                  (__form__ (list (__tag__ ["" "Item"]) head tail)))
                                (__tag__ ["" "End"])))
          __apply__ (: (-> Synthesis Synthesis Synthesis)
                       (function (_ func arg)
                         (__form__ (list func arg))))]
      (|> _end_
          (_item_ (__apply__ (__identifier__ ["" "form$"])
                             (__list__ (list (__apply__ (__identifier__ ["" "tag$"])
                                                        (__tuple__ (list (__text__ .prelude_module)
                                                                         (__text__ "Item"))))
                                             (__identifier__ ["" "export?-meta"])
                                             (__identifier__ ["" "tail"])))))
          (_item_ (__tuple__ (list (__identifier__ ["" "tail"]))))
          ))))

(def: special_path
  Path
  (let [_end_ (synthesis.path/side (#.Left 0))
        _item_ (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
            _item_
            _head_
            _head_ (synthesis.path/bind 2) synthesis.path/pop
            _tail_ _tuple_ _item_
            _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_ _item_
            _head_ (synthesis.path/bind 5) synthesis.path/pop
            _tail_ _end_
            ... 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 (#Item 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)))
        ... (#Item body #End)
        tail (<| analysis.pattern/variant [0 #1]
                 analysis.pattern/tuple (list (analysis.pattern/bind 5))
                 analysis.pattern/variant [0 #0]
                 (analysis.pattern/unit))]
    ... (#Item <head> <tail>)
    (<| analysis.pattern/variant [0 #1]
        (analysis.pattern/tuple (list head tail)))))

(def: special_pattern_path
  Path
  ($_ synthesis.path/alt
      (<| try.trusted
          (phase.result [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: .public (spec run)
  (-> Runner Test)
  ($_ _.and
      (..special_spec run)
      (..let_spec run)
      (..if_spec run)
      (..case_spec run)
      ))