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

--------------------------------------------------------------------------------
-- | `solverInfo` constructs a `SolverInfo` comprising the Solution and various
--   indices needed by the worklist-based refinement loop
--
-- Computes the set of cut and non-cut kvars, computes the hypotheses common
-- to all of the usage sites of each kvar, then initializes the solutions of
-- the non-cut KVars (in the sHyp field).
--
-- This is part of the implementation of the FUSION algorithm described in:
--
-- "Local Refinement Typing", ICFP 2017, https://ranjitjhala.github.io/static/local_refinement_typing.pdf
--
--------------------------------------------------------------------------------
{-# SCC solverInfo #-}
solverInfo :: Config -> SInfo a -> SolverInfo a
--------------------------------------------------------------------------------
solverInfo :: forall a. Config -> SInfo a -> SolverInfo a
solverInfo Config
cfg SInfo a
sI = Sol QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a
forall a.
Sol QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a
SI Sol QBind
forall {a}. Sol a
sHyp SInfo a
sI' CDeps
cD HashSet KVar
cKs
  where
    cD :: CDeps
cD             = SInfo a -> [CEdge] -> HashSet KVar -> CDeps
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> HashSet KVar -> CDeps
elimDeps     SInfo a
sI [CEdge]
es HashSet KVar
nKs
    sI' :: SInfo a
sI'            = SInfo a -> KIndex -> HashSet KVar -> SInfo a
forall a. SInfo a -> KIndex -> HashSet KVar -> SInfo a
cutSInfo     SInfo a
sI KIndex
kI HashSet KVar
cKs
    sHyp :: Sol a
sHyp = Sol.Sol
      { sMap :: HashMap KVar a
Sol.sMap = HashMap KVar a
forall a. Monoid a => a
mempty
      , sHyp :: HashMap KVar Hyp
Sol.sHyp = [(KVar, Hyp)] -> HashMap KVar Hyp
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(KVar, Hyp)]
kHyps
      , sScp :: HashMap KVar IBindEnv
Sol.sScp = HashMap KVar IBindEnv
kS
      }
    kHyps :: [(KVar, Hyp)]
kHyps          = SInfo a -> KIndex -> HashSet KVar -> [(KVar, Hyp)]
forall a. SInfo a -> KIndex -> HashSet KVar -> [(KVar, Hyp)]
nonCutHyps   SInfo a
sI KIndex
kI HashSet KVar
nKs
    kI :: KIndex
kI             = SInfo a -> KIndex
forall a. SInfo a -> KIndex
kIndex       SInfo a
sI
    ([CEdge]
es, HashSet KVar
cKs, HashSet KVar
nKs) = Config -> SInfo a -> ([CEdge], HashSet KVar, HashSet KVar)
forall a.
Config -> SInfo a -> ([CEdge], HashSet KVar, HashSet KVar)
kutVars Config
cfg  SInfo a
sI
    kS :: HashMap KVar IBindEnv
kS             = SInfo a -> [CEdge] -> HashMap KVar IBindEnv
forall a. SInfo a -> [CEdge] -> HashMap KVar IBindEnv
kvScopes     SInfo a
sI [CEdge]
es

--------------------------------------------------------------------------------
-- | For each KVar, provide the intersection of the binding environments
--   of all the constraints in which it appears.
--
-- See Section 2.4 of "Local Refinement Typing", ICFP 2017, for the motivation
-- to collect these.
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
commonBindingsOfConstraints ([Integer] -> IBindEnv) -> KIndex -> HashMap KVar IBindEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KIndex
kvarUses
  where
    -- | The common bindings of a list of constraints
    commonBindingsOfConstraints :: [Integer] -> IBindEnv
    commonBindingsOfConstraints :: [Integer] -> IBindEnv
commonBindingsOfConstraints =
      (IBindEnv -> IBindEnv -> IBindEnv) -> [IBindEnv] -> IBindEnv
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 IBindEnv -> IBindEnv -> IBindEnv
intersectionIBindEnv ([IBindEnv] -> IBindEnv)
-> ([Integer] -> [IBindEnv]) -> [Integer] -> IBindEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer -> IBindEnv) -> [Integer] -> [IBindEnv]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv (SimpC a -> IBindEnv)
-> (Integer -> SimpC a) -> Integer -> IBindEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> Integer -> SimpC a
forall a. SInfo a -> Integer -> SimpC a
getSubC SInfo a
sI)

    -- | The constraints in which each KVar appears
    kvarUses :: M.HashMap KVar [Integer]
    kvarUses :: KIndex
