{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TupleSections #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

-- | Functions to make environments smaller
module Language.Fixpoint.Solver.EnvironmentReduction
  ( reduceEnvironments
  , simplifyBindings
  , dropLikelyIrrelevantBindings
  , 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
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 (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(..)
  , Expr(..)
  , KVar(..)
  , SortedReft(..)
  , Subst(..)
  , 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
fi =
  let constraints :: [(SubcId, SubC a)]
constraints = forall k v. HashMap k v -> [(k, v)]
HashMap.Strict.toList forall a b. (a -> b) -> a -> b
$ 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 (forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae FInfo a
fi)
      reducedEnvs :: [ReducedConstraint a]
reducedEnvs = forall a b. (a -> b) -> [a] -> [b]
map (forall a.
BindEnv a
-> HashMap Symbol (HashSet Symbol)
-> (SubcId, SubC a)
-> ReducedConstraint a
reduceConstraintEnvironment (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi) HashMap Symbol (HashSet Symbol)
aenvMap) [(SubcId, SubC a)]
constraints
      ([(SubcId, SubC a)]
cm', HashMap KVar (WfC a)
ws') = forall a.
BindEnv a
-> ([ReducedConstraint a], HashMap KVar (WfC a))
-> ([(SubcId, SubC a)], HashMap KVar (WfC a))
reduceWFConstraintEnvironments (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi) ([ReducedConstraint a]
reducedEnvs, forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
fi)
      bs' :: SizedEnv (Symbol, SortedReft, a)
bs' = (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi) { beBinds :: BindMap (Symbol, SortedReft, a)
beBinds = forall a.
HashMap BindId (Symbol, SortedReft, a)
-> [(SubcId, SubC a)]
-> HashMap KVar (WfC a)
-> HashMap BindId (Symbol, SortedReft, a)
dropBindsMissingFrom (forall a. SizedEnv a -> BindMap a
beBinds forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi) [(SubcId, SubC a)]
cm' HashMap KVar (WfC a)
ws' }

   in FInfo a
fi
     { bs :: SizedEnv (Symbol, SortedReft, a)
bs = SizedEnv (Symbol, SortedReft, a)
bs'
     , cm :: HashMap SubcId (SubC a)
cm = 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 = forall {a}. SizedEnv a -> [BindId] -> [BindId]
updateEbinds SizedEnv (Symbol, SortedReft, a)
bs' (forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds FInfo a
fi)
     , bindInfo :: HashMap BindId a
bindInfo = forall {w} {v}. SizedEnv w -> HashMap BindId v -> HashMap BindId v
updateBindInfoKeys SizedEnv (Symbol, SortedReft, a)
bs' forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap BindId a
bindInfo FInfo a
fi
     }

  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)
ws =
      let ibindEnv :: IBindEnv
ibindEnv = [IBindEnv] -> IBindEnv
unionsIBindEnv forall a b. (a -> b) -> a -> b
$
            forall a b. (a -> b) -> [a] -> [b]
map (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(SubcId, SubC a)]
cs forall a. [a] -> [a] -> [a]
++
            forall a b. (a -> b) -> [a] -> [b]
map forall a. WfC a -> IBindEnv
wenv (forall k v. HashMap k v -> [v]
HashMap.elems HashMap KVar (WfC a)
ws)
       in
          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 = forall a. (a -> Bool) -> [a] -> [a]
filter (forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`HashMap.member` 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 =
      forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
HashMap.intersection HashMap BindId v
oldBindInfos (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) = 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 =
        forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashMap KVar (HashSet Symbol)
kvarsBinds forall a b. (a -> b) -> a -> b
$
        forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Sort -> HashSet Symbol
sortSymbols forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Symbol
_, Sort
b, KVar
_) -> Sort
b) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. WfC a -> (Symbol, Sort, KVar)
wrft) HashMap KVar (WfC a)
wfs

      kvarsRelevantBinds :: HashMap KVar (HashSet Symbol)
