-- |
-- Graph-based solver for comparing type-level numbers with respect to
-- reflexivity, symmetry, and transitivity properties.
--
module Language.PureScript.TypeChecker.Entailment.IntCompare where

import Protolude

import Data.Graph qualified as G
import Data.Map qualified as M

import Language.PureScript.Names qualified as P
import Language.PureScript.Types qualified as P
import Language.PureScript.Constants.Prim qualified as P

data Relation a
  = Equal a a
  | LessThan a a
  deriving (forall a b. a -> Relation b -> Relation a
forall a b. (a -> b) -> Relation a -> Relation b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Relation b -> Relation a
$c<$ :: forall a b. a -> Relation b -> Relation a
fmap :: forall a b. (a -> b) -> Relation a -> Relation b
$cfmap :: forall a b. (a -> b) -> Relation a -> Relation b
Functor, Int -> Relation a -> ShowS
forall a. Show a => Int -> Relation a -> ShowS
forall a. Show a => [Relation a] -> ShowS
forall a. Show a => Relation a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Relation a] -> ShowS
$cshowList :: forall a. Show a => [Relation a] -> ShowS
show :: Relation a -> String
$cshow :: forall a. Show a => Relation a -> String
showsPrec :: Int -> Relation a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Relation a -> ShowS
Show, Relation a -> Relation a -> Bool
forall a. Eq a => Relation a -> Relation a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Relation a -> Relation a -> Bool
$c/= :: forall a. Eq a => Relation a -> Relation a -> Bool
== :: Relation a -> Relation a -> Bool
$c== :: forall a. Eq a => Relation a -> Relation a -> Bool
Eq, Relation a -> Relation a -> Bool
Relation a -> Relation a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (Relation a)
forall a. Ord a => Relation a -> Relation a -> Bool
forall a. Ord a => Relation a -> Relation a -> Ordering
forall a. Ord a => Relation a -> Relation a -> Relation a
min :: Relation a -> Relation a -> Relation a
$cmin :: forall a. Ord a => Relation a -> Relation a -> Relation a
max :: Relation a -> Relation a -> Relation a
$cmax :: forall a. Ord a => Relation a -> Relation a -> Relation a
>= :: Relation a -> Relation a -> Bool
$c>= :: forall a. Ord a => Relation a -> Relation a -> Bool
> :: Relation a -> Relation a -> Bool
$c> :: forall a. Ord a => Relation a -> Relation a -> Bool
<= :: Relation a -> Relation a -> Bool
$c<= :: forall a. Ord a => Relation a -> Relation a -> Bool
< :: Relation a -> Relation a -> Bool
$c< :: forall a. Ord a => Relation a -> Relation a -> Bool
compare :: Relation a -> Relation a -> Ordering
$ccompare :: forall a. Ord a => Relation a -> Relation a -> Ordering
Ord)

type Context a = [Relation a]

