{-# LANGUAGE CPP           #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}

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

-- This module makes it so no binds with different sorts have the same name.

module Language.Fixpoint.Solver.UniqifyBinds (renameAll) where

import           Language.Fixpoint.Types
import           Language.Fixpoint.Solver.Sanitize (dropDeadSubsts)
import           Language.Fixpoint.Misc          (fst3, mlookup, snd3)

import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
import qualified Data.List           as L
#if !MIN_VERSION_base(4,20,0)
import           Data.Foldable       (foldl')
#endif
import           Data.Maybe          (catMaybes, mapMaybe, fromJust, isJust)
import           Data.Hashable       (Hashable)
import           GHC.Generics        (Generic)
import           Control.DeepSeq     (NFData, ($!!))
-- import Debug.Trace (trace)

--------------------------------------------------------------------------------
renameAll    :: (NFData a) => SInfo a -> SInfo a
--------------------------------------------------------------------------------
renameAll :: forall a. NFData a => SInfo a -> SInfo a
renameAll SInfo a
fi2 = SInfo a
fi6
  where
    fi6 :: SInfo a
fi6       = {- SCC "dropDead"    -} SInfo a -> SInfo a
forall a. SInfo a -> SInfo a
dropDeadSubsts  SInfo a
fi5
    fi5 :: SInfo a
fi5       = {- SCC "dropUnused"  -} SInfo a -> SInfo a
forall a. SInfo a -> SInfo a
dropUnusedBinds SInfo a
fi4
    fi4 :: SInfo a
fi4       = {- SCC "renameBinds" -} SInfo a -> RenameMap -> SInfo a
forall a. SInfo a -> RenameMap -> SInfo a
renameBinds SInfo a
fi3 (RenameMap -> SInfo a) -> RenameMap -> SInfo a
forall a b. NFData a => (a -> b) -> a -> b
$!! RenameMap
rnm
    fi3 :: SInfo a
fi3       = {- SCC "renameVars"  -} SInfo a -> RenameMap -> IdMap -> SInfo a
forall a. SInfo a -> RenameMap -> IdMap -> SInfo a
renameVars SInfo a
fi2 RenameMap
rnm (IdMap -> SInfo a) -> IdMap -> SInfo a
forall a b. NFData a => (a -> b) -> a -> b
$!! IdMap
idm
    rnm :: RenameMap
rnm       = {- SCC "mkRenameMap" -} BindEnv a -> RenameMap
forall a. BindEnv a -> RenameMap
mkRenameMap (BindEnv a -> RenameMap) -> BindEnv a -> RenameMap
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi2
    idm :: IdMap
idm       = {- SCC "mkIdMap"     -} SInfo a -> IdMap
forall a. SInfo a -> IdMap
mkIdMap SInfo a
fi2


--------------------------------------------------------------------------------
-- | `dropUnusedBinds` replaces the refinements of "unused" binders with "true".
--   see tests/pos/unused.fq for an example of why this phase is needed.
--------------------------------------------------------------------------------
dropUnusedBinds :: SInfo a -> SInfo a
dropUnusedBinds :: forall a. SInfo a -> SInfo a
dropUnusedBinds SInfo a
fi = SInfo a
fi {bs = filterBindEnv isUsed (bs fi)}-- { bs = mapBindEnv tx (bs fi) }
  where
    -- _tx i (x, r)
    -- | isUsed i    = (x, r)
    -- | otherwise   = (x, top r)
    isUsed :: BindId -> p -> SortedReft -> Bool
isUsed BindId
i p
_x SortedReft
r  = BindId -> IBindEnv -> Bool
memberIBindEnv BindId
i IBindEnv
usedBinds Bool -> Bool -> Bool
|| ReftV Symbol -> Bool
forall v. Eq v => ReftV v -> Bool
isTautoReft (SortedReft -> ReftV Symbol
sr_reft SortedReft
r)
    usedBinds :: IBindEnv
usedBinds      = (IBindEnv -> IBindEnv -> IBindEnv)
-> IBindEnv -> [IBindEnv] -> IBindEnv
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv IBindEnv
emptyIBindEnv ([IBindEnv]
cEnvs [IBindEnv] -> [IBindEnv] -> [IBindEnv]
forall a. [a] -> [a] -> [a]
++ [IBindEnv]
wEnvs)
    wEnvs :: [IBindEnv]
wEnvs          = WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv (WfC a -> IBindEnv) -> [WfC a] -> [IBindEnv]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar (WfC a) -> [WfC a]
forall k v. HashMap k v -> [v]
M.elems (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
fi)
    cEnvs :: [IBindEnv]
cEnvs          = SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv (SimpC a -> IBindEnv) -> [SimpC a] -> [IBindEnv]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId (SimpC a) -> [SimpC a]
forall k v. HashMap k v -> [v]
M.elems (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi)

data Ref
  = RB !BindId    -- ^ Bind identifier
  | RI !Integer   -- ^ Constraint identifier?
    deriving (Ref -> Ref -> Bool
(Ref -> Ref -> Bool) -> (Ref -> Ref -> Bool) -> Eq Ref
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ref -> Ref -> Bool
== :: Ref -> Ref -> Bool
$c/= :: Ref -> Ref -> Bool
/= :: Ref -> Ref -> Bool
Eq, (forall x. Ref -> Rep Ref x)
-> (forall x. Rep Ref x -> Ref) -> Generic Ref
forall x. Rep Ref x -> Ref
forall x. Ref -> Rep Ref x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Ref -> Rep Ref x
from :: forall x. Ref -> Rep Ref x
$cto :: forall x. Rep Ref x -> Ref
to :: forall x. Rep Ref x -> Ref
Generic)

instance NFData   Ref
instance Hashable Ref

-- | An `IdMap` stores for each constraint and BindId the
--   set of other BindIds that it references, i.e. those
--   where it needs to know when their names gets changed
type IdMap = M.HashMap Ref (S.HashSet BindId)

-- | A `RenameMap` maps an old name and sort to new name,
--   represented by a hashmap containing association lists.
--   `Nothing` as new name means the name is the same as the old.
type RenameMap = M.HashMap Symbol [(Sort, Maybe Symbol)]

--------------------------------------------------------------------------------
mkIdMap :: SInfo a -> IdMap
--------------------------------------------------------------------------------
mkIdMap :: forall a. SInfo a -> IdMap
mkIdMap SInfo a
fi = (IdMap -> SubcId -> SimpC a -> IdMap)
-> IdMap -> HashMap SubcId (SimpC a) -> IdMap
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' (BindEnv a -> IdMap -> SubcId -> SimpC a -> IdMap
forall a. BindEnv a -> IdMap -> SubcId -> SimpC a -> IdMap
updateIdMap (BindEnv a -> IdMap -> SubcId -> SimpC a -> IdMap)
-> BindEnv a -> IdMap -> SubcId -> SimpC a -> IdMap
forall a b. (a -> b) -> a -> b
$ SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) IdMap
forall k v. HashMap k v
M.empty (HashMap SubcId (SimpC a) -> IdMap)
-> HashMap SubcId (SimpC a) -> IdMap
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi

updateIdMap :: BindEnv a -> IdMap -> Integer -> SimpC a -> IdMap
updateIdMap :: forall a. BindEnv a -> IdMap -> SubcId -> SimpC a -> IdMap
updateIdMap BindEnv a
be IdMap
m SubcId
scId SimpC a
s = (HashSet BindId -> HashSet BindId -> HashSet BindId)
-> Ref -> HashSet BindId -> IdMap -> IdMap
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith HashSet BindId -> HashSet BindId -> HashSet BindId
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (SubcId -> Ref
RI SubcId
scId) HashSet BindId
refSet IdMap
m'
  where
    ids :: [BindId]
ids                 = IBindEnv -> [BindId]
elemsIBindEnv (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
s)
    nameMap :: HashMap Symbol BindId
nameMap             = [(Symbol, BindId)] -> HashMap Symbol BindId
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [((Symbol, SortedReft, a) -> Symbol
forall a b c. (a, b, c) -> a
fst3 ((Symbol, SortedReft, a) -> Symbol)
-> (Symbol, SortedReft, a) -> Symbol
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i BindEnv a
be, BindId
i) | BindId
i <- [BindId]
ids]
    m' :: IdMap
m'                  = (IdMap -> BindId -> IdMap) -> IdMap -> [BindId] -> IdMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (BindEnv a -> HashMap Symbol BindId -> IdMap -> BindId -> IdMap
forall a.
BindEnv a -> HashMap Symbol BindId -> IdMap -> BindId -> IdMap
insertIdIdLinks BindEnv a
be HashMap Symbol BindId
nameMap) IdMap
m [BindId]
ids
    symSet :: HashSet Symbol
