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

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

-- | 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
  ( Expr(..)
  , 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
fi = do
  let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg [Char] -> [Char] -> [Char]
`addExtension` [Char]
"prettified"
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Saving prettified Query: "   forall a. [a] -> [a] -> [a]
++ [Char]
fq forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
fq
  [Char] -> [Char] -> IO ()
writeFile [Char]
fq forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (forall a. Fixpoint a => FInfo a -> Doc
prettyConstraints FInfo a
fi)

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

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 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. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
bId BindEnv a
bindEnv
            ]
      mergedEnv :: HashMap Symbol ([(Int, a)], SortedReft)
mergedEnv = forall m.
Semigroup m =>
[(Symbol, (m, SortedReft))] -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings [(Symbol, ([(Int, a)], SortedReft))]
env
      undoANFEnv :: HashMap Symbol ([(Int, a)], SortedReft)
undoANFEnv = forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANFAndVV HashMap Symbol ([(Int, a)], SortedReft)
mergedEnv
      boolSimplEnvDiff :: HashMap Symbol ([(Int, a)], SortedReft)
boolSimplEnvDiff = forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts HashMap Symbol ([(Int, a)], SortedReft)
undoANFEnv
      boolSimplEnv :: HashMap Symbol SortedReft
boolSimplEnv = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map forall a b. (a, b) -> b
snd 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 ([(Int, a)], SortedReft)
boolSimplEnvDiff HashMap Symbol ([(Int, a)], SortedReft)
undoANFEnv

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

      prunedEnv :: HashMap Symbol SortedReft
prunedEnv =
        if forall a. Expression a => a -> Expr
expr SortedReft
simplifiedRhs forall a. Eq a => a -> a -> Bool
/= Expr
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') =
        forall a.
HashMap Symbol SortedReft
-> SubC a -> ([(Symbol, SortedReft)], SubC a)
shortenVarNames HashMap Symbol SortedReft
prunedEnv SubC a
c { slhs :: SortedReft
slhs = SortedReft
simplifiedLhs, srhs :: SortedReft
srhs = SortedReft
simplifiedRhs }
      prettyEnv :: [(Text, SortedReft)]
prettyEnv =
        forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Text, SortedReft) -> (Text, Symbol, Sort, Expr)
bindingSelector forall a b. (a -> b) -> a -> b
$
        HashSet Symbol -> [(Symbol, SortedReft)] -> [(Text, SortedReft)]
