{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Language.Fixpoint.Solver.EnvironmentReduction
( reduceEnvironments
, simplifyBindings
, dropLikelyIrrelevantBindings
, inlineInSortedReft
, mergeDuplicatedBindings
, simplifyBooleanRefts
, undoANF
) where
import Control.Monad (guard, mplus, msum)
import Data.Char (isUpper)
import Data.Hashable (Hashable)
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
import qualified Data.HashMap.Strict as HashMap.Strict
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.List (foldl', nub, partition)
import Data.Maybe (fromMaybe)
import Data.ShareMap (ShareMap)
import qualified Data.ShareMap as ShareMap
import qualified Data.Text as Text
import Language.Fixpoint.SortCheck (exprSort_maybe)
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Types.Constraints
import Language.Fixpoint.Types.Environments
( BindEnv
, BindId
, IBindEnv
, beBinds
, diffIBindEnv
, elemsIBindEnv
, emptyIBindEnv
, filterIBindEnv
, fromListIBindEnv
, insertsIBindEnv
, insertBindEnv
, lookupBindEnv
, memberIBindEnv
, unionIBindEnv
, unionsIBindEnv
)
import Language.Fixpoint.Types.Names
( Symbol
, anfPrefix
, isPrefixOfSym
, prefixOfSym
, symbolText
)
import Language.Fixpoint.Types.PrettyPrint
import Language.Fixpoint.Types.Refinements
( Brel(..)
, Expr(..)
, KVar(..)
, SortedReft(..)
, Subst(..)
, pattern PTrue
, pattern PFalse
, expr
, exprKVars
, exprSymbolsSet
, mapPredReft
, pAnd
, reft
, reftBind
, reftPred
, sortedReftSymbols
, subst1
)
import Language.Fixpoint.Types.Sorts (boolSort, sortSymbols)
import Language.Fixpoint.Types.Visitor (mapExprOnExpr)
reduceEnvironments :: FInfo a -> FInfo a
reduceEnvironments :: FInfo a -> FInfo a
reduceEnvironments FInfo a
fi =
let constraints :: [(SubcId, SubC a)]
constraints = HashMap SubcId (SubC a) -> [(SubcId, SubC a)]
forall k v. HashMap k v -> [(k, v)]
HashMap.Strict.toList (HashMap SubcId (SubC a) -> [(SubcId, SubC a)])
-> HashMap SubcId (SubC a) -> [(SubcId, SubC a)]
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi
aenvMap :: HashMap Symbol (HashSet Symbol)
aenvMap = AxiomEnv -> HashMap Symbol (HashSet Symbol)
axiomEnvSymbols (FInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae FInfo a
fi)
reducedEnvs :: [ReducedConstraint a]
reducedEnvs = ((SubcId, SubC a) -> ReducedConstraint a)
-> [(SubcId, SubC a)] -> [ReducedConstraint a]
forall a b. (a -> b) -> [a] -> [b]
map (BindEnv
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
forall a.
BindEnv
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
reduceConstraintEnvironment (FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi) HashMap Symbol (HashSet Symbol)
aenvMap) [(SubcId, SubC a)]
constraints
([(SubcId, SubC a)]
cm', HashMap KVar (WfC a)
ws') = BindEnv
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
forall a.
BindEnv
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments (FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi) ([ReducedConstraint a]
reducedEnvs, FInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
fi)
bs' :: BindEnv
bs' = (FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi) { beBinds :: BindMap (Symbol, SortedReft)
beBinds = BindMap (Symbol, SortedReft)
-> [(SubcId, SubC a)]
-> HashMap KVar (WfC a)
-> BindMap (Symbol, SortedReft)
forall a.
BindMap (Symbol, SortedReft)
-> [(SubcId, SubC a)]
-> HashMap KVar (WfC a)
-> BindMap (Symbol, SortedReft)
dropBindsMissingFrom (BindEnv -> BindMap (Symbol, SortedReft)
forall a. SizedEnv a -> BindMap a
beBinds (BindEnv -> BindMap (Symbol, SortedReft))
-> BindEnv -> BindMap (Symbol, SortedReft)
forall a b. (a -> b) -> a -> b
$ FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi) [(SubcId, SubC a)]
cm' HashMap KVar (WfC a)
ws' }
in FInfo a
fi
{ bs :: BindEnv
bs = BindEnv
bs'
, cm :: HashMap SubcId (SubC a)
cm = [(SubcId, SubC a)] -> HashMap SubcId (SubC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [(SubcId, SubC a)]
cm'
, ws :: HashMap KVar (WfC a)
ws = HashMap KVar (WfC a)
ws'
, ebinds :: [BindId]
ebinds = BindEnv -> [BindId] -> [BindId]
forall a. SizedEnv a -> [BindId] -> [BindId]
updateEbinds BindEnv
bs' (FInfo a -> [BindId]
forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds FInfo a
fi)
, bindInfo :: HashMap BindId a
bindInfo = BindEnv -> HashMap BindId a -> HashMap BindId a
forall w v. SizedEnv w -> HashMap BindId v -> HashMap BindId v
updateBindInfoKeys BindEnv
bs' (HashMap BindId a -> HashMap BindId a)
-> HashMap BindId a -> HashMap BindId a
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap BindId a
forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo FInfo a
fi
}
where
dropBindsMissingFrom
:: HashMap BindId (Symbol, SortedReft)
-> [(SubcId, SubC a)]
-> HashMap KVar (WfC a)
-> HashMap BindId (Symbol, SortedReft)
dropBindsMissingFrom :: BindMap (Symbol, SortedReft)
-> [(SubcId, SubC a)]
-> HashMap KVar (WfC a)
-> BindMap (Symbol, SortedReft)
dropBindsMissingFrom BindMap (Symbol, SortedReft)
be [(SubcId, SubC a)]
cs HashMap KVar (WfC a)
ws =
let ibindEnv :: IBindEnv
ibindEnv = [IBindEnv] -> IBindEnv
unionsIBindEnv ([IBindEnv] -> IBindEnv) -> [IBindEnv] -> IBindEnv
forall a b. (a -> b) -> a -> b
$
((SubcId, SubC a) -> IBindEnv) -> [(SubcId, SubC a)] -> [IBindEnv]
forall a b. (a -> b) -> [a] -> [b]
map (SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv (SubC a -> IBindEnv)
-> ((SubcId, SubC a) -> SubC a) -> (SubcId, SubC a) -> IBindEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubcId, SubC a) -> SubC a
forall a b. (a, b) -> b
snd) [(SubcId, SubC a)]
cs [IBindEnv] -> [IBindEnv] -> [IBindEnv]
forall a. [a] -> [a] -> [a]
++
(WfC a -> IBindEnv) -> [WfC a] -> [IBindEnv]
forall a b. (a -> b) -> [a] -> [b]
map WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv (HashMap KVar (WfC a) -> [WfC a]
forall k v. HashMap k v -> [v]
HashMap.elems HashMap KVar (WfC a)
ws)
in
(BindId -> (Symbol, SortedReft) -> Bool)
-> BindMap (Symbol, SortedReft) -> BindMap (Symbol, SortedReft)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey (\BindId
bId (Symbol, SortedReft)
_ -> BindId -> IBindEnv -> Bool
memberIBindEnv BindId
bId IBindEnv
ibindEnv) BindMap (Symbol, SortedReft)
be
updateEbinds :: SizedEnv a -> [BindId] -> [BindId]
updateEbinds SizedEnv a
be = (BindId -> Bool) -> [BindId] -> [BindId]
forall a. (a -> Bool) -> [a] -> [a]
filter (BindId -> HashMap BindId a -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`HashMap.member` SizedEnv a -> HashMap BindId a
forall a. SizedEnv a -> BindMap a
beBinds SizedEnv a
be)
updateBindInfoKeys :: SizedEnv w -> HashMap BindId v -> HashMap BindId v
updateBindInfoKeys SizedEnv w
be HashMap BindId v
oldBindInfos =
HashMap BindId v -> HashMap BindId w -> HashMap BindId v
forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
HashMap.intersection HashMap BindId v
oldBindInfos (SizedEnv w -> HashMap BindId w
forall a. SizedEnv a -> BindMap a
beBinds SizedEnv w
be)
reduceWFConstraintEnvironments
:: BindEnv
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments :: BindEnv
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments BindEnv
bindEnv ([ReducedConstraint a]
cs, HashMap KVar (WfC a)
wfs) =
let
(HashMap KVar (HashSet Symbol)
kvarsBinds, HashMap KVar (HashSet Symbol)
kvarSubstSymbols, [[KVar]]
kvarsBySubC) = BindEnv
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol),
[[KVar]])
forall a.
BindEnv
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol),
[[KVar]])
relatedKVarBinds BindEnv
bindEnv [ReducedConstraint a]
cs
wfBindsPlusSortSymbols :: HashMap KVar (HashSet Symbol)
wfBindsPlusSortSymbols =
(HashSet Symbol -> HashSet Symbol -> HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashMap KVar (HashSet Symbol)
kvarsBinds (HashMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol))
-> HashMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$
(WfC a -> HashSet Symbol)
-> HashMap KVar (WfC a) -> HashMap KVar (HashSet Symbol)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Sort -> HashSet Symbol
sortSymbols (Sort -> HashSet Symbol)
-> (WfC a -> Sort) -> WfC a -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Symbol
_, Sort
b, KVar
_) -> Sort
b) ((Symbol, Sort, KVar) -> Sort)
-> (WfC a -> (Symbol, Sort, KVar)) -> WfC a -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft) HashMap KVar (WfC a)
wfs
kvarsRelevantBinds :: HashMap KVar (HashSet Symbol)
kvarsRelevantBinds =
(HashSet Symbol -> HashSet Symbol -> HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashMap KVar (HashSet Symbol)
wfBindsPlusSortSymbols (HashMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol))
-> HashMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$
HashMap KVar (HashSet Symbol)
kvarSubstSymbols
ws' :: HashMap KVar (WfC a)
ws' =
(KVar -> WfC a -> WfC a)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapWithKey
(BindEnv -> HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
forall a.
BindEnv -> HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
reduceWFConstraintEnvironment BindEnv
bindEnv HashMap KVar (HashSet Symbol)
kvarsRelevantBinds)
HashMap KVar (WfC a)
wfs
wsSymbols :: HashMap KVar (HashSet Symbol)
wsSymbols = (WfC a -> HashSet Symbol)
-> HashMap KVar (WfC a) -> HashMap KVar (HashSet Symbol)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (BindEnv -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv
bindEnv (IBindEnv -> HashSet Symbol)
-> (WfC a -> IBindEnv) -> WfC a -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv) HashMap KVar (WfC a)
ws'
kvarsWsBinds :: HashMap KVar (HashSet Symbol)
kvarsWsBinds =
(HashSet Symbol -> HashSet Symbol -> HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.intersection HashMap KVar (HashSet Symbol)
wfBindsPlusSortSymbols HashMap KVar (HashSet Symbol)
wsSymbols
cs' :: [(SubcId, SubC a)]
cs' = ([KVar] -> ReducedConstraint a -> (SubcId, SubC a))
-> [[KVar]] -> [ReducedConstraint a] -> [(SubcId, SubC a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
(BindEnv
-> HashMap KVar (HashSet Symbol)
-> [KVar]
-> ReducedConstraint a
-> (SubcId, SubC a)
forall a.
BindEnv
-> HashMap KVar (HashSet Symbol)
-> [KVar]
-> ReducedConstraint a
-> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds BindEnv
bindEnv HashMap KVar (HashSet Symbol)
kvarsWsBinds)
[[KVar]]
kvarsBySubC
[ReducedConstraint a]
cs
in
([(SubcId, SubC a)]
cs', HashMap KVar (WfC a)
ws')
where
updateSubcEnvsWithKVarBinds
:: BindEnv
-> HashMap KVar (HashSet Symbol)
-> [KVar]
-> ReducedConstraint a
-> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds :: BindEnv
-> HashMap KVar (HashSet Symbol)
-> [KVar]
-> ReducedConstraint a
-> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds BindEnv
be HashMap KVar (HashSet Symbol)
kvarsBinds [KVar]
kvs ReducedConstraint a
c =
let updateIBindEnv :: IBindEnv -> IBindEnv
updateIBindEnv IBindEnv
oldEnv =
IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv (ReducedConstraint a -> IBindEnv
forall a. ReducedConstraint a -> IBindEnv
reducedEnv ReducedConstraint a
c) (IBindEnv -> IBindEnv) -> IBindEnv -> IBindEnv
forall a b. (a -> b) -> a -> b
$
if [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [KVar]
kvs then IBindEnv
emptyIBindEnv
else [BindId] -> IBindEnv
fromListIBindEnv
[ BindId
bId
| BindId
bId <- IBindEnv -> [BindId]
elemsIBindEnv IBindEnv
oldEnv
, let (Symbol
s, SortedReft
_sr) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
bId BindEnv
be
, (KVar -> Bool) -> [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> KVar -> Bool
neededByKVar Symbol
s) [KVar]
kvs
]
neededByKVar :: Symbol -> KVar -> Bool
neededByKVar Symbol
s KVar
kv =
case KVar -> HashMap KVar (HashSet Symbol) -> Maybe (HashSet Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup KVar
kv HashMap KVar (HashSet Symbol)
kvarsBinds of
Maybe (HashSet Symbol)
Nothing -> Bool
False
Just HashSet Symbol
kbindSyms -> Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Symbol
s HashSet Symbol
kbindSyms
in (ReducedConstraint a -> SubcId
forall a. ReducedConstraint a -> SubcId
constraintId ReducedConstraint a
c, SubC a -> (IBindEnv -> IBindEnv) -> SubC a
forall (c :: * -> *) a.
TaggedC c a =>
c a -> (IBindEnv -> IBindEnv) -> c a
updateSEnv (ReducedConstraint a -> SubC a
forall a. ReducedConstraint a -> SubC a
originalConstraint ReducedConstraint a
c) IBindEnv -> IBindEnv
updateIBindEnv)
reduceWFConstraintEnvironment
:: BindEnv
-> HashMap KVar (HashSet Symbol)
-> KVar
-> WfC a
-> WfC a
reduceWFConstraintEnvironment :: BindEnv -> HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
reduceWFConstraintEnvironment BindEnv
bindEnv HashMap KVar (HashSet Symbol)
kvarBinds KVar
k WfC a
c =
case KVar -> HashMap KVar (HashSet Symbol) -> Maybe (HashSet Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup KVar
k HashMap KVar (HashSet Symbol)
kvarBinds of
Maybe (HashSet Symbol)
Nothing -> WfC a
c { wenv :: IBindEnv
wenv = IBindEnv
emptyIBindEnv }
Just HashSet Symbol
kbindSymbols ->
WfC a
c { wenv :: IBindEnv
wenv = (BindId -> Bool) -> IBindEnv -> IBindEnv
filterIBindEnv (HashSet Symbol -> BindId -> Bool
relevantBindIds HashSet Symbol
kbindSymbols) (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv WfC a
c) }
where
relevantBindIds :: HashSet Symbol -> BindId -> Bool
relevantBindIds :: HashSet Symbol -> BindId -> Bool
relevantBindIds HashSet Symbol
kbindSymbols BindId
bId =
let (Symbol
s, SortedReft
_) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
bId BindEnv
bindEnv
in Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Symbol
s HashSet Symbol
kbindSymbols
data ReducedConstraint a = ReducedConstraint
{ ReducedConstraint a -> IBindEnv
reducedEnv :: IBindEnv
, ReducedConstraint a -> SubC a
originalConstraint :: SubC a
, ReducedConstraint a -> SubcId
constraintId :: SubcId
}
reduceConstraintEnvironment
:: BindEnv
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
reduceConstraintEnvironment :: BindEnv
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
reduceConstraintEnvironment BindEnv
bindEnv HashMap Symbol (HashSet Symbol)
aenvMap (SubcId
cid, SubC a
c) =
let env :: [(Symbol, BindId, SortedReft)]
env = [ (Symbol
s, BindId
bId, SortedReft
sr)
| BindId
bId <- IBindEnv -> [BindId]
elemsIBindEnv (IBindEnv -> [BindId]) -> IBindEnv -> [BindId]
forall a b. (a -> b) -> a -> b
$ SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c
, let (Symbol
s, SortedReft
sr) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
bId BindEnv
bindEnv
]
prunedEnv :: IBindEnv
prunedEnv =
[BindId] -> IBindEnv
fromListIBindEnv
[ BindId
bId | (Symbol
_, BindId
bId, SortedReft
_) <- HashMap Symbol (HashSet Symbol)
-> HashSet Symbol
-> [(Symbol, BindId, SortedReft)]
-> [(Symbol, BindId, SortedReft)]
dropIrrelevantBindings HashMap Symbol (HashSet Symbol)
aenvMap HashSet Symbol
constraintSymbols [(Symbol, BindId, SortedReft)]
env ]
constraintSymbols :: HashSet Symbol
constraintSymbols =
HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union (SortedReft -> HashSet Symbol
sortedReftSymbols (SortedReft -> HashSet Symbol) -> SortedReft -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c) (SortedReft -> HashSet Symbol
sortedReftSymbols (SortedReft -> HashSet Symbol) -> SortedReft -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)
in ReducedConstraint :: forall a. IBindEnv -> SubC a -> SubcId -> ReducedConstraint a
ReducedConstraint
{ reducedEnv :: IBindEnv
reducedEnv = IBindEnv
prunedEnv
, originalConstraint :: SubC a
originalConstraint = SubC a
c
, constraintId :: SubcId
constraintId = SubcId
cid
}
dropIrrelevantBindings
:: HashMap Symbol (HashSet Symbol)
-> HashSet Symbol
-> [(Symbol, BindId, SortedReft)]
-> [(Symbol, BindId, SortedReft)]
dropIrrelevantBindings :: HashMap Symbol (HashSet Symbol)
-> HashSet Symbol
-> [(Symbol, BindId, SortedReft)]
-> [(Symbol, BindId, SortedReft)]
dropIrrelevantBindings HashMap Symbol (HashSet Symbol)
aenvMap HashSet Symbol
extraSymbols [(Symbol, BindId, SortedReft)]
env =
((Symbol, BindId, SortedReft) -> Bool)
-> [(Symbol, BindId, SortedReft)] -> [(Symbol, BindId, SortedReft)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, BindId, SortedReft) -> Bool
forall b. (Symbol, b, SortedReft) -> Bool
relevantBind [(Symbol, BindId, SortedReft)]
env
where
allSymbols :: HashSet Symbol
allSymbols =
HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
reachableSymbols (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
extraSymbols HashSet Symbol
envSymbols) HashMap Symbol (HashSet Symbol)
aenvMap
envSymbols :: HashSet Symbol
envSymbols =
[HashSet Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
HashSet.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, BindId, SortedReft) -> HashSet Symbol)
-> [(Symbol, BindId, SortedReft)] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
_, BindId
_, SortedReft
sr) -> SortedReft -> HashSet Symbol
sortedReftSymbols SortedReft
sr) [(Symbol, BindId, SortedReft)]
env
relevantBind :: (Symbol, b, SortedReft) -> Bool
relevantBind (Symbol
s, b
_, SortedReft
sr)
| Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Symbol
s HashSet Symbol
allSymbols = Bool
True
| Bool
otherwise = case Reft -> Expr
reftPred (SortedReft -> Reft
sr_reft SortedReft
sr) of
Expr
PTrue -> Bool
False
PAtom Brel
_ (Expr -> Expr
dropECst -> EVar Symbol
sym) Expr
_e -> Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Reft -> Symbol
reftBind (SortedReft -> Reft
sr_reft SortedReft
sr)
PAtom Brel
_ Expr
_e (Expr -> Expr
dropECst -> EVar Symbol
sym) -> Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Reft -> Symbol
reftBind (SortedReft -> Reft
sr_reft SortedReft
sr)
Expr
_ -> Bool
True
axiomEnvSymbols :: AxiomEnv -> HashMap Symbol (HashSet Symbol)
axiomEnvSymbols :: AxiomEnv -> HashMap Symbol (HashSet Symbol)
axiomEnvSymbols AxiomEnv
ae =
HashMap Symbol (HashSet Symbol)
-> HashMap Symbol (HashSet Symbol)
-> HashMap Symbol (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union
([(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList ([(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol))
-> [(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$ (Equation -> (Symbol, HashSet Symbol))
-> [Equation] -> [(Symbol, HashSet Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> (Symbol, HashSet Symbol)
eqSymbols ([Equation] -> [(Symbol, HashSet Symbol)])
-> [Equation] -> [(Symbol, HashSet Symbol)]
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> [Equation]
aenvEqs AxiomEnv
ae)
([(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList ([(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol))
-> [(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$ (Rewrite -> (Symbol, HashSet Symbol))
-> [Rewrite] -> [(Symbol, HashSet Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map Rewrite -> (Symbol, HashSet Symbol)
rewriteSymbols ([Rewrite] -> [(Symbol, HashSet Symbol)])
-> [Rewrite] -> [(Symbol, HashSet Symbol)]
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
ae)
where
eqSymbols :: Equation -> (Symbol, HashSet Symbol)
eqSymbols Equation
eq =
let bodySymbols :: HashSet Symbol
bodySymbols =
HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
(Expr -> HashSet Symbol
exprSymbolsSet (Equation -> Expr
eqBody Equation
eq) HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.union` Sort -> HashSet Symbol
sortSymbols (Equation -> Sort
eqSort Equation
eq))
([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, Sort)] -> [Symbol]) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)
sortSyms :: HashSet Symbol
sortSyms = [HashSet Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
HashSet.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> HashSet Symbol)
-> [(Symbol, Sort)] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Sort -> HashSet Symbol
sortSymbols (Sort -> HashSet Symbol)
-> ((Symbol, Sort) -> Sort) -> (Symbol, Sort) -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd) ([(Symbol, Sort)] -> [HashSet Symbol])
-> [(Symbol, Sort)] -> [HashSet Symbol]
forall a b. (a -> b) -> a -> b
$ Equation -> [(Symbol, Sort)]
eqArgs Equation
eq
allSymbols :: HashSet Symbol
allSymbols =
if Equation -> Bool
eqRec Equation
eq then
Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (Equation -> Symbol
eqName Equation
eq) (HashSet Symbol
bodySymbols HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.union` HashSet Symbol
sortSyms)
else
HashSet Symbol
bodySymbols HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.union` HashSet Symbol
sortSyms
in
(Equation -> Symbol
eqName Equation
eq, HashSet Symbol
allSymbols)
rewriteSymbols :: Rewrite -> (Symbol, HashSet Symbol)
rewriteSymbols Rewrite
rw =
let bodySymbols :: HashSet Symbol
bodySymbols =
HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
(Expr -> HashSet Symbol
exprSymbolsSet (Rewrite -> Expr
smBody Rewrite
rw))
([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Rewrite -> [Symbol]
smArgs Rewrite
rw)
rwSymbols :: HashSet Symbol
rwSymbols = Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (Rewrite -> Symbol
smDC Rewrite
rw) HashSet Symbol
bodySymbols
in (Rewrite -> Symbol
smName Rewrite
rw, HashSet Symbol
rwSymbols)
unconsHashSet :: (Hashable a, Eq a) => HashSet a -> Maybe (a, HashSet a)
unconsHashSet :: HashSet a -> Maybe (a, HashSet a)
unconsHashSet HashSet a
xs = case HashSet a -> [a]
forall a. HashSet a -> [a]
HashSet.toList HashSet a
xs of
[] -> Maybe (a, HashSet a)
forall a. Maybe a
Nothing
(a
x : [a]
_) -> (a, HashSet a) -> Maybe (a, HashSet a)
forall a. a -> Maybe a
Just (a
x, a -> HashSet a -> HashSet a
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.delete a
x HashSet a
xs)
setOf :: (Hashable k, Eq k) => HashMap k (HashSet a) -> k -> HashSet a
setOf :: HashMap k (HashSet a) -> k -> HashSet a
setOf HashMap k (HashSet a)
m k
x = HashSet a -> Maybe (HashSet a) -> HashSet a
forall a. a -> Maybe a -> a
fromMaybe HashSet a
forall a. HashSet a
HashSet.empty (k -> HashMap k (HashSet a) -> Maybe (HashSet a)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup k
x HashMap k (HashSet a)
m)
mapOf :: (Hashable k, Eq k) => HashMap k (HashMap a b) -> k -> HashMap a b
mapOf :: HashMap k (HashMap a b) -> k -> HashMap a b
mapOf HashMap k (HashMap a b)
m k
x = HashMap a b -> Maybe (HashMap a b) -> HashMap a b
forall a. a -> Maybe a -> a
fromMaybe HashMap a b
forall k v. HashMap k v
HashMap.empty (k -> HashMap k (HashMap a b) -> Maybe (HashMap a b)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup k
x HashMap k (HashMap a b)
m)
relatedKVarBinds
:: BindEnv
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol), [[KVar]])
relatedKVarBinds :: BindEnv
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol),
[[KVar]])
relatedKVarBinds BindEnv
bindEnv [ReducedConstraint a]
cs =
let kvarsSubstSymbolsBySubC :: [HashMap KVar (HashSet Symbol)]
kvarsSubstSymbolsBySubC = (ReducedConstraint a -> HashMap KVar (HashSet Symbol))
-> [ReducedConstraint a] -> [HashMap KVar (HashSet Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map ReducedConstraint a -> HashMap KVar (HashSet Symbol)
forall a. ReducedConstraint a -> HashMap KVar (HashSet Symbol)
kvarBindsFromSubC [ReducedConstraint a]
cs
kvarsBySubC :: [[KVar]]
kvarsBySubC = (HashMap KVar (HashSet Symbol) -> [KVar])
-> [HashMap KVar (HashSet Symbol)] -> [[KVar]]
forall a b. (a -> b) -> [a] -> [b]
map HashMap KVar (HashSet Symbol) -> [KVar]
forall k v. HashMap k v -> [k]
HashMap.keys [HashMap KVar (HashSet Symbol)]
kvarsSubstSymbolsBySubC
bindIdsByKVar :: HashMap KVar (HashSet Symbol)
bindIdsByKVar =
ShareMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol)
forall k v. (Hashable k, Eq k) => ShareMap k v -> HashMap k v
ShareMap.toHashMap (ShareMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol))
-> ShareMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$
(IBindEnv -> HashSet Symbol)
-> ShareMap KVar IBindEnv -> ShareMap KVar (HashSet Symbol)
forall a b k. (a -> b) -> ShareMap k a -> ShareMap k b
ShareMap.map (BindEnv -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv
bindEnv) (ShareMap KVar IBindEnv -> ShareMap KVar (HashSet Symbol))
-> ShareMap KVar IBindEnv -> ShareMap KVar (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$
[(IBindEnv, [KVar])] -> ShareMap KVar IBindEnv
groupIBindEnvByKVar ([(IBindEnv, [KVar])] -> ShareMap KVar IBindEnv)
-> [(IBindEnv, [KVar])] -> ShareMap KVar IBindEnv
forall a b. (a -> b) -> a -> b
$ [IBindEnv] -> [[KVar]] -> [(IBindEnv, [KVar])]
forall a b. [a] -> [b] -> [(a, b)]
zip ((ReducedConstraint a -> IBindEnv)
-> [ReducedConstraint a] -> [IBindEnv]
forall a b. (a -> b) -> [a] -> [b]
map ReducedConstraint a -> IBindEnv
forall a. ReducedConstraint a -> IBindEnv
reducedEnv [ReducedConstraint a]
cs) [[KVar]]
kvarsBySubC
substsByKVar :: HashMap KVar (HashSet Symbol)
substsByKVar =
(HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol))
-> HashMap KVar (HashSet Symbol)
-> [HashMap KVar (HashSet Symbol)]
-> HashMap KVar (HashSet Symbol)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((HashSet Symbol -> HashSet Symbol -> HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union) HashMap KVar (HashSet Symbol)
forall k v. HashMap k v
HashMap.empty [HashMap KVar (HashSet Symbol)]
kvarsSubstSymbolsBySubC
in
(HashMap KVar (HashSet Symbol)
bindIdsByKVar, HashMap KVar (HashSet Symbol)
substsByKVar, [[KVar]]
kvarsBySubC)
where
kvarsByBindId :: HashMap BindId (HashMap KVar [Subst])
kvarsByBindId :: HashMap BindId (HashMap KVar [Subst])
kvarsByBindId =
((Symbol, SortedReft) -> HashMap KVar [Subst])
-> BindMap (Symbol, SortedReft)
-> HashMap BindId (HashMap KVar [Subst])
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Expr -> HashMap KVar [Subst]
exprKVars (Expr -> HashMap KVar [Subst])
-> ((Symbol, SortedReft) -> Expr)
-> (Symbol, SortedReft)
-> HashMap KVar [Subst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred (Reft -> Expr)
-> ((Symbol, SortedReft) -> Reft) -> (Symbol, SortedReft) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft (SortedReft -> Reft)
-> ((Symbol, SortedReft) -> SortedReft)
-> (Symbol, SortedReft)
-> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd) (BindMap (Symbol, SortedReft)
-> HashMap BindId (HashMap KVar [Subst]))
-> BindMap (Symbol, SortedReft)
-> HashMap BindId (HashMap KVar [Subst])
forall a b. (a -> b) -> a -> b
$ BindEnv -> BindMap (Symbol, SortedReft)
forall a. SizedEnv a -> BindMap a
beBinds BindEnv
bindEnv
kvarBindsFromSubC :: ReducedConstraint a -> HashMap KVar (HashSet Symbol)
kvarBindsFromSubC :: ReducedConstraint a -> HashMap KVar (HashSet Symbol)
kvarBindsFromSubC ReducedConstraint a
sc =
let c :: SubC a
c = ReducedConstraint a -> SubC a
forall a. ReducedConstraint a -> SubC a
originalConstraint ReducedConstraint a
sc
unSubst :: Subst -> HashMap Symbol Expr
unSubst (Su HashMap Symbol Expr
su) = HashMap Symbol Expr
su
substsToHashSet :: [Subst] -> HashSet Symbol
substsToHashSet =
HashMap Symbol () -> HashSet Symbol
forall a. HashMap a () -> HashSet a
HashSet.fromMap (HashMap Symbol () -> HashSet Symbol)
-> ([Subst] -> HashMap Symbol ()) -> [Subst] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> ()) -> HashMap Symbol Expr -> HashMap Symbol ()
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (() -> Expr -> ()
forall a b. a -> b -> a
const ()) (HashMap Symbol Expr -> HashMap Symbol ())
-> ([Subst] -> HashMap Symbol Expr) -> [Subst] -> HashMap Symbol ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HashMap Symbol Expr] -> HashMap Symbol Expr
forall k v. (Eq k, Hashable k) => [HashMap k v] -> HashMap k v
HashMap.unions ([HashMap Symbol Expr] -> HashMap Symbol Expr)
-> ([Subst] -> [HashMap Symbol Expr])
-> [Subst]
-> HashMap Symbol Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Subst -> HashMap Symbol Expr) -> [Subst] -> [HashMap Symbol Expr]
forall a b. (a -> b) -> [a] -> [b]
map Subst -> HashMap Symbol Expr
unSubst
in (HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol) -> HashMap KVar (HashSet Symbol))
-> HashMap KVar (HashSet Symbol)
-> [HashMap KVar (HashSet Symbol)]
-> HashMap KVar (HashSet Symbol)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((HashSet Symbol -> HashSet Symbol -> HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
-> HashMap KVar (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union) HashMap KVar (HashSet Symbol)
forall k v. HashMap k v
HashMap.empty ([HashMap KVar (HashSet Symbol)] -> HashMap KVar (HashSet Symbol))
-> [HashMap KVar (HashSet Symbol)] -> HashMap KVar (HashSet Symbol)
forall a b. (a -> b) -> a -> b
$
(HashMap KVar [Subst] -> HashMap KVar (HashSet Symbol))
-> [HashMap KVar [Subst]] -> [HashMap KVar (HashSet Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (([Subst] -> HashSet Symbol)
-> HashMap KVar [Subst] -> HashMap KVar (HashSet Symbol)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map [Subst] -> HashSet Symbol
substsToHashSet) ([HashMap KVar [Subst]] -> [HashMap KVar (HashSet Symbol)])
-> [HashMap KVar [Subst]] -> [HashMap KVar (HashSet Symbol)]
forall a b. (a -> b) -> a -> b
$
(Expr -> HashMap KVar [Subst]
exprKVars (Reft -> Expr
reftPred (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c) HashMap KVar [Subst]
-> [HashMap KVar [Subst]] -> [HashMap KVar [Subst]]
forall a. a -> [a] -> [a]
:) ([HashMap KVar [Subst]] -> [HashMap KVar [Subst]])
-> [HashMap KVar [Subst]] -> [HashMap KVar [Subst]]
forall a b. (a -> b) -> a -> b
$
(Expr -> HashMap KVar [Subst]
exprKVars (Reft -> Expr
reftPred (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft (SortedReft -> Reft) -> SortedReft -> Reft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c) HashMap KVar [Subst]
-> [HashMap KVar [Subst]] -> [HashMap KVar [Subst]]
forall a. a -> [a] -> [a]
:) ([HashMap KVar [Subst]] -> [HashMap KVar [Subst]])
-> [HashMap KVar [Subst]] -> [HashMap KVar [Subst]]
forall a b. (a -> b) -> a -> b
$
(BindId -> HashMap KVar [Subst])
-> [BindId] -> [HashMap KVar [Subst]]
forall a b. (a -> b) -> [a] -> [b]
map (HashMap BindId (HashMap KVar [Subst])
-> BindId -> HashMap KVar [Subst]
forall k a b.
(Hashable k, Eq k) =>
HashMap k (HashMap a b) -> k -> HashMap a b
mapOf HashMap BindId (HashMap KVar [Subst])
kvarsByBindId) ([BindId] -> [HashMap KVar [Subst]])
-> [BindId] -> [HashMap KVar [Subst]]
forall a b. (a -> b) -> a -> b
$
IBindEnv -> [BindId]
elemsIBindEnv (ReducedConstraint a -> IBindEnv
forall a. ReducedConstraint a -> IBindEnv
reducedEnv ReducedConstraint a
sc)
groupIBindEnvByKVar :: [(IBindEnv, [KVar])] -> ShareMap KVar IBindEnv
groupIBindEnvByKVar :: [(IBindEnv, [KVar])] -> ShareMap KVar IBindEnv
groupIBindEnvByKVar = (ShareMap KVar IBindEnv
-> (IBindEnv, [KVar]) -> ShareMap KVar IBindEnv)
-> ShareMap KVar IBindEnv
-> [(IBindEnv, [KVar])]
-> ShareMap KVar IBindEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ShareMap KVar IBindEnv
-> (IBindEnv, [KVar]) -> ShareMap KVar IBindEnv
mergeBinds ShareMap KVar IBindEnv
forall k v. ShareMap k v
ShareMap.empty
mergeBinds
:: ShareMap KVar IBindEnv
-> (IBindEnv, [KVar])
-> ShareMap KVar IBindEnv
mergeBinds :: ShareMap KVar IBindEnv
-> (IBindEnv, [KVar]) -> ShareMap KVar IBindEnv
mergeBinds ShareMap KVar IBindEnv
sm (IBindEnv
bindIds, [KVar]
kvars) = case [KVar]
kvars of
[] -> ShareMap KVar IBindEnv
sm
KVar
k : [KVar]
ks ->
let sm' :: ShareMap KVar IBindEnv
sm' = (IBindEnv -> IBindEnv -> IBindEnv)
-> KVar
-> IBindEnv
-> ShareMap KVar IBindEnv
-> ShareMap KVar IBindEnv
forall k v.
(Hashable k, Eq k) =>
(v -> v -> v) -> k -> v -> ShareMap k v -> ShareMap k v
ShareMap.insertWith IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv KVar
k IBindEnv
bindIds ShareMap KVar IBindEnv
sm
in (KVar -> ShareMap KVar IBindEnv -> ShareMap KVar IBindEnv)
-> ShareMap KVar IBindEnv -> [KVar] -> ShareMap KVar IBindEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((IBindEnv -> IBindEnv -> IBindEnv)
-> KVar -> KVar -> ShareMap KVar IBindEnv -> ShareMap KVar IBindEnv
forall k v.
(Hashable k, Eq k) =>
(v -> v -> v) -> k -> k -> ShareMap k v -> ShareMap k v
ShareMap.mergeKeysWith IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv KVar
k) ShareMap KVar IBindEnv
sm' [KVar]
ks
asSymbolSet :: BindEnv -> IBindEnv -> HashSet Symbol
asSymbolSet :: BindEnv -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv
be IBindEnv
ibinds =
[Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList
[ Symbol
s
| BindId
bId <- IBindEnv -> [BindId]
elemsIBindEnv IBindEnv
ibinds
, let (Symbol
s, SortedReft
_) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
bId BindEnv
be
]
reachableSymbols :: HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
reachableSymbols :: HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
reachableSymbols HashSet Symbol
ss0 HashMap Symbol (HashSet Symbol)
outgoingEdges = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
forall a. HashSet a
HashSet.empty HashSet Symbol
ss0
where
go :: HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go :: HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
acc HashSet Symbol
ss = case HashSet Symbol -> Maybe (Symbol, HashSet Symbol)
forall a. (Hashable a, Eq a) => HashSet a -> Maybe (a, HashSet a)
unconsHashSet HashSet Symbol
ss of
Maybe (Symbol, HashSet Symbol)
Nothing -> HashSet Symbol
acc
Just (Symbol
x, HashSet Symbol
xs) ->
if Symbol
x Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet Symbol
acc then HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
acc HashSet Symbol
xs
else
let relatedToX :: HashSet Symbol
relatedToX = HashMap Symbol (HashSet Symbol) -> Symbol -> HashSet Symbol
forall k a.
(Hashable k, Eq k) =>
HashMap k (HashSet a) -> k -> HashSet a
setOf HashMap Symbol (HashSet Symbol)
outgoingEdges Symbol
x
in HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go (Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Symbol
x HashSet Symbol
acc) (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
relatedToX HashSet Symbol
xs)
simplifyBindings :: Config -> FInfo a -> FInfo a
simplifyBindings :: Config -> FInfo a -> FInfo a
simplifyBindings Config
cfg FInfo a
fi =
let (BindEnv
bs', HashMap SubcId (SubC a)
cm', HashMap BindId [BindId]
oldToNew) = BindEnv
-> HashMap SubcId (SubC a)
-> (BindEnv, HashMap SubcId (SubC a), HashMap BindId [BindId])
forall a.
BindEnv
-> HashMap SubcId (SubC a)
-> (BindEnv, HashMap SubcId (SubC a), HashMap BindId [BindId])
simplifyConstraints (FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi) (FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi)
in FInfo a
fi
{ bs :: BindEnv
bs = BindEnv
bs'
, cm :: HashMap SubcId (SubC a)
cm = HashMap SubcId (SubC a)
cm'
, ebinds :: [BindId]
ebinds = HashMap BindId [BindId] -> [BindId] -> [BindId]
updateEbinds HashMap BindId [BindId]
oldToNew (FInfo a -> [BindId]
forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds FInfo a
fi)
, bindInfo :: HashMap BindId a
bindInfo = HashMap BindId [BindId] -> HashMap BindId a -> HashMap BindId a
forall a.
HashMap BindId [BindId] -> HashMap BindId a -> HashMap BindId a
updateBindInfoKeys HashMap BindId [BindId]
oldToNew (HashMap BindId a -> HashMap BindId a)
-> HashMap BindId a -> HashMap BindId a
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap BindId a
forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo FInfo a
fi
}
where
updateEbinds :: HashMap BindId [BindId] -> [BindId] -> [BindId]
updateEbinds :: HashMap BindId [BindId] -> [BindId] -> [BindId]
updateEbinds HashMap BindId [BindId]
oldToNew [BindId]
ebs =
[BindId] -> [BindId]
forall a. Eq a => [a] -> [a]
nub ([BindId] -> [BindId]) -> [BindId] -> [BindId]
forall a b. (a -> b) -> a -> b
$
[[BindId]] -> [BindId]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ BindId
bId BindId -> [BindId] -> [BindId]
forall a. a -> [a] -> [a]
: [BindId] -> Maybe [BindId] -> [BindId]
forall a. a -> Maybe a -> a
fromMaybe [] (BindId -> HashMap BindId [BindId] -> Maybe [BindId]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup BindId
bId HashMap BindId [BindId]
oldToNew) | BindId
bId <- [BindId]
ebs ]
updateBindInfoKeys
:: HashMap BindId [BindId] -> HashMap BindId a -> HashMap BindId a
updateBindInfoKeys :: HashMap BindId [BindId] -> HashMap BindId a -> HashMap BindId a
updateBindInfoKeys HashMap BindId [BindId]
oldToNew HashMap BindId a
infoMap =
[(BindId, a)] -> HashMap BindId a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
[ (BindId
n, a
a)
| (BindId
bId, a
a) <- HashMap BindId a -> [(BindId, a)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap BindId a
infoMap
, Just [BindId]
news <- [BindId -> HashMap BindId [BindId] -> Maybe [BindId]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup BindId
bId HashMap BindId [BindId]
oldToNew]
, BindId
n <- BindId
bId BindId -> [BindId] -> [BindId]
forall a. a -> [a] -> [a]
: [BindId]
news
]
simplifyConstraints
:: BindEnv
-> HashMap SubcId (SubC a)
-> (BindEnv, HashMap SubcId (SubC a), HashMap BindId [BindId])
simplifyConstraints :: BindEnv
-> HashMap SubcId (SubC a)
-> (BindEnv, HashMap SubcId (SubC a), HashMap BindId [BindId])
simplifyConstraints BindEnv
be HashMap SubcId (SubC a)
cs =
let (BindEnv
be', [(SubcId, SubC a)]
cs', [(BindId, [BindId])]
newToOld) =
((BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])]))
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
-> HashMap SubcId (SubC a)
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
HashMap.foldlWithKey' (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
forall a.
(BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
simplifyConstraintBindings (BindEnv
be, [], []) HashMap SubcId (SubC a)
cs
oldToNew :: HashMap BindId [BindId]
oldToNew =
([BindId] -> [BindId] -> [BindId])
-> [(BindId, [BindId])] -> HashMap BindId [BindId]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith [BindId] -> [BindId] -> [BindId]
forall a. [a] -> [a] -> [a]
(++) ([(BindId, [BindId])] -> HashMap BindId [BindId])
-> [(BindId, [BindId])] -> HashMap BindId [BindId]
forall a b. (a -> b) -> a -> b
$
((BindId, [BindId]) -> [(BindId, [BindId])])
-> [(BindId, [BindId])] -> [(BindId, [BindId])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(BindId
n, [BindId]
olds) -> (BindId -> (BindId, [BindId])) -> [BindId] -> [(BindId, [BindId])]
forall a b. (a -> b) -> [a] -> [b]
map (\BindId
o -> (BindId
o, [BindId
n])) [BindId]
olds) [(BindId, [BindId])]
newToOld
in
(BindEnv
be', [(SubcId, SubC a)] -> HashMap SubcId (SubC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [(SubcId, SubC a)]
cs', HashMap BindId [BindId]
oldToNew)
simplifyConstraintBindings
:: (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
simplifyConstraintBindings :: (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv, [(SubcId, SubC a)], [(BindId, [BindId])])
simplifyConstraintBindings (BindEnv
bindEnv, [(SubcId, SubC a)]
cs, [(BindId, [BindId])]
newToOld) SubcId
cid SubC a
c =
let env :: [(Symbol, ([BindId], SortedReft))]
env =
[ (Symbol
s, ([BindId
bId], SortedReft
sr))
| BindId
bId <- IBindEnv -> [BindId]
elemsIBindEnv (IBindEnv -> [BindId]) -> IBindEnv -> [BindId]
forall a b. (a -> b) -> a -> b
$ SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c
, let (Symbol
s, SortedReft
sr) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
bId BindEnv
bindEnv
]
mergedEnv :: HashMap Symbol ([BindId], SortedReft)
mergedEnv = [(Symbol, ([BindId], SortedReft))]
-> HashMap Symbol ([BindId], SortedReft)
forall m.
Semigroup m =>
[(Symbol, (m, SortedReft))] -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings [(Symbol, ([BindId], SortedReft))]
env
undoANFEnv :: HashMap Symbol ([BindId], SortedReft)
undoANFEnv =
if Config -> Bool
inlineANFBindings Config
cfg then HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANF HashMap Symbol ([BindId], SortedReft)
mergedEnv else HashMap Symbol ([BindId], SortedReft)
forall k v. HashMap k v
HashMap.empty
boolSimplEnv :: HashMap Symbol ([BindId], SortedReft)
boolSimplEnv =
HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts (HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft))
-> HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall a b. (a -> b) -> a -> b
$ HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap Symbol ([BindId], SortedReft)
undoANFEnv HashMap Symbol ([BindId], SortedReft)
mergedEnv
modifiedBinds :: [(Symbol, ([BindId], SortedReft))]
modifiedBinds = HashMap Symbol ([BindId], SortedReft)
-> [(Symbol, ([BindId], SortedReft))]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList (HashMap Symbol ([BindId], SortedReft)
-> [(Symbol, ([BindId], SortedReft))])
-> HashMap Symbol ([BindId], SortedReft)
-> [(Symbol, ([BindId], SortedReft))]
forall a b. (a -> b) -> a -> b
$ HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap Symbol ([BindId], SortedReft)
boolSimplEnv HashMap Symbol ([BindId], SortedReft)
undoANFEnv
modifiedBindIds :: [[BindId]]
modifiedBindIds = ((Symbol, ([BindId], SortedReft)) -> [BindId])
-> [(Symbol, ([BindId], SortedReft))] -> [[BindId]]
forall a b. (a -> b) -> [a] -> [b]
map (([BindId], SortedReft) -> [BindId]
forall a b. (a, b) -> a
fst (([BindId], SortedReft) -> [BindId])
-> ((Symbol, ([BindId], SortedReft)) -> ([BindId], SortedReft))
-> (Symbol, ([BindId], SortedReft))
-> [BindId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, ([BindId], SortedReft)) -> ([BindId], SortedReft)
forall a b. (a, b) -> b
snd) [(Symbol, ([BindId], SortedReft))]
modifiedBinds
unchangedBindIds :: IBindEnv
unchangedBindIds = SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c IBindEnv -> IBindEnv -> IBindEnv
`diffIBindEnv` [BindId] -> IBindEnv
fromListIBindEnv ([[BindId]] -> [BindId]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[BindId]]
modifiedBindIds)
([BindId]
newBindIds, BindEnv
bindEnv') = ([BindId], BindEnv)
-> [(Symbol, ([BindId], SortedReft))] -> ([BindId], BindEnv)
forall a.
([BindId], BindEnv)
-> [(Symbol, (a, SortedReft))] -> ([BindId], BindEnv)
insertBinds ([], BindEnv
bindEnv) [(Symbol, ([BindId], SortedReft))]
modifiedBinds
newIBindEnv :: IBindEnv
newIBindEnv = [BindId] -> IBindEnv -> IBindEnv
insertsIBindEnv [BindId]
newBindIds IBindEnv
unchangedBindIds
newToOld' :: [(BindId, [BindId])]
newToOld' = [BindId] -> [[BindId]] -> [(BindId, [BindId])]
forall a b. [a] -> [b] -> [(a, b)]
zip [BindId]
newBindIds [[BindId]]
modifiedBindIds [(BindId, [BindId])]
-> [(BindId, [BindId])] -> [(BindId, [BindId])]
forall a. [a] -> [a] -> [a]
++ [(BindId, [BindId])]
newToOld
in
(BindEnv
bindEnv', (SubcId
cid, SubC a -> (IBindEnv -> IBindEnv) -> SubC a
forall (c :: * -> *) a.
TaggedC c a =>
c a -> (IBindEnv -> IBindEnv) -> c a
updateSEnv SubC a
c (IBindEnv -> IBindEnv -> IBindEnv
forall a b. a -> b -> a
const IBindEnv
newIBindEnv)) (SubcId, SubC a) -> [(SubcId, SubC a)] -> [(SubcId, SubC a)]
forall a. a -> [a] -> [a]
: [(SubcId, SubC a)]
cs, [(BindId, [BindId])]
newToOld')
insertBinds :: ([BindId], BindEnv)
-> [(Symbol, (a, SortedReft))] -> ([BindId], BindEnv)
insertBinds = (([BindId], BindEnv)
-> (Symbol, (a, SortedReft)) -> ([BindId], BindEnv))
-> ([BindId], BindEnv)
-> [(Symbol, (a, SortedReft))]
-> ([BindId], BindEnv)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((([BindId], BindEnv)
-> (Symbol, (a, SortedReft)) -> ([BindId], BindEnv))
-> ([BindId], BindEnv)
-> [(Symbol, (a, SortedReft))]
-> ([BindId], BindEnv))
-> (([BindId], BindEnv)
-> (Symbol, (a, SortedReft)) -> ([BindId], BindEnv))
-> ([BindId], BindEnv)
-> [(Symbol, (a, SortedReft))]
-> ([BindId], BindEnv)
forall a b. (a -> b) -> a -> b
$ \([BindId]
xs, BindEnv
be) (Symbol
s, (a
_, SortedReft
sr)) ->
let (BindId
bId, BindEnv
be') = Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
insertBindEnv Symbol
s SortedReft
sr BindEnv
be
in (BindId
bId BindId -> [BindId] -> [BindId]
forall a. a -> [a] -> [a]
: [BindId]
xs, BindEnv
be')
mergeDuplicatedBindings
:: Semigroup m
=> [(Symbol, (m, SortedReft))]
-> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings :: [(Symbol, (m, SortedReft))] -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings [(Symbol, (m, SortedReft))]
xs =
((m, Maybe SortedReft) -> Maybe (m, SortedReft))
-> HashMap Symbol (m, Maybe SortedReft)
-> HashMap Symbol (m, SortedReft)
forall v1 v2 k. (v1 -> Maybe v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapMaybe (m, Maybe SortedReft) -> Maybe (m, SortedReft)
forall (f :: * -> *) a b. Functor f => (a, f b) -> f (a, b)
dropNothings (HashMap Symbol (m, Maybe SortedReft)
-> HashMap Symbol (m, SortedReft))
-> HashMap Symbol (m, Maybe SortedReft)
-> HashMap Symbol (m, SortedReft)
forall a b. (a -> b) -> a -> b
$
((m, Maybe SortedReft)
-> (m, Maybe SortedReft) -> (m, Maybe SortedReft))
-> [(Symbol, (m, Maybe SortedReft))]
-> HashMap Symbol (m, Maybe SortedReft)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith (m, Maybe SortedReft)
-> (m, Maybe SortedReft) -> (m, Maybe SortedReft)
forall a.
Semigroup a =>
(a, Maybe SortedReft)
-> (a, Maybe SortedReft) -> (a, Maybe SortedReft)
mergeSortedReft ([(Symbol, (m, Maybe SortedReft))]
-> HashMap Symbol (m, Maybe SortedReft))
-> [(Symbol, (m, Maybe SortedReft))]
-> HashMap Symbol (m, Maybe SortedReft)
forall a b. (a -> b) -> a -> b
$
((Symbol, (m, SortedReft)) -> (Symbol, (m, Maybe SortedReft)))
-> [(Symbol, (m, SortedReft))] -> [(Symbol, (m, Maybe SortedReft))]
forall a b. (a -> b) -> [a] -> [b]
map (((m, SortedReft) -> (m, Maybe SortedReft))
-> (Symbol, (m, SortedReft)) -> (Symbol, (m, Maybe SortedReft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SortedReft -> Maybe SortedReft)
-> (m, SortedReft) -> (m, Maybe SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SortedReft -> Maybe SortedReft
forall a. a -> Maybe a
Just)) [(Symbol, (m, SortedReft))]
xs
where
dropNothings :: (a, f b) -> f (a, b)
dropNothings (a
m, f b
msr) = (,) a
m (b -> (a, b)) -> f b -> f (a, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
msr
mergeSortedReft :: (a, Maybe SortedReft)
-> (a, Maybe SortedReft) -> (a, Maybe SortedReft)
mergeSortedReft (a
bs0, Maybe SortedReft
msr0) (a
bs1, Maybe SortedReft
msr1) =
let msr :: Maybe SortedReft
msr = do
SortedReft
sr0 <- Maybe SortedReft
msr0
SortedReft
sr1 <- Maybe SortedReft
msr1
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SortedReft -> Sort
sr_sort SortedReft
sr0 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== SortedReft -> Sort
sr_sort SortedReft
sr1)
SortedReft -> Maybe SortedReft
forall a. a -> Maybe a
Just SortedReft
sr0 { sr_reft :: Reft
sr_reft = Reft -> Reft -> Reft
mergeRefts (SortedReft -> Reft
sr_reft SortedReft
sr0) (SortedReft -> Reft
sr_reft SortedReft
sr1) }
in
(a
bs0 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
bs1, Maybe SortedReft
msr)
mergeRefts :: Reft -> Reft -> Reft
mergeRefts Reft
r0 Reft
r1 =
Symbol -> Expr -> Reft
reft
(Reft -> Symbol
reftBind Reft
r0)
(ListNE Expr -> Expr
pAnd
[ Reft -> Expr
reftPred Reft
r0
, Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 (Reft -> Expr
reftPred Reft
r1) (Reft -> Symbol
reftBind Reft
r1, Symbol -> Expr
forall a. Expression a => a -> Expr
expr (Reft -> Symbol
reftBind Reft
r0))
]
)
undoANF :: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANF :: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANF HashMap Symbol (m, SortedReft)
env =
let env' :: HashMap Symbol ((m, Bool), SortedReft)
env' = ((m, SortedReft) -> ((m, Bool), SortedReft))
-> HashMap Symbol (m, SortedReft)
-> HashMap Symbol ((m, Bool), SortedReft)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (HashMap Symbol ((m, Bool), SortedReft)
-> (m, SortedReft) -> ((m, Bool), SortedReft)
forall a m.
HashMap Symbol (a, SortedReft)
-> (m, SortedReft) -> ((m, Bool), SortedReft)
inlineInSortedReftChanged HashMap Symbol ((m, Bool), SortedReft)
env') HashMap Symbol (m, SortedReft)
env
in (((m, Bool), SortedReft) -> Maybe (m, SortedReft))
-> HashMap Symbol ((m, Bool), SortedReft)
-> HashMap Symbol (m, SortedReft)
forall v1 v2 k. (v1 -> Maybe v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapMaybe ((m, Bool), SortedReft) -> Maybe (m, SortedReft)
forall a b. ((a, Bool), b) -> Maybe (a, b)
dropUnchanged HashMap Symbol ((m, Bool), SortedReft)
env'
where
dropUnchanged :: ((a, Bool), b) -> Maybe (a, b)
dropUnchanged ((a
m, Bool
b), b
sr) = do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
b
(a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
m, b
sr)
inlineInSortedReft
:: HashMap Symbol (m, SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft :: HashMap Symbol (m, SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft HashMap Symbol (m, SortedReft)
env SortedReft
sr =
((Any, Bool), SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd (((Any, Bool), SortedReft) -> SortedReft)
-> ((Any, Bool), SortedReft) -> SortedReft
forall a b. (a -> b) -> a -> b
$ HashMap Symbol (m, SortedReft)
-> (Any, SortedReft) -> ((Any, Bool), SortedReft)
forall a m.
HashMap Symbol (a, SortedReft)
-> (m, SortedReft) -> ((m, Bool), SortedReft)
inlineInSortedReftChanged HashMap Symbol (m, SortedReft)
env ([Char] -> Any
forall a. HasCallStack => [Char] -> a
error [Char]
"never should evaluate", SortedReft
sr)
inlineInSortedReftChanged
:: HashMap Symbol (a, SortedReft)
-> (m, SortedReft)
-> ((m, Bool), SortedReft)
inlineInSortedReftChanged :: HashMap Symbol (a, SortedReft)
-> (m, SortedReft) -> ((m, Bool), SortedReft)
inlineInSortedReftChanged HashMap Symbol (a, SortedReft)
env (m
m, SortedReft
sr) =
let e :: Expr
e = Reft -> Expr
reftPred (SortedReft -> Reft
sr_reft SortedReft
sr)
e' :: Expr
e' = HashMap Symbol (a, SortedReft) -> Expr -> Expr
forall m. HashMap Symbol (m, SortedReft) -> Expr -> Expr
inlineInExpr HashMap Symbol (a, SortedReft)
env Expr
e
in ((m
m, Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e'), SortedReft
sr { sr_reft :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft (Expr -> Expr -> Expr
forall a b. a -> b -> a
const Expr
e') (SortedReft -> Reft
sr_reft SortedReft
sr) })
inlineInExpr :: HashMap Symbol (m, SortedReft) -> Expr -> Expr
inlineInExpr :: HashMap Symbol (m, SortedReft) -> Expr -> Expr
inlineInExpr HashMap Symbol (m, SortedReft)
env = Expr -> Expr
forall a. Fixpoint a => a -> a
simplify (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
inlineExpr
where
inlineExpr :: Expr -> Expr
inlineExpr (EVar Symbol
sym)
| Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
sym
, Just (m
_, SortedReft
sr) <- Symbol -> HashMap Symbol (m, SortedReft) -> Maybe (m, SortedReft)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup Symbol
sym HashMap Symbol (m, SortedReft)
env
, let r :: Reft
r = SortedReft -> Reft
sr_reft SortedReft
sr
, Just Expr
e <- Symbol -> Expr -> Maybe Expr
isSingletonE (Reft -> Symbol
reftBind Reft
r) (Reft -> Expr
reftPred Reft
r)
= Brel -> Sort -> Expr -> Expr
wrapWithCoercion Brel
Eq (SortedReft -> Sort
sr_sort SortedReft
sr) Expr
e
inlineExpr (PAtom Brel
br Expr
e0 e1 :: Expr
e1@(Expr -> Expr
dropECst -> EVar Symbol
sym))
| Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
sym
, Brel -> Bool
isEq Brel
br
, Just (m
_, SortedReft
sr) <- Symbol -> HashMap Symbol (m, SortedReft) -> Maybe (m, SortedReft)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup Symbol
sym HashMap Symbol (m, SortedReft)
env
, let r :: Reft
r = SortedReft -> Reft
sr_reft SortedReft
sr
, Just Expr
e <- Symbol -> Expr -> Maybe Expr
isSingletonE (Reft -> Symbol
reftBind Reft
r) (Reft -> Expr
reftPred Reft
r)
=
Brel -> Expr -> Expr -> Expr
PAtom Brel
br Expr
e0 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e1 (Symbol
sym, Brel -> Sort -> Expr -> Expr
wrapWithCoercion Brel
br (SortedReft -> Sort
sr_sort SortedReft
sr) Expr
e)
inlineExpr Expr
e = Expr
e
isSingletonE :: Symbol -> Expr -> Maybe Expr
isSingletonE Symbol
v (PAtom Brel
br Expr
e0 Expr
e1)
| Brel -> Bool
isEq Brel
br = Symbol -> Expr -> Expr -> Maybe Expr
isSingEq Symbol
v Expr
e0 Expr
e1 Maybe Expr -> Maybe Expr -> Maybe Expr
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol -> Expr -> Expr -> Maybe Expr
isSingEq Symbol
v Expr
e1 Expr
e0
isSingletonE Symbol
v (PIff Expr
e0 Expr
e1) =
Symbol -> Expr -> Expr -> Maybe Expr
isSingEq Symbol
v Expr
e0 Expr
e1 Maybe Expr -> Maybe Expr -> Maybe Expr
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol -> Expr -> Expr -> Maybe Expr
isSingEq Symbol
v Expr
e1 Expr
e0
isSingletonE Symbol
v (PAnd ListNE Expr
cs) =
[Maybe Expr] -> Maybe Expr
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe Expr] -> Maybe Expr) -> [Maybe Expr] -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Maybe Expr) -> ListNE Expr -> [Maybe Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Expr -> Maybe Expr
isSingletonE Symbol
v) ListNE Expr
cs
isSingletonE Symbol
_ Expr
_ =
Maybe Expr
forall a. Maybe a
Nothing
isSingEq :: Symbol -> Expr -> Expr -> Maybe Expr
isSingEq Symbol
v Expr
e0 Expr
e1 = do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
EVar Symbol
v Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Expr
dropECst Expr
e0 Bool -> Bool -> Bool
&& Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Symbol
v (HashSet Symbol -> Bool) -> HashSet Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> HashSet Symbol
exprSymbolsSet Expr
e1)
Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e1
isEq :: Brel -> Bool
isEq Brel
r = Brel
r Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
r Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ueq
wrapWithCoercion :: Brel -> Sort -> Expr -> Expr
wrapWithCoercion Brel
br Sort
to Expr
e = case Expr -> Maybe Sort
exprSort_maybe Expr
e of
Just Sort
from -> if Sort
from Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
/= Sort
to then Sort -> Sort -> Expr -> Expr
ECoerc Sort
from Sort
to Expr
e else Expr
e
Maybe Sort
Nothing -> if Brel
br Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ueq then Expr -> Sort -> Expr
ECst Expr
e Sort
to else Expr
e
dropECst :: Expr -> Expr
dropECst :: Expr -> Expr
dropECst = \case
ECst Expr
e Sort
_t -> Expr -> Expr
dropECst Expr
e
Expr
e -> Expr
e
simplifyBooleanRefts
:: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts :: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts = ((m, SortedReft) -> Maybe (m, SortedReft))
-> HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
forall v1 v2 k. (v1 -> Maybe v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapMaybe (m, SortedReft) -> Maybe (m, SortedReft)
forall a. (a, SortedReft) -> Maybe (a, SortedReft)
simplifyBooleanSortedReft
where
simplifyBooleanSortedReft :: (a, SortedReft) -> Maybe (a, SortedReft)
simplifyBooleanSortedReft (a
m, SortedReft
sr)
| SortedReft -> Sort
sr_sort SortedReft
sr Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort
, let r :: Reft
r = SortedReft -> Reft
sr_reft SortedReft
sr
, Just (Expr
e, ListNE Expr
rest) <- Symbol -> Expr -> Maybe (Expr, ListNE Expr)
symbolUsedAtTopLevelAnd (Reft -> Symbol
reftBind Reft
r) (Reft -> Expr
reftPred Reft
r)
= let e' :: Expr
e' = ListNE Expr -> Expr
pAnd (ListNE Expr -> Expr) -> ListNE Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e Expr -> ListNE Expr -> ListNE Expr
forall a. a -> [a] -> [a]
: (Expr -> Expr) -> ListNE Expr -> ListNE Expr
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Reft -> Symbol
reftBind Reft
r, Expr -> Expr
atomToBool Expr
e)) ListNE Expr
rest
atomToBool :: Expr -> Expr
atomToBool Expr
a = if Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
EVar (Reft -> Symbol
reftBind Reft
r) then Expr
PTrue else Expr
PFalse
in (a, SortedReft) -> Maybe (a, SortedReft)
forall a. a -> Maybe a
Just (a
m, SortedReft
sr { sr_reft :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft (Expr -> Expr -> Expr
forall a b. a -> b -> a
const Expr
e') Reft
r })
simplifyBooleanSortedReft (a, SortedReft)
_ = Maybe (a, SortedReft)
forall a. Maybe a
Nothing
symbolUsedAtTopLevelAnd :: Symbol -> Expr -> Maybe (Expr, ListNE Expr)
symbolUsedAtTopLevelAnd Symbol
s (PAnd ListNE Expr
ps) =
Expr -> ListNE Expr -> Maybe (Expr, ListNE Expr)
forall a. Eq a => a -> [a] -> Maybe (a, [a])
findExpr (Symbol -> Expr
EVar Symbol
s) ListNE Expr
ps Maybe (Expr, ListNE Expr)
-> Maybe (Expr, ListNE Expr) -> Maybe (Expr, ListNE Expr)
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Expr -> ListNE Expr -> Maybe (Expr, ListNE Expr)
forall a. Eq a => a -> [a] -> Maybe (a, [a])
findExpr (Expr -> Expr
PNot (Symbol -> Expr
EVar Symbol
s)) ListNE Expr
ps
symbolUsedAtTopLevelAnd Symbol
_ Expr
_ = Maybe (Expr, ListNE Expr)
forall a. Maybe a
Nothing
findExpr :: a -> [a] -> Maybe (a, [a])
findExpr a
e [a]
es = do
case (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a
e a -> a -> Bool
forall a. Eq a => a -> a -> Bool
==) [a]
es of
([], [a]
_) -> Maybe (a, [a])
forall a. Maybe a
Nothing
(a
e:[a]
_, [a]
rest) -> (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
e, [a]
rest)
dropLikelyIrrelevantBindings
:: HashSet Symbol
-> HashMap Symbol SortedReft
-> HashMap Symbol SortedReft
dropLikelyIrrelevantBindings :: HashSet Symbol
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
dropLikelyIrrelevantBindings HashSet Symbol
ss HashMap Symbol SortedReft
env = (Symbol -> SortedReft -> Bool)
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey Symbol -> SortedReft -> Bool
forall p. Symbol -> p -> Bool
relevant HashMap Symbol SortedReft
env
where
relatedSyms :: HashSet Symbol
relatedSyms = HashSet Symbol -> HashMap Symbol SortedReft -> HashSet Symbol
relatedSymbols HashSet Symbol
ss HashMap Symbol SortedReft
env
relevant :: Symbol -> p -> Bool
relevant Symbol
s p
_sr =
(Bool -> Bool
not (Symbol -> Bool
capitalizedSym Symbol
s) Bool -> Bool -> Bool
|| Symbol -> Symbol
prefixOfSym Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
s) Bool -> Bool -> Bool
&& Symbol
s Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet Symbol
relatedSyms
capitalizedSym :: Symbol -> Bool
capitalizedSym = (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isUpper (Text -> Bool) -> (Symbol -> Text) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindId -> Text -> Text
Text.take BindId
1 (Text -> Text) -> (Symbol -> Text) -> Symbol -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText
relatedSymbols :: HashSet Symbol -> HashMap Symbol SortedReft -> HashSet Symbol
relatedSymbols :: HashSet Symbol -> HashMap Symbol SortedReft -> HashSet Symbol
relatedSymbols HashSet Symbol
ss0 HashMap Symbol SortedReft
env = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
forall a. HashSet a
HashSet.empty HashSet Symbol
ss0
where
directlyUses :: HashMap Symbol (HashSet Symbol)
directlyUses = (SortedReft -> HashSet Symbol)
-> HashMap Symbol SortedReft -> HashMap Symbol (HashSet Symbol)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Expr -> HashSet Symbol
exprSymbolsSet (Expr -> HashSet Symbol)
-> (SortedReft -> Expr) -> SortedReft -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred (Reft -> Expr) -> (SortedReft -> Reft) -> SortedReft -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft) HashMap Symbol SortedReft
env
usedBy :: HashMap Symbol (HashSet Symbol)
usedBy = (HashSet Symbol -> HashSet Symbol -> HashSet Symbol)
-> [(Symbol, HashSet Symbol)] -> HashMap Symbol (HashSet Symbol)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union
[ (Symbol
x, Symbol -> HashSet Symbol
forall a. Hashable a => a -> HashSet a
HashSet.singleton Symbol
s)
| (Symbol
s, HashSet Symbol
xs) <- HashMap Symbol (HashSet Symbol) -> [(Symbol, HashSet Symbol)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol (HashSet Symbol)
directlyUses
, Symbol
x <- HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
HashSet.toList HashSet Symbol
xs
]
go :: HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go :: HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
acc HashSet Symbol
ss = case HashSet Symbol -> Maybe (Symbol, HashSet Symbol)
forall a. (Hashable a, Eq a) => HashSet a -> Maybe (a, HashSet a)
unconsHashSet HashSet Symbol
ss of
Maybe (Symbol, HashSet Symbol)
Nothing -> HashSet Symbol
acc
Just (Symbol
x, HashSet Symbol
xs) ->
if Symbol
x Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet Symbol
acc then HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
acc HashSet Symbol
xs
else
let usersOfX :: HashSet Symbol
usersOfX = HashMap Symbol (HashSet Symbol)
usedBy HashMap Symbol (HashSet Symbol) -> Symbol -> HashSet Symbol
forall k a.
(Hashable k, Eq k) =>
HashMap k (HashSet a) -> k -> HashSet a
`setOf` Symbol
x
relatedToX :: HashSet Symbol
relatedToX = [HashSet Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
HashSet.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$
HashSet Symbol
usersOfX HashSet Symbol -> [HashSet Symbol] -> [HashSet Symbol]
forall a. a -> [a] -> [a]
: (Symbol -> HashSet Symbol) -> [Symbol] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (HashMap Symbol (HashSet Symbol)
directlyUses HashMap Symbol (HashSet Symbol) -> Symbol -> HashSet Symbol
forall k a.
(Hashable k, Eq k) =>
HashMap k (HashSet a) -> k -> HashSet a
`setOf`) (Symbol
x Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
HashSet.toList HashSet Symbol
usersOfX)
in HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go (Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Symbol
x HashSet Symbol
acc) (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
relatedToX HashSet Symbol
xs)