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

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

import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
import qualified Data.List           as L
import           Data.Foldable       (foldl')
import           Data.Maybe          (catMaybes, fromJust, isJust)
import           Data.Hashable       (Hashable)
import           GHC.Generics        (Generic)
import           Control.Arrow       (second)
import           Control.DeepSeq     (NFData, ($!!))
-- import Debug.Trace (trace)

--------------------------------------------------------------------------------
renameAll    :: SInfo a -> SInfo a
--------------------------------------------------------------------------------
renameAll :: 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 -> RenameMap
mkRenameMap (BindEnv -> RenameMap) -> BindEnv -> RenameMap
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
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 :: SInfo a -> SInfo a
dropUnusedBinds SInfo a
fi = SInfo a
fi {bs :: BindEnv
bs = (BindId -> Symbol -> SortedReft -> Bool) -> BindEnv -> BindEnv
filterBindEnv BindId -> Symbol -> SortedReft -> Bool
forall r p. Reftable r => BindId -> p -> r -> Bool
isUsed (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs SInfo a
fi)}-- { bs = mapBindEnv tx (bs fi) }
  where
    -- _tx i (x, r)
    -- | isUsed i    = (x, r)
    -- | otherwise   = (x, top r)
    isUsed :: BindId -> p -> r -> Bool
isUsed BindId
i p
_x r
r  = {- tracepp (unwords ["isUsed", show i, showpp _x]) $ -} BindId -> IBindEnv -> Bool
memberIBindEnv BindId
i IBindEnv
usedBinds Bool -> Bool -> Bool
|| r -> Bool
forall r. Reftable r => r -> Bool
isTauto r
r
    usedBinds :: IBindEnv
usedBinds      = (IBindEnv -> IBindEnv -> IBindEnv)
-> IBindEnv -> [IBindEnv] -> IBindEnv
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
/= :: Ref -> Ref -> Bool
$c/= :: Ref -> Ref -> Bool
== :: Ref -> Ref -> Bool
$c== :: 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
$cto :: forall x. Rep Ref x -> Ref
$cfrom :: forall x. Ref -> Rep Ref x
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 :: 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 -> IdMap -> SubcId -> SimpC a -> IdMap
forall a. BindEnv -> IdMap -> SubcId -> SimpC a -> IdMap
updateIdMap (BindEnv -> IdMap -> SubcId -> SimpC a -> IdMap)
-> BindEnv -> IdMap -> SubcId -> SimpC a -> IdMap
forall a b. (a -> b) -> a -> b
$ SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
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 -> IdMap -> Integer -> SimpC a -> IdMap
updateIdMap :: BindEnv -> IdMap -> SubcId -> SimpC a -> IdMap
updateIdMap BindEnv
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, Hashable 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) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SortedReft) -> Symbol) -> (Symbol, SortedReft) -> Symbol
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
i BindEnv
be, BindId
i) | BindId
i <- [BindId]
ids]
    m' :: IdMap
m'                  = (IdMap -> BindId -> IdMap) -> IdMap -> [BindId] -> IdMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (BindEnv -> HashMap Symbol BindId -> IdMap -> BindId -> IdMap
insertIdIdLinks BindEnv
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 -> M.HashMap Symbol BindId -> IdMap -> BindId -> IdMap
insertIdIdLinks :: BindEnv -> HashMap Symbol BindId -> IdMap -> BindId -> IdMap
insertIdIdLinks BindEnv
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, Hashable 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) -> SortedReft
forall a b. (a, b) -> b
snd ((Symbol, SortedReft) -> SortedReft)
-> (Symbol, SortedReft) -> SortedReft
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
i BindEnv
be
    symSet :: HashSet Symbol
