(.using
 [library
  [lux "*"
   [abstract
    [monad {"+" Monad do}]]
   [control
    ["[0]" maybe]
    ["<>" parser
     ["<[0]>" type]]]
   [data
    ["[0]" product]
    ["[0]" bit]
    ["[0]" text ("[1]#[0]" monoid)
     ["%" format {"+" format}]]
    [collection
     ["[0]" list ("[1]#[0]" monad)]
     ["[0]" sequence]
     ["[0]" array]
     ["[0]" queue]
     ["[0]" set]
     ["[0]" dictionary {"+" Dictionary}]
     ["[0]" tree]]]
   [macro
    [syntax {"+" syntax:}]
    ["[0]" code]]
   [math
    [number
     ["[0]" nat ("[1]#[0]" decimal)]
     ["[0]" int]
     ["[0]" rev]
     ["[0]" frac]]]
   [time
    ["[0]" duration]
    ["[0]" date]
    ["[0]" instant]
    ["[0]" day]
    ["[0]" month]]
   ["[0]" type
    ["[0]" poly {"+" poly:}]
    ["[0]" unit]]]]
 [\\library
  ["[0]" /]])

(poly: .public equivalence
  (`` (do [! <>.monad]
        [.let [g!_ (code.local "_____________")]
         *env* <type>.env
         inputT <type>.next
         .let [@Equivalence (is (-> Type Code)
                                (function (_ type)
                                  (` ((~! /.Equivalence) (~ (poly.code *env* type))))))]]
        (all <>.either
             ... Basic types
             (~~ (template [<matcher> <eq>]
                   [(do !
                      [_ <matcher>]
                      (in (` (is (~ (@Equivalence inputT))
                                 <eq>))))]

                   [(<type>.exactly Any) (function ((~ g!_) (~ g!_) (~ g!_)) #1)]
                   [(<type>.sub Bit)     (~! bit.equivalence)]
                   [(<type>.sub Nat)     (~! nat.equivalence)]
                   [(<type>.sub Int)     (~! int.equivalence)]
                   [(<type>.sub Rev)     (~! rev.equivalence)]
                   [(<type>.sub Frac)    (~! frac.equivalence)]
                   [(<type>.sub Text)    (~! text.equivalence)]))
             ... Composite types
             (~~ (template [<name> <eq>]
                   [(do !
                      [[_ argC] (<type>.applied (<>.and (<type>.exactly <name>)
                                                        equivalence))]
                      (in (` (is (~ (@Equivalence inputT))
                                 (<eq> (~ argC))))))]

                   [.Maybe            (~! maybe.equivalence)]
                   [.List             (~! list.equivalence)]
                   [sequence.Sequence (~! sequence.equivalence)]
                   [array.Array       (~! array.equivalence)]
                   [queue.Queue       (~! queue.equivalence)]
                   [set.Set           (~! set.equivalence)]
                   [tree.Tree         (~! tree.equivalence)]
                   ))
             (do !
               [[_ _ valC] (<type>.applied (all <>.and
                                                (<type>.exactly dictionary.Dictionary)
                                                <type>.any
                                                equivalence))]
               (in (` (is (~ (@Equivalence inputT))
                          ((~! dictionary.equivalence) (~ valC))))))
             ... Models
             (~~ (template [<type> <eq>]
                   [(do !
                      [_ (<type>.exactly <type>)]
                      (in (` (is (~ (@Equivalence inputT))
                                 <eq>))))]

                   [duration.Duration duration.equivalence]
                   [instant.Instant instant.equivalence]
                   [date.Date date.equivalence]
                   [day.Day day.equivalence]
                   [month.Month month.equivalence]
                   ))
             (do !
               [_ (<type>.applied (<>.and (<type>.exactly unit.Qty)
                                          <type>.any))]
               (in (` (is (~ (@Equivalence inputT))
                          unit.equivalence))))
             ... Variants
             (do !
               [members (<type>.variant (<>.many equivalence))
                .let [last (-- (list.size members))
                      g!_ (code.local "_____________")
                      g!left (code.local "_____________left")
                      g!right (code.local "_____________right")]]
               (in (` (is (~ (@Equivalence inputT))
                          (function ((~ g!_) (~ g!left) (~ g!right))
                            (case [(~ g!left) (~ g!right)]
                              (~+ (list#conjoint (list#each (function (_ [tag g!eq])
                                                              (if (nat.= last tag)
                                                                (list (` [{(~ (code.nat (-- tag))) #1 (~ g!left)}
                                                                          {(~ (code.nat (-- tag))) #1 (~ g!right)}])
                                                                      (` ((~ g!eq) (~ g!left) (~ g!right))))
                                                                (list (` [{(~ (code.nat tag)) #0 (~ g!left)}
                                                                          {(~ (code.nat tag)) #0 (~ g!right)}])
                                                                      (` ((~ g!eq) (~ g!left) (~ g!right))))))
                                                            (list.enumeration members))))
                              (~ g!_)
                              #0))))))
             ... Tuples
             (do !
               [g!eqs (<type>.tuple (<>.many equivalence))
                .let [g!_ (code.local "_____________")
                      indices (list.indices (list.size g!eqs))
                      g!lefts (list#each (|>> nat#encoded (text#composite "left") code.local) indices)
                      g!rights (list#each (|>> nat#encoded (text#composite "right") code.local) indices)]]
               (in (` (is (~ (@Equivalence inputT))
                          (function ((~ g!_) [(~+ g!lefts)] [(~+ g!rights)])
                            (and (~+ (|> (list.zipped_3 g!eqs g!lefts g!rights)
                                         (list#each (function (_ [g!eq g!left g!right])
                                                      (` ((~ g!eq) (~ g!left) (~ g!right)))))))))))))
             ... Type recursion
             (do !
               [[g!self bodyC] (<type>.recursive equivalence)
                .let [g!_ (code.local "_____________")]]
               (in (` (is (~ (@Equivalence inputT))
                          ((~! /.rec) (.function ((~ g!_) (~ g!self))
                                        (~ bodyC)))))))
             <type>.recursive_self
             ... Type applications
             (do !
               [[funcC argsC] (<type>.applied (<>.and equivalence (<>.many equivalence)))]
               (in (` ((~ funcC) (~+ argsC)))))
             ... Parameters
             <type>.parameter
             ... Polymorphism
             (do !
               [[funcC varsC bodyC] (<type>.polymorphic equivalence)]
               (in (` (is (All ((~ g!_) (~+ varsC))
                            (-> (~+ (list#each (|>> (~) ((~! /.Equivalence)) (`)) varsC))
                                ((~! /.Equivalence) ((~ (poly.code *env* inputT)) (~+ varsC)))))
                          (function ((~ funcC) (~+ varsC))
                            (~ bodyC))))))
             <type>.recursive_call
             ... If all else fails...
             (|> <type>.any
                 (# ! each (|>> %.type (format "Cannot create Equivalence for: ") <>.failure))
                 (# ! conjoint))
             ))))