type PSOrdering = P.Qualified (P.ProperName 'P.TypeName)

-- Commentary:
--
-- In essence, this solver builds a directed graph using the provided
-- context, which is then used to determine the relationship between
-- the two elements being compared.
--
-- Given the context [a < b, b < c], we can infer that a < c as a
-- path exists from a to c. Likewise, we can also infer that c > a
-- as a path exists from c to a.
--
-- ╔═══╗    ╔═══╗    ╔═══╗
-- ║ a ║ -> ║ b ║ -> ║ c ║
-- ╚═══╝    ╚═══╝    ╚═══╝
--
-- Introducing equality to the context augments the graph further,
-- and it is represented by creating cycles between equal nodes.
-- For example, [a < b, b < c, c = d] yields the following graph:
--
-- ╔═══╗    ╔═══╗    ╔═══╗     ╔═══╗
-- ║ a ║ -> ║ b ║ -> ║ c ║ <-> ║ d ║
-- ╚═══╝    ╚═══╝    ╚═══╝     ╚═══╝
solveRelation :: forall a. Ord a => Context a -> a -> a -> Maybe PSOrdering
solveRelation :: forall a. Ord a => Context a -> a -> a -> Maybe PSOrdering
solveRelation Context a
context a
lhs a
rhs =
  if a
lhs forall a. Eq a => a -> a -> Bool
== a
rhs then
    forall (f :: * -> *) a. Applicative f => a -> f a
pure PSOrdering
P.EQ
  else do
    let (Graph
graph, a -> Maybe Int
search) = (Graph, a -> Maybe Int)
inequalities
    Int
lhs' <- a -> Maybe Int
search a
lhs
    Int
rhs' <- a -> Maybe Int
search a
rhs
    case (Graph -> Int -> Int -> Bool
G.path Graph
graph Int
lhs' Int
rhs', Graph -> Int -> Int -> Bool
G.path Graph
graph Int
rhs' Int
lhs') of
      (Bool
True, Bool
True) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure PSOrdering
P.EQ
      (Bool
True, Bool
False) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure PSOrdering
P.LT
      (Bool
False, Bool
True) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure PSOrdering
P.GT
      (Bool, Bool)
_ ->
        forall a. Maybe a
Nothing
  where
  inequalities :: (G.Graph, a -> Maybe G.Vertex)
  inequalities :: (Graph, a -> Maybe Int)
inequalities = [(a, [a])] -> (Graph, a -> Maybe Int)
makeGraph forall a b. (a -> b) -> a -> b
$ forall k. Ord k => [(k, [k])] -> [(k, [k])]
clean forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Relation a -> [(a, [a])]
convert Context a
context
    where
    convert :: Relation a -> [(a, [a])]
    convert :: Relation a -> [(a, [a])]
convert (Equal a
a a
b)    = [(a
a, [a
b]), (a
b, [a
a])]
    convert (LessThan a
a a
b) = [(a
a, [a
b]), (a
b, [])]

    makeGraph :: [(a, [a])] -> (G.Graph, a -> Maybe G.Vertex)
    makeGraph :: [(a, [a])] -> (Graph, a -> Maybe Int)
makeGraph [(a, [a])]
m =
      case forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
G.graphFromEdges forall a b. (a -> b) -> a -> b
$ (\(a
a, [a]
b) -> (a
a, a
a, [a]
b)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, [a])]
m of
        (Graph
g, Int -> (a, a, [a])
_, a -> Maybe Int
f) -> (Graph
g, a -> Maybe Int
f)

    clean :: forall k. Ord k => [(k, [k])] -> [(k, [k])]
    clean :: forall k. Ord k => [(k, [k])] -> [(k, [k])]
clean = forall k a. Map k a -> [(k, a)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a. Semigroup a => a -> a -> a
(<>)

mkRelation :: P.Type a -> P.Type a -> P.Type a -> Maybe (Relation (P.Type a))
mkRelation :: forall a. Type a -> Type a -> Type a -> Maybe (Relation (Type a))
mkRelation Type a
lhs Type a
rhs Type a
rel = case Type a
rel of
  P.TypeConstructor a
_ PSOrdering
ordering
    | PSOrdering
ordering forall a. Eq a => a -> a -> Bool
== PSOrdering
P.EQ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> Relation a
Equal Type a
lhs Type a
rhs
    | PSOrdering
ordering forall a. Eq a => a -> a -> Bool
== PSOrdering
P.LT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> Relation a
LessThan Type a
lhs Type a
rhs
    | PSOrdering
ordering forall a. Eq a => a -> a -> Bool
== PSOrdering
P.GT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> Relation a
LessThan Type a
rhs Type a
lhs
  Type a
_ ->
    forall a. Maybe a
Nothing

mkFacts :: [[P.Type a]] -> [Relation (P.Type a)]
mkFacts :: forall a. [[Type a]] -> [Relation (Type a)]
mkFacts = forall {a}. [[Relation a]] -> [a] -> [Relation a]
mkRels [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [[Type a]] -> [Type a]
findFacts
  where
  mkRels :: [[Relation a]] -> [a] -> [Relation a]
mkRels [[Relation a]]
a [] = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Relation a]]
a
  mkRels [[Relation a]]
a (a
x : [a]
xs) = [[Relation a]] -> [a] -> [Relation a]
mkRels (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (forall a. a -> a -> Relation a
LessThan a
x) [a]
xs forall a. a -> [a] -> [a]
: [[Relation a]]
a) [a]
xs

  findFacts :: [[Type a]] -> [Type a]
findFacts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a b. (a -> b) -> a -> b
$ \case
    [P.TypeLevelInt a
_ Integer
_, P.TypeLevelInt a
_ Integer
_, Type a
_] ->
      forall a. Maybe a
Nothing
    [i :: Type a
i@(P.TypeLevelInt a
_ Integer
_), Type a
_, Type a
_] ->
      forall a. a -> Maybe a
Just Type a
i
    [Type a
_, i :: Type a
i@(P.TypeLevelInt a
_ Integer
_), Type a
_] ->
      forall a. a -> Maybe a
Just Type a
i
    [Type a]
_ ->
      forall a. Maybe a
Nothing