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

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

prettyConstraints :: Fixpoint a => FInfo a -> Doc
prettyConstraints :: FInfo a -> Doc
prettyConstraints FInfo a
fi =
  [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
  (SubC a -> Doc) -> [SubC a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (BindEnv -> SubC a -> Doc
forall a. Fixpoint a => BindEnv -> SubC a -> Doc
prettyConstraint (FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi)) ([SubC a] -> [Doc]) -> [SubC a] -> [Doc]
forall a b. (a -> b) -> a -> b
$
  ((SubcId, SubC a) -> SubC a) -> [(SubcId, SubC a)] -> [SubC a]
forall a b. (a -> b) -> [a] -> [b]
map (SubcId, SubC a) -> SubC a
forall a b. (a, b) -> b
snd ([(SubcId, SubC a)] -> [SubC a]) -> [(SubcId, SubC a)] -> [SubC a]
forall a b. (a -> b) -> a -> b
$
  ((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
fi)

prettyConstraint
  :: Fixpoint a
  => BindEnv
  -> SubC a
  -> Doc
prettyConstraint :: BindEnv -> SubC a -> Doc
prettyConstraint BindEnv
bindEnv SubC a
c =
  let env :: [(Symbol, ([BindId], SortedReft))]
env = [ (Symbol
s, ([BindId
bId], SortedReft
sr))
            | BindId
bId <- IBindEnv -> [BindId]
elemsIBindEnv (IBindEnv -> [BindId]) -> IBindEnv -> [BindId]
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) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
bId BindEnv
bindEnv
            ]
      mergedEnv :: HashMap Symbol ([BindId], SortedReft)
mergedEnv = [(Symbol, ([BindId], SortedReft))]
-> HashMap Symbol ([BindId], SortedReft)
forall m.
Semigroup m =>
[(Symbol, (m, SortedReft))] -> HashMap Symbol (m, SortedReft)
mergeDuplicatedBindings [(Symbol, ([BindId], SortedReft))]
env
      undoANFEnv :: HashMap Symbol ([BindId], SortedReft)
undoANFEnv = HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union (HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
undoANF HashMap Symbol ([BindId], SortedReft)
mergedEnv) HashMap Symbol ([BindId], SortedReft)
mergedEnv
      boolSimplEnv :: HashMap Symbol ([BindId], SortedReft)
boolSimplEnv = HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall k v.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k v -> HashMap k v
HashMap.union (HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
forall m.
HashMap Symbol (m, SortedReft) -> HashMap Symbol (m, SortedReft)
simplifyBooleanRefts HashMap Symbol ([BindId], SortedReft)
undoANFEnv) HashMap Symbol ([BindId], SortedReft)
undoANFEnv

      simplifiedLhs :: SortedReft
simplifiedLhs = HashMap Symbol ([BindId], SortedReft) -> SortedReft -> SortedReft
forall m.
HashMap Symbol (m, SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft HashMap Symbol ([BindId], SortedReft)
boolSimplEnv (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c)
      simplifiedRhs :: SortedReft
simplifiedRhs = HashMap Symbol ([BindId], SortedReft) -> SortedReft -> SortedReft
forall m.
HashMap Symbol (m, SortedReft) -> SortedReft -> SortedReft
inlineInSortedReft HashMap Symbol ([BindId], SortedReft)
boolSimplEnv (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)

      prunedEnv :: HashMap Symbol SortedReft
prunedEnv =
        HashSet Symbol
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
dropLikelyIrrelevantBindings (SortedReft -> SortedReft -> HashSet Symbol
constraintSymbols SortedReft
simplifiedLhs SortedReft
simplifiedRhs) (HashMap Symbol SortedReft -> HashMap Symbol SortedReft)
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall a b. (a -> b) -> a -> b
$
        (([BindId], SortedReft) -> SortedReft)
-> HashMap Symbol ([BindId], SortedReft)
-> HashMap Symbol SortedReft
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map ([BindId], SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd HashMap Symbol ([BindId], 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 :: SortedReft
slhs = SortedReft
simplifiedLhs, srhs :: SortedReft
srhs = SortedReft
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 -> BindId -> Doc -> Doc
hang (FilePath -> Doc
text FilePath
"\n\nconstraint:") BindId
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
          FilePath -> Doc
text FilePath
"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
$+$ FilePath -> Doc
text FilePath
"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
<+> FilePath -> Doc
text FilePath
"tag" Doc -> Doc -> Doc
<+> [BindId] -> Doc
forall a. Fixpoint a => a -> Doc
toFix (SubC a -> [BindId]
forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SubC a
c)
      Doc -> Doc -> Doc
$+$ Doc -> Doc -> Doc
toFixMeta (FilePath -> Doc
text FilePath
"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 -> BindId -> Doc -> Doc
hang (FilePath -> Doc
text FilePath
"environment:") BindId
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
":", BindId -> Doc -> Doc
nest BindId
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 (Reft -> Symbol
reftBind (SortedReft -> Reft
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
"|"
      , BindId -> Doc -> Doc
nest BindId
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]
conjuncts (Expr -> [Expr]) -> Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred (Reft -> Expr) -> Reft -> Expr
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 =
      HashSet Symbol -> HashSet Symbol -> HashSet Symbol
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
"{" Text -> Text -> 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 (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr
      )

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

toFixMeta :: Doc -> Doc -> Doc
toFixMeta :: Doc -> Doc -> Doc
toFixMeta Doc
k Doc
v = FilePath -> Doc
text FilePath
"// META" Doc -> Doc -> Doc
<+> Doc
k Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
":" 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 (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, Hashable 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, Hashable 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
. Reft -> Expr
reftPred (Reft -> Expr)
-> ((Symbol, SortedReft) -> Reft) -> (Symbol, SortedReft) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft (SortedReft -> Reft)
-> ((Symbol, SortedReft) -> SortedReft)
-> (Symbol, SortedReft)
-> Reft
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 :: 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 ([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
c)
  where
    renameSubC :: HashMap Symbol Symbol -> SubC a -> SubC a
    renameSubC :: HashMap Symbol Symbol -> SubC a -> SubC a
renameSubC HashMap Symbol Symbol
symMap SubC a
c =
      IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> a
-> SubC a
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe SubcId
-> [BindId]
-> 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 -> [BindId]
forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
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 Reft
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 -> 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 = 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 (Reft -> Symbol
reftBind Reft
r) (Symbol -> Symbol
prefixOfSym (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Reft -> Symbol
reftBind Reft
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 -> Reft
reft (HashMap Symbol Symbol -> Symbol -> Symbol
at HashMap Symbol Symbol
m (Reft -> Symbol
reftBind Reft
r)) (Expr -> Reft) -> Expr -> Reft
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
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)) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred Reft
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, Hashable 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 p. Symbol -> [(Symbol, [p])] -> [(p, 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, [p])] -> [(p, Symbol)]
renameWithSuffixes Symbol
pfx = \case
      [(Symbol
_sfx, [p]
ss)] -> Symbol -> (Symbol, [p]) -> [(p, Symbol)]
forall p. Symbol -> (Symbol, [p]) -> [(p, Symbol)]
renameWithAppendages Symbol
pfx (Symbol
"", [p]
ss)
      [(Symbol, [p])]
sfxs -> ((Symbol, [p]) -> [(p, Symbol)])
-> [(Symbol, [p])] -> [(p, Symbol)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol -> (Symbol, [p]) -> [(p, Symbol)]
forall p. Symbol -> (Symbol, [p]) -> [(p, Symbol)]
renameWithAppendages Symbol
pfx) [(Symbol, [p])]
sfxs

    renameWithAppendages :: Symbol -> (Symbol, [p]) -> [(p, Symbol)]
renameWithAppendages Symbol
pfx (Symbol
sfx, [p]
ss) = [p] -> [Symbol] -> [(p, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [p]
ss ([Symbol] -> [(p, Symbol)]) -> [Symbol] -> [(p, Symbol)]
forall a b. (a -> b) -> a -> b
$ case [p]
ss of
      [p
_s] -> [Symbol
pfx Symbol -> Symbol -> Symbol
`suffixIfNotNull` Symbol
sfx]
      [p]
ss -> (SubcId -> p -> Symbol) -> [SubcId] -> [p] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Symbol -> Symbol -> SubcId -> p -> Symbol
forall a p. Show a => Symbol -> Symbol -> a -> p -> Symbol
rename Symbol
pfx Symbol
sfx) [SubcId
1..] [p]
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` FilePath -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (a -> FilePath
forall a. Show a => a -> FilePath
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