{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TupleSections #-}

-- | Functions to make environments smaller
module Language.Fixpoint.Solver.EnvironmentReduction
  ( reduceEnvironments
  , simplifyBindings
  , dropLikelyIrrelevantBindings
  , relatedSymbols
  , inlineInExpr
  , inlineInSortedReft
  , mergeDuplicatedBindings
  , simplifyBooleanRefts
  , undoANF
  , undoANFAndVV

  -- for use in tests
  , undoANFSimplifyingWith
  ) 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
#if MIN_VERSION_base(4,20,0)
import           Data.List (nub, partition)
#else
import           Data.List (foldl', nub, partition)
#endif
import           Data.Maybe (fromMaybe)
import           Data.ShareMap (ShareMap)
import qualified Data.ShareMap as ShareMap
import qualified Data.Text as Text
import           Language.Fixpoint.SortCheck (exprSortMaybe)
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
  , vvName
  )
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Refinements
  ( Brel(..)
  , ExprV(..)
  , Expr
  , KVar(..)
  , SortedReft(..)
  , Subst
  , SubstV(..)
  , pattern PTrue
  , pattern PFalse
  , dropECst
  , expr
  , exprKVars
  , exprSymbolsSet
  , mapPredReft
  , pAnd
  , reft
  , reftBind
  , reftPred
  , sortedReftSymbols
  , subst1
  )
import           Language.Fixpoint.Types.Sorts (boolSort, sortSymbols)
import           Language.Fixpoint.Types.Visitor (mapExprOnExpr)
import           Lens.Family2 (Lens', view, (%~))
import           Lens.Family2.Stock (_2)
import Language.Fixpoint.Misc (snd3)

-- | Strips from all the constraint environments the bindings that are
-- irrelevant for their respective constraints.
--
-- Environment reduction has the following stages.
--
-- Stage 1)
-- Compute the binding dependencies of each constraint ignoring KVars.
--
-- A binding is a dependency of a constraint if it is mentioned in the lhs, or
-- the rhs of the constraint, or in a binding that is a dependency, or in a
-- @define@ or @match@ clause that is mentioned in the lhs or rhs or another
-- binding dependency, or if it appears in the environment of the constraint and
-- can't be discarded as trivial (see 'dropIrrelevantBindings').
--
-- Stage 2)
-- Compute the binding dependencies of KVars.
--
-- A binding is a dependency of a KVar K1 if it is a dependency of a constraint
-- in which the K1 appears, or if it is a dependency of another KVar appearing
-- in a constraint in which K1 appears.
--
-- Stage 3)
-- Drop from the environment of each constraint the bindings that aren't
-- dependencies of the constraint, or that aren't dependencies of any KVar
-- appearing in the constraint.
--
--
-- Note on SInfo:
--
-- This function can be changed to work on 'SInfo' rather than 'FInfo'. However,
-- this causes some tests to fail. At least:
--
--    liquid-fixpoint/tests/proof/rewrite.fq
--    tests/import/client/ReflectClient4a.hs
--
-- lhs bindings are numbered with the highest numbers when FInfo
-- is converted to SInfo. Environment reduction, however, rehashes
-- the binding identifiers and lhss could end up with a lower numbering.
-- For most of the tests, this doesn't seem to make a difference, but it
-- causes the two tests referred above to fail.
--
-- See #473 for more discussion.
--
reduceEnvironments :: FInfo a -> FInfo a
reduceEnvironments :: forall a. FInfo a -> FInfo a
reduceEnvironments FInfo a
finfo =
  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
finfo
      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
finfo)
      reducedEnvs :: [ReducedConstraint a]
reducedEnvs = ((SubcId, SubC a) -> ReducedConstraint a)
-> [(SubcId, SubC a)] -> [ReducedConstraint a]
forall a b. (a -> b) -> [a] -> [b]
map (BindEnv a
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
forall a.
BindEnv a
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
reduceConstraintEnvironment (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
finfo) HashMap Symbol (HashSet Symbol)
aenvMap) [(SubcId, SubC a)]
constraints
      ([(SubcId, SubC a)]
cm', HashMap KVar (WfC a)
ws') = BindEnv a
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
forall a.
BindEnv a
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
finfo) ([ReducedConstraint a]
reducedEnvs, FInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
finfo)
      bs' :: BindEnv a
bs' = (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
finfo) { beBinds = dropBindsMissingFrom (beBinds $ bs finfo) cm' ws' }

   in FInfo a
finfo
     { bs = bs'
     , cm = HashMap.fromList cm'
     , ws = ws'
     , ebinds = updateEbinds bs' (ebinds finfo)
     , bindInfo = updateBindInfoKeys bs' $ bindInfo finfo
     }

  where
    dropBindsMissingFrom
      :: HashMap BindId (Symbol, SortedReft, a)
      -> [(SubcId, SubC a)]
      -> HashMap KVar (WfC a)
      -> HashMap BindId (Symbol, SortedReft, a)
    dropBindsMissingFrom :: forall a.
HashMap BindId (Symbol, SortedReft, a)
-> [(SubcId, SubC a)]
-> HashMap KVar (WfC a)
-> HashMap BindId (Symbol, SortedReft, a)
dropBindsMissingFrom HashMap BindId (Symbol, SortedReft, a)
be [(SubcId, SubC a)]
cs HashMap KVar (WfC a)
wmap =
      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)
wmap)
       in
          (BindId -> (Symbol, SortedReft, a) -> Bool)
-> HashMap BindId (Symbol, SortedReft, a)
-> HashMap BindId (Symbol, SortedReft, a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey (\BindId
bId (Symbol, SortedReft, a)
_ -> BindId -> IBindEnv -> Bool
memberIBindEnv BindId
bId IBindEnv
ibindEnv) HashMap BindId (Symbol, SortedReft, a)
be

    -- Updates BindIds in an ebinds list
    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)

    -- Updates BindId keys in a bindInfos map
    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 => 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)

