{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Functions to make environments easier to read
module Language.Fixpoint.Solver.Prettify (savePrettifiedQuery) where

import           Data.Bifunctor (first)
import           Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as HashMap
import           Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import           Data.List (intersperse, sortOn)
import           Data.Maybe (fromMaybe)
import           Data.Text (Text)
import qualified Data.Text as Text
import           Language.Fixpoint.Misc (ensurePath)
import           Language.Fixpoint.Solver.EnvironmentReduction
  ( dropLikelyIrrelevantBindings
  , inlineInSortedReft
  , mergeDuplicatedBindings
  , simplifyBooleanRefts
  , undoANFAndVV
  )
import           Language.Fixpoint.Types.Config (Config, queryFile)
import           Language.Fixpoint.Types.Constraints
import           Language.Fixpoint.Types.Environments
  (BindEnv, elemsIBindEnv, lookupBindEnv)
import           Language.Fixpoint.Types.Names
  ( Symbol
  , dropPrefixOfSym
  , prefixOfSym
  , suffixOfSym
  , suffixSymbol
  , symbol
  , symbolText
  )
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Refinements
  ( ExprV(..)
  , pattern PFalse
  , Reft
  , SortedReft(..)
  , conjuncts
  , expr
  , reft
  , reftBind
  , reftPred
  , sortedReftSymbols
  , substf
  , substSortInExpr
  )
import           Language.Fixpoint.Types.Sorts (Sort(..), substSort)
import           Language.Fixpoint.Types.Substitutions (exprSymbolsSet)
import qualified Language.Fixpoint.Utils.Files as Files
import           System.FilePath (addExtension)
import           Text.PrettyPrint.HughesPJ.Compat
  (Doc, braces, hang, nest, render, sep, text, vcat, (<+>), ($+$))


savePrettifiedQuery :: Fixpoint a => Config -> FInfo a -> IO ()
savePrettifiedQuery :: forall a. Fixpoint a => Config -> FInfo a -> IO ()
savePrettifiedQuery Config
cfg FInfo a
info = do
  let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg [Char] -> [Char] -> [Char]
`addExtension` [Char]
"prettified"
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Saving prettified Query: "   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
fq
  [Char] -> [Char] -> IO ()
writeFile [Char]
fq ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (FInfo a -> Doc
forall a. Fixpoint a => FInfo a -> Doc
prettyConstraints FInfo a
info)

prettyConstraints :: Fixpoint a => FInfo a -> Doc
prettyConstraints :: forall a. Fixpoint a => FInfo a -> Doc
prettyConstraints FInfo a
info =
  [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  ((SubcId, SubC a) -> Doc) -> [(SubcId, SubC a)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map
    (BindEnv a -> SubC a -> Doc
forall a. Fixpoint a => BindEnv a -> SubC a -> Doc
prettyConstraint (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
info) (SubC a -> Doc)
-> ((SubcId, SubC a) -> SubC a) -> (SubcId, SubC a) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SubcId, SubC a) -> SubC a
forall a b. (a, b) -> b
snd)
    (((SubcId, SubC a) -> SubcId)
-> [(SubcId, SubC a)] -> [(SubcId, SubC a)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (SubcId, SubC a) -> SubcId
forall a b. (a, b) -> a
fst ([(SubcId, SubC a)] -> [(SubcId, SubC a)])
-> [(SubcId, SubC a)] -> [(SubcId, SubC a)]
forall a b. (a -> b) -> a -> b
$ HashMap SubcId (SubC a) -> [(SubcId, SubC a)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList (FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
info))

prettyConstraint
  :: Fixpoint a
  => BindEnv a
  -> SubC a
  -> Doc
prettyConstraint :: forall a. Fixpoint a => BindEnv a -> SubC a -> Doc
prettyConstraint BindEnv a
bindEnv SubC a
c =
  let env :: [(Symbol, ([(Int, a)], SortedReft))]
env = [ (Symbol
s, ([(Int
bId, a
a)], SortedReft
sr))
            | Int
bId <- IBindEnv -> Tag
elemsIBindEnv (IBindEnv -> Tag) -> IBindEnv -> Tag
forall a b. (a -> b) -> a -> b
$ SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c
            , let (Symbol
s, SortedReft
sr, a
a) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
bId BindEnv a
bindEnv
            ]
      mergedEnv :: HashMap Symbol ([(Int, a)], SortedReft)
mergedEnv = [(Symbol, ([(Int, a)], SortedReft))]
-> HashMap Symbol ([(Int, a)], SortedReft)
forall m.
Semigroup m =>
[(Symbol, (m, SortedReft))] -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings [(Symbol, ([(Int, a)], SortedReft))]
env
      undoANFEnv :: HashMap Symbol ([(Int, a)], SortedReft)
undoANFEnv = HashMap Symbol ([(Int, a)], SortedReft)
-> HashMap Symbol ([(Int, a)], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFAndVV HashMap Symbol ([(Int, a)], SortedReft)
mergedEnv
      boolSimplEnvDiff :: HashMap Symbol ([(Int, a)], SortedReft)
boolSimplEnvDiff = HashMap Symbol ([(Int, a)], SortedReft)
-> HashMap Symbol ([(Int, a)], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts HashMap Symbol ([(Int, a)], SortedReft)
undoANFEnv
      boolSimplEnv :: HashMap Symbol SortedReft
boolSimplEnv = (([(Int, a)], SortedReft) -> SortedReft)
-> HashMap Symbol ([(Int, a)], SortedReft)
-> HashMap Symbol SortedReft
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map ([(Int, a)], SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd (HashMap Symbol ([(Int, a)], SortedReft)
 -> HashMap Symbol SortedReft)
-> HashMap Symbol ([(Int, a)], SortedReft)
-> HashMap Symbol SortedReft
forall a b. (a -> b) -> a -> b
$ HashMap Symbol ([(Int, a)], SortedReft)
-> HashMap Symbol ([(Int, a)], SortedReft)
-> HashMap Symbol ([(Int, a)], SortedReft)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
HashMap.union HashMap Symbol ([(Int, a)], SortedReft)
boolSimplEnvDiff HashMap Symbol ([(Int, a)], SortedReft)
undoANFEnv

      simplifiedLhs :: SortedReft
simplifiedLhs = SortedReft -> SortedReft
forall a. Fixpoint a => a -> a
simplify (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Maybe SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft (Symbol -> HashMap Symbol SortedReft -> Maybe SortedReft
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`HashMap.lookup` HashMap Symbol SortedReft
boolSimplEnv) (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c)
      simplifiedRhs :: SortedReft
simplifiedRhs = SortedReft -> SortedReft
forall a. Fixpoint a => a -> a
simplify (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Maybe SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft (Symbol -> HashMap Symbol SortedReft -> Maybe SortedReft
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`HashMap.lookup` HashMap Symbol SortedReft
boolSimplEnv) (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)

      prunedEnv :: HashMap Symbol SortedReft
prunedEnv =
        if SortedReft -> Expr
forall a. Expression a => a -> Expr
expr SortedReft
simplifiedRhs Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
forall v. ExprV v
PFalse then
          HashSet Symbol
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
dropLikelyIrrelevantBindings
            (SortedReft -> SortedReft -> HashSet Symbol
constraintSymbols SortedReft
simplifiedLhs SortedReft
simplifiedRhs)
            HashMap Symbol SortedReft
boolSimplEnv
        else
          HashMap Symbol SortedReft
boolSimplEnv
      ([(Symbol, SortedReft)]
renamedEnv, SubC a
c') =
        HashMap Symbol SortedReft
-> SubC a -> ([(Symbol, SortedReft)], SubC a)
forall a.
HashMap Symbol SortedReft
-> SubC a -> ([(Symbol, SortedReft)], SubC a)
shortenVarNames HashMap Symbol SortedReft
prunedEnv SubC a
c { slhs = simplifiedLhs, srhs = simplifiedRhs }
      prettyEnv :: [(Text, SortedReft)]
prettyEnv =
        ((Text, SortedReft) -> (Text, Symbol, Sort, Expr))
-> [(Text, SortedReft)] -> [(Text, SortedReft)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Text, SortedReft) -> (Text, Symbol, Sort, Expr)
bindingSelector ([(Text, SortedReft)] -> [(Text, SortedReft)])
-> [(Text, SortedReft)] -> [(Text, SortedReft)]
forall a b. (a -> b) -> a -> b
$
        HashSet Symbol -> [(Symbol, SortedReft)] -> [(Text, SortedReft)]
eraseUnusedBindings (SortedReft -> SortedReft -> HashSet Symbol
constraintSymbols (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c') (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c')) [(Symbol, SortedReft)]
renamedEnv
   in Doc -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"\n\nconstraint:") Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
          [Char] -> Doc
text [Char]
"lhs" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c')
      Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c')
      Doc -> Doc -> Doc
$+$ Maybe SubcId -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c) Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
"tag" Doc -> Doc -> Doc
<+> Tag -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
c)
      Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta ([Char] -> Doc
text [Char]
"constraint" Doc -> Doc -> Doc
<+> Maybe SubcId -> Doc
forall a. Show a => Maybe a -> Doc
pprId (SubC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c)) (a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c))
      Doc -> Doc -> Doc
$+$ Doc -> Int -> Doc -> Doc
hang ([Char] -> Doc
text [Char]
"environment:") Int
2
            ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
intersperse Doc
"" ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Doc
elidedMessage Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Text, SortedReft) -> Doc) -> [(Text, SortedReft)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Text, SortedReft) -> Doc
forall {a}. Fixpoint a => (a, SortedReft) -> Doc
prettyBind [(Text, SortedReft)]
prettyEnv)
  where
    prettyBind :: (a, SortedReft) -> Doc
prettyBind (a
s, SortedReft
sr) = [Doc] -> Doc
sep [a -> Doc
forall a. Fixpoint a => a -> Doc
toFix a
s Doc -> Doc -> Doc
<+> Doc
":", Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ SortedReft -> Doc
prettySortedRef SortedReft
sr]
    prettySortedRef :: SortedReft -> Doc
prettySortedRef SortedReft
sr = Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
      [ Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind (SortedReft -> ReftV Symbol
sr_reft SortedReft
sr)) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SortedReft -> Sort
sr_sort SortedReft
sr) Doc -> Doc -> Doc
<+> Doc
"|"
      , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Expr] -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([Expr] -> Doc) -> [Expr] -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts (Expr -> [Expr]) -> Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr) -> ReftV Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
      ]

    elidedMessage :: Doc
