-- |
-- Module      :  Disco.Exhaustiveness.Constraint
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- The heart of the Lower Your Guards algorithm.
-- Functions for converting constraints detailing
-- pattern matches into a normalized description
-- of everything that is left uncovered.
module Disco.Exhaustiveness.Constraint where

import Control.Applicative (Alternative)
import Control.Monad (foldM, guard)
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Maybe (MaybeT, runMaybeT)
import Data.Bifunctor (first)
import Data.List (partition)
import Data.Maybe (isJust, listToMaybe, mapMaybe)
import Disco.Effects.Fresh (Fresh)
import qualified Disco.Exhaustiveness.TypeInfo as TI
import qualified Disco.Types as Ty
import Polysemy
import Polysemy.Reader

data Constraint where
  CMatch :: TI.DataCon -> [TI.TypedVar] -> Constraint
  CNot :: TI.DataCon -> Constraint
  CWasOriginally :: TI.TypedVar -> Constraint
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constraint -> ShowS
showsPrec :: Int -> Constraint -> ShowS
$cshow :: Constraint -> String
show :: Constraint -> String
$cshowList :: [Constraint] -> ShowS
showList :: [Constraint] -> ShowS
Show, Constraint -> Constraint -> Bool
(Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool) -> Eq Constraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Constraint -> Constraint -> Bool
== :: Constraint -> Constraint -> Bool
$c/= :: Constraint -> Constraint -> Bool
/= :: Constraint -> Constraint -> Bool
Eq, Eq Constraint
Eq Constraint =>
(Constraint -> Constraint -> Ordering)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Constraint)
-> (Constraint -> Constraint -> Constraint)
-> Ord Constraint
Constraint -> Constraint -> Bool
Constraint -> Constraint -> Ordering
Constraint -> Constraint -> Constraint
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
$ccompare :: Constraint -> Constraint -> Ordering
compare :: Constraint -> Constraint -> Ordering
$c< :: Constraint -> Constraint -> Bool
< :: Constraint -> Constraint -> Bool
$c<= :: Constraint -> Constraint -> Bool
<= :: Constraint -> Constraint -> Bool
$c> :: Constraint -> Constraint -> Bool
> :: Constraint -> Constraint -> Bool
$c>= :: Constraint -> Constraint -> Bool
>= :: Constraint -> Constraint -> Bool
$cmax :: Constraint -> Constraint -> Constraint
max :: Constraint -> Constraint -> Constraint
$cmin :: Constraint -> Constraint -> Constraint
min :: Constraint -> Constraint -> Constraint
Ord)

posMatch :: [Constraint] -> Maybe (TI.DataCon, [TI.TypedVar])
posMatch :: [Constraint] -> Maybe (DataCon, [TypedVar])
posMatch [Constraint]
constraints = [(DataCon, [TypedVar])] -> Maybe (DataCon, [TypedVar])
forall a. [a] -> Maybe a
listToMaybe ([(DataCon, [TypedVar])] -> Maybe (DataCon, [TypedVar]))
-> [(DataCon, [TypedVar])] -> Maybe (DataCon, [TypedVar])
forall a b. (a -> b) -> a -> b
$ (Constraint -> Maybe (DataCon, [TypedVar]))
-> [Constraint] -> [(DataCon, [TypedVar])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case (CMatch DataCon
k [TypedVar]
ys) -> (DataCon, [TypedVar]) -> Maybe (DataCon, [TypedVar])
forall a. a -> Maybe a
Just (DataCon
k, [TypedVar]
ys); Constraint
_ -> Maybe (DataCon, [TypedVar])
forall a. Maybe a
Nothing) [Constraint]
constraints

negMatches :: [Constraint] -> [TI.DataCon]
negMatches :: [Constraint] -> [DataCon]
negMatches = (Constraint -> Maybe DataCon) -> [Constraint] -> [DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case (CNot DataCon
k) -> DataCon -> Maybe DataCon
forall a. a -> Maybe a
Just DataCon
k; Constraint
_ -> Maybe DataCon
forall a. Maybe a
Nothing)

type ConstraintFor = (TI.TypedVar, Constraint)