-- | Reduces the environments of WF constraints.
--
-- @reduceWFConstraintEnvironments bindEnv (cs, ws)@
--  * enlarges the environments in cs with bindings needed by the kvars they use
--  * replaces the environment in ws with reduced environments
--
-- Reduction of wf environments gets rid of any bindings not mentioned by
-- 'relatedKVarBinds' or any substitution on the corresponding KVar anywhere.
--
reduceWFConstraintEnvironments
  :: BindEnv a    -- ^ Environment before reduction
  -> ([ReducedConstraint a], HashMap KVar (WfC a))
     -- ^ @(cs, ws)@:
     --  * @cs@ are the constraints with reduced environments
     --  * @ws@ are the wf constraints in which to reduce environments
  -> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments :: forall a.
BindEnv a
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments BindEnv a
bindEnv ([ReducedConstraint a]
cs, HashMap KVar (WfC a)
wfs) =
  let
      (HashMap KVar (HashSet Symbol)
kvarsBinds, HashMap KVar (HashSet Symbol)
kvarSubstSymbols, [[KVar]]
kvarsBySubC) = BindEnv a
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol),
    [[KVar]])
forall a.
BindEnv a
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol),
    [[KVar]])
relatedKVarBinds BindEnv a
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 =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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 =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union HashMap KVar (HashSet Symbol)
wfBindsPlusSortSymbols 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
          (HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
forall a. HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
reduceWFConstraintEnvironment 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 a -> IBindEnv -> HashSet Symbol
forall a. BindEnv a -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv a
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 =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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
              (HashMap KVar (HashSet Symbol)
-> [KVar] -> ReducedConstraint a -> (SubcId, SubC a)
forall a.
HashMap KVar (HashSet Symbol)
-> [KVar] -> ReducedConstraint a -> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds HashMap KVar (HashSet Symbol)
kvarsWsBinds)
              [[KVar]]
kvarsBySubC
              [ReducedConstraint a]
cs
   in
      ([(SubcId, SubC a)]
cs', HashMap KVar (WfC a)
ws')

  where
    -- Initially, the constraint environment only includes the information
    -- relevant to the rhs and the lhs. If a kvar is present, it may need
    -- additional bindings that are required by the kvar. These are added
    -- in this function.
    updateSubcEnvsWithKVarBinds
      :: HashMap KVar (HashSet Symbol)
      -> [KVar]
      -> ReducedConstraint a
      -> (SubcId, SubC a)
    updateSubcEnvsWithKVarBinds :: forall a.
HashMap KVar (HashSet Symbol)
-> [KVar] -> ReducedConstraint a -> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds 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 a. [a] -> 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, a
_) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
bindEnv
              , (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
kvar =
            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
kvar 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 be kbinds k c@ drops bindings from @c@
    -- that aren't present in @kbinds ! k@.
    reduceWFConstraintEnvironment
      :: HashMap KVar (HashSet Symbol)
      -> KVar
      -> WfC a
      -> WfC a
    reduceWFConstraintEnvironment :: forall a. HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
reduceWFConstraintEnvironment 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 = emptyIBindEnv }
        Just HashSet Symbol
kbindSymbols ->
          WfC a
c { wenv = filterIBindEnv (relevantBindIds kbindSymbols) (wenv c) }
      where
        relevantBindIds :: HashSet Symbol -> BindId -> Bool
        relevantBindIds :: HashSet Symbol -> BindId -> Bool
relevantBindIds HashSet Symbol
kbindSymbols BindId
bId =
          let (Symbol
s, SortedReft
_, a
_) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
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
  { forall a. ReducedConstraint a -> IBindEnv
reducedEnv :: IBindEnv       -- ^ Environment which has been reduced
  , forall a. ReducedConstraint a -> SubC a
originalConstraint :: SubC a -- ^ The original constraint
  , forall a. ReducedConstraint a -> SubcId
constraintId :: SubcId       -- ^ Id of the constraint
  }

reduceConstraintEnvironment
  :: BindEnv a
  -> HashMap Symbol (HashSet Symbol)
  -> (SubcId, SubC a)
  -> ReducedConstraint a
reduceConstraintEnvironment :: forall a.
BindEnv a
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
reduceConstraintEnvironment BindEnv a
bindEnv HashMap Symbol (HashSet Symbol)
aenvMap (SubcId
cid, SubC a
c) =
  let env :: [(Symbol, BindId, SortedReft, a)]
env = [ (Symbol
s, BindId
bId, SortedReft
sr, a
a)
            | 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, a
a) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
bindEnv
            ]
      prunedEnv :: IBindEnv
prunedEnv =
        [BindId] -> IBindEnv
fromListIBindEnv
        [ BindId
bId | (Symbol
_, BindId
bId, SortedReft
_,a
_) <- HashMap Symbol (HashSet Symbol)
-> HashSet Symbol
-> [(Symbol, BindId, SortedReft, a)]
-> [(Symbol, BindId, SortedReft, a)]
forall a.
HashMap Symbol (HashSet Symbol)
-> HashSet Symbol
-> [(Symbol, BindId, SortedReft, a)]
-> [(Symbol, BindId, SortedReft, a)]
dropIrrelevantBindings HashMap Symbol (HashSet Symbol)
aenvMap HashSet Symbol
constraintSymbols [(Symbol, BindId, SortedReft, a)]
env ]
      constraintSymbols :: HashSet Symbol
constraintSymbols =
        HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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
        { reducedEnv :: IBindEnv
reducedEnv = IBindEnv
prunedEnv
        , originalConstraint :: SubC a
originalConstraint = SubC a
c
        , constraintId :: SubcId
constraintId = SubcId
cid
        }

-- | @dropIrrelevantBindings aenvMap ss env@ drops bindings from @env@ which
-- aren't referenced neither in a refinement type in the environment nor in
-- @ss@, and not reachable in definitions of @aenv@ referred from @env@ or
-- @ss@, and which can't possibly affect the outcome of verification.
--
-- Right now, it drops bindings of the form @a : {v | true }@ and
-- @b : {v | v [>=|<=|=|!=|etc] e }@
-- whenever @a@ and @b@ aren't referenced from any formulas.
--
dropIrrelevantBindings
  :: HashMap Symbol (HashSet Symbol)
  -> HashSet Symbol
  -> [(Symbol, BindId, SortedReft, a)]
  -> [(Symbol, BindId, SortedReft, a)]