kvarUses =
      [(KVar, Integer)] -> KIndex
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group ([(KVar, Integer)] -> KIndex) -> [(KVar, Integer)] -> KIndex
forall a b. (a -> b) -> a -> b
$ [(KVar
k, Integer
i) | (Cstr Integer
i, KVar KVar
k) <- [CEdge]
es ] [(KVar, Integer)] -> [(KVar, Integer)] -> [(KVar, Integer)]
forall a. [a] -> [a] -> [a]
++
              [(KVar
k, Integer
i) | (KVar KVar
k, Cstr Integer
i) <- [CEdge]
es ]

--------------------------------------------------------------------------------
-- | @cutSInfo si kI cKs@ drops well-formed constraints that don't refer to the
-- KVars in @cKs@. Also drops subtyping constraints that don't refer in their
-- RHS to any of the KVars in @cKs@ or which aren't concrete.
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 = ws', cm = cm' }
  where
    ws' :: HashMap KVar (WfC a)
ws'   = (KVar -> WfC a -> Bool)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\KVar
k WfC a
_ -> KVar -> HashSet KVar -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member KVar
k HashSet KVar
cKs) (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
si)
    cm' :: HashMap Integer (SimpC a)
cm'   = (Integer -> SimpC a -> Bool)
-> HashMap Integer (SimpC a) -> HashMap Integer (SimpC a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (\Integer
i SimpC a
c -> Integer -> HashSet Integer -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member Integer
i HashSet Integer
cs Bool -> Bool -> Bool
|| SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isConcC SimpC a
c) (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
    cs :: HashSet Integer
cs    = [Integer] -> HashSet Integer
forall a. Hashable a => [a] -> HashSet a
S.fromList      ((KVar -> [Integer]) -> HashSet KVar -> [Integer]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap KVar -> [Integer]
kCs HashSet KVar
cKs)
    kCs :: KVar -> [Integer]
kCs KVar
k = [Integer] -> KVar -> KIndex -> [Integer]
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KIndex
kI

-- | Compute Dependencies and Cuts
--
-- Yields the edges of the dependency graph, then the set of KVars whose removal
-- makes the graph acyclic (cuts), and finally the rest of the KVars.
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, Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
depCuts Elims KVar
ds, Elims KVar -> HashSet KVar
forall a. Elims a -> HashSet a
depNonCuts Elims KVar
ds)
  where
    ([CEdge]
es, Elims KVar
ds)     = Config -> SInfo a -> ([CEdge], Elims KVar)
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  = [(KVar, Integer)] -> KIndex
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    = HashMap Integer (SimpC a) -> [(Integer, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
    rkvars :: SimpC a -> [KVar]
rkvars = ExprV Symbol -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr (ExprV Symbol -> [KVar])
-> (SimpC a -> ExprV Symbol) -> SimpC a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> ExprV Symbol
forall (c :: * -> *) a. TaggedC c a => c a -> ExprV Symbol
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, KIndex -> SInfo a -> KVar -> Hyp
forall a. KIndex -> SInfo a -> KVar -> Hyp
nonCutHyp KIndex
kI SInfo a
si KVar
k) | KVar
k <- HashSet KVar -> [KVar]
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 = SimpC a -> Cube
forall a. SimpC a -> Cube
nonCutCube (SimpC a -> Cube) -> [SimpC a] -> Hyp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SimpC a]
cs
  where
    cs :: [SimpC a]
cs            = SInfo a -> Integer -> SimpC a
forall a. SInfo a -> Integer -> SimpC a
getSubC   SInfo a
si (Integer -> SimpC a) -> [Integer] -> [SimpC a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer] -> KVar -> KIndex -> [Integer]
forall k v. 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 -> Tag -> Cube
Sol.Cube (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c) (SimpC a -> Subst
forall a. SimpC a -> Subst
rhsSubst SimpC a
c) (SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
subcId SimpC a
c) (SimpC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SimpC a
c)

rhsSubst :: SimpC a -> Subst
rhsSubst :: forall a. SimpC a -> Subst
rhsSubst             = ExprV Symbol -> Subst
forall {v}. ExprV v -> SubstV v
rsu (ExprV Symbol -> Subst)
-> (SimpC a -> ExprV Symbol) -> SimpC a -> Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> ExprV Symbol
forall (c :: * -> *) a. TaggedC c a => c a -> ExprV Symbol
crhs
  where
    rsu :: ExprV v -> SubstV v
rsu (PKVar KVar
_ SubstV v
su) = SubstV v
su
    rsu ExprV v
_            = String -> SubstV v
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 = String -> Integer -> HashMap Integer (SimpC a) -> SimpC a
forall k v.
(?callStack::CallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
safeLookup String
msg Integer
i (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
  where
    msg :: String
msg = String
"getSubC: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i