path: root/stdlib/source/parser/lux/meta/type.lux

(.require
 [library
  [lux (.except function local parameter)
   [abstract
    ["[0]" monad (.only do)]]
   [control
    ["//" parser]
    ["[0]" try (.only Try)]
    ["[0]" exception (.only Exception)]
    ["[0]" function]]
   [data
    ["[0]" text (.use "[1]#[0]" monoid)
     ["%" \\format (.only format)]]
    [collection
     ["[0]" list (.use "[1]#[0]" functor)]
     ["[0]" dictionary (.only Dictionary)]]]
   [math
    [number
     ["n" nat (.use "[1]#[0]" decimal)]]]
   [meta
    ["[0]" code]
    [macro
     ["^" pattern]]]]]
 [\\library
  ["[0]" / (.use "[1]#[0]" equivalence)
   ["[0]" check]]])

(def |recursion_dummy|
  (template (|recursion_dummy|)
    [{.#Primitive "" {.#End}}]))

(with_template [<name>]
  [(exception.def .public (<name> type)
     (Exception Type)
     (exception.report
      (list ["Type" (%.type type)])))]

  [not_existential]
  [not_recursive]
  [not_named]
  [not_parameter]
  [unknown_parameter]
  [not_function]
  [not_application]
  [not_polymorphic]
  [not_variant]
  [not_tuple]
  )

(with_template [<name>]
  [(exception.def .public (<name> [expected actual])
     (Exception [Type Type])
     (exception.report
      (list ["Expected" (%.type expected)]
            ["Actual" (%.type actual)])))]

  [types_do_not_match]
  [wrong_parameter]
  )

(exception.def .public empty_input)

(exception.def .public (unconsumed_input remaining)
  (Exception (List Type))
  (exception.report
   (list ["Types" (|> remaining
                      (list#each (|>> %.type (format text.new_line "* ")))
                      (text.interposed ""))])))

(type .public Env
  (Dictionary Nat [Type Code]))

(type .public (Parser a)
  (//.Parser [Env (List Type)] a))

(def .public fresh
  Env
  (dictionary.empty n.hash))

(def (result' env poly types)
  (All (_ a) (-> Env (Parser a) (List Type) (Try a)))
  (when (//.result poly [env types])
    {try.#Failure error}
    {try.#Failure error}

    {try.#Success [[env' remaining] output]}
    (when remaining
      {.#End}
      {try.#Success output}

      _
      (exception.except ..unconsumed_input remaining))))

(def .public (result poly type)
  (All (_ a) (-> (Parser a) Type (Try a)))
  (result' ..fresh poly (list type)))

(def .public env
  (Parser Env)
  (.function (_ [env inputs])
    {try.#Success [[env inputs] env]}))

(def (with_env temp poly)
  (All (_ a) (-> Env (Parser a) (Parser a)))
  (.function (_ [env inputs])
    (when (//.result poly [temp inputs])
      {try.#Failure error}
      {try.#Failure error}

      {try.#Success [[_ remaining] output]}
      {try.#Success [[env remaining] output]})))

(def .public next
  (Parser Type)
  (.function (_ [env inputs])
    (when inputs
      {.#End}
      (exception.except ..empty_input [])

      {.#Item headT tail}
      {try.#Success [[env inputs] headT]})))

(def .public any
  (Parser Type)
  (.function (_ [env inputs])
    (when inputs
      {.#End}
      (exception.except ..empty_input [])

      {.#Item headT tail}
      {try.#Success [[env tail] headT]})))

(def .public (local types poly)
  (All (_ a) (-> (List Type) (Parser a) (Parser a)))
  (.function (_ [env pass_through])
    (when (result' env poly types)
      {try.#Failure error}
      {try.#Failure error}

      {try.#Success output}
      {try.#Success [[env pass_through] output]})))

(def (label idx)
  (-> Nat Code)
  (code.local (all text#composite "label" text.tab (n#encoded idx))))

(def .public (with_extension type poly)
  (All (_ a) (-> Type (Parser a) (Parser [Code a])))
  (.function (_ [env inputs])
    (let [current_id (dictionary.size env)
          g!var (label current_id)]
      (when (//.result poly
                       [(dictionary.has current_id [type g!var] env)
                        inputs])
        {try.#Failure error}
        {try.#Failure error}

        {try.#Success [[_ inputs'] output]}
        {try.#Success [[env inputs'] [g!var output]]}))))

(with_template [<name> <flattener> <exception>]
  [(`` (def .public (<name> poly)
         (All (_ a) (-> (Parser a) (Parser a)))
         (do //.monad
           [headT ..any]
           (let [members (<flattener> (/.anonymous headT))]
             (if (n.> 1 (list.size members))
               (local members poly)
               (//.failure (exception.error <exception> headT)))))))]

  [variant /.flat_variant ..not_variant]
  [tuple   /.flat_tuple   ..not_tuple]
  )

(def polymorphic'
  (Parser [Nat Type])
  (do //.monad
    [headT any
     .let [[num_arg bodyT] (/.flat_univ_q (/.anonymous headT))]]
    (if (n.= 0 num_arg)
      (//.failure (exception.error ..not_polymorphic headT))
      (in [num_arg bodyT]))))

(def .public (polymorphic poly)
  (All (_ a) (-> (Parser a) (Parser [Code (List Code) a])))
  (do [! //.monad]
    [headT any
     funcI (at ! each dictionary.size ..env)
     [num_args non_poly] (local (list headT) ..polymorphic')
     env ..env
     .let [funcL (label funcI)
           [all_varsL env'] (loop (again [current_arg 0
                                          env' env
                                          all_varsL (is (List Code) (list))])
                              (if (n.< num_args current_arg)
                                (if (n.= 0 current_arg)
                                  (let [varL (label (++ funcI))]
                                    (again (++ current_arg)
                                           (|> env'
                                               (dictionary.has funcI [headT funcL])
                                               (dictionary.has (++ funcI) [{.#Parameter (++ funcI)} varL]))
                                           {.#Item varL all_varsL}))
                                  (let [partialI (|> current_arg (n.* 2) (n.+ funcI))
                                        partial_varI (++ partialI)
                                        partial_varL (label partial_varI)
                                        partialC (` ((, funcL) (,* (|> (list.indices num_args)
                                                                       (list#each (|>> (n.* 2) ++ (n.+ funcI) label))
                                                                       list.reversed))))]
                                    (again (++ current_arg)
                                           (|> env'
                                               (dictionary.has partialI [(|recursion_dummy|) partialC])
                                               (dictionary.has partial_varI [{.#Parameter partial_varI} partial_varL]))
                                           {.#Item partial_varL all_varsL})))
                                [all_varsL env']))]]
    (<| (with_env env')
        (local (list non_poly))
        (do !
          [output poly]
          (in [funcL all_varsL output])))))

(def .public (function in_poly out_poly)
  (All (_ i o) (-> (Parser i) (Parser o) (Parser [i o])))
  (do //.monad
    [headT any
     .let [[inputsT outputT] (/.flat_function (/.anonymous headT))]]
    (if (n.> 0 (list.size inputsT))
      (//.and (local inputsT in_poly)
              (local (list outputT) out_poly))
      (//.failure (exception.error ..not_function headT)))))

(def .public (applied poly)
  (All (_ a) (-> (Parser a) (Parser a)))
  (do //.monad
    [headT any
     .let [[funcT paramsT] (/.flat_application (/.anonymous headT))]]
    (if (n.= 0 (list.size paramsT))
      (//.failure (exception.error ..not_application headT))
      (..local {.#Item funcT paramsT} poly))))

(with_template [<name> <test>]
  [(def .public (<name> expected)
     (-> Type (Parser Any))
     (do //.monad
       [actual any]
       (if (<test> expected actual)
         (in [])
         (//.failure (exception.error ..types_do_not_match [expected actual])))))]

  [exactly /#=]
  [sub     check.subsumes?]
  [super   (function.flipped check.subsumes?)]
  )

(def .public (argument env idx)
  (-> Env Nat Nat)
  (let [env_level (n./ 2 (dictionary.size env))
        parameter_level (n./ 2 idx)
        parameter_idx (n.% 2 idx)]
    (|> env_level -- (n.- parameter_level) (n.* 2) (n.+ parameter_idx))))

(def .public parameter
  (Parser Code)
  (do //.monad
    [env ..env
     headT any]
    (when headT
      {.#Parameter idx}
      (when (dictionary.value (..argument env idx) env)
        {.#Some [poly_type poly_code]}
        (in poly_code)

        {.#None}
        (//.failure (exception.error ..unknown_parameter headT)))

      _
      (//.failure (exception.error ..not_parameter headT)))))

(def .public (this_parameter id)
  (-> Nat (Parser Any))
  (do //.monad
    [env ..env
     headT any]
    (when headT
      {.#Parameter idx}
      (if (n.= id (..argument env idx))
        (in [])
        (//.failure (exception.error ..wrong_parameter [{.#Parameter id} headT])))

      _
      (//.failure (exception.error ..not_parameter headT)))))

(def .public existential
  (Parser Nat)
  (do //.monad
    [headT any]
    (when headT
      {.#Ex ex_id}
      (in ex_id)

      _
      (//.failure (exception.error ..not_existential headT)))))

(def .public named
  (Parser [Symbol Type])
  (do //.monad
    [inputT any]
    (when inputT
      {.#Named name anonymousT}
      (in [name anonymousT])

      _
      (//.failure (exception.error ..not_named inputT)))))

(def .public (recursive poly)
  (All (_ a) (-> (Parser a) (Parser [Code a])))
  (do [! //.monad]
    [headT any]
    (when (/.anonymous headT)
      {.#Apply (|recursion_dummy|) {.#UnivQ _ headT'}}
      (do !
        [[recT _ output] (|> poly
                             (with_extension (|recursion_dummy|))
                             (with_extension headT)
                             (local (list headT')))]
        (in [recT output]))

      _
      (//.failure (exception.error ..not_recursive headT)))))

(def .public recursive_self
  (Parser Code)
  (do //.monad
    [env ..env
     headT any]
    (when (/.anonymous headT)
      (^.multi {.#Apply (|recursion_dummy|) {.#Parameter funcT_idx}}
               (n.= 0 (..argument env funcT_idx))
               [(dictionary.value 0 env) {.#Some [self_type self_call]}])
      (in self_call)

      _
      (//.failure (exception.error ..not_recursive headT)))))

(def .public recursive_call
  (Parser Code)
  (do [! //.monad]
    [env ..env
     [funcT argsT] (..applied (//.and any (//.many any)))
     _ (local (list funcT) (..this_parameter 0))
     allC (let [allT (list.partial funcT argsT)]
            (|> allT
                (monad.each ! (function.constant ..parameter))
                (local allT)))]
    (in (` ((,* allC))))))