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

(.require
 [library
  [lux (.except try except with)
   [abstract
    [functor (.only Functor)]
    [apply (.only Apply)]
    ["[0]" monad (.only Monad do)]]
   [control
    ["[0]" maybe]
    ["[0]" try (.only Try)]
    ["[0]" exception (.only Exception)]]
   [data
    ["[0]" product]
    ["[0]" text (.use "[1]#[0]" monoid equivalence)]
    [collection
     ["[0]" list (.use "[1]#[0]" mix)]
     ["[0]" set (.only Set)]]]
   [math
    [number
     ["n" nat (.use "[1]#[0]" decimal)]]]
   [meta
    ["@" target]
    [macro
     ["^" pattern]]]]]
 ["[0]" // (.use "[1]#[0]" equivalence)])

(def !n#=
  (template (_ reference subject)
    [(.i64_=# reference subject)]))

(def !text#=
  (template (_ reference subject)
    [(.text_=# reference subject)]))

(with_template [<name>]
  [(exception.def .public (<name> id)
     (Exception Nat)
     (exception.report
      (list ["ID" (n#encoded id)])))]

  [unknown_type_var]
  [unbound_type_var]
  )

(exception.def .public (invalid_type_application [funcT argT])
  (Exception [Type Type])
  (exception.report
   (list ["Type function" (//.format funcT)]
         ["Type argument" (//.format argT)])))

(exception.def .public (cannot_rebind_var [id type bound])
  (Exception [Nat Type Type])
  (exception.report
   (list ["Var" (n#encoded id)]
         ["Wanted type" (//.format type)]
         ["Current type" (//.format bound)])))

(exception.def .public (type_check_failed [expected actual])
  (Exception [Type Type])
  (exception.report
   (list ["Expected" (//.format expected)]
         ["Actual" (//.format actual)])))

(type .public Var
  Nat)

(type Assumption
  [Type Type])

(type .public (Check a)
  (-> Type_Context (Try [Type_Context a])))

(type (Checker a)
  (-> (List Assumption) a a (Check (List Assumption))))

(type Type_Vars
  (List [Var (Maybe Type)]))

(def .public functor
  (Functor Check)
  (implementation
   (def (each f fa)
     (function (_ context)
       (when (fa context)
         {try.#Success [context' output]}
         {try.#Success [context' (f output)]}

         {try.#Failure error}
         {try.#Failure error})))))

(def .public apply
  (Apply Check)
  (implementation
   (def functor ..functor)

   (def (on fa ff)
     (function (_ context)
       (when (ff context)
         {try.#Success [context' f]}
         (when (fa context')
           {try.#Success [context'' a]}
           {try.#Success [context'' (f a)]}

           {try.#Failure error}
           {try.#Failure error})

         {try.#Failure error}
         {try.#Failure error}
         )))
   ))

(def .public monad
  (Monad Check)
  (implementation
   (def functor ..functor)

   (def (in x)
     (function (_ context)
       {try.#Success [context x]}))

   (def (conjoint ffa)
     (function (_ context)
       (when (ffa context)
         {try.#Success [context' fa]}
         (when (fa context')
           {try.#Success [context'' a]}
           {try.#Success [context'' a]}

           {try.#Failure error}
           {try.#Failure error})

         {try.#Failure error}
         {try.#Failure error}
         )))
   ))

(use "check#[0]" ..monad)

(def (var::new id property_list)
  (-> Var Type_Vars Type_Vars)
  {.#Item [id {.#None}] property_list})

(def (var::get id property_list)
  (-> Var Type_Vars (Maybe (Maybe Type)))
  (when property_list
    {.#Item [var_id var_type]
            property_list'}
    (if (!n#= id var_id)
      {.#Some var_type}
      (var::get id property_list'))

    {.#End}
    {.#None}))

(def (var::put id value property_list)
  (-> Var (Maybe Type) Type_Vars Type_Vars)
  (when property_list
    {.#End}
    (list [id value])

    {.#Item [var_id var_type]
            property_list'}
    (if (!n#= id var_id)
      {.#Item [var_id value]
              property_list'}
      {.#Item [var_id var_type]
              (var::put id value property_list')})))

(def .public (result context proc)
  (All (_ a) (-> Type_Context (Check a) (Try a)))
  (when (proc context)
    {try.#Success [context' output]}
    {try.#Success output}

    {try.#Failure error}
    {try.#Failure error}))

(def .public (failure message)
  (All (_ a) (-> Text (Check a)))
  (function (_ context)
    {try.#Failure message}))

(def .public (assertion message test)
  (-> Text Bit (Check Any))
  (function (_ context)
    (if test
      {try.#Success [context []]}
      {try.#Failure message})))

(def .public (except exception message)
  (All (_ e a) (-> (Exception e) e (Check a)))
  (..failure (exception.error exception message)))

(def .public existential
  (Check [Nat Type])
  (function (_ context)
    (let [id (the .#ex_counter context)]
      {try.#Success [(revised .#ex_counter ++ context)
                     [id {.#Ex id}]]})))

(with_template [<name> <outputT> <fail> <succeed>]
  [(def .public (<name> id)
     (-> Var (Check <outputT>))
     (function (_ context)
       (when (|> context (the .#var_bindings) (var::get id))
         (^.or {.#Some {.#Some {.#Var _}}}
               {.#Some {.#None}})
         {try.#Success [context <fail>]}
         
         {.#Some {.#Some bound}}
         {try.#Success [context <succeed>]}

         {.#None}
         (exception.except ..unknown_type_var id))))]

  [bound? Bit          false    true]
  [peek   (Maybe Type) {.#None} {.#Some bound}]
  )

(def .public (read id)
  (-> Var (Check Type))
  (do ..monad
    [?type (peek id)]
    (when ?type
      {.#Some type}
      (in type)

      {.#None}
      (..except ..unbound_type_var id))))

(def (bound id)
  (-> Var (Check Type))
  (function (_ context)
    (when (|> context (the .#var_bindings) (var::get id))
      {.#Some {.#Some bound}}
      {try.#Success [context bound]}

      {.#Some _}
      (exception.except ..unbound_type_var id)

      _
      (exception.except ..unknown_type_var id))))

(def .public (bind type id)
  (-> Type Var (Check Any))
  (function (_ context)
    (when (|> context (the .#var_bindings) (var::get id))
      {.#Some {.#None}}
      {try.#Success [(revised .#var_bindings (var::put id {.#Some type}) context)
                     []]}

      {.#Some {.#Some bound}}
      (exception.except ..cannot_rebind_var [id type bound])
      
      _
      (exception.except ..unknown_type_var id))))

(def (re_bind' ?type id)
  (-> (Maybe Type) Var (Check Any))
  (function (_ context)
    (when (|> context (the .#var_bindings) (var::get id))
      {.#Some _}
      {try.#Success [(revised .#var_bindings (var::put id ?type) context)
                     []]}
      
      _
      (exception.except ..unknown_type_var id))))

(def (re_bind type id)
  (-> Type Var (Check Any))
  (re_bind' {.#Some type} id))

(def .public var
  (Check [Var Type])
  (function (_ context)
    (let [id (the .#var_counter context)]
      {try.#Success [(|> context
                         (revised .#var_counter ++)
                         (revised .#var_bindings (var::new id)))
                     [id {.#Var id}]]})))

(def (on argT funcT)
  (-> Type Type (Check Type))
  (when funcT
    {.#Var func_id}
    (do ..monad
      [?funcT' (peek func_id)]
      (when ?funcT'
        {.#Some funcT'}
        (on argT funcT')

        _
        (except ..invalid_type_application [funcT argT])))

    {.#Apply argT' funcT'}
    (do ..monad
      [funcT'' (on argT' funcT')]
      (on argT funcT''))

    _
    (when (//.applied (list argT) funcT)
      {.#Some output}
      (check#in output)

      _
      (except ..invalid_type_application [funcT argT]))))

(def .public (ring' start)
  (-> Var (Check (List Var)))
  (function (_ context)
    (loop (again [current start
                  output (list start)])
      (when (|> context (the .#var_bindings) (var::get current))
        {.#Some {.#Some type}}
        (when type
          {.#Var next}
          (if (!n#= start next)
            {try.#Success [context output]}
            (again next (list.partial next output)))
          
          _
          {try.#Success [context (list)]})

        {.#Some {.#None}}
        {try.#Success [context output]}
        
        {.#None}
        (exception.except ..unknown_type_var current)))))

... TODO: Optimize this by not using sets anymore.
(def ring
  (-> Var (Check (Set Var)))
  (|>> ..ring'
       (check#each (set.of_list n.hash))))

(def .public (linked? @0 @1)
  (-> Var Var (Check Bit))
  (check#each (function (_ it)
                (set.member? it @1))
              (..ring @0)))

(exception.def .public (cannot_identify var)
  (Exception Var)
  (exception.report
   (list ["Var" (n#encoded var)])))

(def .public (identity aliases @)
  (-> (List Var) Var (Check Type))
  (do [! ..monad]
    [:bound: (..peek @)]
    (when :bound:
      {.#Some :bound:}
      (in :bound:)

      {.#None}
      (do !
        [existing_aliases (..ring @)]
        (if (n.< 2 (set.size existing_aliases))
          (..except ..cannot_identify [@])
          (do !
            [.let [forbidden_aliases (set.of_list n.hash (list.partial @ aliases))
                   allowed_aliases (set.difference forbidden_aliases existing_aliases)]]
            (when (set.list allowed_aliases)
              {.#Item identity _}
              (in {.#Var identity})
              
              {.#None}
              (..except ..cannot_identify [@]))))))))

(def (erase! @)
  (-> Var (Check Any))
  (function (_ context)
    {try.#Success [(revised .#var_bindings
                            (list#mix (is (//.let [binding [Nat (Maybe Type)]]
                                            (-> binding
                                                (List binding)
                                                (List binding)))
                                          (function (_ in out)
                                            (let [[@var :var:] in]
                                              (if (n.= @ @var)
                                                out
                                                (list.partial in out)))))
                                      (is (List [Nat (Maybe Type)])
                                          (list)))
                            context)
                   []]}))

(def .public (forget! @)
  (-> Var (Check Any))
  (do [! ..monad]
    [ring (..ring' @)]
    (when ring
      (list)
      (in [])
      
      (list @me)
      (erase! @me)
      
      (list @other @me)
      (do !
        [_ (re_bind' {.#None} @other)]
        (erase! @me))
      
      (list.partial @prev _)
      (when (list.reversed ring)
        (list.partial @me @next _)
        (do !
          [_ (re_bind {.#Var @next} @prev)
           _ (re_bind {.#Var @prev} @next)]
          (erase! @me))

        _
        (undefined)))))

(def .public (try it)
  (All (_ a) (-> (Check a) (Check (Try a))))
  (function (_ context)
    (when (it context)
      {try.#Success [context' output]}
      {try.#Success [context' {try.#Success output}]}

      {try.#Failure error}
      {try.#Success [context {try.#Failure error}]})))

(def .public fresh_context
  Type_Context
  [.#var_counter 0
   .#ex_counter 0
   .#var_bindings (list)])

(def (either left right)
  (All (_ a) (-> (Check a) (Check a) (Check a)))
  (function (_ context)
    (when (left context)
      {try.#Failure _}
      (right context)

      output
      output)))

(def (assumed? [e a] assumptions)
  (-> Assumption (List Assumption) Bit)
  (list.any? (function (_ [e' a'])
               (and (//#= e e')
                    (//#= a a')))
             assumptions))

... TODO: "if_can_bind" can be optimized...
(def (if_can_bind id type then else)
  (All (_ a)
    (-> Var Type (Check a) (-> Type (Check a))
        (Check a)))
  (all either
       (do ..monad
         [_ (..bind type id)]
         then)
       (do [! ..monad]
         [ring (..ring id)
          _ (..assertion "" (n.> 1 (set.size ring)))
          _ (monad.each ! (re_bind type) (set.list ring))]
         then)
       (do ..monad
         [?bound (peek id)]
         (else (maybe.else {.#Var id} ?bound)))))

... TODO: "link/2" can be optimized...
(def (link/2 left right)
  (-> Var Var (Check Any))
  (do ..monad
    [_ (..bind {.#Var right} left)]
    (..bind {.#Var left} right)))

... TODO: "link/3" can be optimized...
(def (link/3 interpose to from)
  (-> Var Var Var (Check Any))
  (do ..monad
    [_ (re_bind {.#Var interpose} from)]
    (re_bind {.#Var to} interpose)))

... TODO: "check_vars" can be optimized...
(def (check_vars check' assumptions idE idA)
  (-> (Checker Type) (Checker Var))
  (if (!n#= idE idA)
    (check#in assumptions)
    (do [! ..monad]
      [ebound (..try (..bound idE))
       abound (..try (..bound idA))]
      (when [ebound abound]
        ... Link the 2 variables circularly
        [{try.#Failure _} {try.#Failure _}]
        (do !
          [_ (link/2 idE idA)]
          (in assumptions))

        ... Interpose new variable between 2 existing links
        [{try.#Success etype} {try.#Failure _}]
        (when etype
          {.#Var targetE}
          (do !
            [_ (link/3 idA targetE idE)]
            (in assumptions))

          _
          (check' assumptions etype {.#Var idA}))

        ... Interpose new variable between 2 existing links
        [{try.#Failure _} {try.#Success atype}]
        (when atype
          {.#Var targetA}
          (do !
            [_ (link/3 idE targetA idA)]
            (in assumptions))

          _
          (check' assumptions {.#Var idE} atype))

        [{try.#Success etype} {try.#Success atype}]
        (when [etype atype]
          [{.#Var targetE} {.#Var targetA}]
          (do !
            [ringE (..ring idE)
             ringA (..ring idA)]
            (if (at set.equivalence = ringE ringA)
              (in assumptions)
              ... Fuse 2 rings
              (do !
                [_ (monad.mix ! (function (_ interpose to)
                                  (do !
                                    [_ (link/3 interpose to idE)]
                                    (in interpose)))
                              targetE
                              (set.list ringA))]
                (in assumptions))))

          (^.with_template [<pattern> <id> <type>]
            [<pattern>
             (do !
               [ring (..ring <id>)
                _ (monad.each ! (re_bind <type>) (set.list ring))]
               (in assumptions))])
          ([[{.#Var _} _] idE atype]
           [[_ {.#Var _}] idA etype])
          
          _
          (check' assumptions etype atype))))))

(def silent_failure!
  (All (_ a) (Check a))
  (..failure ""))

... TODO: "check_apply" can be optimized...
(def (check_apply check' assumptions expected actual)
  (-> (Checker Type) (Checker [Type Type]))
  (let [[expected_input expected_function] expected
        [actual_input actual_function] actual]
    (when [expected_function actual_function]
      [{.#Ex exE} {.#Ex exA}]
      (if (!n#= exE exA)
        (check' assumptions expected_input actual_input)
        ..silent_failure!)

      [{.#UnivQ _ _} {.#Ex _}]
      (do ..monad
        [expected' (..on expected_input expected_function)]
        (check' assumptions expected' {.#Apply actual}))

      [{.#Ex _} {.#UnivQ _ _}]
      (do ..monad
        [actual' (..on actual_input actual_function)]
        (check' assumptions {.#Apply expected} actual'))

      [{.#Apply [expected_input' expected_function']} {.#Ex _}]
      (do ..monad
        [expected_function'' (..on expected_input' expected_function')]
        (check' assumptions {.#Apply [expected_input expected_function'']} {.#Apply actual}))

      [{.#Ex _} {.#Apply [actual_input' actual_function']}]
      (do ..monad
        [actual_function'' (..on actual_input' actual_function')]
        (check' assumptions {.#Apply expected} {.#Apply [actual_input actual_function'']}))

      (^.or [{.#Ex _} _] [_ {.#Ex _}])
      (do ..monad
        [assumptions (check' assumptions expected_function actual_function)]
        (check' assumptions expected_input actual_input))

      [{.#Var id} _]
      (function (_ context)
        (when ((do ..monad
                 [expected_function' (..read id)]
                 (check' assumptions {.#Apply expected_input expected_function'} {.#Apply actual}))
               context)
          {try.#Success output}
          {try.#Success output}

          {try.#Failure _}
          (when actual_function
            {.#UnivQ _ _}
            ((do ..monad
               [actual' (..on actual_input actual_function)]
               (check' assumptions {.#Apply expected} actual'))
             context)
            
            {.#Ex exA}
            ((do ..monad
               [assumptions (check' assumptions expected_function actual_function)]
               (check' assumptions expected_input actual_input))
             context)

            _
            ((do ..monad
               [assumptions (check' assumptions expected_function actual_function)
                expected' (..on expected_input actual_function)
                actual' (..on actual_input actual_function)]
               (check' assumptions expected' actual'))
             context))))

      [_ {.#Var id}]
      (function (_ context)
        (when ((do ..monad
                 [actual_function' (read id)]
                 (check' assumptions {.#Apply expected} {.#Apply actual_input actual_function'}))
               context)
          {try.#Success output}
          {try.#Success output}

          _
          ((do ..monad
             [assumptions (check' assumptions expected_function actual_function)
              expected' (..on expected_input expected_function)
              actual' (..on actual_input expected_function)]
             (check' assumptions expected' actual'))
           context)))

      _
      ..silent_failure!)))

(def (with_exception exception parameter check)
  (All (_ e a) (-> (Exception e) e (Check a) (Check a)))
  (|>> check
       (exception.with exception parameter)))

... TODO: "check'" can be optimized...
... Type-check to ensure that the 'expected' type subsumes the 'actual' type.
(def (check' assumptions expected actual)
  (Checker Type)
  (if (for @.php
           ... TODO: Remove this once JPHP is gone.
           false
           (same? expected actual))
    (check#in assumptions)
    (with_exception ..type_check_failed [expected actual]
      (when [expected actual]
        [{.#Var idE} {.#Var idA}]
        (check_vars check' assumptions idE idA)
        
        [{.#Var id} _]
        (if_can_bind id actual
                     (check#in assumptions)
                     (function (_ bound)
                       (check' assumptions bound actual)))
        
        [_ {.#Var id}]
        (if_can_bind id expected
                     (check#in assumptions)
                     (function (_ bound)
                       (check' assumptions expected bound)))

        (^.with_template [<fE> <fA>]
          [[{.#Apply aE <fE>} {.#Apply aA <fA>}]
           (check_apply check' assumptions [aE <fE>] [aA <fA>])])
        ([F1 {.#Ex ex}]
         [{.#Ex exE} fA]
         [fE {.#Var idA}]
         [{.#Var idE} fA])
        
        [{.#Apply A F} _]
        (let [new_assumption [expected actual]]
          (if (assumed? new_assumption assumptions)
            (check#in assumptions)
            (do ..monad
              [expected' (..on A F)]
              (check' {.#Item new_assumption assumptions} expected' actual))))

        [_ {.#Apply A F}]
        (do ..monad
          [actual' (..on A F)]
          (check' assumptions expected actual'))

        ... TODO: Refactor-away as cold-code
        (^.with_template [<tag> <instancer>]
          [[{<tag> _} _]
           (do ..monad
             [[_ paramT] <instancer>
              expected' (..on paramT expected)]
             (check' assumptions expected' actual))])
        ([.#UnivQ ..existential]
         [.#ExQ ..var])

        ... TODO: Refactor-away as cold-code
        (^.with_template [<tag> <instancer>]
          [[_ {<tag> _}]
           (do ..monad
             [[_ paramT] <instancer>
              actual' (..on paramT actual)]
             (check' assumptions expected actual'))])
        ([.#UnivQ ..var]
         [.#ExQ ..existential])

        [{.#Primitive e_name e_params} {.#Primitive a_name a_params}]
        (if (!text#= e_name a_name)
          (loop (again [assumptions assumptions
                        e_params e_params
                        a_params a_params])
            (when [e_params a_params]
              [{.#End} {.#End}]
              (check#in assumptions)
              
              [{.#Item e_head e_tail} {.#Item a_head a_tail}]
              (do ..monad
                [assumptions' (check' assumptions e_head a_head)]
                (again assumptions' e_tail a_tail))

              _
              ..silent_failure!))
          ..silent_failure!)

        (^.with_template [<composite>]
          [[{<composite> eL eR} {<composite> aL aR}]
           (do ..monad
             [assumptions (check' assumptions eL aL)]
             (check' assumptions eR aR))])
        ([.#Sum]
         [.#Product])
        
        [{.#Function eI eO} {.#Function aI aO}]
        (do ..monad
          [assumptions (check' assumptions aI eI)]
          (check' assumptions eO aO))

        [{.#Ex e!id} {.#Ex a!id}]
        (if (!n#= e!id a!id)
          (check#in assumptions)
          ..silent_failure!)

        [{.#Named _ ?etype} _]
        (check' assumptions ?etype actual)

        [_ {.#Named _ ?atype}]
        (check' assumptions expected ?atype)

        _
        ..silent_failure!))))

(def .public (check expected actual)
  (-> Type Type (Check Any))
  (check' (list) expected actual))

(def .public (subsumes? expected actual)
  (-> Type Type Bit)
  (when (..result ..fresh_context
                  (..check expected actual))
    {try.#Failure _}
    false

    {try.#Success _}
    true))

(def .public context
  (Check Type_Context)
  (function (_ context)
    {try.#Success [context context]}))

(def .public (with context)
  (-> Type_Context (Check Any))
  (function (_ _)
    {try.#Success [context []]}))

(def .public (clean aliases inputT)
  (-> (List Var) Type (Check Type))
  (when inputT
    {.#Primitive name paramsT+}
    (|> paramsT+
        (monad.each ..monad (clean aliases))
        (check#each (|>> {.#Primitive name})))

    (^.or {.#Parameter _}
          {.#Ex _}
          {.#Named _})
    (check#in inputT)

    (^.with_template [<tag>]
      [{<tag> leftT rightT}
       (do ..monad
         [leftT' (clean aliases leftT)]
         (|> (clean aliases rightT)
             (check#each (|>> {<tag> leftT'}))))])
    ([.#Sum]
     [.#Product]
     [.#Function]
     [.#Apply])

    {.#Var @it}
    (when aliases
      (list)
      (do ..monad
        [?actualT (..peek @it)]
        (when ?actualT
          {.#Some actualT}
          (clean aliases actualT)

          _
          (in inputT)))

      _
      (do ..monad
        [:it: (..try (..identity aliases @it))]
        (when :it:
          {try.#Success :it:}
          (when :it:
            {.#Var _}
            (in inputT)

            _
            (clean aliases :it:))

          failure
          (in inputT))))

    (^.with_template [<tag>]
      [{<tag> envT+ unquantifiedT}
       (do [! ..monad]
         [envT+' (monad.each ! (clean aliases) envT+)
          unquantifiedT' (clean aliases unquantifiedT)]
         (in {<tag> envT+' unquantifiedT'}))])
    ([.#UnivQ]
     [.#ExQ])
    ))