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)
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