dropIrrelevantBindings :: forall a.
HashMap Symbol (HashSet Symbol)
-> HashSet Symbol
-> [(Symbol, BindId, SortedReft, a)]
-> [(Symbol, BindId, SortedReft, a)]
dropIrrelevantBindings HashMap Symbol (HashSet Symbol)
aenvMap HashSet Symbol
extraSymbols [(Symbol, BindId, SortedReft, a)]
env =
  ((Symbol, BindId, SortedReft, a) -> Bool)
-> [(Symbol, BindId, SortedReft, a)]
-> [(Symbol, BindId, SortedReft, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, BindId, SortedReft, a) -> Bool
forall {b} {d}. (Symbol, b, SortedReft, d) -> Bool
relevantBind [(Symbol, BindId, SortedReft, a)]
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 => 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 => [HashSet a] -> HashSet a
HashSet.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, BindId, SortedReft, a) -> HashSet Symbol)
-> [(Symbol, BindId, SortedReft, a)] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
_, BindId
_, SortedReft
sr,a
_) -> SortedReft -> HashSet Symbol
sortedReftSymbols SortedReft
sr) [(Symbol, BindId, SortedReft, a)]
env

    relevantBind :: (Symbol, b, SortedReft, d) -> Bool
relevantBind (Symbol
s, b
_, SortedReft
sr, d
_)
      | 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 ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred (SortedReft -> ReftV Symbol
sr_reft SortedReft
sr) of
          ExprV Symbol
PTrue -> Bool
False
          PAtom Brel
_ (ExprV Symbol -> ExprV Symbol
dropECst -> EVar Symbol
sym) ExprV Symbol
_e -> Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind (SortedReft -> ReftV Symbol
sr_reft SortedReft
sr)
          PAtom Brel
_ ExprV Symbol
_e (ExprV Symbol -> ExprV Symbol
dropECst -> EVar Symbol
sym) -> Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind (SortedReft -> ReftV Symbol
sr_reft SortedReft
sr)
          ExprV Symbol
_ -> Bool
True

-- | For each Equation and Rewrite, collects the symbols that it needs.
axiomEnvSymbols :: AxiomEnv -> HashMap Symbol (HashSet Symbol)
axiomEnvSymbols :: AxiomEnv -> HashMap Symbol (HashSet Symbol)
axiomEnvSymbols AxiomEnv
axiomEnv =
  HashMap Symbol (HashSet Symbol)
-> HashMap Symbol (HashSet Symbol)
-> HashMap Symbol (HashSet Symbol)
forall k v. Eq 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
axiomEnv)
    ([(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
axiomEnv)
  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
              (ExprV Symbol -> HashSet Symbol
exprSymbolsSet (Equation -> ExprV Symbol
forall v. EquationV v -> ExprV v
eqBody Equation
eq) HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`HashSet.union` Sort -> HashSet Symbol
sortSymbols (Equation -> Sort
forall v. EquationV v -> 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)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs Equation
eq)
          sortSyms :: HashSet Symbol
sortSyms = [HashSet Symbol] -> HashSet Symbol
forall a. Eq 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)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs Equation
eq
          allSymbols :: HashSet Symbol
allSymbols =
            if Equation -> Bool
forall v. EquationV v -> 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
forall v. EquationV v -> Symbol
eqName Equation
eq) (HashSet Symbol
bodySymbols HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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 => HashSet a -> HashSet a -> HashSet a
`HashSet.union` HashSet Symbol
sortSyms
       in
          (Equation -> Symbol
forall v. EquationV v -> 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
              (ExprV Symbol -> HashSet Symbol
exprSymbolsSet (Rewrite -> ExprV Symbol
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 :: forall a. (Hashable a, Eq a) => 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 :: forall k a.
(Hashable k, Eq k) =>
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 :: forall k a b.
(Hashable k, Eq k) =>
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 binds cs@ yields:
-- 1) the set of all bindings that might be needed by each KVar mentioned
-- in the constraints @cs@, and
-- 2) the set of symbols appearing in substitutions of the KVar in any
-- constraint. That is: @kv@ is associated with @i@, @j@, and @h@ if there
-- is some constraint with the KVar substitution @kv[i:=e0][j:=e1]@ and
-- some constraint with the KVar substitution @kv[h:=e2]@ appearing in
-- the rhs, lhs, or the environment.
-- 3) The list of kvars used in each constraint.
--
-- We assume that if a KVar is mentioned in a constraint or in its
-- environment, then all the bindings in the environment of the constraint
-- might be needed by the KVar.
--
-- Moreover, if two KVars are mentioned together in the same constraint,
-- then the bindings that might be needed for either of them might
-- be needed by the other.
--
relatedKVarBinds
  :: BindEnv a
  -> [ReducedConstraint a]
  -> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol), [[KVar]])
relatedKVarBinds :: forall a.
BindEnv a
-> [ReducedConstraint a]
-> (HashMap KVar (HashSet Symbol), HashMap KVar (HashSet Symbol),
    [[KVar]])
relatedKVarBinds BindEnv a
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 a -> IBindEnv -> HashSet Symbol
forall a. BindEnv a -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv a
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 b a. (b -> a -> b) -> b -> [a] -> b
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 =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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, a) -> HashMap KVar [Subst])
-> HashMap BindId (Symbol, SortedReft, a)
-> HashMap BindId (HashMap KVar [Subst])
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (ExprV Symbol -> HashMap KVar [Subst]
exprKVars (ExprV Symbol -> HashMap KVar [Subst])
-> ((Symbol, SortedReft, a) -> ExprV Symbol)
-> (Symbol, SortedReft, a)
-> HashMap KVar [Subst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> ExprV Symbol)
-> ((Symbol, SortedReft, a) -> ReftV Symbol)
-> (Symbol, SortedReft, a)
-> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> ReftV Symbol
sr_reft (SortedReft -> ReftV Symbol)
-> ((Symbol, SortedReft, a) -> SortedReft)
-> (Symbol, SortedReft, a)
-> ReftV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft, a) -> SortedReft
forall a b c. (a, b, c) -> b
snd3) (HashMap BindId (Symbol, SortedReft, a)
 -> HashMap BindId (HashMap KVar [Subst]))
