(.module:
  [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]" row]
      ["[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_identifier "_____________")]
         *env* <type>.env
         inputT <type>.next
         .let [@Equivalence (: (-> Type Code)
                               (function (_ type)
                                 (` ((~! /.Equivalence) (~ (poly.code *env* type))))))]]
        ($_ <>.either
            ... Basic types
            (~~ (template [<matcher> <eq>]
                  [(do !
                     [_ <matcher>]
                     (in (` (: (~ (@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 (` (: (~ (@Equivalence inputT))
                               (<eq> (~ argC))))))]

                  [.Maybe      (~! maybe.equivalence)]
                  [.List       (~! list.equivalence)]
                  [row.Row     (~! row.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 (` (: (~ (@Equivalence inputT))
                        ((~! dictionary.equivalence) (~ valC))))))
            ... Models
            (~~ (template [<type> <eq>]
                  [(do !
                     [_ (<type>.exactly <type>)]
                     (in (` (: (~ (@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 (` (: (~ (@Equivalence inputT))
                        unit.equivalence))))
            ... Variants
            (do !
              [members (<type>.variant (<>.many equivalence))
               .let [last (-- (list.size members))
                     g!_ (code.local_identifier "_____________")
                     g!left (code.local_identifier "_____________left")
                     g!right (code.local_identifier "_____________right")]]
              (in (` (: (~ (@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_identifier "_____________")
                     indices (list.indices (list.size g!eqs))
                     g!lefts (list\each (|>> nat\encoded (text\composite "left") code.local_identifier) indices)
                     g!rights (list\each (|>> nat\encoded (text\composite "right") code.local_identifier) indices)]]
              (in (` (: (~ (@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_identifier "_____________")]]
              (in (` (: (~ (@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 (` (: (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))
            ))))