symSet              = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (Expr -> [Symbol]) -> Expr -> [Symbol]
forall a b. (a -> b) -> a -> b
$ SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
s
    refSet :: HashSet BindId
refSet              = HashSet Symbol -> HashMap Symbol BindId -> HashSet BindId
namesToIds HashSet Symbol
symSet HashMap Symbol BindId
nameMap

insertIdIdLinks :: BindEnv a -> M.HashMap Symbol BindId -> IdMap -> BindId -> IdMap
insertIdIdLinks :: forall a.
BindEnv a -> HashMap Symbol BindId -> IdMap -> BindId -> IdMap
insertIdIdLinks BindEnv a
be HashMap Symbol BindId
nameMap IdMap
m BindId
i = (HashSet BindId -> HashSet BindId -> HashSet BindId)
-> Ref -> HashSet BindId -> IdMap -> IdMap
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith HashSet BindId -> HashSet BindId -> HashSet BindId
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (BindId -> Ref
RB BindId
i) HashSet BindId
refSet IdMap
m
  where
    sr :: SortedReft
sr     = (Symbol, SortedReft, a) -> SortedReft
forall a b c. (a, b, c) -> b
snd3 ((Symbol, SortedReft, a) -> SortedReft)
-> (Symbol, SortedReft, a) -> SortedReft
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i BindEnv a
be
    symSet :: HashSet Symbol
