(.require
 [lux (.except)
  ["_" test (.only Test)]
  [abstract
   [monad (.only do)]]
  [control
   ["[0]" pipe]
   ["[0]" io]
   ["[0]" try]]
  [math
   ["r" random (.only Random)]]
  [meta
   ["[0]" code]
   [compiler
    [analysis (.only State+)]
    ["[0]" phase
     [macro (.only Expander)]
     ["[0]" analysis
      ["[1]/[0]" scope]
      ["[1]/[0]" type]]]]]])

(def (check_success+ expander state extension params output_type)
  (-> Expander State+ Text (List Code) Type Bit)
  (|> (analysis/scope.with_scope ""
        (analysis/type.with_type output_type
          (analysis.phase expander (` ((, (code.text extension)) (,* params))))))
      (phase.result state)
      (pipe.case
        {try.#Success _}
        true

        {try.#Failure _}
        false)))

(def check
  (Random [Code Type Code])
  (`` (all r.either
           (,, (with_template [<random> <type> <code>]
                 [(do r.monad
                    [value <random>]
                    (in [(` <type>)
                         <type>
                         (<code> value)]))]

                 [r.bit {0 #0 "#Bit" {0 #0}} code.bit]
                 [r.nat {0 #0 "#I64" {0 #1 {0 #0 "#Nat" {0 #0}} {0 #0}}} code.nat]
                 [r.int {0 #0 "#I64" {0 #1 {0 #0 "#Int" {0 #0}} {0 #0}}} code.int]
                 [r.rev {0 #0 "#I64" {0 #1 {0 #0 "#Rev" {0 #0}} {0 #0}}} code.rev]
                 [r.safe_frac {0 #0 "#Frac" {0 #0}} code.frac]
                 [(r.upper_case_alpha 5) {0 #0 "#Text" {0 #0}} code.text]
                 )))))

(def .public (spec expander state)
  (-> Expander State+ Test)
  (do r.monad
    [[typeC exprT exprC] ..check
     [other_typeC other_exprT other_exprC] ..check]
    (all _.and
         (_.property "lux check"
           (check_success+ expander state "lux check" (list typeC exprC) exprT))
         (_.property "lux coerce"
           (check_success+ expander state "lux coerce" (list typeC other_exprC) exprT))
         )))