(.require
 [library
  [lux (.except case)
   [abstract
    [monad (.only do)]]
   [control
    ["[0]" pipe]
    ["[0]" try (.only Try)]]
   [data
    ["[0]" text (.use "[1]#[0]" equivalence)
     ["%" \\format (.only format)]]
    [number
     ["n" nat]
     ["f" frac]]
    [collection
     ["[0]" list (.use "[1]#[0]" mix)]]]
   [math
    ["r" random (.only Random)]]
   [meta
    [compiler
     ["[0]" reference]
     ["[0]" analysis]
     ["[0]" synthesis (.only Path Synthesis)]
     ["[0]" phase
      ["[1]/[0]" synthesis
       ["[0]" case]]
      ["[0]" extension/synthesis]]]]
   [test
    ["_" property (.only Test)]]]]
 [///
  [common (.only Runner)]])

(def limit Nat 10)

(def size
  (Random Nat)
  (|> r.nat (at r.monad each (|>> (n.% ..limit) (n.max 2)))))

(def (tail? size idx)
  (-> Nat Nat Bit)
  (n.= (-- size) idx))

(def .public (verify expected)
  (-> Frac (Try Any) Bit)
  (|>> (pipe.case
         {try.#Success actual}
         (f.= expected (as Frac actual))

         {try.#Failure _}
         false)))

(def case
  (Random [Synthesis Path])
  (<| r.rec (function (_ case))
      (`` (all r.either
               (do r.monad
                 [value r.i64]
                 (in [(synthesis.i64 value)
                      synthesis.path/pop]))
               (,, (with_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 (at ! each (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 (all 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 (at ! each (n.% size)))
                  [subS subP] case
                  .let [right? (tail? size idx)
                        caseS (synthesis.variant
                               [analysis.#lefts idx
                                analysis.#right? right?
                                analysis.#value subS])
                        caseP (all 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 (%.symbol (symbol 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 (%.symbol (symbol 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 (%.symbol (symbol synthesis.branch/case))
      (|> (synthesis.branch/case
           [inputS
            (all synthesis.path/alt
                 (all 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_ (is Synthesis
                     (synthesis.tuple (list (synthesis.text .prelude)
                                            (synthesis.i64 +901)
                                            (synthesis.i64 +13))))
        _code_ (is (-> Synthesis Synthesis)
                   (function (_ content)
                     (synthesis.tuple (list _cursor_ content))))
        _end_ (is Synthesis
                  (synthesis.variant [0 #0 (synthesis.text "")]))
        _item_ (is (-> Synthesis Synthesis Synthesis)
                   (function (_ head tail)
                     (synthesis.variant [0 #1 (synthesis.tuple (list head tail))])))
        _list_ (is (-> (List Synthesis) Synthesis)
                   (list#mix _item_ _end_))]
    (let [__tuple__ (is (-> (List Synthesis) Synthesis)
                        (|>> list.reversed _list_ [9 #0] synthesis.variant _code_))
          __form__ (is (-> (List Synthesis) Synthesis)
                       (|>> list.reversed _list_ [7 #0] synthesis.variant _code_))
          __text__ (is (-> Text Synthesis)
                       (function (_ value)
                         (_code_ (synthesis.variant [5 #0 (synthesis.text value)]))))
          __symbol__ (is (-> Symbol Synthesis)
                         (function (_ [module short])
                           (_code_ (synthesis.variant [6 #0 (synthesis.tuple (list (synthesis.text module)
                                                                                   (synthesis.text short)))]))))
          __list__ (is (-> (List Synthesis) Synthesis)
                       (list#mix (function (_ head tail)
                                   (__form__ (list (__tag__ ["" "Item"]) head tail)))
                                 (__tag__ ["" "End"])))
          __apply__ (is (-> Synthesis Synthesis Synthesis)
                        (function (_ func arg)
                          (__form__ (list func arg))))]
      (|> _end_
          (_item_ (__apply__ (__symbol__ ["" "form$"])
                             (__list__ (list (__apply__ (__symbol__ ["" "tag$"])
                                                        (__tuple__ (list (__text__ .prelude)
                                                                         (__text__ "Item"))))
                                             (__symbol__ ["" "export?-meta"])
                                             (__symbol__ ["" "tail"])))))
          (_item_ (__tuple__ (list (__symbol__ ["" "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})]
    (all synthesis.path/alt
         (all 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)))
         (all 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
  (all synthesis.path/alt
       (<| try.trusted
           (phase.result [extension/synthesis.bundle
                          synthesis.init])
           (case.path phase/synthesis.phase
                      special_pattern)
           (analysis.bit #1))
       (all 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)
  (all _.and
       (_.test "==="
         (and (text#= (synthesis.%path special_path)
                      (synthesis.%path special_pattern_path))
              (at synthesis.path_equivalence = special_path special_pattern_path)))
       (_.test "CODE"
         (|> special_input
             (run "special_input")
             (pipe.case
               {try.#Success output}
               true
               
               {try.#Failure _}
               false)))
       (_.test "PATTERN_MATCHING 0"
         (|> (synthesis.branch/case [special_input
                                     special_path])
             (run "special_path")
             (pipe.case
               {try.#Success output}
               true
               
               {try.#Failure _}
               false)))
       (_.test "PATTERN_MATCHING 1"
         (|> (synthesis.branch/case [special_input
                                     special_pattern_path])
             (run "special_pattern_path")
             (pipe.case
               {try.#Success output}
               true
               
               {try.#Failure _}
               false)))
       ))

(def .public (spec run)
  (-> Runner Test)
  (all _.and
       (..special_spec run)
       (..let_spec run)
       (..if_spec run)
       (..case_spec run)
       ))