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

(poly: #export equivalence
  (`` (do {@ p.monad}
        [#let [g!_ (code.local-identifier "_____________")]
         *env* <type>.env
         inputT <type>.peek
         #let [@Equivalence (: (-> Type Code)
                               (function (_ type)
                                 (` ((~! /.Equivalence) (~ (poly.to-code *env* type))))))]]
        ($_ p.either
            ## Basic types
            (~~ (template [<matcher> <eq>]
                  [(do @
                     [_ <matcher>]
                     (wrap (` (: (~ (@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>.apply (p.and (<type>.exactly <name>)
                                                    equivalence))]
                     (wrap (` (: (~ (@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>.apply ($_ p.and
                                            (<type>.exactly dictionary.Dictionary)
                                            <type>.any
                                            equivalence))]
              (wrap (` (: (~ (@Equivalence inputT))
                          ((~! dictionary.equivalence) (~ valC))))))
            ## Models
            (~~ (template [<type> <eq>]
                  [(do @
                     [_ (<type>.exactly <type>)]
                     (wrap (` (: (~ (@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>.apply (p.and (<type>.exactly unit.Qty)
                                      <type>.any))]
              (wrap (` (: (~ (@Equivalence inputT))
                          unit.equivalence))))
            ## Variants
            (do @
              [members (<type>.variant (p.many equivalence))
               #let [g!_ (code.local-identifier "_____________")
                     g!left (code.local-identifier "_____________left")
                     g!right (code.local-identifier "_____________right")]]
              (wrap (` (: (~ (@Equivalence inputT))
                          (function ((~ g!_) (~ g!left) (~ g!right))
                            (case [(~ g!left) (~ g!right)]
                              (~+ (list@join (list@map (function (_ [tag g!eq])
                                                         (list (` [((~ (code.nat tag)) (~ g!left))
                                                                   ((~ (code.nat tag)) (~ g!right))])
                                                               (` ((~ g!eq) (~ g!left) (~ g!right)))))
                                                       (list.enumerate members))))
                              (~ g!_)
                              #0))))))
            ## Tuples
            (do @
              [g!eqs (<type>.tuple (p.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)]]
              (wrap (` (: (~ (@Equivalence inputT))
                          (function ((~ g!_) [(~+ g!lefts)] [(~+ g!rights)])
                            (and (~+ (|> (list.zip3 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 "_____________")]]
              (wrap (` (: (~ (@Equivalence inputT))
                          ((~! /.rec) (.function ((~ g!_) (~ g!self))
                                        (~ bodyC)))))))
            <type>.recursive-self
            ## Type applications
            (do @
              [[funcC argsC] (<type>.apply (p.and equivalence (p.many equivalence)))]
              (wrap (` ((~ funcC) (~+ argsC)))))
            ## Parameters
            <type>.parameter
            ## Polymorphism
            (do @
              [[funcC varsC bodyC] (<type>.polymorphic equivalence)]
              (wrap (` (: (All [(~+ varsC)]
                            (-> (~+ (list@map (|>> (~) ((~! /.Equivalence)) (`)) varsC))
                                ((~! /.Equivalence) ((~ (poly.to-code *env* inputT)) (~+ varsC)))))
                          (function ((~ funcC) (~+ varsC))
                            (~ bodyC))))))
            <type>.recursive-call
            ## If all else fails...
            (|> <type>.any
                (:: @ map (|>> %.type (format "Cannot create Equivalence for: ") p.fail))
                (:: @ join))
            ))))