(.module:
  [library
   [lux {"-" [function :as]}
    ["@" target]
    [abstract
     [equivalence {"+" [Equivalence]}]
     [monad {"+" [Monad do]}]]
    [control
     ["." function]
     ["." maybe]
     ["." exception {"+" [exception:]}]
     ["<>" parser
      ["<.>" code {"+" [Parser]}]]]
    [data
     ["." product]
     ["." text ("#\." monoid equivalence)]
     ["." name ("#\." equivalence codec)]
     [collection
      ["." array]
      ["." list ("#\." functor monoid mix)]]]
    ["." macro
     [syntax {"+" [syntax:]}]
     ["." code]]
    [math
     [number
      ["n" nat ("#\." decimal)]]]
    ["." meta
     ["." location]]]])

(template [<name> <tag>]
  [(def: .public (<name> type)
     (-> Type [Nat Type])
     (loop [num_args 0
            type type]
       (case type
         (<tag> env sub_type)
         (recur (++ num_args) sub_type)

         _
         [num_args type])))]

  [flat_univ_q #.UnivQ]
  [flat_ex_q   #.ExQ]
  )

(def: .public (flat_function type)
  (-> Type [(List Type) Type])
  (case type
    (#.Function in out')
    (let [[ins out] (flat_function out')]
      [(list& in ins) out])

    _
    [(list) type]))

(def: .public (flat_application type)
  (-> Type [Type (List Type)])
  (case type
    (#.Apply arg func')
    (let [[func args] (flat_application func')]
      [func (list\composite args (list arg))])

    _
    [type (list)]))

(template [<name> <tag>]
  [(def: .public (<name> type)
     (-> Type (List Type))
     (case type
       (<tag> left right)
       (list& left (<name> right))

       _
       (list type)))]

  [flat_variant #.Sum]
  [flat_tuple   #.Product]
  )

(def: .public (format type)
  (-> Type Text)
  (case type
    (#.Primitive name params)
    ($_ text\composite
        "(primitive "
        (text.enclosed' text.double_quote name)
        (|> params
            (list\each (|>> format (text\composite " ")))
            (list\mix (function.flipped text\composite) ""))
        ")")

    (^template [<tag> <open> <close> <flat>]
      [(<tag> _)
       ($_ text\composite <open>
           (|> (<flat> type)
               (list\each format)
               list.reversed
               (list.interposed " ")
               (list\mix text\composite ""))
           <close>)])
    ([#.Sum  "(Or " ")" flat_variant]
     [#.Product "["   "]" flat_tuple])

    (#.Function input output)
    (let [[ins out] (flat_function type)]
      ($_ text\composite  "(-> "
          (|> ins
              (list\each format)
              list.reversed
              (list.interposed " ")
              (list\mix text\composite ""))
          " " (format out) ")"))

    (#.Parameter idx)
    (n\encoded idx)

    (#.Var id)
    ($_ text\composite "⌈v:" (n\encoded id) "⌋")

    (#.Ex id)
    ($_ text\composite "⟨e:" (n\encoded id) "⟩")

    (#.Apply param fun)
    (let [[type_func type_args] (flat_application type)]
      ($_ text\composite  "(" (format type_func) " " (|> type_args (list\each format) list.reversed (list.interposed " ") (list\mix text\composite "")) ")"))

    (^template [<tag> <desc>]
      [(<tag> env body)
       ($_ text\composite "(" <desc> " {" (|> env (list\each format) (text.interposed " ")) "} " (format body) ")")])
    ([#.UnivQ "All"]
     [#.ExQ "Ex"])

    (#.Named [module name] type)
    ($_ text\composite module "." name)
    ))

... https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
(def: (reduced env type)
  (-> (List Type) Type Type)
  (case type
    (#.Primitive name params)
    (#.Primitive name (list\each (reduced env) params))
    
    (^template [<tag>]
      [(<tag> left right)
       (<tag> (reduced env left) (reduced env right))])
    ([#.Sum]      [#.Product]
     [#.Function] [#.Apply])
    
    (^template [<tag>]
      [(<tag> old_env def)
       (case old_env
         #.End
         (<tag> env def)

         _
         (<tag> (list\each (reduced env) old_env) def))])
    ([#.UnivQ]
     [#.ExQ])
    
    (#.Parameter idx)
    (maybe.else (panic! ($_ text\composite
                            "Unknown type parameter" text.new_line
                            "      Index: " (n\encoded idx) text.new_line
                            "Environment: " (|> env
                                                list.enumeration
                                                (list\each (.function (_ [index type])
                                                             ($_ text\composite
                                                                 (n\encoded index)
                                                                 " " (..format type))))
                                                (text.interposed (text\composite text.new_line "             ")))))
                (list.item idx env))
    
    _
    type
    ))

(implementation: .public equivalence
  (Equivalence Type)
  
  (def: (= x y)
    (or (for {@.php false} ... TODO: Remove this once JPHP is gone.
             (same? x y))
        (case [x y]
          [(#.Primitive xname xparams) (#.Primitive yname yparams)]
          (and (text\= xname yname)
               (n.= (list.size yparams) (list.size xparams))
               (list\mix (.function (_ [x y] prev) (and prev (= x y)))
                         #1
                         (list.zipped/2 xparams yparams)))

          (^template [<tag>]
            [[(<tag> xid) (<tag> yid)]
             (n.= yid xid)])
          ([#.Var] [#.Ex] [#.Parameter])

          (^or [(#.Function xleft xright) (#.Function yleft yright)]
               [(#.Apply xleft xright) (#.Apply yleft yright)])
          (and (= xleft yleft)
               (= xright yright))

          [(#.Named xname xtype) (#.Named yname ytype)]
          (and (name\= xname yname)
               (= xtype ytype))

          (^template [<tag>]
            [[(<tag> xL xR) (<tag> yL yR)]
             (and (= xL yL) (= xR yR))])
          ([#.Sum] [#.Product])
          
          (^or [(#.UnivQ xenv xbody) (#.UnivQ yenv ybody)]
               [(#.ExQ xenv xbody) (#.ExQ yenv ybody)])
          (and (n.= (list.size yenv) (list.size xenv))
               (= xbody ybody)
               (list\mix (.function (_ [x y] prev) (and prev (= x y)))
                         #1
                         (list.zipped/2 xenv yenv)))

          _
          #0
          ))))

(def: .public (applied params func)
  (-> (List Type) Type (Maybe Type))
  (case params
    #.End
    (#.Some func)

    (#.Item param params')
    (case func
      (^template [<tag>]
        [(<tag> env body)
         (|> body
             (reduced (list& func param env))
             (applied params'))])
      ([#.UnivQ] [#.ExQ])

      (#.Apply A F)
      (applied (list& A params) F)

      (#.Named name unnamed)
      (applied params unnamed)
      
      _
      #.None)))

(def: .public (code type)
  (-> Type Code)
  (case type
    (#.Primitive name params)
    (` (#.Primitive (~ (code.text name))
                    (.list (~+ (list\each code params)))))

    (^template [<tag>]
      [(<tag> idx)
       (` (<tag> (~ (code.nat idx))))])
    ([#.Var] [#.Ex] [#.Parameter])

    (^template [<tag>]
      [(<tag> left right)
       (` (<tag> (~ (code left))
                 (~ (code right))))])
    ([#.Sum] [#.Product] [#.Function] [#.Apply])

    (#.Named name sub_type)
    (code.identifier name)

    (^template [<tag>]
      [(<tag> env body)
       (` (<tag> (.list (~+ (list\each code env)))
                 (~ (code body))))])
    ([#.UnivQ] [#.ExQ])
    ))

(def: .public (de_aliased type)
  (-> Type Type)
  (case type
    (#.Named _ (#.Named name type'))
    (de_aliased (#.Named name type'))

    _
    type))

(def: .public (anonymous type)
  (-> Type Type)
  (case type
    (#.Named name type')
    (anonymous type')

    _
    type))

(template [<name> <base> <ctor>]
  [(def: .public (<name> types)
     (-> (List Type) Type)
     (case types
       #.End
       <base>

       (#.Item type #.End)
       type

       (#.Item type types')
       (<ctor> type (<name> types'))))]

  [variant Nothing #.Sum]
  [tuple   Any     #.Product]
  )

(def: .public (function inputs output)
  (-> (List Type) Type Type)
  (case inputs
    #.End
    output

    (#.Item input inputs')
    (#.Function input (function inputs' output))))

(def: .public (application params quant)
  (-> (List Type) Type Type)
  (case params
    #.End
    quant

    (#.Item param params')
    (application params' (#.Apply param quant))))

(template [<name> <tag>]
  [(def: .public (<name> size body)
     (-> Nat Type Type)
     (case size
       0 body
       _  (|> body (<name> (-- size)) (<tag> (list)))))]

  [univ_q #.UnivQ]
  [ex_q   #.ExQ]
  )

(def: .public (quantified? type)
  (-> Type Bit)
  (case type
    (#.Named [module name] _type)
    (quantified? _type)

    (#.Apply A F)
    (|> (..applied (list A) F)
        (\ maybe.monad each quantified?)
        (maybe.else #0))
    
    (^or (#.UnivQ _) (#.ExQ _))
    #1

    _
    #0))

(def: .public (array depth element_type)
  (-> Nat Type Type)
  (case depth
    0 element_type
    _ (|> element_type
          (array (-- depth))
          (list)
          (#.Primitive array.type_name))))

(def: .public (flat_array type)
  (-> Type [Nat Type])
  (case type
    (^multi (^ (#.Primitive name (list element_type)))
            (text\= array.type_name name))
    (let [[depth element_type] (flat_array element_type)]
      [(++ depth) element_type])

    _
    [0 type]))

(def: .public array?
  (-> Type Bit)
  (|>> ..flat_array
       product.left
       (n.> 0)))

(syntax: (new_secret_marker [])
  (macro.with_identifiers [g!_secret_marker_]
    (in (list g!_secret_marker_))))

(def: secret_marker
  (`` (name_of (~~ (new_secret_marker)))))

(syntax: .public (:log! [input (<>.or (<>.and <code>.identifier
                                              (<>.maybe (<>.after (<code>.identifier! ..secret_marker) <code>.any)))
                                      <code>.any)])
  (case input
    (#.Left [valueN valueC])
    (do meta.monad
      [location meta.location
       valueT (meta.type valueN)
       .let [_ ("lux io log"
                ($_ text\composite
                    (name\encoded (name_of ..:log!)) " " (location.format location) text.new_line
                    "Expression: " (case valueC
                                     (#.Some valueC)
                                     (code.format valueC)
                                     
                                     #.None
                                     (name\encoded valueN))
                    text.new_line
                    "      Type: " (..format valueT)))]]
      (in (list (code.identifier valueN))))
    
    (#.Right valueC)
    (macro.with_identifiers [g!value]
      (in (list (` (.let [(~ g!value) (~ valueC)]
                     (..:log! (~ valueC) (~ (code.identifier ..secret_marker)) (~ g!value)))))))))

(def: type_parameters
  (Parser (List Text))
  (<code>.tuple (<>.some <code>.local_identifier)))

(syntax: .public (:as [type_vars type_parameters
                       input <code>.any
                       output <code>.any
                       value (<>.maybe <code>.any)])
  (macro.with_identifiers [g!_]
    (let [casterC (` (: (All ((~ g!_) (~+ (list\each code.local_identifier type_vars)))
                          (-> (~ input) (~ output)))
                        (|>> :expected)))]
      (case value
        #.None
        (in (list casterC))
        
        (#.Some value)
        (in (list (` ((~ casterC) (~ value)))))))))

(type: Typed
  (Record
   [#type Code
    #expression Code]))

(def: typed
  (Parser Typed)
  (<>.and <code>.any <code>.any))

... TODO: Make sure the generated code always gets optimized away.
(syntax: .public (:sharing [type_vars ..type_parameters
                            exemplar ..typed
                            computation ..typed])
  (macro.with_identifiers [g!_]
    (let [typeC (` (All ((~ g!_) (~+ (list\each code.local_identifier type_vars)))
                     (-> (~ (value@ #type exemplar))
                         (~ (value@ #type computation)))))
          shareC (` (: (~ typeC)
                       (.function ((~ g!_) (~ g!_))
                         (~ (value@ #expression computation)))))]
      (in (list (` ((~ shareC) (~ (value@ #expression exemplar)))))))))

(syntax: .public (:by_example [type_vars ..type_parameters
                               exemplar ..typed
                               extraction <code>.any])
  (in (list (` (:of ((~! ..:sharing)
                     [(~+ (list\each code.local_identifier type_vars))]

                     (~ (value@ #type exemplar))
                     (~ (value@ #expression exemplar))
                     
                     (~ extraction)
                     ... The value of this expression will never be relevant, so it doesn't matter what it is.
                     (.:as .Nothing [])))))))