symSet = ReftV Symbol -> HashSet Symbol
reftFreeVars (ReftV Symbol -> HashSet Symbol) -> ReftV Symbol -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
    refSet :: HashSet BindId
refSet = HashSet Symbol -> HashMap Symbol BindId -> HashSet BindId
namesToIds HashSet Symbol
symSet HashMap Symbol BindId
nameMap

namesToIds :: S.HashSet Symbol -> M.HashMap Symbol BindId -> S.HashSet BindId
namesToIds :: HashSet Symbol -> HashMap Symbol BindId -> HashSet BindId
namesToIds HashSet Symbol
xs HashMap Symbol BindId
m = [BindId] -> HashSet BindId
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([BindId] -> HashSet BindId) -> [BindId] -> HashSet BindId
forall a b. (a -> b) -> a -> b
$ [Maybe BindId] -> [BindId]
forall a. [Maybe a] -> [a]
catMaybes [Symbol -> HashMap Symbol BindId -> Maybe BindId
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol BindId
m | Symbol
x <- HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
xs] --TODO why any Nothings?

--------------------------------------------------------------------------------
mkRenameMap :: BindEnv a -> RenameMap
--------------------------------------------------------------------------------
mkRenameMap :: forall a. BindEnv a -> RenameMap
mkRenameMap BindEnv a
be = (RenameMap -> BindId -> RenameMap)
-> RenameMap -> [BindId] -> RenameMap
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (BindEnv a -> RenameMap -> BindId -> RenameMap
forall a. BindEnv a -> RenameMap -> BindId -> RenameMap
addId BindEnv a
be) RenameMap
forall k v. HashMap k v
M.empty [BindId]
ids
  where
    ids :: [BindId]