-> HashMap BindId (Symbol, SortedReft, a)
-> HashMap BindId (HashMap KVar [Subst])
forall a b. (a -> b) -> a -> b
$ BindEnv a -> HashMap BindId (Symbol, SortedReft, a)
forall a. SizedEnv a -> BindMap a
beBinds BindEnv a
bindEnv

    -- Returns all of the KVars used in the constraint, together with
    -- the symbols that appear in substitutions of those KVars.
    kvarBindsFromSubC :: ReducedConstraint a -> HashMap KVar (HashSet Symbol)
    kvarBindsFromSubC :: forall a. 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 :: SubstV v -> HashMap Symbol (ExprV v)
unSubst (Su HashMap Symbol (ExprV v)
su) = HashMap Symbol (ExprV v)
su
          substsToHashSet :: [SubstV v] -> HashSet Symbol
substsToHashSet =
            HashMap Symbol () -> HashSet Symbol
forall a. HashMap a () -> HashSet a
HashSet.fromMap (HashMap Symbol () -> HashSet Symbol)
-> ([SubstV v] -> HashMap Symbol ())
-> [SubstV v]
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExprV v -> ()) -> HashMap Symbol (ExprV v) -> HashMap Symbol ()
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (() -> ExprV v -> ()
forall a b. a -> b -> a
const ()) (HashMap Symbol (ExprV v) -> HashMap Symbol ())
-> ([SubstV v] -> HashMap Symbol (ExprV v))
-> [SubstV v]
-> HashMap Symbol ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HashMap Symbol (ExprV v)] -> HashMap Symbol (ExprV v)
forall k v. Eq k => [HashMap k v] -> HashMap k v
HashMap.unions ([HashMap Symbol (ExprV v)] -> HashMap Symbol (ExprV v))
-> ([SubstV v] -> [HashMap Symbol (ExprV v)])
-> [SubstV v]
-> HashMap Symbol (ExprV v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubstV v -> HashMap Symbol (ExprV v))
-> [SubstV v] -> [HashMap Symbol (ExprV v)]
forall a b. (a -> b) -> [a] -> [b]
map SubstV v -> HashMap Symbol (ExprV v)
forall {v}. SubstV v -> HashMap Symbol (ExprV v)
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 b a. (b -> a -> b) -> b -> [a] -> b
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 =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq 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
forall {v}. [SubstV v] -> HashSet Symbol
substsToHashSet) ([HashMap KVar [Subst]] -> [HashMap KVar (HashSet Symbol)])
-> [HashMap KVar [Subst]] -> [HashMap KVar (HashSet Symbol)]
forall a b. (a -> b) -> a -> b
$
          (ExprV Symbol -> HashMap KVar [Subst]
exprKVars (ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> ExprV Symbol) -> ReftV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft (SortedReft -> ReftV Symbol) -> SortedReft -> ReftV Symbol
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
$
          (ExprV Symbol -> HashMap KVar [Subst]
exprKVars (ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> ExprV Symbol) -> ReftV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft (SortedReft -> ReftV Symbol) -> SortedReft -> ReftV Symbol
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 kvs@ is a map of KVars to all the bindings that
    -- they can potentially use.
    --
    -- @kvars@ tells for each environment what KVars it uses.
    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 b a. (b -> a -> b) -> b -> [a] -> b
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 sm bs (bindIds, kvars)@ merges the binds used by all KVars in
    -- @kvars@ and also adds to the result the bind Ids in @bindIds@.
    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 a b. (a -> b -> b) -> b -> [a] -> b
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 a -> IBindEnv -> HashSet Symbol
asSymbolSet :: forall a. BindEnv a -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv a
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
_,a
_) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
be
    ]

-- | @reachableSymbols x r@ computes the set of symbols reachable from @x@
-- in the graph represented by @r@. Includes @x@ in the result.
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 acc ss@ contains @acc@ and @ss@ plus any symbols reachable from @ss@
    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 => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
relatedToX HashSet Symbol
xs)

-- | Simplifies bindings in constraint environments.
--
-- It runs 'mergeDuplicatedBindings' and 'simplifyBooleanRefts'
-- on the environment of each constraint.
--
-- If 'inlineANFBindings cfg' is on, also runs 'undoANFAndVV' to inline
-- @lq_anf@ bindings.
simplifyBindings :: Config -> FInfo a -> FInfo a
simplifyBindings :: forall a. Config -> FInfo a -> FInfo a
simplifyBindings Config
cfg FInfo a
finfo =
  let (BindEnv a
bs', HashMap SubcId (SubC a)
cm', HashMap BindId [BindId]
oldToNew) = BindEnv a
-> HashMap SubcId (SubC a)
-> (BindEnv a, HashMap SubcId (SubC a), HashMap BindId [BindId])
forall a.
BindEnv a
-> HashMap SubcId (SubC a)
-> (BindEnv a, HashMap SubcId (SubC a), HashMap BindId [BindId])
simplifyConstraints (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
finfo) (FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
finfo)
   in FInfo a
finfo
        { bs = bs'
        , cm = cm'
        , ebinds = updateEbinds oldToNew (ebinds finfo)
        , bindInfo = updateBindInfoKeys oldToNew $ bindInfo finfo
        }
  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 :: forall a.
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 a
      -> HashMap SubcId (SubC a)
      -> (BindEnv a, HashMap SubcId (SubC a), HashMap BindId [BindId])
    simplifyConstraints :: forall a.
BindEnv a
-> HashMap SubcId (SubC a)
-> (BindEnv a, HashMap SubcId (SubC a), HashMap BindId [BindId])
simplifyConstraints BindEnv a
be HashMap SubcId (SubC a)
cs =
      let (BindEnv a
be', [(SubcId, SubC a)]
cs', [(BindId, [BindId])]
newToOld) =
             ((BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
 -> SubcId
 -> SubC a
 -> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])]))
-> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
-> HashMap SubcId (SubC a)
-> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
HashMap.foldlWithKey' (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
forall a.
(BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
simplifyConstraintBindings (BindEnv a
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
n]) [BindId]
olds) [(BindId, [BindId])]
newToOld
       in
          (BindEnv a
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 a, [(SubcId, SubC a)], [(BindId, [BindId])])
      -> SubcId
      -> SubC a
      -> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
    simplifyConstraintBindings :: forall a.
(BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
-> SubcId
-> SubC a
-> (BindEnv a, [(SubcId, SubC a)], [(BindId, [BindId])])
simplifyConstraintBindings (BindEnv a
bindEnv, [(SubcId, SubC a)]
cs, [(BindId, [BindId])]
newToOld) SubcId
cid SubC a
c =
      let env :: [(Symbol, ([(BindId, a)], SortedReft))]
env =
            [ (Symbol
s, ([(BindId
bId, a
a)], 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, a
a) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
bindEnv
            ]

          mergedEnv :: HashMap Symbol ([(BindId, a)], SortedReft)
mergedEnv = [(Symbol, ([(BindId, a)], SortedReft))]
-> HashMap Symbol ([(BindId, a)], SortedReft)
forall m.
Semigroup m =>
[(Symbol, (m, SortedReft))] -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings [(Symbol, ([(BindId, a)], SortedReft))]
env
          undoANFEnv :: HashMap Symbol ([(BindId, a)], SortedReft)
undoANFEnv =
            if Config -> Bool
inlineANFBindings Config
cfg then HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFOnlyModified HashMap Symbol ([(BindId, a)], SortedReft)
mergedEnv else HashMap Symbol ([(BindId, a)], SortedReft)
forall k v. HashMap k v
HashMap.empty
          boolSimplEnv :: HashMap Symbol ([(BindId, a)], SortedReft)
boolSimplEnv =
            HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts (HashMap Symbol ([(BindId, a)], SortedReft)
 -> HashMap Symbol ([(BindId, a)], SortedReft))
-> HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
forall a b. (a -> b) -> a -> b
$ HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap Symbol ([(BindId, a)], SortedReft)
undoANFEnv HashMap Symbol ([(BindId, a)], SortedReft)
mergedEnv

          modifiedBinds :: [(Symbol, ([(BindId, a)], SortedReft))]
modifiedBinds = HashMap Symbol ([(BindId, a)], SortedReft)
-> [(Symbol, ([(BindId, a)], SortedReft))]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList (HashMap Symbol ([(BindId, a)], SortedReft)
 -> [(Symbol, ([(BindId, a)], SortedReft))])
-> HashMap Symbol ([(BindId, a)], SortedReft)
-> [(Symbol, ([(BindId, a)], SortedReft))]
forall a b. (a -> b) -> a -> b
$ HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
-> HashMap Symbol ([(BindId, a)], SortedReft)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap Symbol ([(BindId, a)], SortedReft)
boolSimplEnv HashMap Symbol ([(BindId, a)], SortedReft)
undoANFEnv

          modifiedBindIds :: [[BindId]]
modifiedBindIds = [ (BindId, a) -> BindId
forall a b. (a, b) -> a
fst ((BindId, a) -> BindId) -> [(BindId, a)] -> [BindId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BindId, a)]
bindIds | (Symbol
_, ([(BindId, a)]
bindIds,SortedReft
_)) <- [(Symbol, ([(BindId, a)], 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 a
bindEnv') = ([BindId], BindEnv a)
-> [(Symbol, ([(BindId, a)], SortedReft))] -> ([BindId], BindEnv a)
forall {a} {a}.
([BindId], BindEnv a)
-> [(Symbol, ([(a, a)], SortedReft))] -> ([BindId], BindEnv a)
insertBinds ([], BindEnv a
bindEnv) [(Symbol, ([(BindId, a)], 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 a
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 a)
-> [(Symbol, ([(a, a)], SortedReft))] -> ([BindId], BindEnv a)
insertBinds = (([BindId], BindEnv a)
 -> (Symbol, ([(a, a)], SortedReft)) -> ([BindId], BindEnv a))
-> ([BindId], BindEnv a)
-> [(Symbol, ([(a, a)], SortedReft))]
-> ([BindId], BindEnv a)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((([BindId], BindEnv a)
  -> (Symbol, ([(a, a)], SortedReft)) -> ([BindId], BindEnv a))
 -> ([BindId], BindEnv a)
 -> [(Symbol, ([(a, a)], SortedReft))]
 -> ([BindId], BindEnv a))
-> (([BindId], BindEnv a)
    -> (Symbol, ([(a, a)], SortedReft)) -> ([BindId], BindEnv a))
-> ([BindId], BindEnv a)
-> [(Symbol, ([(a, a)], SortedReft))]
-> ([BindId], BindEnv a)
forall a b. (a -> b) -> a -> b
$ \([BindId]
xs, BindEnv a
be) (Symbol
s, ([(a, a)]
bIdAs, SortedReft
sr)) ->
      let (BindId
bId, BindEnv a
be') = Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv Symbol
s SortedReft
sr ((a, a) -> a
forall a b. (a, b) -> b
snd ((a, a) -> a) -> ([(a, a)] -> (a, a)) -> [(a, a)] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, a)] -> (a, a)
forall a. HasCallStack => [a] -> a
head ([(a, a)] -> a) -> [(a, a)] -> a
forall a b. (a -> b) -> a -> b
$ [(a, a)]
bIdAs) BindEnv a
be
      in (BindId
bId BindId -> [BindId] -> [BindId]
forall a. a -> [a] -> [a]
: [BindId]
xs, BindEnv a
be')

-- | If the environment contains duplicated bindings, they are
-- combined with conjunctions.
--
-- This means that @[ a : {v | P v }, a : {z | Q z }, b : {v | S v} ]@
-- is combined into @[ a : {v | P v && Q v }, b : {v | S v} ]@
--
-- If a symbol has two bindings with different sorts, none of the bindings
-- for that symbol are merged.
mergeDuplicatedBindings
  :: Semigroup m
  => [(Symbol, (m, SortedReft))]
  -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings :: forall m.
Semigroup m =>
[(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} {a}. Functor f => (a, f a) -> f (a, a)
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 a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SortedReft -> Maybe SortedReft)
-> (m, SortedReft) -> (m, Maybe SortedReft)
forall a b. (a -> b) -> (m, a) -> (m, b)
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 a) -> f (a, a)
dropNothings (a
m, f a
msr) = (,) a
m (a -> (a, a)) -> f a -> f (a, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
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 = mergeRefts (sr_reft sr0) (sr_reft sr1) }
       in
          (a
bs0 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
bs1, Maybe SortedReft
msr)

    mergeRefts :: ReftV v -> ReftV v -> ReftV v
mergeRefts ReftV v
r0 ReftV v
r1 =
      Symbol -> ExprV v -> ReftV v
forall v. Symbol -> ExprV v -> ReftV v
reft
        (ReftV v -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV v
r0)
        (ListNE (ExprV v) -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd
          [ ReftV v -> ExprV v
forall v. ReftV v -> ExprV v
reftPred ReftV v
r0
          , ExprV v -> (Symbol, ExprV Symbol) -> ExprV v
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
subst1 (ReftV v -> ExprV v
forall v. ReftV v -> ExprV v
reftPred ReftV v
r1) (ReftV v -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV v
r1, Symbol -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
expr (ReftV v -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV v
r0))
          ]
        )

-- | Inlines some of the bindings whose symbol satisfies a given predicate.
--
-- Only works if the bindings don't form cycles.
substBindingsSimplifyingWith
  :: (SortedReft -> SortedReft)
  -> Lens' v SortedReft
  -> (Symbol -> Bool)
  -> HashMap Symbol v
  -> HashMap Symbol v
substBindingsSimplifyingWith :: forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
substBindingsSimplifyingWith SortedReft -> SortedReft
simplifier Lens' v SortedReft
vLens Symbol -> Bool
p HashMap Symbol v
env =
    -- Circular program here. This should terminate as long as the
    -- bindings introduced by ANF don't form cycles.
    let env' :: HashMap Symbol v
env' = (v -> v) -> HashMap Symbol v -> HashMap Symbol v
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (LensLike' f v SortedReft
Lens' v SortedReft
forall {f :: * -> *}. Identical f => LensLike' f v SortedReft
vLens (forall {f :: * -> *}. Identical f => LensLike' f v SortedReft)
-> (SortedReft -> SortedReft) -> v -> v
forall s t a b. Setter s t a b -> (a -> b) -> s -> t
%~ SortedReft -> SortedReft
simplifier (SortedReft -> SortedReft)
-> (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Maybe SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft (HashMap Symbol v -> Symbol -> Maybe SortedReft
forall {k}. Hashable k => HashMap k v -> k -> Maybe SortedReft
srLookup HashMap Symbol v
filteredEnv)) HashMap Symbol v
env
        filteredEnv :: HashMap Symbol v
filteredEnv = (Symbol -> v -> Bool) -> HashMap Symbol v -> HashMap Symbol v
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey (\Symbol
sym v
_v -> Symbol -> Bool
p Symbol
sym) HashMap Symbol v
env'
     in HashMap Symbol v
env'
  where
    srLookup :: HashMap k v -> k -> Maybe SortedReft
srLookup HashMap k v
env' k
sym = FoldLike SortedReft v v SortedReft SortedReft -> v -> SortedReft
forall a s t b. FoldLike a s t a b -> s -> a
view FoldLike SortedReft v v SortedReft SortedReft
Lens' v SortedReft
vLens (v -> SortedReft) -> Maybe v -> Maybe SortedReft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> k -> HashMap k v -> Maybe v
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup k
sym HashMap k v
env'

substBindings
  :: Lens' v SortedReft
  -> (Symbol -> Bool)
  -> HashMap Symbol v
  -> HashMap Symbol v
substBindings :: forall v.
Lens' v SortedReft
-> (Symbol -> Bool) -> HashMap Symbol v -> HashMap Symbol v
substBindings = (SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
substBindingsSimplifyingWith SortedReft -> SortedReft
forall a. Fixpoint a => a -> a
simplify

-- | Like 'substBindings' but specialized for ANF bindings.
--
-- Only bindings with prefix lq_anf$... might be inlined.
--
undoANFSimplifyingWith :: (SortedReft -> SortedReft) -> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANFSimplifyingWith :: forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANFSimplifyingWith SortedReft -> SortedReft
simplifier Lens' v SortedReft
vLens = (SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
substBindingsSimplifyingWith SortedReft -> SortedReft
simplifier LensLike' f v SortedReft
Lens' v SortedReft
vLens ((Symbol -> Bool) -> HashMap Symbol v -> HashMap Symbol v)
-> (Symbol -> Bool) -> HashMap Symbol v -> HashMap Symbol v
forall a b. (a -> b) -> a -> b
$ \Symbol
sym -> Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
sym

undoANF :: Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANF :: forall v.
Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANF = (SortedReft -> SortedReft)
-> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANFSimplifyingWith SortedReft -> SortedReft
forall a. Fixpoint a => a -> a
simplify

-- | Like 'undoANF' but also inlines VV bindings
--
-- This function is used to produced the prettified output, and the user
-- can request to use it in the verification pipeline with
-- @--inline-anf-bindings@. However, using it in the verification
-- pipeline causes some tests in liquidhaskell to blow up.
--
-- Note: This function simplifies.
undoANFAndVV :: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFAndVV :: forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFAndVV = Lens' (m, SortedReft) SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol (m, SortedReft)
-> HashMap Symbol (m, SortedReft)
forall v.
Lens' v SortedReft
-> (Symbol -> Bool) -> HashMap Symbol v -> HashMap Symbol v
substBindings LensLike f (m, SortedReft) (m, SortedReft) SortedReft SortedReft
forall r a b (f :: * -> *).
Functor f =>
LensLike f (r, a) (r, b) a b
Lens' (m, SortedReft) SortedReft
_2 ((Symbol -> Bool)
 -> HashMap Symbol (m, SortedReft)
 -> HashMap Symbol (m, SortedReft))
-> (Symbol -> Bool)
-> HashMap Symbol (m, SortedReft)
-> HashMap Symbol (m, SortedReft)
forall a b. (a -> b) -> a -> b
$ \Symbol
sym -> Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
sym Bool -> Bool -> Bool
|| Symbol
vvName Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
sym

-- | Like 'undoANF' but returns only modified bindings and **DOES NOT SIMPLIFY**.
undoANFOnlyModified :: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFOnlyModified :: forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFOnlyModified HashMap Symbol (m, SortedReft)
env =
    let undoANFEnv :: HashMap Symbol (m, SortedReft)
undoANFEnv = (SortedReft -> SortedReft)
-> Lens' (m, SortedReft) SortedReft
-> HashMap Symbol (m, SortedReft)
-> HashMap Symbol (m, SortedReft)
forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANFSimplifyingWith SortedReft -> SortedReft
forall a. a -> a
id LensLike f (m, SortedReft) (m, SortedReft) SortedReft SortedReft
forall r a b (f :: * -> *).
Functor f =>
LensLike f (r, a) (r, b) a b
Lens' (m, SortedReft) SortedReft
_2 HashMap Symbol (m, SortedReft)
env
     in ((m, SortedReft) -> (m, SortedReft) -> Maybe (m, SortedReft))
-> HashMap Symbol (m, SortedReft)
-> HashMap Symbol (m, SortedReft)
-> HashMap Symbol (m, SortedReft)
forall k v w.
(Eq k, Hashable k) =>
(v -> w -> Maybe v) -> HashMap k v -> HashMap k w -> HashMap k v
HashMap.differenceWith (m, SortedReft) -> (m, SortedReft) -> Maybe (m, SortedReft)
forall {a} {a} {a}. Eq a => (a, a) -> (a, a) -> Maybe (a, a)
dropUnchanged HashMap Symbol (m, SortedReft)
env HashMap Symbol (m, SortedReft)
undoANFEnv
  where
    dropUnchanged :: (a, a) -> (a, a) -> Maybe (a, a)
dropUnchanged (a
_, a
a) v :: (a, a)
v@(a
_, a
b) | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b = (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (a, a)
v
      | Bool
otherwise = Maybe (a, a)
forall a. Maybe a
Nothing

-- | Inlines bindings in env in the given 'SortedReft'.
inlineInSortedReft
  :: (Symbol -> Maybe SortedReft)
  -> SortedReft
  -> SortedReft
inlineInSortedReft :: (Symbol -> Maybe SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft Symbol -> Maybe SortedReft
srLookup SortedReft
sr =
    let reft' :: ReftV Symbol
reft' = SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
     in SortedReft
sr { sr_reft = mapPredReft (inlineInExpr (filterBind (reftBind reft'))) reft' }
  where
    filterBind :: Symbol -> Symbol -> Maybe SortedReft
filterBind Symbol
b Symbol
sym = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
b)
      Symbol -> Maybe SortedReft
srLookup Symbol
sym

-- | Inlines bindings given by @srLookup@ in the given expression
-- if they appear in equalities.
--
-- Given a binding like @a : { v | v = e1 && e2 }@ and an expression @... e0 = a ...@,
-- this function produces the expression @... e0 = e1 ...@
-- if @v@ does not appear free in @e1@.
--
-- @... e0 = (a : s) ...@ is equally transformed to
-- @... e0 = (e1 : s) ...@
--
-- Given a binding like @a : { v | v = e1 }@ and an expression @... a ...@,
-- this function produces the expression @... e1 ...@ if @v@ does not
-- appear free in @e1@.
inlineInExpr :: (Symbol -> Maybe SortedReft) -> Expr -> Expr
inlineInExpr :: (Symbol -> Maybe SortedReft) -> ExprV Symbol -> ExprV Symbol
inlineInExpr Symbol -> Maybe SortedReft
srLookup = (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
mapExprOnExpr ExprV Symbol -> ExprV Symbol
inlineExpr
  where
    inlineExpr :: ExprV Symbol -> ExprV Symbol
inlineExpr (EVar Symbol
sym)
      | Just SortedReft
sr <- Symbol -> Maybe SortedReft
srLookup Symbol
sym
      , let r :: ReftV Symbol
r = SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
      , Just ExprV Symbol
e <- Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingletonE (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r) (ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred ReftV Symbol
r)
      = Brel -> Sort -> ExprV Symbol -> ExprV Symbol
wrapWithCoercion Brel
Eq (SortedReft -> Sort
sr_sort SortedReft
sr) ExprV Symbol
e
    inlineExpr (PAtom Brel
br ExprV Symbol
e0 e1 :: ExprV Symbol
e1@(ExprV Symbol -> ExprV Symbol
dropECst -> EVar Symbol
sym))
      | Brel -> Bool
isEq Brel
br
      , Just SortedReft
sr <- Symbol -> Maybe SortedReft
srLookup Symbol
sym
      , let r :: ReftV Symbol
r = SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
      , Just ExprV Symbol
e <- Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingletonE (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r) (ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred ReftV Symbol
r)
      =
        Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
br ExprV Symbol
e0 (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
subst1 ExprV Symbol
e1 (Symbol
sym, Brel -> Sort -> ExprV Symbol -> ExprV Symbol
wrapWithCoercion Brel
br (SortedReft -> Sort
sr_sort SortedReft
sr) ExprV Symbol
e)
    inlineExpr ExprV Symbol
e = ExprV Symbol
e

    isSingletonE :: Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingletonE Symbol
v (PAtom Brel
br ExprV Symbol
e0 ExprV Symbol
e1)
      | Brel -> Bool
isEq Brel
br = Symbol -> ExprV Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingEq Symbol
v ExprV Symbol
e0 ExprV Symbol
e1 Maybe (ExprV Symbol)
-> Maybe (ExprV Symbol) -> Maybe (ExprV Symbol)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol -> ExprV Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingEq Symbol
v ExprV Symbol
e1 ExprV Symbol
e0
    isSingletonE Symbol
v (PIff ExprV Symbol
e0 ExprV Symbol
e1) =
      Symbol -> ExprV Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingEq Symbol
v ExprV Symbol
e0 ExprV Symbol
e1 Maybe (ExprV Symbol)
-> Maybe (ExprV Symbol) -> Maybe (ExprV Symbol)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol -> ExprV Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingEq Symbol
v ExprV Symbol
e1 ExprV Symbol
e0
    isSingletonE Symbol
v (PAnd [ExprV Symbol]
cs) =
      [Maybe (ExprV Symbol)] -> Maybe (ExprV Symbol)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe (ExprV Symbol)] -> Maybe (ExprV Symbol))
-> [Maybe (ExprV Symbol)] -> Maybe (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> Maybe (ExprV Symbol))
-> [ExprV Symbol] -> [Maybe (ExprV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingletonE Symbol
v) [ExprV Symbol]
cs
    isSingletonE Symbol
_ ExprV Symbol
_ =
      Maybe (ExprV Symbol)
forall a. Maybe a
Nothing

    isSingEq :: Symbol -> ExprV Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingEq Symbol
v ExprV Symbol
e0 ExprV Symbol
e1 = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol -> ExprV Symbol
dropECst ExprV Symbol
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
$ ExprV Symbol -> HashSet Symbol
exprSymbolsSet ExprV Symbol
e1)
      ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
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 -> ExprV Symbol -> ExprV Symbol
wrapWithCoercion Brel
br Sort
to ExprV Symbol
e = case ExprV Symbol -> Maybe Sort
exprSortMaybe ExprV Symbol
e of
      Just Sort
from -> if Sort
from Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
/= Sort
to then Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
from Sort
to ExprV Symbol
e else ExprV Symbol
e
      Maybe Sort
Nothing -> if Brel
br Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ueq then ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst ExprV Symbol
e Sort
to else ExprV Symbol
e

-- | Transforms bindings of the form @{v:bool | v && P v}@ into
-- @{v:Bool | v && P true}@, and bindings of the form @{v:bool | ~v && P v}@
-- into @{v:bool | ~v && P false}@.
--
-- Only yields the modified bindings.
simplifyBooleanRefts
  :: HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts :: forall m.
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 :: ReftV Symbol
r = SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
      , Just (ExprV Symbol
e, [ExprV Symbol]
rest) <- Symbol -> ExprV Symbol -> Maybe (ExprV Symbol, [ExprV Symbol])
forall {v}. Eq v => v -> ExprV v -> Maybe (ExprV v, [ExprV v])
symbolUsedAtTopLevelAnd (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r) (ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred ReftV Symbol
r)
      = let e' :: ExprV Symbol
e' = [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ ExprV Symbol
e ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
: (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`subst1` (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r, ExprV Symbol -> ExprV Symbol
forall {v}. ExprV Symbol -> ExprV v
atomToBool ExprV Symbol
e)) [ExprV Symbol]
rest
            atomToBool :: ExprV Symbol -> ExprV v
atomToBool ExprV Symbol
a = if ExprV Symbol
a ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r) then ExprV v
forall v. ExprV v
PTrue else ExprV v
forall v. ExprV v
PFalse
         in (a, SortedReft) -> Maybe (a, SortedReft)
forall a. a -> Maybe a
Just (a
m, SortedReft
sr { sr_reft = mapPredReft (const e') r })
    simplifyBooleanSortedReft (a, SortedReft)
_ = Maybe (a, SortedReft)
forall a. Maybe a
Nothing

    symbolUsedAtTopLevelAnd :: v -> ExprV v -> Maybe (ExprV v, [ExprV v])
symbolUsedAtTopLevelAnd v
s (PAnd [ExprV v]
ps) =
      ExprV v -> [ExprV v] -> Maybe (ExprV v, [ExprV v])
forall {a}. Eq a => a -> [a] -> Maybe (a, [a])
findExpr (v -> ExprV v
forall v. v -> ExprV v
EVar v
s) [ExprV v]
ps Maybe (ExprV v, [ExprV v])
-> Maybe (ExprV v, [ExprV v]) -> Maybe (ExprV v, [ExprV v])
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` ExprV v -> [ExprV v] -> Maybe (ExprV v, [ExprV v])
forall {a}. Eq a => a -> [a] -> Maybe (a, [a])
findExpr (ExprV v -> ExprV v
forall v. ExprV v -> ExprV v
PNot (v -> ExprV v
forall v. v -> ExprV v
EVar v
s)) [ExprV v]
ps
    symbolUsedAtTopLevelAnd v
_ ExprV v
_ = Maybe (ExprV v, [ExprV v])
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
f:[a]
_, [a]
rest) -> (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
f, [a]
rest)

-- | @dropLikelyIrrelevantBindings ss env@ is like @dropIrrelevantBindings@
-- but drops bindings that could potentially be necessary to validate a
-- constraint.
--
-- This function drops any bindings in the reachable set of symbols of @ss@.
-- See 'relatedSymbols'.
--
-- A constraint might be rendered unverifiable if the verification depends on
-- the environment being inconsistent. For instance, suppose the constraint
-- is @a < 0@ and we call this function like
--
-- > dropLikelyIrrelevantBindings ["a"] [a : { v | v > 0 }, b : { v | false }]
-- >   == [a : { v | v > 0 }]
--
-- The binding for @b@ is dropped since it is not otherwise related to @a@,
-- making the corresponding constraint unverifiable.
--
-- Bindings refered only from @match@ or @define@ clauses will be dropped as
-- well.
--
-- Symbols starting with a capital letter will be dropped too, as these are
-- usually global identifiers with either uninteresting or known types.
--
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
    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 (ExprV Symbol -> HashSet Symbol
exprSymbolsSet (ExprV Symbol -> HashSet Symbol)
-> (SortedReft -> ExprV Symbol) -> SortedReft -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReftV Symbol -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> ExprV Symbol)
-> (SortedReft -> ReftV Symbol) -> SortedReft -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> ReftV Symbol
sr_reft) HashMap Symbol SortedReft
env
    relatedSyms :: HashSet Symbol
relatedSyms = HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
relatedSymbols HashSet Symbol
ss HashMap Symbol (HashSet Symbol)
directlyUses
    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 ss env@ is the set of all symbols used transitively
-- by @ss@ in @env@ or used together with it in a refinement type.
-- The output includes @ss@.
--
-- For instance, say @ss@ contains @a@, and the environment is
--
-- > a : { v | v > b }, b : int, c : { v | v >= b && b >= d}, d : int
--
-- @a@ uses @b@. Because the predicate of @c@ relates @b@ with @d@,
-- @d@ can also influence the validity of the predicate of @a@, and therefore
-- we include both @b@, @c@, and @d@ in the set of related symbols.
relatedSymbols
  :: HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
relatedSymbols :: HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol
relatedSymbols HashSet Symbol
ss0 HashMap Symbol (HashSet Symbol)
directlyUses = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go HashSet Symbol
forall a. HashSet a
HashSet.empty HashSet Symbol
ss0
  where
    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 => 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 acc ss@ contains @acc@ and @ss@ plus any symbols reachable from @ss@
    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 => [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 => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
relatedToX HashSet Symbol
xs)