elidedMessage = Doc
"// elided some likely irrelevant bindings"

    constraintSymbols :: SortedReft -> SortedReft -> HashSet Symbol
constraintSymbols SortedReft
sr0 SortedReft
sr1 =
      HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union (SortedReft -> HashSet Symbol
sortedReftSymbols SortedReft
sr0) (SortedReft -> HashSet Symbol
sortedReftSymbols SortedReft
sr1)

    -- Sort by symbol then reft
    bindingSelector :: (Text, SortedReft) -> (Text, Symbol, Sort, Expr)
bindingSelector (Text
s, SortedReft
sr) =
      ( -- put unused symbols at the end
        if Text
"_" Text -> Text -> Bool
`Text.isPrefixOf` Text
s then Text
"{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s else Text
s
      , ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind (SortedReft -> ReftV Symbol
sr_reft SortedReft
sr)
      , SortedReft -> Sort
sr_sort SortedReft
sr
      , ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr) -> ReftV Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft SortedReft
sr
      )

pprId :: Show a => Maybe a -> Doc
pprId :: forall a. Show a => Maybe a -> Doc
pprId (Just a
i)  = Doc
"id" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (a -> [Char]
forall a. Show a => a -> [Char]
show a
i)
pprId Maybe a
_         = Doc
""

