{-# LANGUAGE FlexibleContexts     #-}

-- | This module exports a single function that computes the dependency
-- information needed to eliminate non-cut KVars, and then transitively
-- collapse the resulting constraint dependencies.
-- See the type of `SolverInfo` for details.

module Language.Fixpoint.Solver.Eliminate ( solverInfo ) where

import qualified Data.HashSet        as S
import qualified Data.HashMap.Strict as M

import           Language.Fixpoint.Types.Config    (Config)
import qualified Language.Fixpoint.Types.Solutions as Sol
import           Language.Fixpoint.Types
import           Language.Fixpoint.Types.Visitor   (kvarsExpr, isConcC)
import           Language.Fixpoint.Graph
import           Language.Fixpoint.Misc            (safeLookup, group, errorstar)
import           Language.Fixpoint.Solver.Sanitize

--------------------------------------------------------------------------------
-- | `solverInfo` constructs a `SolverInfo` comprising the Solution and various
--   indices needed by the worklist-based refinement loop
--------------------------------------------------------------------------------
{-# SCC solverInfo #-}
solverInfo :: Config -> SInfo a -> SolverInfo a b
--------------------------------------------------------------------------------
solverInfo :: forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo a
sI = forall a b.
Sol b QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a b
SI forall {a} {b}. Sol a b
sHyp SInfo a
sI' CDeps
cD HashSet KVar
cKs
  where
    cD :: CDeps
cD             = forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> HashSet KVar -> HashSet Symbol -> CDeps
elimDeps     SInfo a
sI [CEdge]
es HashSet KVar
nKs HashSet Symbol
ebs
    sI' :: SInfo a
sI'            = forall a. SInfo a -> KIndex -> HashSet KVar -> SInfo a
cutSInfo     SInfo a
sI KIndex
kI HashSet KVar
cKs
    sHyp :: Sol a b
sHyp           = forall a b.
SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(BindId, EbindSol)]
-> SEnv (BindId, Sort)
-> Sol a b
Sol.fromList SymEnv
sE forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty [(KVar, Hyp)]
kHyps HashMap KVar IBindEnv
kS [] SEnv (BindId, Sort)
sEnv
    sEnv :: SEnv (BindId, Sort)
sEnv           = forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [ (Symbol
x, (BindId
i, SortedReft -> Sort
sr_sort SortedReft
sr)) | (BindId
i, (Symbol
x,SortedReft
sr, a
_)) <- forall a. BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
bindEnvToList (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
sI)]
    kHyps :: [(KVar, Hyp)]
kHyps          = forall a. SInfo a -> KIndex -> HashSet KVar -> [(KVar, Hyp)]
nonCutHyps   SInfo a
sI KIndex
kI HashSet KVar
nKs
    kI :: KIndex
kI             = forall a. SInfo a -> KIndex
kIndex       SInfo a
sI
    ([CEdge]
es, HashSet KVar
cKs, HashSet KVar
nKs) = forall a.
Config -> SInfo a -> ([CEdge], HashSet KVar, HashSet KVar)
kutVars Config
cfg  SInfo a
sI
    kS :: HashMap KVar IBindEnv
kS             = forall a. SInfo a -> [CEdge] -> HashMap KVar IBindEnv
kvScopes     SInfo a
sI [CEdge]
es
    sE :: SymEnv
sE             = forall a. Config -> SInfo a -> SymEnv
symbolEnv   Config
cfg SInfo a
sI
    ebs :: HashSet Symbol
ebs            = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Symbol
x | BindId
i <- forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds SInfo a
sI, let (Symbol
x, SortedReft
_, a
_) = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
sI) ]


--------------------------------------------------------------------------------
kvScopes :: SInfo a -> [CEdge] -> M.HashMap KVar IBindEnv
kvScopes :: forall a. SInfo a -> [CEdge] -> HashMap KVar IBindEnv
kvScopes SInfo a
sI [CEdge]
es = [Integer] -> IBindEnv
is2env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KIndex
kiM
  where
    is2env :: [Integer] -> IBindEnv
is2env = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SInfo a -> Integer -> SimpC a
getSubC SInfo a
sI)
    kiM :: KIndex
kiM    = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group forall a b. (a -> b) -> a -> b
$ [(KVar
k, Integer
i) | (Cstr Integer
i, KVar KVar
k) <- [CEdge]
es ] forall a. [a] -> [a] -> [a]
++
                     [(KVar
k, Integer
i) | (KVar KVar
k, Cstr Integer
i) <- [CEdge]
es ]

--------------------------------------------------------------------------------

