(;module: {#;doc "Basic functionality for working with types."}
  [lux #- function]
  (lux (control [eq #+ Eq]
                ["M" monad #+ do Monad])
       (data [text "Text/" Monoid<Text> Eq<Text>]
             [ident "Ident/" Eq<Ident>]
             [number "Nat/" Codec<Text,Nat>]
             [maybe]
             (coll [list #+ "List/" Monad<List> Monoid<List> Fold<List>]))
       (macro [code])
       ))

## [Utils]
(def: (beta-reduce env type)
  (-> (List Type) Type Type)
  (case type
    (#;Host name params)
    (#;Host name (List/map (beta-reduce env) params))
    
    (^template [<tag>]
      (<tag> left right)
      (<tag> (beta-reduce env left) (beta-reduce env right)))
    ([#;Sum]      [#;Product]
     [#;Function] [#;Apply])
    
    (^template [<tag>]
      (<tag> old-env def)
      (case old-env
        #;Nil
        (<tag> env def)

        _
        type))
    ([#;UnivQ]
     [#;ExQ])
    
    (#;Bound idx)
    (default (error! (Text/append "Unknown type var: " (Nat/encode idx)))
      (list;nth idx env))
    
    _
    type
    ))

## [Structures]
(struct: #export _ (Eq Type)
  (def: (= x y)
    (case [x y]
      [(#;Host xname xparams) (#;Host yname yparams)]
      (and (Text/= xname yname)
           (n.= (list;size yparams) (list;size xparams))
           (List/fold (;function [[x y] prev] (and prev (= x y)))
                      true
                      (list;zip2 xparams yparams)))

      (^template [<tag>]
        [<tag> <tag>]
        true)
      ([#;Void] [#;Unit])
      
      (^template [<tag>]
        [(<tag> xid) (<tag> yid)]
        (n.= yid xid))
      ([#;Var] [#;Ex] [#;Bound])

      (^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 (Ident/= 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/fold (;function [[x y] prev] (and prev (= x y)))
                      true
                      (list;zip2 xenv yenv)))

      _
      false
      )))

## [Values]
(do-template [<name> <tag>]
  [(def: #export (<name> type)
     (-> Type [Nat Type])
     (loop [num-args +0
            type type]
       (case type
         (<tag> env sub-type)
         (recur (n.inc num-args) sub-type)

         _
         [num-args type])))]

  [flatten-univ-q #;UnivQ]
  [flatten-ex-q   #;ExQ]
  )

(def: #export (flatten-function type)
  (-> Type [(List Type) Type])
  (case type
    (#;Function in out')
    (let [[ins out] (flatten-function out')]
      [(list& in ins) out])

    _
    [(list) type]))

(def: #export (flatten-application type)
  (-> Type [Type (List Type)])
  (case type
    (#;Apply arg func')
    (let [[func args] (flatten-application func')]
      [func (List/append args (list arg))])

    _
    [type (list)]))

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

       _
       (list type)))]

  [flatten-variant #;Sum]
  [flatten-tuple   #;Product]
  )

(def: #export (apply params func)
  (-> (List Type) Type (Maybe Type))
  (case params
    #;Nil
    (#;Some func)

    (#;Cons param params')
    (case func
      (^template [<tag>]
        (<tag> env body)
        (|> body
            (beta-reduce (list& func param env))
            (apply params')))
      ([#;UnivQ] [#;ExQ])

      (#;Apply A F)
      (apply (list& A params) F)

      (#;Named name unnamed)
      (apply params unnamed)
      
      _
      #;None)))

(def: #export (to-ast type)
  (-> Type Code)
  (case type
    (#;Host name params)
    (` (#;Host (~ (code;text name))
               (list (~@ (List/map to-ast params)))))

    (^template [<tag>]
      <tag>
      (` <tag>))
    ([#;Void] [#;Unit])

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

    (^template [<tag>]
      (<tag> left right)
      (` (<tag> (~ (to-ast left))
                (~ (to-ast right)))))
    ([#;Function] [#;Apply])

    (^template [<tag> <macro> <flattener>]
      (<tag> left right)
      (` (<macro> (~@ (List/map to-ast (<flattener> type))))))
    ([#;Sum  | flatten-variant]
     [#;Product & flatten-tuple])

    (#;Named name sub-type)
    (code;symbol name)

    (^template [<tag>]
      (<tag> env body)
      (` (<tag> (list (~@ (List/map to-ast env)))
                (~ (to-ast body)))))
    ([#;UnivQ] [#;ExQ])
    ))

(def: #export (to-text type)
  (-> Type Text)
  (case type
    (#;Host name params)
    (case params
      #;Nil
      ($_ Text/append "(host " name ")")

      _
      ($_ Text/append "(host " name " " (|> params (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")"))

    #;Void
    "Void"
    
    #;Unit
    "Unit"

    (^template [<tag> <open> <close> <flatten>]
      (<tag> _)
      ($_ Text/append <open>
          (|> (<flatten> type)
              (List/map to-text)
              list;reverse
              (list;interpose " ")
              (List/fold Text/append ""))
          <close>))
    ([#;Sum  "(| " ")" flatten-variant]
     [#;Product "["   "]" flatten-tuple])

    (#;Function input output)
    (let [[ins out] (flatten-function type)]
      ($_ Text/append  "(-> "
          (|> ins
              (List/map to-text)
              list;reverse
              (list;interpose " ")
              (List/fold Text/append ""))
          " " (to-text out) ")"))

    (#;Bound idx)
    (Nat/encode idx)

    (#;Var id)
    ($_ Text/append "⌈v:" (Nat/encode id) "⌋")

    (#;Ex id)
    ($_ Text/append "⟨e:" (Nat/encode id) "⟩")

    (#;Apply param fun)
    (let [[type-func type-args] (flatten-application type)]
      ($_ Text/append  "(" (to-text type-func) " " (|> type-args (List/map to-text) list;reverse (list;interpose " ") (List/fold Text/append "")) ")"))

    (^template [<tag> <desc>]
      (<tag> env body)
      ($_ Text/append "(" <desc> " {" (|> env (List/map to-text) (text;join-with " ")) "} " (to-text body) ")"))
    ([#;UnivQ "All"]
     [#;ExQ "Ex"])

    (#;Named [module name] type)
    ($_ Text/append module ";" name)
    ))

(def: #export (un-alias type)
  (-> Type Type)
  (case type
    (#;Named _ (#;Named ident type'))
    (un-alias (#;Named ident type'))

    _
    type))

(def: #export (un-name type)
  (-> Type Type)
  (case type
    (#;Named ident type')
    (un-name type')

    _
    type))

(do-template [<name> <base> <ctor>]
  [(def: #export (<name> types)
     (-> (List Type) Type)
     (case types
       #;Nil
       <base>

       (#;Cons type #;Nil)
       type

       (#;Cons type types')
       (<ctor> type (<name> types'))))]

  [variant Void #;Sum]
  [tuple   Unit #;Product]
  )

(def: #export (function inputs output)
  (-> (List Type) Type Type)
  (case inputs
    #;Nil
    output

    (#;Cons input inputs')
    (#;Function input (function inputs' output))))

(def: #export (application params quant)
  (-> (List Type) Type Type)
  (case params
    #;Nil
    quant

    (#;Cons param params')
    (application params' (#;Apply param quant))))

(do-template [<name> <tag>]
  [(def: #export (<name> size body)
     (-> Nat Type Type)
     (case size
       +0 body
       _  (<tag> (list) (<name> (n.dec size) body))))]

  [univ-q #;UnivQ]
  [ex-q   #;ExQ]
  )

(def: #export (quantified? type)
  (-> Type Bool)
  (case type
    (#;Named [module name] _type)
    (quantified? _type)

    (#;Apply A F)
    (default false
      (do maybe;Monad<Maybe>
        [applied (apply (list A) F)]
        (wrap (quantified? applied))))
    
    (^or (#;UnivQ _) (#;ExQ _))
    true

    _
    false))