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

(.require
 [library
  [lux (.except function as let)
   [abstract
    [equivalence (.only Equivalence)]
    [monad (.only Monad do)]]
   [control
    ["<>" parser]
    ["[0]" function]
    ["[0]" maybe]]
   [data
    ["[0]" product]
    ["[0]" text (.use "[1]#[0]" monoid equivalence)]
    [collection
     ["[0]" array]
     ["[0]" list (.use "[1]#[0]" monad monoid mix)]]]
   [math
    [number
     ["n" nat (.use "[1]#[0]" decimal)]]]
   ["[0]" meta (.only)
    ["@" target]
    ["[0]" location]
    ["[0]" symbol (.use "[1]#[0]" equivalence codec)]
    ["[0]" code (.only)
     ["<[1]>" \\parser (.only Parser)]]
    ["[0]" macro (.only)
     [syntax (.only syntax)]
     ["^" pattern]]]]])

(with_template [<name> <tag>]
  [(def .public (<name> type)
     (-> Type [Nat Type])
     (loop (again [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.partial 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)]))

(with_template [<name> <tag>]
  [(def .public (<name> type)
     (-> Type (List Type))
     (case type
       {<tag> left right}
       (list.partial left (<name> right))

       _
       (list type)))]

  [flat_variant .#Sum]
  [flat_tuple   .#Product]
  )

(def .public (format type)
  (-> Type Text)
  (case type
    {.#Primitive name params}
    (all text#composite
         "(Primitive "
         (text.enclosed' text.double_quote name)
         (|> params
             (list#each (|>> format (text#composite " ")))
             (list#mix (function.flipped text#composite) ""))
         ")")

    (^.with_template [<tag> <open> <close> <flat>]
      [{<tag> _}
       (all 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)]
      (all text#composite  "(-> "
           (|> ins
               (list#each format)
               list.reversed
               (list.interposed " ")
               (list#mix text#composite ""))
           " " (format out) ")"))

    {.#Parameter idx}
    (n#encoded idx)

    {.#Var id}
    (all text#composite "-" (n#encoded id))

    {.#Ex id}
    (all text#composite "+" (n#encoded id))

    {.#Apply param fun}
    (.let [[type_func type_args] (flat_application type)]
      (all text#composite  "(" (format type_func) " " (|> type_args (list#each format) list.reversed (list.interposed " ") (list#mix text#composite "")) ")"))

    (^.with_template [<tag> <desc>]
      [{<tag> env body}
       (all text#composite "(" <desc> " {" (|> env (list#each format) (text.interposed " ")) "} " (format body) ")")])
    ([.#UnivQ "All"]
     [.#ExQ "Ex"])

    {.#Named [module name] type}
    (all 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)}
    
    (^.with_template [<tag>]
      [{<tag> left right}
       {<tag> (reduced env left) (reduced env right)}])
    ([.#Sum]      [.#Product]
     [.#Function] [.#Apply])
    
    (^.with_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! (all text#composite
                             "Unknown type parameter" text.new_line
                             "      Index: " (n#encoded idx) text.new_line
                             "Environment: " (|> env
                                                 list.enumeration
                                                 (list#each (.function (_ [index type])
                                                              (all text#composite
                                                                   (n#encoded index)
                                                                   " " (..format type))))
                                                 (text.interposed (text#composite text.new_line "             ")))))
                (list.item idx env))
    
    _
    type
    ))

(def .public equivalence
  (Equivalence Type)
  (implementation
   (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)))

           (^.with_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))

           (^.with_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
      (^.with_template [<tag>]
        [{<tag> env body}
         (|> body
             (reduced (list.partial func param env))
             (applied params'))])
      ([.#UnivQ] [.#ExQ])

      {.#Apply A F}
      (applied (list.partial 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)))})

    (^.with_template [<tag>]
      [{<tag> idx}
       (` {<tag> (, (code.nat idx))})])
    ([.#Var] [.#Ex] [.#Parameter])

    (^.with_template [<tag>]
      [{<tag> left right}
       (` {<tag> (, (code left))
                 (, (code right))})])
    ([.#Sum] [.#Product] [.#Function] [.#Apply])

    {.#Named name sub_type}
    (code.symbol name)

    (^.with_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))

(with_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})))

(with_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)
        (at 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)))

(def new_secret_marker
  (syntax (_ [])
    (macro.with_symbols [g!_secret_marker_]
      (in (list g!_secret_marker_)))))

(def secret_marker
  (`` (symbol (,, (new_secret_marker)))))

(def .public log!
  (syntax (_ [input (<>.or (<>.and <code>.symbol
                                   (<>.maybe (<>.after (<code>.this_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"
                  (all 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)))

(def .public as
  (syntax (_ [type_vars type_parameters
              input <code>.any
              output <code>.any
              value (<>.maybe <code>.any)])
    (macro.with_symbols [g!_]
      (.let [casterC (` (is (All ((, g!_) (,* (list#each code.local type_vars)))
                              (-> (, input) (, output)))
                            (|>> as_expected)))]
        (case value
          {.#None}
          (in (list casterC))
          
          {.#Some value}
          (in (list (` ((, casterC) (, value))))))))))

(type Typed
  (Record
   [#type Code
    #expression Code]))

(def (typed lux)
  (-> Lux (Parser Typed))
  (do <>.monad
    [it <code>.any
     type_check (<>.lifted (meta.result lux (macro.expansion it)))]
    (<| (<code>.locally type_check)
        <code>.form
        (<>.after (<code>.this (` "lux type check")))
        (<>.and <code>.any <code>.any))))

... TODO: Make sure the generated code always gets optimized away.
(def .public sharing
  (syntax (_ lux [type_vars ..type_parameters
                  exemplar (..typed lux)
                  computation (..typed lux)])
    (macro.with_symbols [g!_]
      (.let [typeC (` (All ((, g!_) (,* (list#each code.local type_vars)))
                        (-> (, (the #type exemplar))
                            (, (the #type computation)))))
             shareC (` (is (, typeC)
                           (.function ((, g!_) (, g!_))
                             (, (the #expression computation)))))]
        (in (list (` ((, shareC) (, (the #expression exemplar))))))))))

(def .public by_example
  (syntax (_ lux [type_vars ..type_parameters
                  exemplar (..typed lux)
                  extraction <code>.any])
    (in (list (` (.type_of ((,! ..sharing) [(,* (list#each code.local type_vars))]
                            (is (, (the #type exemplar))
                                (, (the #expression exemplar)))
                            (is (, 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 (at ..equivalence = before it)
      after
      (case it
        {.#Primitive name co_variant}
        {.#Primitive name (list#each again co_variant)}

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

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

(def .public let
  (syntax (_ [bindings (<code>.tuple (<>.some (<>.and <code>.any <code>.any)))
              bodyT <code>.any])
    (in (list (` (..with_expansions [(,* (|> bindings
                                             (list#each (.function (_ [localT valueT])
                                                          (list localT (` (.these (, valueT))))))
                                             list#conjoint))]
                   (, bodyT)))))))