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

(template [<name> <tag>]
  [(def: .public (<name> type)
     (-> Type [Nat Type])
     (loop [num_args 0
            type type]
       (case type
         {<tag> env sub_type}
         (again (++ 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 "-" (n#encoded id))

    {.#Ex id}
    ($_ text#composite "+" (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
             ... TODO: Remove this once JPHP is gone.
             false
             (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 (symbol#= 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.symbol 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_symbols [g!_secret_marker_]
    (in (list g!_secret_marker_))))

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

(syntax: .public (:log! [input (<>.or (<>.and <code>.symbol
                                              (<>.maybe (<>.after (<code>.symbol! ..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
                    (symbol#encoded (symbol ..:log!)) " " (location.format location) text.new_line
                    "Expression: " (case valueC
                                     {.#Some valueC}
                                     (code.format valueC)
                                     
                                     {.#None}
                                     (symbol#encoded valueN))
                    text.new_line
                    "      Type: " (..format valueT)))]]
      (in (list (code.symbol valueN))))
    
    {.#Right valueC}
    (macro.with_symbols [g!value]
      (in (list (` (.let [(~ g!value) (~ valueC)]
                     (..:log! (~ valueC) (~ (code.symbol ..secret_marker)) (~ g!value)))))))))

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

(syntax: .public (:as [type_vars type_parameters
                       input <code>.any
                       output <code>.any
                       value (<>.maybe <code>.any)])
  (macro.with_symbols [g!_]
    (let [casterC (` (: (All ((~ g!_) (~+ (list#each code.local_symbol 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_symbols [g!_]
    (let [typeC (` (All ((~ g!_) (~+ (list#each code.local_symbol type_vars)))
                     (-> (~ (the #type exemplar))
                         (~ (the #type computation)))))
          shareC (` (: (~ typeC)
                       (.function ((~ g!_) (~ g!_))
                         (~ (the #expression computation)))))]
      (in (list (` ((~ shareC) (~ (the #expression exemplar)))))))))

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

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

(def: .public (replaced before after)
  (-> Type Type Type Type)
  (.function (again it)
    (if (# ..equivalence = before it)
      after
      (case it
        {.#Primitive name co_variant}
        {.#Primitive name (list#each again co_variant)}

        (^template [<tag>]
          [{<tag> left right}
           {<tag> (again left) (again right)}])
        ([.#Sum]
         [.#Product]
         [.#Function]
         [.#Apply])

        (^template [<tag>]
          [{<tag> env body}
           {<tag> (list#each again env) (again body)}])
        ([.#UnivQ]
         [.#ExQ])
        
        (^or {.#Parameter _}
             {.#Var _}
             {.#Ex _}
             {.#Named _})
        it))))