-- Resolves term equalities, finding the leftmost id for a variable
-- I believe I3 of section 3.4 allows us to
-- do a linear scan from right to left
lookupVar :: TI.TypedVar -> [ConstraintFor] -> TI.TypedVar
lookupVar :: TypedVar -> [ConstraintFor] -> TypedVar
lookupVar TypedVar
x = (ConstraintFor -> TypedVar -> TypedVar)
-> TypedVar -> [ConstraintFor] -> TypedVar
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ConstraintFor -> TypedVar -> TypedVar
getNextId TypedVar
x
 where
  getNextId :: ConstraintFor -> TypedVar -> TypedVar
getNextId (TypedVar
x', CWasOriginally TypedVar
y) | TypedVar
x' TypedVar -> TypedVar -> Bool
forall a. Eq a => a -> a -> Bool
== TypedVar
x = TypedVar -> TypedVar -> TypedVar
forall a b. a -> b -> a
const TypedVar
y
  getNextId ConstraintFor
_ = TypedVar -> TypedVar
forall a. a -> a
id

alistLookup :: (Eq a) => a -> [(a, b)] -> [b]
alistLookup :: forall a b. Eq a => a -> [(a, b)] -> [b]
alistLookup a
a = ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd ([(a, b)] -> [b]) -> ([(a, b)] -> [(a, b)]) -> [(a, b)] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> Bool) -> [(a, b)] -> [(a, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a) (a -> Bool) -> ((a, b) -> a) -> (a, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst)

onVar :: TI.TypedVar -> [ConstraintFor] -> [Constraint]
onVar :: TypedVar -> [ConstraintFor] -> [Constraint]
onVar TypedVar
x [ConstraintFor]
cs = TypedVar -> [ConstraintFor] -> [Constraint]
forall a b. Eq a => a -> [(a, b)] -> [b]
alistLookup (TypedVar -> [ConstraintFor] -> TypedVar
lookupVar TypedVar
x [ConstraintFor]
cs) [ConstraintFor]
cs

type NormRefType = [ConstraintFor]

addConstraints :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> [ConstraintFor] -> MaybeT (Sem r) NormRefType
addConstraints :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor]
-> [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
addConstraints = ([ConstraintFor]
 -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor])
-> [ConstraintFor]
-> [ConstraintFor]
-> MaybeT (Sem r) [ConstraintFor]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
addConstraint

addConstraint :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType
addConstraint :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
addConstraint [ConstraintFor]
cns (TypedVar
x, Constraint
c) = do
  Bool -> MaybeT (Sem r) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