ids = (BindId, (Symbol, SortedReft, a)) -> BindId
forall a b. (a, b) -> a
fst ((BindId, (Symbol, SortedReft, a)) -> BindId)
-> [(BindId, (Symbol, SortedReft, a))] -> [BindId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
forall a. BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
bindEnvToList BindEnv a
be

addId :: BindEnv a -> RenameMap -> BindId -> RenameMap
addId :: forall a. BindEnv a -> RenameMap -> BindId -> RenameMap
addId BindEnv a
be RenameMap
m BindId
i
  | Symbol -> RenameMap -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
sym RenameMap
m = RenameMap -> Symbol -> Sort -> BindId -> RenameMap
addDupId RenameMap
m Symbol
sym Sort
t BindId
i
  | Bool
otherwise      = Symbol -> [(Sort, Maybe Symbol)] -> RenameMap -> RenameMap
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
sym [(Sort
t, Maybe Symbol
forall a. Maybe a
Nothing)] RenameMap
m
  where
    t :: Sort
t              = SortedReft -> Sort
sr_sort SortedReft
sr
    (Symbol
sym, SortedReft
sr, a
_)   = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i BindEnv a
be

addDupId :: RenameMap -> Symbol -> Sort -> BindId -> RenameMap
addDupId :: RenameMap -> Symbol -> Sort -> BindId -> RenameMap
addDupId RenameMap
m Symbol
sym Sort
t BindId
i
  | Maybe (Maybe Symbol) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Maybe Symbol) -> Bool) -> Maybe (Maybe Symbol) -> Bool
forall a b. (a -> b) -> a -> b
$ Sort -> [(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Sort
t [(Sort, Maybe Symbol)]
mapping = RenameMap
m
  | Bool
otherwise                   = Symbol -> [(Sort, Maybe Symbol)] -> RenameMap -> RenameMap
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
sym ((Sort
t, Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Symbol -> Maybe Symbol) -> Symbol -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> BindId -> Symbol
renameSymbol Symbol
sym BindId
i) (Sort, Maybe Symbol)
-> [(Sort, Maybe Symbol)] -> [(Sort, Maybe Symbol)]
forall a. a -> [a] -> [a]
: [(Sort, Maybe Symbol)]
mapping) RenameMap
m
  where
    mapping :: [(Sort, Maybe Symbol)]
mapping = Maybe [(Sort, Maybe Symbol)] -> [(Sort, Maybe Symbol)]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [(Sort, Maybe Symbol)] -> [(Sort, Maybe Symbol)])
-> Maybe [(Sort, Maybe Symbol)] -> [(Sort, Maybe Symbol)]
forall a b. (a -> b) -> a -> b
$ Symbol -> RenameMap -> Maybe [(Sort, Maybe Symbol)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
sym RenameMap
m

--------------------------------------------------------------------------------
-- | `renameVars` seems to do the actual work of renaming all the binders
--   to use their sort-specific names.
--------------------------------------------------------------------------------
renameVars :: SInfo a -> RenameMap -> IdMap -> SInfo a
--------------------------------------------------------------------------------
renameVars :: forall a. SInfo a -> RenameMap -> IdMap -> SInfo a
renameVars SInfo a
fi RenameMap
rnMap IdMap
idMap = (SInfo a -> Ref -> HashSet BindId -> SInfo a)
-> SInfo a -> IdMap -> SInfo a
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' (RenameMap -> SInfo a -> Ref -> HashSet BindId -> SInfo a
forall a. RenameMap -> SInfo a -> Ref -> HashSet BindId -> SInfo a
updateRef RenameMap
rnMap) SInfo a
fi IdMap
idMap

updateRef :: RenameMap -> SInfo a -> Ref -> S.HashSet BindId -> SInfo a
updateRef :: forall a. RenameMap -> SInfo a -> Ref -> HashSet BindId -> SInfo a
updateRef RenameMap
rnMap SInfo a
fi Ref
rf HashSet BindId
bset = Subst -> SInfo a -> Ref -> SInfo a
forall a. Subst -> SInfo a -> Ref -> SInfo a
applySub ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
subs) SInfo a
fi Ref
rf
  where
    symTList :: [(Symbol, Sort)]
symTList = [ (Symbol
sym, SortedReft -> Sort
sr_sort SortedReft
sr) | BindId
i <- HashSet BindId -> [BindId]
forall a. HashSet a -> [a]
S.toList HashSet BindId
bset, let (Symbol
sym, SortedReft
sr, a
_) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i BindEnv a
bEnv]
    bEnv :: BindEnv a
