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

(poly: .public equivalence
  (`` (do {! <>.monad}
        [.let [g!_ (code.local_identifier "_____________")]
         *env* <type>.env
         inputT <type>.peek
         .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 (dec (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\join (list\map (function (_ [tag g!eq])
                                                       (if (nat.= last tag)
                                                         (list (` [((~ (code.nat (dec tag))) #1 (~ g!left))
                                                                   ((~ (code.nat (dec 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\map (|>> nat\encode (text\compose "left") code.local_identifier) indices)
                     g!rights (list\map (|>> nat\encode (text\compose "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\map (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 [(~+ varsC)]
                          (-> (~+ (list\map (|>> (~) ((~! /.Equivalence)) (`)) varsC))
                              ((~! /.Equivalence) ((~ (poly.code *env* inputT)) (~+ varsC)))))
                        (function ((~ funcC) (~+ varsC))
                          (~ bodyC))))))
            <type>.recursive_call
            ... If all else fails...
            (|> <type>.any
                (\ ! map (|>> %.type (format "Cannot create Equivalence for: ") <>.failure))
                (\ ! join))
            ))))