(;module:
  lux
  (lux (control codec
                monad)
       (data [text]
             (text format
                   ["l" lexer "l/" Monad<Lexer>])
             [number]
             ["e" error]
             (coll [list "L/" Functor<List>]))
       (meta [type "type/" Eq<Type>]))
  ["&" ../common])

(do-template [<name> <code>]
  [(def: <name> &;Signal <code>)]

  [type-signal        "T"]
  [primitive-signal   "^"]
  [void-signal        "0"]
  [unit-signal        "1"]
  [product-signal     "*"]
  [sum-signal         "+"]
  [function-signal    ">"]
  [application-signal "%"]
  [uq-signal          "U"]
  [eq-signal          "E"]
  [bound-signal       "$"]
  [ex-signal          "!"]
  [var-signal         "?"]
  [named-signal       "@"]
  )

(def: (encode-type type)
  (-> Type Text)
  (if (or (is Type type)
          (type/= Type type))
    type-signal
    (case type
      (#;Primitive name params)
      (format primitive-signal name &;stop-signal (&;encode-list encode-type params))

      #;Void
      void-signal

      #;Unit
      unit-signal

      (^template [<tag> <prefix>]
        (<tag> left right)
        (format <prefix> (encode-type left) (encode-type right)))
      ([#;Product      product-signal]
       [#;Sum      sum-signal]
       [#;Function function-signal]
       [#;App      application-signal])


      (^template [<tag> <prefix>]
        (<tag> env body)
        (format <prefix> (&;encode-list encode-type env) (encode-type body)))
      ([#;UnivQ uq-signal]
       [#;ExQ   eq-signal])

      (^template [<tag> <prefix>]
        (<tag> idx)
        (format <prefix> (%i (nat-to-int idx)) &;stop-signal))
      ([#;Bound bound-signal]
       [#;Ex ex-signal]
       [#;Var var-signal])

      (#;Named [module name] type*)
      (format named-signal module &;ident-separator name &;stop-signal (encode-type type*))
      )))

(def: type-decoder
  (l;Lexer Type)
  (l;rec
   (function [type-decoder]
     (with-expansions
       [<simple> (do-template [<type> <signal>]
                   [(|> (l/wrap <type>) (l;after (l;text <signal>)))]

                   [Type    type-signal]
                   [#;Void void-signal]
                   [#;Unit unit-signal])
        <combinators> (do-template [<tag> <prefix>]
                        [(do l;Monad<Lexer>
                           [_ (l;text <prefix>)
                            left type-decoder
                            right type-decoder]
                           (wrap (<tag> left right)))]

                        [#;Product     product-signal]
                        [#;Sum      sum-signal]
                        [#;Function function-signal]
                        [#;App      application-signal])
        <abstractions> (do-template [<tag> <prefix>]
                         [(do l;Monad<Lexer>
                            [_ (l;text <prefix>)
                             env (&;decode-list type-decoder)
                             body type-decoder]
                            (wrap (<tag> env body)))]

                         [#;UnivQ uq-signal]
                         [#;ExQ   eq-signal])
        <wildcards> (do-template [<tag> <prefix>]
                      [(do l;Monad<Lexer>
                         [_ (l;text <prefix>)
                          id (l;codec number;Codec<Text,Int>
                                      (l;some' l;digit))
                          _ (l;text &;stop-signal)]
                         (wrap (<tag> (int-to-nat id))))]

                      [#;Bound bound-signal]
                      [#;Ex    ex-signal]
                      [#;Var   var-signal])]
       ($_ l;either
           (do l;Monad<Lexer>
             [_ (l;text primitive-signal)
              name (l;many' (l;none-of &;stop-signal))
              _ (l;text &;stop-signal)
              params (&;decode-list type-decoder)]
             (wrap (#;Primitive name params)))
           <simple>
           <combinators>
           <abstractions>
           <wildcards>
           (do l;Monad<Lexer>
             [_ (l;text named-signal)
              module (l;some' (l;none-of &;ident-separator))
              _ (l;text &;ident-separator)
              name (l;many' (l;none-of &;stop-signal))
              _ (l;text &;stop-signal)
              unnamed type-decoder]
             (wrap (#;Named [module name] unnamed)))
           )))))

(def: (decode-type input)
  (-> Text (e;Error Type))
  (|> type-decoder
      (l;before l;end)
      (l;run input)))

(struct: #export _ (Codec Text Type)
  (def: encode encode-type)
  (def: decode decode-type))