breakIf (Bool -> MaybeT (Sem r) ()) -> Bool -> MaybeT (Sem r) ()
forall a b. (a -> b) -> a -> b
$ (Constraint -> Bool) -> [Constraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Constraint -> Constraint -> Bool
conflictsWith Constraint
c) (TypedVar -> [ConstraintFor] -> [Constraint]
onVar TypedVar
x [ConstraintFor]
cns)
  [ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
addConstraintHelper [ConstraintFor]
cns (TypedVar -> [ConstraintFor] -> TypedVar
lookupVar TypedVar
x [ConstraintFor]
cns, Constraint
c)

addConstraintHelper :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> ConstraintFor -> MaybeT (Sem r) NormRefType
addConstraintHelper :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
addConstraintHelper [ConstraintFor]
cns cf :: ConstraintFor
cf@(TypedVar
origX, Constraint
c) = case Constraint
c of
  --- Equation (10)
  CMatch DataCon
k [TypedVar]
args -> do
    case DataCon -> [Constraint] -> Maybe [TypedVar]
getConstructorArgs DataCon
k (TypedVar -> [ConstraintFor] -> [Constraint]
onVar TypedVar
origX [ConstraintFor]
cns) of
      -- 10c
      Just [TypedVar]
args' ->
        [ConstraintFor]
-> [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor]
-> [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
addConstraints
          [ConstraintFor]
cns
          ((TypedVar -> TypedVar -> ConstraintFor)
-> [TypedVar] -> [TypedVar] -> [ConstraintFor]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\TypedVar
a TypedVar
b -> (TypedVar
a, TypedVar -> Constraint
CWasOriginally TypedVar
b)) [TypedVar]
args [TypedVar]
args')
      Maybe [TypedVar]
Nothing -> [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
forall a. a -> MaybeT (Sem r) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ConstraintFor]
added
  --- Equation (11)
  CNot DataCon
_ -> do
    Bool
inh <- Sem r Bool -> MaybeT (Sem r) Bool
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ([ConstraintFor] -> TypedVar -> Sem r Bool
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> TypedVar -> Sem r Bool
inhabited [ConstraintFor]
added TypedVar
origX)
    Bool -> MaybeT (Sem r) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
inh -- ensure that origX is still inhabited, as per I2
    [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
forall a. a -> MaybeT (Sem r) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ConstraintFor]
added
  -- Equation (14)
  CWasOriginally TypedVar
y -> do
    let origY :: TypedVar
origY = TypedVar -> [ConstraintFor] -> TypedVar
lookupVar TypedVar
y [ConstraintFor]
cns
    if TypedVar
origX TypedVar -> TypedVar -> Bool
forall a. Eq a => a -> a -> Bool
== TypedVar
origY
      then [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
forall a. a -> MaybeT (Sem r) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ConstraintFor]
cns
      else do
        let ([ConstraintFor]
noX', [ConstraintFor]
withX') = (ConstraintFor -> Bool)
-> [ConstraintFor] -> ([ConstraintFor], [ConstraintFor])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((TypedVar -> TypedVar -> Bool
forall a. Eq a => a -> a -> Bool
/= TypedVar
origX) (TypedVar -> Bool)
-> (ConstraintFor -> TypedVar) -> ConstraintFor -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintFor -> TypedVar
forall a b. (a, b) -> a
fst) [ConstraintFor]
cns
        [ConstraintFor]
-> [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor]
-> [ConstraintFor] -> MaybeT (Sem r) [ConstraintFor]
addConstraints ([ConstraintFor]
noX' [ConstraintFor] -> [ConstraintFor] -> [ConstraintFor]
forall a. [a] -> [a] -> [a]
++ [ConstraintFor
cf]) (TypedVar -> TypedVar -> [ConstraintFor] -> [ConstraintFor]
substituteVarIDs TypedVar
origY TypedVar
origX [ConstraintFor]
withX')
 where
  added :: [ConstraintFor]
added = [ConstraintFor]
cns [ConstraintFor] -> [ConstraintFor] -> [ConstraintFor]
forall a. [a] -> [a] -> [a]
++ [ConstraintFor
cf]

-----
----- Helper functions for adding constraints:
-----

breakIf :: (Alternative f) => Bool -> f ()
breakIf :: forall (f :: * -> *). Alternative f => Bool -> f ()
breakIf = Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> f ()) -> (Bool -> Bool) -> Bool -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not

-- | Returns a predicate that returns true if another
--   constraint conflicts with the one given.
--   This alone is not sufficient to test
--   if a constraint can be added, but it
--   filters out the easy negatives early on
conflictsWith :: Constraint -> (Constraint -> Bool)
conflictsWith :: Constraint -> Constraint -> Bool
conflictsWith Constraint
c = case Constraint
c of
  CMatch DataCon
k [TypedVar]
_ -> \case
    (CMatch DataCon
k' [TypedVar]
_) | DataCon
k DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
/= DataCon
k' -> Bool
True -- 10a
    (CNot DataCon
k') | DataCon
k DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
k' -> Bool
True -- 10b
    Constraint
_ -> Bool
False
  CNot DataCon
k -> \case
    (CMatch DataCon
k' [TypedVar]
_) | DataCon
k DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
k' -> Bool
True -- 11a
    Constraint
_ -> Bool
False
  CWasOriginally TypedVar
_ -> Bool -> Constraint -> Bool
forall a b. a -> b -> a
const Bool
False

-- | Search for a MatchDataCon that is matching on k specifically
--   (there should be at most one, see I4 in section 3.4)
--   and if it exists, return the variable ids of its arguments
getConstructorArgs :: TI.DataCon -> [Constraint] -> Maybe [TI.TypedVar]
getConstructorArgs :: DataCon -> [Constraint] -> Maybe [TypedVar]
getConstructorArgs DataCon
k [Constraint]
cfs =
  [[TypedVar]] -> Maybe [TypedVar]
forall a. [a] -> Maybe a
listToMaybe ([[TypedVar]] -> Maybe [TypedVar])
-> [[TypedVar]] -> Maybe [TypedVar]
forall a b. (a -> b) -> a -> b
$
    (Constraint -> Maybe [TypedVar]) -> [Constraint] -> [[TypedVar]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\case (CMatch DataCon
k' [TypedVar]
vs) | DataCon
k' DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
k -> [TypedVar] -> Maybe [TypedVar]
forall a. a -> Maybe a
Just [TypedVar]
vs; Constraint
_ -> Maybe [TypedVar]
forall a. Maybe a
Nothing) [Constraint]
cfs

-- | substituting y *for* x
--   ie replace the second with the first, replace x with y
substituteVarIDs :: TI.TypedVar -> TI.TypedVar -> [ConstraintFor] -> [ConstraintFor]
substituteVarIDs :: TypedVar -> TypedVar -> [ConstraintFor] -> [ConstraintFor]
substituteVarIDs TypedVar
y TypedVar
x = (ConstraintFor -> ConstraintFor)
-> [ConstraintFor] -> [ConstraintFor]
forall a b. (a -> b) -> [a] -> [b]
map ((TypedVar -> TypedVar) -> ConstraintFor -> ConstraintFor
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TypedVar -> TypedVar
subst)
 where
  subst :: TypedVar -> TypedVar
subst TypedVar
var = if TypedVar
var TypedVar -> TypedVar -> Bool
forall a. Eq a => a -> a -> Bool
== TypedVar
x then TypedVar
y else TypedVar
x

-- | Deals with I2 from section 3.4
--   if a variable in the context has a resolvable type, there must be at least one constructor
--   which can be instantiated without contradiction of the refinement type
--   This function tests if this is true
inhabited :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> Sem r Bool
inhabited :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> TypedVar -> Sem r Bool
inhabited [ConstraintFor]
n TypedVar
var = do
  TyDefCtx
tyCtx <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @Ty.TyDefCtx
  case Type -> TyDefCtx -> Constructors
TI.tyDataCons (TypedVar -> Type
TI.getType TypedVar
var) TyDefCtx
tyCtx of
    TI.Infinite [DataCon]
_ -> Bool -> Sem r Bool
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- assume opaque types are inhabited
    TI.Finite [DataCon]
constructors -> do
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> Sem r [Bool] -> Sem r Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataCon -> Sem r Bool) -> [DataCon] -> Sem r [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([ConstraintFor] -> TypedVar -> DataCon -> Sem r Bool
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> TypedVar -> DataCon -> Sem r Bool
instantiate [ConstraintFor]
n TypedVar
var) [DataCon]
constructors

-- | Attempts to "instantiate" a match of the dataconstructor k on x
--   If we can add the MatchDataCon constraint to the normalized refinement
--   type without contradiction (a Nothing value),
--   then x is inhabited by k and we return true
instantiate :: Members '[Fresh, Reader Ty.TyDefCtx] r => NormRefType -> TI.TypedVar -> TI.DataCon -> Sem r Bool
instantiate :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> TypedVar -> DataCon -> Sem r Bool
instantiate [ConstraintFor]
cns TypedVar
var DataCon
k = do
  [TypedVar]
args <- [Type] -> Sem r [TypedVar]
forall (r :: EffectRow).
Member Fresh r =>
[Type] -> Sem r [TypedVar]
TI.newVars ([Type] -> Sem r [TypedVar]) -> [Type] -> Sem r [TypedVar]
forall a b. (a -> b) -> a -> b
$ DataCon -> [Type]
TI.dcTypes DataCon
k
  let attempt :: MaybeT (Sem r) [ConstraintFor]
attempt = [ConstraintFor]
cns [ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[ConstraintFor] -> ConstraintFor -> MaybeT (Sem r) [ConstraintFor]
`addConstraint` (TypedVar
var, DataCon -> [TypedVar] -> Constraint
CMatch DataCon
k [TypedVar]
args)
  Maybe [ConstraintFor] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [ConstraintFor] -> Bool)
-> Sem r (Maybe [ConstraintFor]) -> Sem r Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (Sem r) [ConstraintFor] -> Sem r (Maybe [ConstraintFor])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT MaybeT (Sem r) [ConstraintFor]
attempt