eraseUnusedBindings (SortedReft -> SortedReft -> HashSet Symbol
constraintSymbols (forall a. SubC a -> SortedReft
slhs SubC a
c') (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 forall a b. (a -> b) -> a -> b
$
          [Char] -> Doc
text [Char]
"lhs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall a. SubC a -> SortedReft
slhs SubC a
c')
      Doc -> Doc -> Doc
$+$ [Char] -> Doc
text [Char]
"rhs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (forall a. SubC a -> SortedReft
srhs SubC a
c')
      Doc -> Doc -> Doc
$+$ forall a. Show a => Maybe a -> Doc
pprId (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
<+> forall a. Fixpoint a => a -> Doc
toFix (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
<+> forall a. Show a => Maybe a -> Doc
pprId (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c)) (forall a. Fixpoint a => a -> Doc
toFix (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 forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse Doc
"" forall a b. (a -> b) -> a -> b
$ Doc
elidedMessage forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Fixpoint a => (a, SortedReft) -> Doc
prettyBind [(Text, SortedReft)]
prettyEnv)
  where
    prettyBind :: (a, SortedReft) -> Doc
prettyBind (a
s, SortedReft
sr) = [Doc] -> Doc
sep [forall a. Fixpoint a => a -> Doc
toFix a
s Doc -> Doc -> Doc
<+> Doc
":", Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ SortedReft -> Doc
prettySortedRef SortedReft
sr]
    prettySortedRef :: SortedReft -> Doc
prettySortedRef SortedReft
sr = Doc -> Doc
braces forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
      [ forall a. Fixpoint a => a -> Doc
toFix (Reft -> Symbol
reftBind (SortedReft -> Reft
sr_reft SortedReft
sr)) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (SortedReft -> Sort
sr_sort SortedReft
sr) Doc -> Doc -> Doc
<+> Doc
"|"
      , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
conjuncts forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr
      ]

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

    constraintSymbols :: SortedReft -> SortedReft -> HashSet Symbol
constraintSymbols SortedReft
sr0 SortedReft
sr1 =
      forall a. (Eq a, Hashable 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
"{" forall a. Semigroup a => a -> a -> a
<> Text
s else Text
s
      , Reft -> Symbol
reftBind (SortedReft -> Reft
sr_reft SortedReft
sr)
      , SortedReft -> Sort
sr_sort SortedReft
sr
      , Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
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 (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 = forall a b. (a -> b) -> [a] -> [b]
map (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 = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union HashSet Symbol
ss HashSet Symbol
envSymbols
    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 (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Symbol, SortedReft)]
env

    reachable :: Symbol -> Text
reachable Symbol
s =
      if Symbol
s forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet Symbol
allSymbols then
        Symbol -> Text
symbolText Symbol
s
      else
        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
c =
  let bindsRenameMap :: HashMap Symbol Symbol
bindsRenameMap = [Symbol] -> HashMap Symbol Symbol
proposeRenamings forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [k]
HashMap.keys HashMap Symbol SortedReft
env
      env' :: [(Symbol, SortedReft)]
env' = forall a b. (a -> b) -> [a] -> [b]
map (HashMap Symbol Symbol
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
renameBind HashMap Symbol Symbol
bindsRenameMap) (forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol SortedReft
env)
   in
      ([(Symbol, SortedReft)]
env', forall a. HashMap Symbol Symbol -> SubC a -> SubC a
renameSubC HashMap Symbol Symbol
bindsRenameMap SubC a
c)
  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 =
      forall a.
IBindEnv
-> SortedReft -> SortedReft -> Maybe SubcId -> Tag -> a -> SubC a
mkSubC
        (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SubC a
c)
        (HashMap Symbol Symbol -> SortedReft -> SortedReft
renameSortedReft HashMap Symbol Symbol
symMap forall a b. (a -> b) -> a -> b
$ forall a. SubC a -> SortedReft
slhs SubC a
c)
        (HashMap Symbol Symbol -> SortedReft -> SortedReft
renameSortedReft HashMap Symbol Symbol
symMap forall a b. (a -> b) -> a -> b
$ forall a. SubC a -> SortedReft
srhs SubC a
c)
        (forall (c :: * -> *) a. TaggedC c a => c a -> Maybe SubcId
sid SubC a
c)
        (forall (c :: * -> *) a. TaggedC c a => c a -> Tag
stag SubC a
c)
        (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 Reft
r) =
      let sortSubst :: Symbol -> Sort
sortSubst = Symbol -> Sort
FObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
symMap
       in Sort -> Reft -> SortedReft
RR ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
sortSubst Sort
t) (HashMap Symbol Symbol -> Reft -> Reft
renameReft HashMap Symbol Symbol
symMap Reft
r)

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

    at :: HashMap Symbol Symbol -> Symbol -> Symbol
    at :: HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
m Symbol
k = forall a. a -> Maybe a -> a
fromMaybe Symbol
k forall a b. (a -> b) -> a -> b
$ 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 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 = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
HashMap.fromListWith (forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith forall a. [a] -> [a] -> [a]
(++))
  [ (Symbol
pfx, 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 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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
  [ (Symbol, Symbol)
r
  | (Symbol
pfx, HashMap Symbol [Symbol]
h) <- forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap Symbol (HashMap Symbol [Symbol])
prefixMap
  , (Symbol, Symbol)
r <- forall {b}. Symbol -> [(Symbol, [b])] -> [(b, Symbol)]
renameWithSuffixes Symbol
pfx (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)] -> forall {b}. Symbol -> (Symbol, [b]) -> [(b, Symbol)]
renameWithAppendages Symbol
pfx (Symbol
"", [b]
ss)
      [(Symbol, [b])]
sfxs -> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (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]
ss) = forall a b. [a] -> [b] -> [(a, b)]
zip [b]
ss forall a b. (a -> b) -> a -> b
$ case [b]
ss of
      [b
_s] -> [Symbol
pfx Symbol -> Symbol -> Symbol
`suffixIfNotNull` Symbol
sfx]
      [b]
ss -> forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (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` forall a. Symbolic a => a -> Symbol
symbol (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