cutSInfo :: SInfo a -> KIndex -> S.HashSet KVar -> SInfo a
cutSInfo :: forall a. SInfo a -> KIndex -> HashSet KVar -> SInfo a
cutSInfo SInfo a
si KIndex
kI HashSet KVar
cKs = SInfo a
si { ws :: HashMap KVar (WfC a)
ws = HashMap KVar (WfC a)
ws', cm :: HashMap Integer (SimpC a)
cm = HashMap Integer (SimpC a)
cm' }
  where
    ws' :: HashMap KVar (WfC a)
ws'   = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\KVar
k WfC a
_ -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member KVar
k HashSet KVar
cKs) (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
si)
    cm' :: HashMap Integer (SimpC a)
cm'   = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Integer
i SimpC a
c -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Integer
i HashSet Integer
cs Bool -> Bool -> Bool
|| forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isConcC SimpC a
c) (forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
    cs :: HashSet Integer
cs    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList      (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap KVar -> [Integer]
kCs HashSet KVar
cKs)
    kCs :: KVar -> [Integer]
kCs KVar
k = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KIndex
kI

kutVars :: Config -> SInfo a -> ([CEdge], S.HashSet KVar, S.HashSet KVar)
kutVars :: forall a.
Config -> SInfo a -> ([CEdge], HashSet KVar, HashSet KVar)
kutVars Config
cfg SInfo a
si   = ([CEdge]
es, forall a. Elims a -> HashSet a
depCuts Elims KVar
ds, forall a. Elims a -> HashSet a
depNonCuts Elims KVar
ds)
  where
    ([CEdge]
es, Elims KVar
ds)     = forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> ([CEdge], Elims KVar)
elimVars Config
cfg SInfo a
si

--------------------------------------------------------------------------------
-- | Map each `KVar` to the list of constraints on which it appears on RHS
--------------------------------------------------------------------------------
type KIndex = M.HashMap KVar [Integer]

--------------------------------------------------------------------------------
kIndex     :: SInfo a -> KIndex
--------------------------------------------------------------------------------
kIndex :: forall a. SInfo a -> KIndex
kIndex SInfo a
si  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [(KVar
k, Integer
i) | (Integer
i, SimpC a
c) <- [(Integer, SimpC a)]
iCs, KVar
k <- SimpC a -> [KVar]
rkvars SimpC a
c]
  where
    iCs :: [(Integer, SimpC a)]
iCs    = forall k v. HashMap k v -> [(k, v)]
M.toList (forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
    rkvars :: SimpC a -> [KVar]
rkvars = Expr -> [KVar]
kvarsExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs

nonCutHyps :: SInfo a -> KIndex -> S.HashSet KVar -> [(KVar, Sol.Hyp)]
nonCutHyps :: forall a. SInfo a -> KIndex -> HashSet KVar -> [(KVar, Hyp)]
nonCutHyps SInfo a
si KIndex
kI HashSet KVar
nKs = [ (KVar
k, forall a. KIndex -> SInfo a -> KVar -> Hyp
nonCutHyp KIndex
kI SInfo a
si KVar
k) | KVar
k <- forall a. HashSet a -> [a]
S.toList HashSet KVar
nKs ]


nonCutHyp  :: KIndex -> SInfo a -> KVar -> Sol.Hyp
nonCutHyp :: forall a. KIndex -> SInfo a -> KVar -> Hyp
nonCutHyp KIndex
kI SInfo a
si KVar
k = forall a. SimpC a -> Cube
nonCutCube forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SimpC a]
cs
  where
    cs :: [SimpC a]
cs            = forall a. SInfo a -> Integer -> SimpC a
getSubC   SInfo a
si forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KIndex
kI

nonCutCube :: SimpC a -> Sol.Cube
nonCutCube :: forall a. SimpC a -> Cube
nonCutCube SimpC a
c = IBindEnv -> Subst -> Integer -> [BindId] -> Cube
Sol.Cube (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c) (forall a. SimpC a -> Subst
rhsSubst SimpC a
c) (forall (c :: * -> *) a. TaggedC c a => c a -> Integer
subcId SimpC a
c) (forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SimpC a
c)

rhsSubst :: SimpC a -> Subst
rhsSubst :: forall a. SimpC a -> Subst
rhsSubst             = Expr -> Subst
rsu forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs
  where
    rsu :: Expr -> Subst
rsu (PKVar KVar
_ Subst
su) = Subst
su
    rsu Expr
_            = forall a. (?callStack::CallStack) => String -> a
errorstar String
"Eliminate.rhsSubst called on bad input"

getSubC :: SInfo a -> Integer -> SimpC a
getSubC :: forall a. SInfo a -> Integer -> SimpC a
getSubC SInfo a
si Integer
i = forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
safeLookup String
msg Integer
i (forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
  where
    msg :: String
msg = String
"getSubC: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
i