(.require
 [lux (.except i64)
  ["_" test (.only Test)]
  [abstract
   [monad (.only do)]]
  [control
   ["[0]" pipe]
   ["[0]" try (.only Try)]]
  [data
   ["[0]" bit (.use "[1]#[0]" equivalence)]
   [number
    ["[0]" i64]
    ["n" nat]
    ["i" int]
    ["f" frac]]
   ["[0]" text (.use "[1]#[0]" equivalence)
    ["%" \\format (.only format)]]
   [collection
    ["[0]" list]]]
  [math
   ["r" random (.only Random)]]
  [meta
   [macro
    ["^" pattern]]
   [compiler
    ["[0]" reference]
    ["[0]" synthesis]]]]
 ["[0]" //
  ["[1][0]" case]
  [//
   [common (.only Runner)]]])

(def safe
  (-> Text Text)
  (text.replaced " " "_"))

(def (bit run)
  (-> Runner Test)
  (do r.monad
    [param r.i64
     subject r.i64]
    (with_expansions [<binary> (with_template [<extension> <reference> <param_expr>]
                                 [(_.property <extension>
                                    (|> {synthesis.#Extension <extension> (list (synthesis.i64 param)
                                                                                (synthesis.i64 subject))}
                                        (run (..safe <extension>))
                                        (pipe.case
                                          {try.#Success valueT}
                                          (n.= (<reference> param subject) (as Nat valueT))

                                          {try.#Failure _}
                                          false)
                                        (let [param <param_expr>])))]

                                 ["lux i64 and"                 i64.and               param]
                                 ["lux i64 or"                  i64.or                param]
                                 ["lux i64 xor"                 i64.xor               param]
                                 ["lux i64 left-shift"          i64.left_shifted        (n.% 64 param)]
                                 ["lux i64 logical-right-shift" i64.logic_right_shifted (n.% 64 param)]
                                 )]
      (all _.and
           <binary>
           (_.property "lux i64 arithmetic-right-shift"
             (|> {synthesis.#Extension "lux i64 arithmetic-right-shift"
                                       (list (synthesis.i64 subject)
                                             (synthesis.i64 param))}
                 (run (..safe "lux i64 arithmetic-right-shift"))
                 (pipe.case
                   {try.#Success valueT}
                   ("lux i64 ="
                    (i64.arithmetic_right_shifted param subject)
                    (as I64 valueT))

                   {try.#Failure _}
                   false)
                 (let [param (n.% 64 param)])))
           ))))

(def (i64 run)
  (-> Runner Test)
  (do r.monad
    [param (|> r.i64 (r.only (|>> ("lux i64 =" 0) not)))
     subject r.i64]
    (`` (all _.and
             (,, (with_template [<extension> <type> <prepare> <comp> <subject_expr>]
                   [(_.property <extension>
                      (|> {synthesis.#Extension <extension> (list (synthesis.i64 subject))}
                          (run (..safe <extension>))
                          (pipe.case
                            {try.#Success valueT}
                            (<comp> (<prepare> subject) (as <type> valueT))

                            {try.#Failure _}
                            false)
                          (let [subject <subject_expr>])))]

                   ["lux i64 f64"  Frac i.frac f.= subject]
                   ["lux i64 char" Text (|>> (as Nat) text.from_code) text#= (|> subject
                                                                                 (as Nat)
                                                                                 (n.% (i64.left_shifted 8 1))
                                                                                 (as Int))]
                   ))
             (,, (with_template [<extension> <reference> <outputT> <comp>]
                   [(_.property <extension>
                      (|> {synthesis.#Extension <extension> (list (synthesis.i64 param)
                                                                  (synthesis.i64 subject))}
                          (run (..safe <extension>))
                          (pipe.case
                            {try.#Success valueT}
                            (<comp> (<reference> param subject) (as <outputT> valueT))

                            {try.#Failure _}
                            false)))]

                   ["lux i64 +" i.+ Int  i.=]
                   ["lux i64 -" i.- Int  i.=]
                   ["lux i64 *" i.* Int  i.=]
                   ["lux i64 /" i./ Int  i.=]
                   ["lux i64 %" i.% Int  i.=]
                   ["lux i64 =" i.= Bit bit#=]
                   ["lux i64 <" i.< Bit bit#=]
                   ))
             ))))

(def simple_frac
  (Random Frac)
  (|> r.nat (at r.monad each (|>> (n.% 1000) .int i.frac))))

(def (f64 run)
  (-> Runner Test)
  (do r.monad
    [param (|> ..simple_frac (r.only (|>> (f.= +0.0) not)))
     subject ..simple_frac]
    (`` (all _.and
             (,, (with_template [<extension> <reference> <comp>]
                   [(_.property <extension>
                      (|> {synthesis.#Extension <extension> (list (synthesis.f64 param)
                                                                  (synthesis.f64 subject))}
                          (run (..safe <extension>))
                          (//case.verify (<reference> param subject))))]

                   ["lux f64 +" f.+ f.=]
                   ["lux f64 -" f.- f.=]
                   ["lux f64 *" f.* f.=]
                   ["lux f64 /" f./ f.=]
                   ["lux f64 %" f.% f.=]
                   ))
             (,, (with_template [<extension> <text>]
                   [(_.property <extension>
                      (|> {synthesis.#Extension <extension> (list (synthesis.f64 param)
                                                                  (synthesis.f64 subject))}
                          (run (..safe <extension>))
                          (pipe.case
                            {try.#Success valueV}
                            (bit#= (<text> param subject)
                                   (as Bit valueV))

                            _
                            false)))]

                   ["lux f64 =" f.=]
                   ["lux f64 <" f.<]
                   ))
             (,, (with_template [<extension> <reference>]
                   [(_.property <extension>
                      (|> {synthesis.#Extension <extension> (list)}
                          (run (..safe <extension>))
                          (//case.verify <reference>)))]

                   ["lux f64 min"      ("lux f64 min")]
                   ["lux f64 max"      ("lux f64 max")]
                   ["lux f64 smallest" ("lux f64 smallest")]
                   ))
             (_.property "'lux f64 i64 && 'lux i64 f64'"
               (|> (run (..safe "lux f64 i64")
                        (|> subject synthesis.f64
                            (list) {synthesis.#Extension "lux f64 i64"}
                            (list) {synthesis.#Extension "lux i64 f64"}))
                   (//case.verify subject)))
             ))))

(def (text run)
  (-> Runner Test)
  (do [! r.monad]
    [sample_size (|> r.nat (at ! each (|>> (n.% 10) (n.max 1))))
     sample_lower (r.lower_case_alpha sample_size)
     sample_upper (r.upper_case_alpha sample_size)
     sample_alpha (|> (r.alphabetic sample_size)
                      (r.only (|>> (text#= sample_upper) not)))
     char_idx (|> r.nat (at ! each (n.% sample_size)))
     .let [sample_lowerS (synthesis.text sample_lower)
           sample_upperS (synthesis.text sample_upper)
           sample_alphaS (synthesis.text sample_alpha)
           concatenatedS {synthesis.#Extension "lux text concat" (list sample_lowerS sample_upperS)}
           pre_rep_once (format sample_lower sample_upper)
           post_rep_once (format sample_lower sample_alpha)
           pre_rep_all (|> sample_lower (list.repeated sample_size) (text.interposed sample_upper))
           post_rep_all (|> sample_lower (list.repeated sample_size) (text.interposed sample_alpha))]]
    (all _.and
         (_.property "Can compare texts for equality."
           (and (|> {synthesis.#Extension "lux text =" (list sample_lowerS sample_lowerS)}
                    (run (..safe "lux text ="))
                    (pipe.case
                      {try.#Success valueV}
                      (as Bit valueV)

                      _
                      false))
                (|> {synthesis.#Extension "lux text =" (list sample_upperS sample_lowerS)}
                    (run (..safe "lux text ="))
                    (pipe.case
                      {try.#Success valueV}
                      (not (as Bit valueV))

                      _
                      false))))
         (_.property "Can compare texts for order."
           (|> {synthesis.#Extension "lux text <" (list sample_lowerS sample_upperS)}
               (run (..safe "lux text <"))
               (pipe.case
                 {try.#Success valueV}
                 (as Bit valueV)

                 {try.#Failure _}
                 false)))
         (_.property "Can get length of text."
           (|> {synthesis.#Extension "lux text size" (list sample_lowerS)}
               (run (..safe "lux text size"))
               (pipe.case
                 {try.#Success valueV}
                 (n.= sample_size (as Nat valueV))

                 _
                 false)))
         (_.property "Can concatenate text."
           (|> {synthesis.#Extension "lux text size" (list concatenatedS)}
               (run (..safe "lux text size"))
               (pipe.case
                 {try.#Success valueV}
                 (n.= (n.* 2 sample_size) (as Nat valueV))

                 _
                 false)))
         (_.property "Can find index of sub-text."
           (and (|> {synthesis.#Extension "lux text index"
                                          (list concatenatedS sample_lowerS
                                                (synthesis.i64 +0))}
                    (run (..safe "lux text index"))
                    (pipe.case
                      (^.multi {try.#Success valueV}
                               [(as (Maybe Nat) valueV)
                                {.#Some valueV}])
                      (n.= 0 valueV)

                      _
                      false))
                (|> {synthesis.#Extension "lux text index"
                                          (list concatenatedS sample_upperS
                                                (synthesis.i64 +0))}
                    (run (..safe "lux text index"))
                    (pipe.case
                      (^.multi {try.#Success valueV}
                               [(as (Maybe Nat) valueV)
                                {.#Some valueV}])
                      (n.= sample_size valueV)

                      _
                      false))))
         (let [test_clip (is (-> (I64 Any) (I64 Any) Text Bit)
                             (function (_ offset length expected)
                               (|> {synthesis.#Extension "lux text clip"
                                                         (list concatenatedS
                                                               (synthesis.i64 offset)
                                                               (synthesis.i64 length))}
                                   (run (..safe "lux text clip"))
                                   (pipe.case
                                     (^.multi {try.#Success valueV}
                                              [(as (Maybe Text) valueV)
                                               {.#Some valueV}])
                                     (text#= expected valueV)

                                     _
                                     false))))]
           (_.property "Can clip text to extract sub-text."
             (and (test_clip 0 sample_size sample_lower)
                  (test_clip sample_size sample_size sample_upper))))
         (_.property "Can extract individual characters from text."
           (|> {synthesis.#Extension "lux text char"
                                     (list sample_lowerS
                                           (synthesis.i64 char_idx))}
               (run (..safe "lux text char"))
               (pipe.case
                 (^.multi {try.#Success valueV}
                          [(as (Maybe Int) valueV)
                           {.#Some valueV}])
                 (text.contains? ("lux i64 char" valueV)
                                 sample_lower)

                 _
                 false)))
         )))

(def (io run)
  (-> Runner Test)
  (do r.monad
    [message (r.alphabetic 5)]
    (all _.and
         (_.property "Can log messages."
           (|> {synthesis.#Extension "lux io log"
                                     (list (synthesis.text (format "LOG: " message)))}
               (run (..safe "lux io log"))
               (pipe.case
                 {try.#Success valueV}
                 true

                 {try.#Failure _}
                 false)))
         (_.property "Can throw runtime errors."
           (and (|> {synthesis.#Extension "lux try"
                                          (list (synthesis.function/abstraction
                                                 [synthesis.#environment (list)
                                                  synthesis.#arity 1
                                                  synthesis.#body {synthesis.#Extension "lux io error"
                                                                                        (list (synthesis.text message))}]))}
                    (run (..safe "lux try"))
                    (pipe.case
                      (^.multi {try.#Success valueV}
                               [(as (Try Text) valueV)
                                {try.#Failure error}])
                      (text.contains? message error)

                      _
                      false))
                (|> {synthesis.#Extension "lux try"
                                          (list (synthesis.function/abstraction
                                                 [synthesis.#environment (list)
                                                  synthesis.#arity 1
                                                  synthesis.#body (synthesis.text message)]))}
                    (run (..safe "lux try"))
                    (pipe.case
                      (^.multi {try.#Success valueV}
                               [(as (Try Text) valueV)
                                {try.#Success valueV}])
                      (text#= message valueV)

                      _
                      false))))
         (_.property "Can obtain current time in milli-seconds."
           (|> (synthesis.tuple (list {synthesis.#Extension "lux io current-time" (list)}
                                      {synthesis.#Extension "lux io current-time" (list)}))
               (run (..safe "lux io current-time"))
               (pipe.case
                 {try.#Success valueV}
                 (let [[pre post] (as [Nat Nat] valueV)]
                   (n.>= pre post))

                 {try.#Failure _}
                 false)))
         )))

(def .public (spec runner)
  (-> Runner Test)
  (all _.and
       (..bit runner)
       (..i64 runner)
       (..f64 runner)
       (..text runner)
       (..io runner)
       ))