bEnv     = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi
    subs :: [(Symbol, Expr)]
subs     = ((Symbol, Sort) -> Maybe (Symbol, Expr))
-> [(Symbol, Sort)] -> [(Symbol, Expr)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (RenameMap -> (Symbol, Sort) -> Maybe (Symbol, Expr)
mkSubUsing RenameMap
rnMap) [(Symbol, Sort)]
symTList

mkSubUsing :: RenameMap -> (Symbol, Sort) -> Maybe (Symbol, Expr)
mkSubUsing :: RenameMap -> (Symbol, Sort) -> Maybe (Symbol, Expr)
mkSubUsing RenameMap
m (Symbol
sym, Sort
t) = do
  Symbol
newName <- Maybe (Maybe Symbol) -> Maybe Symbol
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Maybe Symbol) -> Maybe Symbol)
-> Maybe (Maybe Symbol) -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Sort -> [(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Sort
t ([(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol))
-> [(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol)
forall a b. (a -> b) -> a -> b
$ RenameMap -> Symbol -> [(Sort, Maybe Symbol)]
forall k v.
(HasCallStack, Eq k, Show k, Hashable k) =>
HashMap k v -> k -> v
mlookup RenameMap
m Symbol
sym
  (Symbol, Expr) -> Maybe (Symbol, Expr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
sym, Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
newName)

applySub :: Subst -> SInfo a -> Ref -> SInfo a
applySub :: forall a. Subst -> SInfo a -> Ref -> SInfo a
applySub Subst
sub SInfo a
fi (RB BindId
i) = SInfo a
fi { bs = adjustBindEnv go i (bs fi) }
  where
    go :: (a, b) -> (a, b)
go (a
sym, b
sr)       = (a
sym, Subst -> b -> b
forall a. Subable a => Subst -> a -> a
subst Subst
sub b
sr)

applySub Subst
sub SInfo a
fi (RI SubcId
i) = SInfo a
fi { cm = M.adjust go i (cm fi) }
  where
    go :: SimpC a -> SimpC a
go SimpC a
c               = SimpC a
c { _crhs = subst sub (_crhs c) }

--------------------------------------------------------------------------------
renameBinds :: SInfo a -> RenameMap -> SInfo a
--------------------------------------------------------------------------------
renameBinds :: forall a. SInfo a -> RenameMap -> SInfo a
renameBinds SInfo a
fi RenameMap
m = SInfo a
fi { bs = bindEnvFromList $ renameBind m <$> beList }
  where
    beList :: [(BindId, (Symbol, SortedReft, a))]
beList       = BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
forall a. BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
bindEnvToList (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi)

renameBind :: RenameMap -> (BindId, (Symbol, SortedReft, a)) -> (BindId, (Symbol, SortedReft, a))
renameBind :: forall a.
RenameMap
-> (BindId, (Symbol, SortedReft, a))
-> (BindId, (Symbol, SortedReft, a))
renameBind RenameMap
m (BindId
i, (Symbol
sym, SortedReft
sr, a
ann))
  | Just Symbol
newSym <- Maybe Symbol
mnewSym = (BindId
i, (Symbol
newSym, SortedReft
sr, a
ann))
  | Bool
otherwise              = (BindId
i, (Symbol
sym,    SortedReft
sr, a
ann))
  where
    t :: Sort
t                      = SortedReft -> Sort
sr_sort SortedReft
sr
    mnewSym :: Maybe Symbol
mnewSym                = Maybe (Maybe Symbol) -> Maybe Symbol
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Maybe Symbol) -> Maybe Symbol)
-> Maybe (Maybe Symbol) -> Maybe Symbol
forall a b. (a -> b) -> a -> b
$ Sort -> [(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Sort
t ([(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol))
-> [(Sort, Maybe Symbol)] -> Maybe (Maybe Symbol)
forall a b. (a -> b) -> a -> b
$ RenameMap -> Symbol -> [(Sort, Maybe Symbol)]
forall k v.
(HasCallStack, Eq k, Show k, Hashable k) =>
HashMap k v -> k -> v
mlookup RenameMap
m Symbol
sym