(.module:
  [library
   [lux {"-" [Definition Module type]}
    ["[0]" meta]
    ["[0]" type ("[1]\[0]" equivalence)]
    [abstract
     [monad {"+" [do]}]
     ["[0]" enum]]
    [control
     ["[0]" maybe ("[1]\[0]" functor)]
     ["[0]" exception {"+" [exception:]}]
     ["<>" parser ("[1]\[0]" monad)
      ["<[0]>" code {"+" [Parser]}]]]
    [data
     ["[0]" product]
     ["[0]" text {"+" [\n]} ("[1]\[0]" order)
      ["%" format {"+" [format]}]]
     [collection
      ["[0]" list ("[1]\[0]" monad mix monoid)]
      ["[0]" set {"+" [Set]}]
      ["[0]" sequence {"+" [Sequence]}]]
     [format
      ["md" markdown {"+" [Markdown Block]}]]]
    ["[0]" macro
     [syntax {"+" [syntax:]}]
     ["[0]" code]
     ["[0]" template]]
    [math
     [number
      ["n" nat]]]
    [tool
     [compiler
      [language
       [lux
        ["[0]" syntax]]]]]]])

(template: (|recursion_dummy|)
  [(#.Primitive "" #.End)])

(type: Fragment
  (Variant
   (#Comment Text)
   (#Code Code)))

(def: fragment
  (Parser Fragment)
  (<>.or <code>.text
         <code>.any))

(def: (reference_column code)
  (-> Code Nat)
  (case code
    (^template [<tag>]
      [[[_ _ column] (<tag> _)]
       column])
    ([#.Bit]
     [#.Nat]
     [#.Int]
     [#.Rev]
     [#.Frac]
     [#.Text]
     [#.Identifier]
     [#.Tag])

    (^template [<tag>]
      [[[_ _ column] (<tag> members)]
       (|> members
           (list\each reference_column)
           (list\mix n.min column))])
    ([#.Form]
     [#.Tuple])

    [[_ _ column] (#.Record pairs)]
    (|> (list\composite (list\each (|>> product.left reference_column) pairs)
                        (list\each (|>> product.right reference_column) pairs))
        (list\mix n.min column))
    ))

(def: (padding reference_column [_ old_line old_column] [_ new_line new_column])
  (-> Nat Location Location Text)
  (if (n.= old_line new_line)
    (if (n.< old_column new_column)
      ""
      (text.together (list.repeated (n.- old_column new_column) " ")))
    (format (if (n.< old_line new_line)
              ""
              (text.together (list.repeated (n.- old_line new_line) \n)))
            (if (n.< reference_column new_column)
              ""
              (text.together (list.repeated (n.- reference_column new_column) " "))))))

(def: un_paired
  (All (_ a) (-> (List [a a]) (List a)))
  (let [melded (: (All (_ a) (-> [a a] (List a) (List a)))
                  (function (_ [left right] tail)
                    (list& left right tail)))]
    (|>> list.reversed
         (list\mix melded #.End))))

(def: (code_documentation expected_module old_location reference_column example)
  (-> Text Location Nat Code [Location Text])
  (case example
    (^template [<tag> <prefix>]
      [[new_location (<tag> [module short])]
       (let [documentation (<| (text.prefix <prefix>)
                               (cond (text\= expected_module module)
                                     short

                                     (text\= .prelude_module module)
                                     (format "." short)
                                     
                                     ... else
                                     (%.name [module short])))]
         [(revised@ #.column (n.+ (text.size documentation)) new_location)
          (format (padding reference_column old_location new_location)
                  documentation)])])
    ([#.Identifier ""]
     [#.Tag syntax.sigil])
    
    (^template [<tag> <format>]
      [[new_location (<tag> value)]
       (let [documentation (`` (|> value (~~ (template.spliced <format>))))]
         [(revised@ #.column (n.+ (text.size documentation)) new_location)
          (format (padding reference_column old_location new_location)
                  documentation)])])
    ([#.Bit [%.bit]]
     [#.Nat [%.nat]]
     [#.Int [%.int]]
     [#.Rev [%.rev]]
     [#.Frac [%.frac]]
     [#.Text [%.text]])

    (^template [|<| |>| <tag> <prep>]
      [[group_location (<tag> members)]
       (let [[group_location' members_documentation] (list\mix (function (_ part [last_location text_accum])
                                                                 (let [[member_location member_documentation] (code_documentation expected_module last_location reference_column part)]
                                                                   [member_location (format text_accum member_documentation)]))
                                                               [(revised@ #.column ++ group_location) ""]
                                                               (<prep> members))]
         [(revised@ #.column ++ group_location')
          (format (padding reference_column old_location group_location)
                  |<| members_documentation |>|)])])
    ([syntax.open_form   syntax.close_form   #.Form   |>]
     [syntax.open_tuple  syntax.close_tuple  #.Tuple  |>]
     [syntax.open_record syntax.close_record #.Record ..un_paired])
    ))

(def: blank_line
  Text
  (format \n \n))

(def: single_line_comment
  (-> Text Text)
  (text.prefix "... "))

(def: (fragment_documentation module fragment)
  (-> Text Fragment Text)
  (case fragment
    (#Comment comment)
    (..single_line_comment comment)

    (#Code example)
    (let [reference_column (..reference_column example)
          [location _] example]
      (|> example
          (..code_documentation module (with@ #.column reference_column location) reference_column)
          product.right))))

(def: parameter_name_options "abcdefghijklmnopqrstuvwxyz")
(def: parameter_name_options_count (text.size parameter_name_options))

(def: (parameter_type_name id)
  (-> Nat Text)
  (format "_" (%.nat id))
  ... (case (text.char id ..parameter_name_options)
  ...   (#.Some char)
  ...   (text.of_char char)

  ...   #.None
  ...   (format (parameter_type_name (n./ parameter_name_options_count id))
  ...           (parameter_type_name (n.% parameter_name_options_count id))))
  )

(def: type_variable_names
  (Sequence Text)
  (sequence.iterations (product.forked ++ parameter_type_name)
                       0))

(template [<name> <partition>]
  [(def: (<name> id)
     (-> Nat Bit)
     (<partition> id))]

  [type_function? n.even?]
  [type_parameter? n.odd?]
  )

(def: (parameter_id level id)
  (-> Nat Nat Nat)
  (n.- (n./ 2 id) level))

(def: (parameter_name [type_function_name type_function_arguments] level id)
  (-> [Text (List Text)] Nat Nat Text)
  (if (type_parameter? id)
    (let [parameter_id (..parameter_id level id)]
      (case (list.item parameter_id type_function_arguments)
        (#.Some found)
        found

        _
        (let [parameter_id (n.- (list.size type_function_arguments) parameter_id)]
          (|> type_variable_names
              (sequence.only (function (_ var_name)
                               (not (list.member? text.equivalence type_function_arguments var_name))))
              (sequence.item parameter_id)))))      
    type_function_name))

(def: (level_parameters offset level)
  (-> Nat Nat (List Text))
  (if (n.= 0 level)
    (list)
    (|> level
        --
        (enum.range n.enum 0)
        (list\each (|>> (n.+ (++ offset)) parameter_type_name)))))

(def: (nested line_prefix body)
  (-> Text Text Text)
  (|> body
      (text.all_split_by \n)
      (list\each (text.prefix line_prefix))
      (text.interposed \n)))

(def: (%type' level type_function_name nestable? module type)
  (-> Nat Text Bit Text Type Text)
  (case type
    (#.Primitive name params)
    (|> params
        (list\each (|>> (%type' level type_function_name false module)
                        (format " ")))
        (#.Item (%.text name))
        text.together
        (text.enclosed ["(primitive " ")"]))

    (#.Sum _)
    (|> type
        type.flat_variant
        (list\each (%type' level type_function_name false module))
        (text.interposed " ")
        (text.enclosed ["(Or " ")"]))

    (#.Product _)
    (|> type
        type.flat_tuple
        (list\each (%type' level type_function_name false module))
        (text.interposed " ")
        (text.enclosed ["[" "]"]))

    (#.Function input output)
    (let [[ins out] (type.flat_function type)]
      (format  "(-> "
               (|> ins (list\each (%type' level type_function_name false module)) (text.interposed " "))
               " "
               (%type' level type_function_name false module out)
               ")"))

    (#.Parameter idx)
    (parameter_name [type_function_name (list)] level idx)

    (^template [<tag> <pre> <post>]
      [(<tag> id)
       (format <pre> (%.nat id) <post>)])
    ([#.Var "⌈" "⌋"]
     [#.Ex  "⟨" "⟩"])

    (^template [<tag> <name> <flat>]
      [(<tag> _)
       (let [[level' body] (<flat> type)
             args (level_parameters level level')
             body_doc (%type' (n.+ level level') type_function_name nestable? module body)]
         (format "(" <name> " " "(_ " (|> args (text.interposed " ")) ")"
                 (if nestable?
                   (format \n (nested "  " body_doc))
                   (format " " body_doc))
                 ")"))])
    ([#.UnivQ "All" type.flat_univ_q]
     [#.ExQ   "Ex"  type.flat_ex_q])

    (^ (#.Apply (|recursion_dummy|) (#.Parameter 0)))
    type_function_name

    (^ (#.Apply (|recursion_dummy|) (#.UnivQ _ body)))
    (format "(Rec " type_function_name
            \n (nested " " (%type' level type_function_name nestable? module body))
            ")")

    (#.Apply param fun)
    (let [[type_func type_arguments] (type.flat_application type)]
      (format  "(" (%type' level type_function_name false module type_func)
               " " (|> type_arguments
                       (list\each (%type' level type_function_name false module))
                       (text.interposed " "))
               ")"))

    (#.Named [_module _name] type)
    (cond (text\= module _module)
          _name

          (text\= .prelude_module _module)
          (format "." _name)

          ... else
          (%.name [_module _name]))
    ))

(def: type
  (-> Text Type Text)
  (%type' (-- 0) "?" true))

(def: (parameterized_type arity type)
  (-> Nat Type (Maybe Type))
  (case arity
    0 (#.Some type)
    _ (case type
        (#.UnivQ _env _type)
        (parameterized_type (-- arity) _type)

        _
        #.None)))

(def: (type_definition' nestable? level arity type_function_info tags module type)
  (-> Bit Nat Nat [Text (List Text)] (List Text) Text Type Text)
  (case tags
    (^ (list single_tag))
    (format "(Record" \n
            " [#" single_tag " " (type_definition' false level arity type_function_info #.None module type) "])")

    _
    (case type
      (#.Primitive name params)
      (case params
        #.End
        (format "(primitive " (%.text name) ")")

        _
        (format "(primitive " (%.text name) " " (|> params (list\each (type_definition' false level arity type_function_info #.None module)) (text.interposed " ")) ")"))

      (#.Sum _)
      (let [members (type.flat_variant type)]
        (case tags
          #.End
          (format "(Or "
                  (|> members
                      (list\each (type_definition' false level arity type_function_info #.None module))
                      (text.interposed " "))
                  ")")

          _
          (|> members
              (list.zipped/2 tags)
              (list\each (function (_ [t_name type])
                           (case type
                             (#.Product _)
                             (let [types (type.flat_tuple type)]
                               (format " (#" t_name " "
                                       (|> types
                                           (list\each (type_definition' false level arity type_function_info #.None module))
                                           (text.interposed " "))
                                       ")"))

                             _
                             (format " (#" t_name " " (type_definition' false level arity type_function_info #.None module type) ")"))))
              (text.interposed \n)
              (text.enclosed [(format "(Variant" \n) ")"]))))

      (#.Product _)
      (let [members (type.flat_tuple type)]
        (case tags
          #.End
          (format "[" (|> members (list\each (type_definition' false level arity type_function_info #.None module)) (text.interposed " ")) "]")

          _
          (|> members
              (list.zipped/2 tags)
              (list\each (function (_ [t_name type])
                           (format "#" t_name " " (type_definition' false level arity type_function_info #.None module type))))
              (text.interposed (format \n "  "))
              (text.enclosed [" [" "]"])
              (text.enclosed [(format "(Record" \n) ")"]))))

      (#.Function input output)
      (let [[ins out] (type.flat_function type)]
        (format  "(-> " (|> ins (list\each (type_definition' false level arity type_function_info #.None module)) (text.interposed " "))
                 " "
                 (type_definition' false level arity type_function_info #.None module out)
                 ")"))

      (#.Parameter idx)
      (parameter_name type_function_info level idx)

      (^template [<tag> <pre>]
        [(<tag> id)
         (format <pre> (%.nat id))])
      ([#.Var "-"]
       [#.Ex  "+"])

      (^template [<tag> <name> <flat>]
        [(<tag> _)
         (let [[level' body] (<flat> type)
               args (level_parameters (n.- arity level) level')
               body_doc (type_definition' nestable? (n.+ level level') arity type_function_info tags module body)
               fn_name (case type_function_info
                         [fn_name #.End] fn_name
                         _ "_")]
           (format "(" <name> " " "(" fn_name " " (text.interposed " " args) ")"
                   (if nestable?
                     (format \n (..nested "  " body_doc))
                     (format " " body_doc))
                   ")"))])
      ([#.UnivQ "All" type.flat_univ_q]
       [#.ExQ   "Ex"  type.flat_ex_q])

      ... Recursive call
      (^ (#.Apply (|recursion_dummy|) (#.Parameter 0)))
      (product.left type_function_info)

      (^ (#.Apply (|recursion_dummy|) (#.UnivQ _ body)))
      (|> (type_definition' nestable? level arity type_function_info tags module body)
          (text.all_split_by \n)
          (list\each (text.prefix " "))
          (text.interposed \n)
          (text.enclosed [(format "(Rec " (product.left type_function_info) \n)
                          ")"]))

      (#.Apply param fun)
      (let [[type_func type_arguments] (type.flat_application type)]
        (format  "(" (type_definition' false level arity type_function_info tags module type_func)
                 " " (|> type_arguments
                         (list\each (type_definition' false level arity type_function_info #.None module))
                         (text.interposed " "))
                 ")"))

      (#.Named [_module _name] type)
      (cond (text\= module _module)
            _name

            (text\= .prelude_module _module)
            (format "." _name)

            ... else
            (%.name [_module _name]))
      )))

(def: (type_definition module [name parameters] tags type)
  (-> Text [Text (List Text)] (List Text) Type Text)
  (let [arity (list.size parameters)]
    (case (parameterized_type arity type)
      (#.Some type)
      (type_definition' true (-- arity) arity [name parameters] tags module type)

      #.None
      (..type module type))))

(def: description
  (Parser (Maybe Code))
  (<>.or (<code>.text! "")
         <code>.any))

(exception: .public (unqualified_identifier {name Name})
  (exception.report
   ["Name" (%.name name)]))

(def: qualified_identifier
  (Parser Name)
  (do <>.monad
    [name <code>.identifier]
    (case name
      ["" _]
      (<>.failure (exception.error ..unqualified_identifier [name]))
      
      _
      (in name))))

(def: example_separator
  Code
  (let [c/01 "...."
        c/04 (format c/01 c/01 c/01 c/01)
        c/16 (format c/04 c/04 c/04 c/04)]
    (code.text (format blank_line
                       c/16 \n c/16
                       blank_line))))

(type: Example
  (List Fragment))

(def: example
  (Parser Example)
  (<code>.tuple (<>.many ..fragment)))

(def: (example_documentation module example)
  (-> Text Example Code)
  (|> example
      (list\each (..fragment_documentation module))
      (list.interposed ..blank_line)
      (text.interposed "")
      code.text))

(type: Declaration
  [Name (List Text)])

(def: declaration
  (Parser Declaration)
  (<>.either (<>.and ..qualified_identifier (<>\in (list)))
             (<code>.form (<>.and ..qualified_identifier
                                  (<>.some (<code>.local_identifier))))))

(syntax: (minimal_definition_documentation
          [[name parameters] ..declaration])
  (do meta.monad
    [.let [g!module (code.text (product.left name))]
     [[_ def_type def_value]] (meta.export name)
     tags (meta.tags_of name)]
    (with_expansions [<\n> (~! text.\n)]
      (macro.with_identifiers [g!type]
        (in (list (` ($_ ((~! md.then))
                         ... Name
                         (<| ((~! md.heading/3))
                             (~ (code.text (%.code (let [g!name (|> name product.right code.local_identifier)]
                                                     (case parameters
                                                       #.End
                                                       g!name

                                                       _
                                                       (` ((~ g!name) (~+ (list\each code.local_identifier parameters))))))))))
                         ... Type
                         (let [(~ g!type) ("lux in-module"
                                           (~ g!module)
                                           (.:of (~ (code.identifier name))))]
                           ((~! md.code) "clojure"
                            (~ (if (type\= .Type def_type)
                                 (` (|> (~ (code.identifier name))
                                        (:as .Type)
                                        ((~! type.anonymous))
                                        ((~! ..type_definition)
                                         (~ g!module)
                                         [(~ (code.text (product.right name))) (list (~+ (list\each code.text parameters)))]
                                         (.list (~+ (|> tags
                                                        (maybe.else (list))
                                                        (list\each (|>> product.right code.text))))))
                                        ((~! %.format)
                                         ((~! ..single_line_comment) ((~! ..type) (~ g!module) (~ g!type)))
                                         <\n>)))
                                 (` ((~! ..type) (~ g!module) (~ g!type))))))))
                     )))))))

(syntax: (definition_documentation
          [[name parameters] ..declaration
           description ..description
           examples (<>.some ..example)])
  (with_expansions [<\n> (~! text.\n)]
    (in (list (` ($_ ((~! md.then))
                     ((~! ..minimal_definition_documentation)
                      ((~ (code.identifier name))
                       (~+ (list\each code.local_identifier parameters))))
                     ... Description
                     (~+ (case description
                           (#.Some description)
                           (list (` (<| ((~! md.paragraph))
                                        ((~! md.text))
                                        (~ description))))
                           
                           #.None
                           (list)))
                     ... Examples
                     (~+ (case examples
                           #.End
                           (list)
                           
                           _
                           (list (` (<| ((~! md.code) "clojure")
                                        ((~! %.format)
                                         (~+ (|> examples
                                                 (list\each (..example_documentation (product.left name)))
                                                 (list.interposed ..example_separator))))))))))
                 )))))

(type: .public Definition
  (Record
   [#definition Text
    #documentation (Markdown Block)]))

(type: .public Module
  (Record
   [#module Text
    #description Text
    #expected (Set Text)
    #definitions (List Definition)]))

(syntax: .public (default [[name parameters] ..declaration])
  (let [[_ short] name]
    (in (list (` (: (.List ..Definition)
                    (list [#..definition (~ (code.text short))
                           #..documentation ((~! ..minimal_definition_documentation)
                                             ((~ (code.identifier name))
                                              (~+ (list\each code.local_identifier parameters))))])))))))

(syntax: .public (documentation: [[name parameters] ..declaration
                                  extra (<>.some <code>.any)])
  (let [[_ short] name]
    (in (list (` (.def: .public (~ (code.local_identifier short))
                   (.List ..Definition)
                   (.list [#..definition (~ (code.text short))
                           #..documentation ((~! ..definition_documentation)
                                             ((~ (code.identifier name))
                                              (~+ (list\each code.local_identifier parameters)))
                                             (~+ extra))])))))))

(def: definitions_documentation
  (-> (List Definition) (Markdown Block))
  (|>> (list.sorted (function (_ left right)
                      (text\< (value@ #definition right)
                              (value@ #definition left))))
       (list\each (value@ #documentation))
       (list\mix md.then md.empty)))

(def: expected_separator
  Text
  (text.of_char 31))

(def: expected_format
  (-> (List Text) Text)
  (list\mix (function (_ short aggregate)
              (case aggregate
                "" short
                _ (format aggregate ..expected_separator short)))
            ""))

(def: expected
  (-> Text (Set Text))
  (|>> (text.all_split_by ..expected_separator)
       (set.of_list text.hash)))

(syntax: .public (module [[name _] ..qualified_identifier
                          description <code>.any
                          definitions (<code>.tuple (<>.some <code>.any))
                          subs (<code>.tuple (<>.some <code>.any))])
  (do meta.monad
    [expected (meta.exports name)]
    (in (list (` (: (List Module)
                    (list& [#..module (~ (code.text name))
                            #..description (~ description)
                            #..expected ((~! ..expected)
                                         (~ (code.text (|> expected
                                                           (list\each product.left)
                                                           ..expected_format))))
                            #..definitions ((~! list.together) (list (~+ definitions)))]
                           ($_ (\ (~! list.monoid) (~' composite))
                               (: (List Module)
                                  (\ (~! list.monoid) (~' identity)))
                               (~+ subs)))))))))

(def: listing
  (-> (List Text) (Markdown Block))
  (|>> (list.sorted text\<)
       (list\each (function (_ definition)
                    [(md.snippet definition)
                     #.None]))
       md.numbered_list))

(def: (module_documentation module)
  (-> Module (Markdown Block))
  (let [(^slots [#expected]) module]
    ($_ md.then
        ... Name
        (md.heading/1 (value@ #module module))
        ... Description
        (case (value@ #description module)
          "" md.empty
          description (<| md.paragraph
                          md.text
                          description))
        ... Definitions
        (md.heading/2 "Definitions")
        (|> module
            (value@ #definitions)
            (list.only (|>> (value@ #definition)
                            (set.member? expected)))
            ..definitions_documentation)
        ... Missing documentation
        (case (|> module
                  (value@ #definitions)
                  (list\mix (function (_ definition missing)
                              (set.lacks (value@ #definition definition) missing))
                            expected)
                  set.list)
          #.End
          md.empty

          missing
          ($_ md.then
              (md.heading/2 "Missing documentation")
              (..listing missing)))
        ... Un-expected documentation
        (case (|> module
                  (value@ #definitions)
                  (list.only (|>> (value@ #definition) (set.member? expected) not))
                  (list\each (value@ #definition)))
          #.End
          md.empty
          
          un_expected
          ($_ md.then
              (md.heading/2 "Un-expected documentation")
              (..listing un_expected)))
        )))

(def: .public documentation
  (-> (List Module) Text)
  (|>> (list.sorted (function (_ left right)
                      (text\< (value@ #module right) (value@ #module left))))
       (list\each ..module_documentation)
       (list.interposed md.horizontal_rule)
       (list\mix md.then (: (Markdown Block) md.empty))
       md.markdown))