symSet = Reft -> HashSet Symbol
reftFreeVars (Reft -> HashSet Symbol) -> Reft -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
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 -> RenameMap
--------------------------------------------------------------------------------
mkRenameMap :: BindEnv -> RenameMap
mkRenameMap BindEnv
be = (RenameMap -> BindId -> RenameMap)
-> RenameMap -> [BindId] -> RenameMap
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (BindEnv -> RenameMap -> BindId -> RenameMap
addId BindEnv
be) RenameMap
forall k v. HashMap k v
M.empty [BindId]
ids
  where
    ids :: [BindId]
ids = (BindId, Symbol, SortedReft) -> BindId
forall a b c. (a, b, c) -> a
fst3 ((BindId, Symbol, SortedReft) -> BindId)
-> [(BindId, Symbol, SortedReft)] -> [BindId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BindEnv -> [(BindId, Symbol, SortedReft)]
bindEnvToList BindEnv
be

addId :: BindEnv -> RenameMap -> BindId -> RenameMap
addId :: BindEnv -> RenameMap -> BindId -> RenameMap
addId BindEnv
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
    (Symbol
sym, Sort
t)       = (SortedReft -> Sort) -> (Symbol, SortedReft) -> (Symbol, Sort)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second SortedReft -> Sort
sr_sort ((Symbol, SortedReft) -> (Symbol, Sort))
-> (Symbol, SortedReft) -> (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
i BindEnv
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 :: 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 :: 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 = [(SortedReft -> Sort) -> (Symbol, SortedReft) -> (Symbol, Sort)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second SortedReft -> Sort
sr_sort ((Symbol, SortedReft) -> (Symbol, Sort))
-> (Symbol, SortedReft) -> (Symbol, Sort)
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
i (BindEnv -> (Symbol, SortedReft))
-> BindEnv -> (Symbol, SortedReft)
forall a b. (a -> b) -> a -> b
$ SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs SInfo a
fi | BindId
i <- HashSet BindId -> [BindId]
forall a. HashSet a -> [a]
S.toList HashSet BindId
bset]
    subs :: [(Symbol, Expr)]
subs     = [Maybe (Symbol, Expr)] -> [(Symbol, Expr)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Symbol, Expr)] -> [(Symbol, Expr)])
-> [Maybe (Symbol, Expr)] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ RenameMap -> (Symbol, Sort) -> Maybe (Symbol, Expr)
mkSubUsing RenameMap
rnMap ((Symbol, Sort) -> Maybe (Symbol, Expr))
-> [(Symbol, Sort)] -> [Maybe (Symbol, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(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 (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 :: Subst -> SInfo a -> Ref -> SInfo a
applySub Subst
sub SInfo a
fi (RB BindId
i) = SInfo a
fi { bs :: BindEnv
bs = ((Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindId -> BindEnv -> BindEnv
adjustBindEnv (Symbol, SortedReft) -> (Symbol, SortedReft)
forall b a. Subable b => (a, b) -> (a, b)
go BindId
i (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs SInfo a
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 :: HashMap SubcId (SimpC a)
cm = (SimpC a -> SimpC a)
-> SubcId -> HashMap SubcId (SimpC a) -> HashMap SubcId (SimpC a)
forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust SimpC a -> SimpC a
forall a. SimpC a -> SimpC a
go SubcId
i (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi) }
  where
    go :: SimpC a -> SimpC a
go SimpC a
c               = SimpC a
c { _crhs :: Expr
_crhs = Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
sub (SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
c) }

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

renameBind :: RenameMap -> (BindId, Symbol, SortedReft) -> (BindId, Symbol, SortedReft)
renameBind :: RenameMap
-> (BindId, Symbol, SortedReft) -> (BindId, Symbol, SortedReft)
renameBind RenameMap
m (BindId
i, Symbol
sym, SortedReft
sr)
  | Just Symbol
newSym <- Maybe Symbol
mnewSym = (BindId
i, Symbol
newSym, SortedReft
sr)
  | Bool
otherwise              = (BindId
i, Symbol
sym,    SortedReft
sr)
  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