(.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))))))]]
        ($_ <>.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 ($_ <>.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))
            ))))