kvarsRelevantBinds =
        forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith forall a. (Eq a, Hashable 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' =
        forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapWithKey
          (forall a.
BindEnv a
-> HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
reduceWFConstraintEnvironment BindEnv a
bindEnv HashMap KVar (HashSet Symbol)
kvarsRelevantBinds)
          HashMap KVar (WfC a)
wfs

      wsSymbols :: HashMap KVar (HashSet Symbol)
wsSymbols = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (forall a. BindEnv a -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv a
bindEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. WfC a -> IBindEnv
wenv) HashMap KVar (WfC a)
ws'

      kvarsWsBinds :: HashMap KVar (HashSet Symbol)
kvarsWsBinds =
        forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith 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' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
              (forall a.
BindEnv a
-> HashMap KVar (HashSet Symbol)
-> [KVar]
-> ReducedConstraint a
-> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds BindEnv a
bindEnv 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
      :: BindEnv a
      -> HashMap KVar (HashSet Symbol)
      -> [KVar]
      -> ReducedConstraint a
      -> (SubcId, SubC a)
    updateSubcEnvsWithKVarBinds :: forall a.
BindEnv a
-> HashMap KVar (HashSet Symbol)
-> [KVar]
-> ReducedConstraint a
-> (SubcId, SubC a)
updateSubcEnvsWithKVarBinds BindEnv a
be HashMap KVar (HashSet Symbol)
kvarsBinds [KVar]
kvs ReducedConstraint a
c =
      let updateIBindEnv :: IBindEnv -> IBindEnv
updateIBindEnv IBindEnv
oldEnv =
            IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv (forall a. ReducedConstraint a -> IBindEnv
reducedEnv ReducedConstraint a
c) forall a b. (a -> b) -> a -> b
$
            if 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
_) = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
be
              , 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 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 -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Symbol
s HashSet Symbol
kbindSyms
       in (forall a. ReducedConstraint a -> SubcId
constraintId ReducedConstraint a
c, forall (c :: * -> *) a.
TaggedC c a =>
c a -> (IBindEnv -> IBindEnv) -> c a
updateSEnv (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
      :: BindEnv a
      -> HashMap KVar (HashSet Symbol)
      -> KVar
      -> WfC a
      -> WfC a
    reduceWFConstraintEnvironment :: forall a.
BindEnv a
-> HashMap KVar (HashSet Symbol) -> KVar -> WfC a -> WfC a
reduceWFConstraintEnvironment BindEnv a
bindEnv HashMap KVar (HashSet Symbol)
kvarBinds KVar
k WfC a
c =
      case 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) (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
_, a
_) = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
bindEnv
           in 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 forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c
            , let (Symbol
s, SortedReft
sr, a
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
_) <- 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 =
        forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union (SortedReft -> HashSet Symbol
sortedReftSymbols forall a b. (a -> b) -> a -> b
$ forall a. SubC a -> SortedReft
slhs SubC a
c) (SortedReft -> HashSet Symbol
sortedReftSymbols forall a b. (a -> b) -> a -> b
$ 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 =
  forall a. (a -> Bool) -> [a] -> [a]
filter 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 (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 =
      forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
HashSet.unions forall a b. (a -> b) -> a -> b
$ 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
_)
      | 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 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 forall a. Eq a => a -> a -> Bool
/= Reft -> Symbol
reftBind (SortedReft -> Reft
sr_reft SortedReft
sr)
          Expr
_ -> 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
ae =
  forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union
    (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Equation -> (Symbol, HashSet Symbol)
eqSymbols forall a b. (a -> b) -> a -> b
$ AxiomEnv -> [Equation]
aenvEqs AxiomEnv
ae)
    (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Rewrite -> (Symbol, HashSet Symbol)
rewriteSymbols 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 =
            forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
              (Expr -> HashSet Symbol
exprSymbolsSet (Equation -> Expr
eqBody Equation
eq) forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.union` Sort -> HashSet Symbol
sortSymbols (Equation -> Sort
eqSort Equation
eq))
              (forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)
          sortSyms :: HashSet Symbol
sortSyms = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
HashSet.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Sort -> HashSet Symbol
sortSymbols forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ Equation -> [(Symbol, Sort)]
eqArgs Equation
eq
          allSymbols :: HashSet Symbol
allSymbols =
            if Equation -> Bool
eqRec Equation
eq then
              forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert (Equation -> Symbol
eqName Equation
eq) (HashSet Symbol
bodySymbols forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.union` HashSet Symbol
sortSyms)
            else
              HashSet Symbol
bodySymbols 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 =
            forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.difference
              (Expr -> HashSet Symbol
exprSymbolsSet (Rewrite -> Expr
smBody Rewrite
rw))
              (forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList forall a b. (a -> b) -> a -> b
$ Rewrite -> [Symbol]
smArgs Rewrite
rw)
          rwSymbols :: HashSet Symbol
rwSymbols = 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 forall a. HashSet a -> [a]
HashSet.toList HashSet a
xs of
  [] -> forall a. Maybe a
Nothing
  (a
x : [a]
_) -> forall a. a -> Maybe a
Just (a
x, 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HashSet a
HashSet.empty (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 = forall a. a -> Maybe a -> a
fromMaybe forall k v. HashMap k v
HashMap.empty (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 = forall a b. (a -> b) -> [a] -> [b]
map forall a. ReducedConstraint a -> HashMap KVar (HashSet Symbol)
kvarBindsFromSubC [ReducedConstraint a]
cs
      kvarsBySubC :: [[KVar]]
kvarsBySubC = forall a b. (a -> b) -> [a] -> [b]
map forall k v. HashMap k v -> [k]
HashMap.keys [HashMap KVar (HashSet Symbol)]
kvarsSubstSymbolsBySubC
      bindIdsByKVar :: HashMap KVar (HashSet Symbol)
bindIdsByKVar =
       forall k v. (Hashable k, Eq k) => ShareMap k v -> HashMap k v
ShareMap.toHashMap forall a b. (a -> b) -> a -> b
$
       forall a b k. (a -> b) -> ShareMap k a -> ShareMap k b
ShareMap.map (forall a. BindEnv a -> IBindEnv -> HashSet Symbol
asSymbolSet BindEnv a
bindEnv) forall a b. (a -> b) -> a -> b
$
       [(IBindEnv, [KVar])] -> ShareMap KVar IBindEnv
groupIBindEnvByKVar forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a. ReducedConstraint a -> IBindEnv
reducedEnv [ReducedConstraint a]
cs) [[KVar]]
kvarsBySubC
      substsByKVar :: HashMap KVar (HashSet Symbol)
substsByKVar =
        forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union) 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 =
      forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Expr -> HashMap KVar [Subst]
exprKVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> b
snd3) forall a b. (a -> b) -> a -> b
$ 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 = 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 =
            forall a. HashMap a () -> HashSet a
HashSet.fromMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (forall a b. a -> b -> a
const ()) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [HashMap k v] -> HashMap k v
HashMap.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Subst -> HashMap Symbol Expr
unSubst
       in forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union) forall k v. HashMap k v
HashMap.empty forall a b. (a -> b) -> a -> b
$
          forall a b. (a -> b) -> [a] -> [b]
map (forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map [Subst] -> HashSet Symbol
substsToHashSet) forall a b. (a -> b) -> a -> b
$
          (Expr -> HashMap KVar [Subst]
exprKVars (Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft forall a b. (a -> b) -> a -> b
$ forall a. SubC a -> SortedReft
srhs SubC a
c) forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
          (Expr -> HashMap KVar [Subst]
exprKVars (Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft forall a b. (a -> b) -> a -> b
$ forall a. SubC a -> SortedReft
slhs SubC a
c) forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
          forall a b. (a -> b) -> [a] -> [b]
map (forall k a b.
(Hashable k, Eq k) =>
HashMap k (HashMap a b) -> k -> HashMap a b
mapOf HashMap BindId (HashMap KVar [Subst])
kvarsByBindId) forall a b. (a -> b) -> a -> b
$
          IBindEnv -> [BindId]
elemsIBindEnv (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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ShareMap KVar IBindEnv
-> (IBindEnv, [KVar]) -> ShareMap KVar IBindEnv
mergeBinds 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' = 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 forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (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 =
  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
_) = 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 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 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 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 = 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 (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Symbol
x HashSet Symbol
acc) (forall a. (Eq a, Hashable 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
fi =
  let (BindEnv a
bs', HashMap SubcId (SubC a)
cm', HashMap BindId [BindId]
oldToNew) = forall a.
BindEnv a
-> HashMap SubcId (SubC a)
-> (BindEnv a, HashMap SubcId (SubC a), HashMap BindId [BindId])
simplifyConstraints (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi) (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi)
   in FInfo a
fi
        { bs :: BindEnv a
bs = BindEnv a
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 (forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds FInfo a
fi)
        , bindInfo :: HashMap BindId a
bindInfo = forall a.
HashMap BindId [BindId] -> HashMap BindId a -> HashMap BindId a
updateBindInfoKeys HashMap BindId [BindId]
oldToNew forall a b. (a -> b) -> a -> b
$ 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 =
      forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ BindId
bId forall a. a -> [a] -> [a]
: forall a. a -> Maybe a -> a
fromMaybe [] (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 =
      forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
        [ (BindId
n, a
a)
        | (BindId
bId, a
a) <- forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap BindId a
infoMap
        , Just [BindId]
news <- [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 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) =
             forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
HashMap.foldlWithKey' 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 =
            forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith forall a. [a] -> [a] -> [a]
(++) forall a b. (a -> b) -> a -> b
$
            forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(BindId
n, [BindId]
olds) -> forall a b. (a -> b) -> [a] -> [b]
map (, [BindId
n]) [BindId]
olds) [(BindId, [BindId])]
newToOld
       in
          (BindEnv a
be', 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 forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c
            , let (Symbol
s, SortedReft
sr, a
a) = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
bId BindEnv a
bindEnv
            ]

          mergedEnv :: HashMap Symbol ([(BindId, a)], SortedReft)
mergedEnv = 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 forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFOnlyModified HashMap Symbol ([(BindId, a)], SortedReft)
mergedEnv else forall k v. HashMap k v
HashMap.empty
          boolSimplEnv :: HashMap Symbol ([(BindId, a)], SortedReft)
boolSimplEnv =
            forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable 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 = forall k v. HashMap k v -> [(k, v)]
HashMap.toList forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable 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 = [ forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BindId, a)]
bs | (Symbol
_, ([(BindId, a)]
bs,SortedReft
_)) <- [(Symbol, ([(BindId, a)], SortedReft))]
modifiedBinds ]

          unchangedBindIds :: IBindEnv
unchangedBindIds = forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c IBindEnv -> IBindEnv -> IBindEnv
`diffIBindEnv` [BindId] -> IBindEnv
fromListIBindEnv (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[BindId]]
modifiedBindIds)

          ([BindId]
newBindIds, BindEnv a
bindEnv') = 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' = forall a b. [a] -> [b] -> [(a, b)]
zip [BindId]
newBindIds [[BindId]]
modifiedBindIds forall a. [a] -> [a] -> [a]
++ [(BindId, [BindId])]
newToOld
       in
          (BindEnv a
bindEnv', (SubcId
cid, forall (c :: * -> *) a.
TaggedC c a =>
c a -> (IBindEnv -> IBindEnv) -> c a
updateSEnv SubC a
c (forall a b. a -> b -> a
const IBindEnv
newIBindEnv)) forall a. a -> [a] -> [a]
: [(SubcId, SubC a)]
cs, [(BindId, [BindId])]
newToOld')

    insertBinds :: ([BindId], BindEnv a)
-> [(Symbol, ([(a, a)], SortedReft))] -> ([BindId], BindEnv a)
insertBinds = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' 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') = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv Symbol
s SortedReft
sr (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [(a, a)]
bIdAs) BindEnv a
be
      in (BindId
bId 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 =
    forall v1 v2 k. (v1 -> Maybe v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapMaybe forall {f :: * -> *} {a} {a}. Functor f => (a, f a) -> f (a, a)
dropNothings forall a b. (a -> b) -> a -> b
$
    forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith forall {a}.
Semigroup a =>
(a, Maybe SortedReft)
-> (a, Maybe SortedReft) -> (a, Maybe SortedReft)
mergeSortedReft forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 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
            forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SortedReft -> Sort
sr_sort SortedReft
sr0 forall a. Eq a => a -> a -> Bool
== SortedReft -> Sort
sr_sort SortedReft
sr1)
            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 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
          , forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 (Reft -> Expr
reftPred Reft
r1) (Reft -> Symbol
reftBind Reft
r1, forall a. Expression a => a -> Expr
expr (Reft -> Symbol
reftBind Reft
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' = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Lens' v SortedReft
vLens forall s t a b. Setter s t a b -> (a -> b) -> s -> t
%~ SortedReft -> SortedReft
simplifier forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Maybe SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft (forall {k}. Hashable k => HashMap k v -> k -> Maybe SortedReft
srLookup HashMap Symbol v
filteredEnv)) HashMap Symbol v
env
        filteredEnv :: HashMap Symbol v
filteredEnv = 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 = forall a s t b. FoldLike a s t a b -> s -> a
view Lens' v SortedReft
vLens forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
substBindingsSimplifyingWith 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 = forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft
-> (Symbol -> Bool)
-> HashMap Symbol v
-> HashMap Symbol v
substBindingsSimplifyingWith SortedReft -> SortedReft
simplifier Lens' v SortedReft
vLens 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 = forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANFSimplifyingWith 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 = forall v.
Lens' v SortedReft
-> (Symbol -> Bool) -> HashMap Symbol v -> HashMap Symbol v
substBindings forall r a b. Lens (r, a) (r, b) a b
_2 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 = forall v.
(SortedReft -> SortedReft)
-> Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANFSimplifyingWith forall a. a -> a
id forall r a b. Lens (r, a) (r, b) a b
_2 HashMap Symbol (m, SortedReft)
env
     in forall k v w.
(Eq k, Hashable k) =>
(v -> w -> Maybe v) -> HashMap k v -> HashMap k w -> HashMap k v
HashMap.differenceWith 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 forall a. Eq a => a -> a -> Bool
== a
b = forall a. a -> Maybe a
Just (a, a)
v
      | Bool
otherwise = 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 :: Reft
reft = SortedReft -> Reft
sr_reft SortedReft
sr
     in SortedReft
sr { sr_reft :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft ((Symbol -> Maybe SortedReft) -> Expr -> Expr
inlineInExpr (forall {m :: * -> *} {t} {b}.
(Monad m, Alternative m, Eq t) =>
t -> (t -> m b) -> t -> m b
filterBind (Reft -> Symbol
reftBind Reft
reft) Symbol -> Maybe SortedReft
srLookup)) Reft
reft }
  where
    filterBind :: t -> (t -> m b) -> t -> m b
filterBind t
b t -> m b
srLookup t
sym = do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t
sym forall a. Eq a => a -> a -> Bool
/= t
b)
      t -> m b
srLookup t
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) -> Expr -> Expr
inlineInExpr Symbol -> Maybe SortedReft
srLookup = (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
inlineExpr
  where
    inlineExpr :: Expr -> Expr
inlineExpr (EVar Symbol
sym)
      | Just SortedReft
sr <- Symbol -> Maybe SortedReft
srLookup Symbol
sym
      , 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))
      | Brel -> Bool
isEq Brel
br
      , Just SortedReft
sr <- Symbol -> Maybe SortedReft
srLookup Symbol
sym
      , 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 forall a b. (a -> b) -> a -> b
$ 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 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 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) =
      forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Symbol -> Expr -> Maybe Expr
isSingletonE Symbol
v) ListNE Expr
cs
    isSingletonE Symbol
_ Expr
_ =
      forall a. Maybe a
Nothing

    isSingEq :: Symbol -> Expr -> Expr -> Maybe Expr
isSingEq Symbol
v Expr
e0 Expr
e1 = do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
EVar Symbol
v forall a. Eq a => a -> a -> Bool
== Expr -> Expr
dropECst Expr
e0 Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HashSet.member Symbol
v forall a b. (a -> b) -> a -> b
$ Expr -> HashSet Symbol
exprSymbolsSet Expr
e1)
      forall a. a -> Maybe a
Just Expr
e1

    isEq :: Brel -> Bool
isEq Brel
r = Brel
r forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
r 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
exprSortMaybe Expr
e of
      Just Sort
from -> if Sort
from 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 forall a. Eq a => a -> a -> Bool
== Brel
Ueq then Expr -> Sort -> Expr
ECst Expr
e Sort
to else Expr
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 = forall v1 v2 k. (v1 -> Maybe v2) -> HashMap k v1 -> HashMap k v2
HashMap.mapMaybe 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 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 forall a b. (a -> b) -> a -> b
$ Expr
e forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (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 forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
EVar (Reft -> Symbol
reftBind Reft
r) then Expr
PTrue else Expr
PFalse
         in forall a. a -> Maybe a
Just (a
m, SortedReft
sr { sr_reft :: Reft
sr_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft (forall a b. a -> b -> a
const Expr
e') Reft
r })
    simplifyBooleanSortedReft (a, SortedReft)
_ = forall a. Maybe a
Nothing

    symbolUsedAtTopLevelAnd :: Symbol -> Expr -> Maybe (Expr, ListNE Expr)
symbolUsedAtTopLevelAnd Symbol
s (PAnd ListNE Expr
ps) =
      forall {a}. Eq a => a -> [a] -> Maybe (a, [a])
findExpr (Symbol -> Expr
EVar Symbol
s) ListNE Expr
ps forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall {a}. Eq a => a -> [a] -> Maybe (a, [a])
findExpr (Expr -> Expr
PNot (Symbol -> Expr
EVar Symbol
s)) ListNE Expr
ps
    symbolUsedAtTopLevelAnd Symbol
_ Expr
_ = forall a. Maybe a
Nothing

    findExpr :: a -> [a] -> Maybe (a, [a])
findExpr a
e [a]
es = do
      case forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (a
e forall a. Eq a => a -> a -> Bool
==) [a]
es of
        ([], [a]
_) -> forall a. Maybe a
Nothing
        (a
e:[a]
_, [a]
rest) -> forall a. a -> Maybe a
Just (a
e, [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 = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.filterWithKey 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 forall a. Eq a => a -> a -> Bool
/= Symbol
s) Bool -> Bool -> Bool
&& Symbol
s 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindId -> Text -> Text
Text.take BindId
1 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 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 forall a. HashSet a
HashSet.empty HashSet Symbol
ss0
  where
    directlyUses :: HashMap Symbol (HashSet Symbol)
directlyUses = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map (Expr -> HashSet Symbol
exprSymbolsSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft) HashMap Symbol SortedReft
env
    usedBy :: HashMap Symbol (HashSet Symbol)
usedBy = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union
               [ (Symbol
x, forall a. Hashable a => a -> HashSet a
HashSet.singleton Symbol
s)
               | (Symbol
s, HashSet Symbol
xs) <- forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol (HashSet Symbol)
directlyUses
               , Symbol
x <- 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 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 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 forall k a.
(Hashable k, Eq k) =>
HashMap k (HashSet a) -> k -> HashSet a
`setOf` Symbol
x
              relatedToX :: HashSet Symbol
relatedToX = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
HashSet.unions forall a b. (a -> b) -> a -> b
$
                HashSet Symbol
usersOfX forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (HashMap Symbol (HashSet Symbol)
directlyUses forall k a.
(Hashable k, Eq k) =>
HashMap k (HashSet a) -> k -> HashSet a
`setOf`) (Symbol
x forall a. a -> [a] -> [a]
: forall a. HashSet a -> [a]
HashSet.toList HashSet Symbol
usersOfX)
           in HashSet Symbol -> HashSet Symbol -> HashSet Symbol
go (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert Symbol
x HashSet Symbol
acc) (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
relatedToX HashSet Symbol
xs)