toFixMeta :: Doc -> Doc -> Doc
toFixMeta :: Doc -> Doc -> Doc
toFixMeta Doc
k Doc
v = [Char] -> Doc
text [Char]
"// META" Doc -> Doc -> Doc
<+> Doc
k Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
":" Doc -> Doc -> Doc
<+> Doc
v

-- | @eraseUnusedBindings ss env@ prefixes with @_@ the symbols that aren't
-- refered from @ss@ or refinement types in the environment.
eraseUnusedBindings
  :: HashSet Symbol -> [(Symbol, SortedReft)] -> [(Text, SortedReft)]
eraseUnusedBindings :: HashSet Symbol -> [(Symbol, SortedReft)] -> [(Text, SortedReft)]
eraseUnusedBindings HashSet Symbol
ss [(Symbol, SortedReft)]
env = ((Symbol, SortedReft) -> (Text, SortedReft))
-> [(Symbol, SortedReft)] -> [(Text, SortedReft)]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> Text) -> (Symbol, SortedReft) -> (Text, SortedReft)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Symbol -> Text
reachable) [(Symbol, SortedReft)]
env
  where
    allSymbols :: HashSet Symbol
allSymbols = HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
ss HashSet Symbol
envSymbols
    envSymbols :: HashSet Symbol
envSymbols =
      [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
HashSet.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$
      ((Symbol, SortedReft) -> HashSet Symbol)
-> [(Symbol, SortedReft)] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> HashSet Symbol
exprSymbolsSet (Expr -> HashSet Symbol)
-> ((Symbol, SortedReft) -> Expr)
-> (Symbol, SortedReft)
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr)
-> ((Symbol, SortedReft) -> ReftV Symbol)
-> (Symbol, SortedReft)
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> ReftV Symbol
sr_reft (SortedReft -> ReftV Symbol)
-> ((Symbol, SortedReft) -> SortedReft)
-> (Symbol, SortedReft)
-> ReftV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd) [(Symbol, SortedReft)]
env

    reachable :: Symbol -> Text
reachable Symbol
s =
      if Symbol
s Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet Symbol
allSymbols then
        Symbol -> Text
symbolText Symbol
s
      else
        Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Symbol -> Text
symbolText Symbol
s

-- | Shortens the names of refinements types in a given environment
-- and constraint
shortenVarNames
  :: HashMap Symbol SortedReft
  -> SubC a
  -> ([(Symbol, SortedReft)], SubC a)
shortenVarNames :: forall a.
HashMap Symbol SortedReft
-> SubC a -> ([(Symbol, SortedReft)], SubC a)
shortenVarNames HashMap Symbol SortedReft
env SubC a
subc =
  let bindsRenameMap :: HashMap Symbol Symbol
bindsRenameMap = [Symbol] -> HashMap Symbol Symbol
proposeRenamings ([Symbol] -> HashMap Symbol Symbol)
-> [Symbol] -> HashMap Symbol Symbol
forall a b. (a -> b) -> a -> b
$ HashMap Symbol SortedReft -> [Symbol]
forall k v. HashMap k v -> [k]
HashMap.keys HashMap Symbol SortedReft
env
      env' :: [(Symbol, SortedReft)]
env' = ((Symbol, SortedReft) -> (Symbol, SortedReft))
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> [a] -> [b]
map (HashMap Symbol Symbol
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
renameBind HashMap Symbol Symbol
bindsRenameMap) (HashMap Symbol SortedReft -> [(Symbol, SortedReft)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol SortedReft
env)
   in
      ([(Symbol, SortedReft)]
env', HashMap Symbol Symbol -> SubC a -> SubC a
forall a. HashMap Symbol Symbol -> SubC a -> SubC a
renameSubC HashMap Symbol Symbol
bindsRenameMap SubC a
subc)
  where
    renameSubC :: HashMap Symbol Symbol -> SubC a -> SubC a
    renameSubC :: forall a. HashMap Symbol Symbol -> SubC a -> SubC a
renameSubC HashMap Symbol Symbol
symMap SubC a
c =
      IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> Tag -> a -> SubC a
forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> Tag -> a -> SubC a
mkSubC
        (SubC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
        (HashMap Symbol Symbol -> SortedReft -> SortedReft
renameSortedReft HashMap Symbol Symbol
symMap (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c)
        (HashMap Symbol Symbol -> SortedReft -> SortedReft
renameSortedReft HashMap Symbol Symbol
symMap (SortedReft -> SortedReft) -> SortedReft -> SortedReft
forall a b. (a -> b) -> a -> b
$ SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)
        (SubC a -> Maybe SubcId
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c)
        (SubC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
c)
        (SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c)

    renameBind
      :: HashMap Symbol Symbol -> (Symbol, SortedReft) -> (Symbol, SortedReft)
    renameBind :: HashMap Symbol Symbol
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
renameBind HashMap Symbol Symbol
symMap (Symbol
s, SortedReft
sr) =
      (HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
symMap Symbol
s, HashMap Symbol Symbol -> SortedReft -> SortedReft
renameSortedReft HashMap Symbol Symbol
symMap SortedReft
sr)

    renameSortedReft
      :: HashMap Symbol Symbol -> SortedReft -> SortedReft
    renameSortedReft :: HashMap Symbol Symbol -> SortedReft -> SortedReft
renameSortedReft HashMap Symbol Symbol
symMap (RR Sort
t ReftV Symbol
r) =
      let sortSubst :: Symbol -> Sort
sortSubst = Symbol -> Sort
FObj (Symbol -> Sort) -> (Symbol -> Symbol) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
symMap
       in Sort -> ReftV Symbol -> SortedReft
RR ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
sortSubst Sort
t) (HashMap Symbol Symbol -> ReftV Symbol -> ReftV Symbol
renameReft HashMap Symbol Symbol
symMap ReftV Symbol
r)

    renameReft :: HashMap Symbol Symbol -> Reft -> Reft
    renameReft :: HashMap Symbol Symbol -> ReftV Symbol -> ReftV Symbol
renameReft HashMap Symbol Symbol
symMap ReftV Symbol
r =
      let m :: HashMap Symbol Symbol
m = Symbol -> Symbol -> HashMap Symbol Symbol -> HashMap Symbol Symbol
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r) (Symbol -> Symbol
prefixOfSym (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r) HashMap Symbol Symbol
symMap
          sortSubst :: Symbol -> Sort
sortSubst = Symbol -> Sort
FObj (Symbol -> Sort) -> (Symbol -> Symbol) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
symMap
       in Symbol -> Expr -> ReftV Symbol
forall v. Symbol -> ExprV v -> ReftV v
reft (HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
m (ReftV Symbol -> Symbol
forall v. ReftV v -> Symbol
reftBind ReftV Symbol
r)) (Expr -> ReftV Symbol) -> Expr -> ReftV Symbol
forall a b. (a -> b) -> a -> b
$
            (Symbol -> Sort) -> Expr -> Expr
substSortInExpr Symbol -> Sort
sortSubst (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$
            (Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> (Symbol -> Symbol) -> Symbol -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
m) (ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred ReftV Symbol
r)

    at :: HashMap Symbol Symbol -> Symbol -> Symbol
    at :: HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
m Symbol
k = Symbol -> Maybe Symbol -> Symbol
forall a. a -> Maybe a -> a
fromMaybe Symbol
k (Maybe Symbol -> Symbol) -> Maybe Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol Symbol -> Maybe Symbol
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup Symbol
k HashMap Symbol Symbol
m

-- | Given a list of symbols with no duplicates, it proposes shorter
-- names to use for them.
--
-- All proposals preserve the prefix of the original name. A prefix is
-- the longest substring containing the initial character and no separator
-- ## ('symSepName').
--
-- Suffixes are preserved, except when symbols with a given prefix always
-- use the same suffix.
--
proposeRenamings :: [Symbol] -> HashMap Symbol Symbol
proposeRenamings :: [Symbol] -> HashMap Symbol Symbol
proposeRenamings = HashMap Symbol (HashMap Symbol [Symbol]) -> HashMap Symbol Symbol
toSymMap (HashMap Symbol (HashMap Symbol [Symbol]) -> HashMap Symbol Symbol)
-> ([Symbol] -> HashMap Symbol (HashMap Symbol [Symbol]))
-> [Symbol]
-> HashMap Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> HashMap Symbol (HashMap Symbol [Symbol])
toPrefixSuffixMap

-- | Indexes symbols by prefix and then by suffix. If the prefix
-- equals the symbol, then the suffix is the empty symbol.
--
-- For instance,
--
-- > toPrefixSuffixMap ["a##b##c"] ! "a" ! "c" == ["a##b##c"]
-- > toPrefixSuffixMap ["a"] ! "a" ! "" == ["a"]
--
-- In general,
--
-- > forall ss.
-- > Set.fromList ss == Set.fromList $ concat [ xs | m <- elems (toPrefixSuffixMap ss), xs <- elems m ]
--
-- > forall ss.
-- > and [ all (pfx `isPrefixOfSym`) xs && all (sfx `isSuffixOfSym`) xs
-- >     | (pfx, m) <- toList (toPrefixSuffixMap ss)
-- >     , (sfx, xs) <- toList m
-- >     ]
--
-- TODO: put the above in unit tests
--
toPrefixSuffixMap :: [Symbol] -> HashMap Symbol (HashMap Symbol [Symbol])
toPrefixSuffixMap :: [Symbol] -> HashMap Symbol (HashMap Symbol [Symbol])
toPrefixSuffixMap [Symbol]
xs = (HashMap Symbol [Symbol]
 -> HashMap Symbol [Symbol] -> HashMap Symbol [Symbol])
-> [(Symbol, HashMap Symbol [Symbol])]
-> HashMap Symbol (HashMap Symbol [Symbol])
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith (([Symbol] -> [Symbol] -> [Symbol])
-> HashMap Symbol [Symbol]
-> HashMap Symbol [Symbol]
-> HashMap Symbol [Symbol]
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
(++))
  [ (Symbol
pfx, Symbol -> [Symbol] -> HashMap Symbol [Symbol]
forall k v. Hashable k => k -> v -> HashMap k v
HashMap.singleton Symbol
sfx [Symbol
s])
  | Symbol
s <- [Symbol]
xs
  , let pfx :: Symbol
pfx = Symbol -> Symbol
prefixOfSym Symbol
s
        sfx :: Symbol
sfx = Symbol -> Symbol
suffixOfSym (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
dropPrefixOfSym Symbol
s
  ]

-- | Suggests renamings for every symbol in a given prefix/suffix map.
toSymMap :: HashMap Symbol (HashMap Symbol [Symbol]) -> HashMap Symbol Symbol
toSymMap :: HashMap Symbol (HashMap Symbol [Symbol]) -> HashMap Symbol Symbol
toSymMap HashMap Symbol (HashMap Symbol [Symbol])
prefixMap = [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
  [ (Symbol, Symbol)
r
  | (Symbol
pfx, HashMap Symbol [Symbol]
h) <- HashMap Symbol (HashMap Symbol [Symbol])
-> [(Symbol, HashMap Symbol [Symbol])]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol (HashMap Symbol [Symbol])
prefixMap
  , (Symbol, Symbol)
r <- Symbol -> [(Symbol, [Symbol])] -> [(Symbol, Symbol)]
forall {b}. Symbol -> [(Symbol, [b])] -> [(b, Symbol)]
renameWithSuffixes Symbol
pfx (HashMap Symbol [Symbol] -> [(Symbol, [Symbol])]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol [Symbol]
h)
  ]
  where
    renameWithSuffixes :: Symbol -> [(Symbol, [b])] -> [(b, Symbol)]
renameWithSuffixes Symbol
pfx = \case
      [(Symbol
_sfx, [b]
ss)] -> Symbol -> (Symbol, [b]) -> [(b, Symbol)]
forall {b}. Symbol -> (Symbol, [b]) -> [(b, Symbol)]
renameWithAppendages Symbol
pfx (Symbol
"", [b]
ss)
      [(Symbol, [b])]
sfxs -> ((Symbol, [b]) -> [(b, Symbol)])
-> [(Symbol, [b])] -> [(b, Symbol)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol -> (Symbol, [b]) -> [(b, Symbol)]
forall {b}. Symbol -> (Symbol, [b]) -> [(b, Symbol)]
renameWithAppendages Symbol
pfx) [(Symbol, [b])]
sfxs

    renameWithAppendages :: Symbol -> (Symbol, [b]) -> [(b, Symbol)]
renameWithAppendages Symbol
pfx (Symbol
sfx, [b]
xs) = [b] -> [Symbol] -> [(b, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [b]
xs ([Symbol] -> [(b, Symbol)]) -> [Symbol] -> [(b, Symbol)]
forall a b. (a -> b) -> a -> b
$ case [b]
xs of
      [b
_s] -> [Symbol
pfx Symbol -> Symbol -> Symbol
`suffixIfNotNull` Symbol
sfx]
      [b]
ss -> (SubcId -> b -> Symbol) -> [SubcId] -> [b] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Symbol -> Symbol -> SubcId -> b -> Symbol
forall {a} {p}. Show a => Symbol -> Symbol -> a -> p -> Symbol
rename Symbol
pfx Symbol
sfx) [SubcId
1 :: Integer ..] [b]
ss

    rename :: Symbol -> Symbol -> a -> p -> Symbol
rename Symbol
pfx Symbol
sfx a
i p
_s =
      Symbol
pfx Symbol -> Symbol -> Symbol
`suffixIfNotNull` Symbol
sfx Symbol -> Symbol -> Symbol
`suffixSymbol` [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (a -> [Char]
forall a. Show a => a -> [Char]
show a
i)

    suffixIfNotNull :: Symbol -> Symbol -> Symbol
suffixIfNotNull Symbol
a Symbol
b =
      if Text -> Bool
Text.null (Symbol -> Text
symbolText Symbol
b) then Symbol
a else Symbol
a Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol
b