{-# LANGUAGE DeriveGeneric #-}

module Language.Fixpoint.Solver.TrivialSort (nontrivsorts) where

import           GHC.Generics        (Generic)
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Visitor
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types hiding (simplify)
import           Language.Fixpoint.Utils.Files
import           Language.Fixpoint.Misc
import qualified Data.HashSet            as S
import           Data.Hashable
import qualified Data.HashMap.Strict     as M
import           Data.List (foldl')
import qualified Data.Graph              as G
import           Data.Maybe
import           Text.Printf
import           Debug.Trace

-------------------------------------------------------------------------
nontrivsorts :: (Fixpoint a) => Config -> FInfo a -> IO (Result a)
-------------------------------------------------------------------------
nontrivsorts :: Config -> FInfo a -> IO (Result a)
nontrivsorts Config
cfg FInfo a
fi = do
  let fi' :: FInfo a
fi' = Config -> FInfo a -> FInfo a
forall a. Config -> FInfo a -> FInfo a
simplify' Config
cfg FInfo a
fi
  Config -> FInfo a -> FilePath -> IO ()
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> FilePath -> IO ()
writeFInfo Config
cfg FInfo a
fi' (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Ext -> Config -> FilePath
queryFile Ext
Out Config
cfg
  Result a -> IO (Result a)
forall (m :: * -> *) a. Monad m => a -> m a
return Result a
forall a. Monoid a => a
mempty

simplify' :: Config -> FInfo a -> FInfo a
simplify' :: Config -> FInfo a -> FInfo a
simplify' Config
_ FInfo a
fi = NonTrivSorts -> FInfo a -> FInfo a
forall a. NonTrivSorts -> FInfo a -> FInfo a
simplifyFInfo (FInfo a -> NonTrivSorts
forall a. FInfo a -> NonTrivSorts
mkNonTrivSorts FInfo a
fi) FInfo a
fi

--------------------------------------------------------------------
-- | The main data types
--------------------------------------------------------------------
type NonTrivSorts = S.HashSet Sort
type KVarMap      = M.HashMap KVar [Sort]
data Polarity     = Lhs | Rhs
type TrivInfo     = (NonTrivSorts, KVarMap)
--------------------------------------------------------------------

--------------------------------------------------------------------
mkNonTrivSorts :: FInfo a -> NonTrivSorts
--------------------------------------------------------------------
mkNonTrivSorts :: FInfo a -> NonTrivSorts
mkNonTrivSorts = {- tracepp "mkNonTrivSorts: " . -}  TrivInfo -> NonTrivSorts
nonTrivSorts (TrivInfo -> NonTrivSorts)
-> (FInfo a -> TrivInfo) -> FInfo a -> NonTrivSorts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FInfo a -> TrivInfo
forall a. FInfo a -> TrivInfo
trivInfo

--------------------------------------------------------------------
nonTrivSorts :: TrivInfo -> NonTrivSorts
--------------------------------------------------------------------
nonTrivSorts :: TrivInfo -> NonTrivSorts
nonTrivSorts TrivInfo
ti = [Sort] -> NonTrivSorts
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Sort
s | S Sort
s <- [NTV]
ntvs]
  where
    ntvs :: [NTV]
ntvs        = [(NTV, NTV, [NTV]) -> NTV
forall a b c. (a, b, c) -> a
fst3 (Vertex -> (NTV, NTV, [NTV])
f Vertex
v) | Vertex
v <- Graph -> Vertex -> [Vertex]
G.reachable Graph
g Vertex
root]
    (Graph
g, Vertex -> (NTV, NTV, [NTV])
f, NTV -> Maybe Vertex
fv)  = [(NTV, NTV, [NTV])]
-> (Graph, Vertex -> (NTV, NTV, [NTV]), NTV -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
G.graphFromEdges ([(NTV, NTV, [NTV])]
 -> (Graph, Vertex -> (NTV, NTV, [NTV]), NTV -> Maybe Vertex))
-> [(NTV, NTV, [NTV])]
-> (Graph, Vertex -> (NTV, NTV, [NTV]), NTV -> Maybe Vertex)
forall a b. (a -> b) -> a -> b
$ TrivInfo -> [(NTV, NTV, [NTV])]
ntGraph TrivInfo
ti
    root :: Vertex
root        = Vertex -> Maybe Vertex -> Vertex
forall a. a -> Maybe a -> a
fromMaybe Vertex
forall a. a
err    (Maybe Vertex -> Vertex) -> Maybe Vertex -> Vertex
forall a b. (a -> b) -> a -> b
$ NTV -> Maybe Vertex
fv NTV
NTV
    err :: a
err         = FilePath -> a
forall a. (?callStack::CallStack) => FilePath -> a
errorstar FilePath
"nonTrivSorts: cannot find root!"

ntGraph :: TrivInfo -> NTG
ntGraph :: TrivInfo -> [(NTV, NTV, [NTV])]
ntGraph TrivInfo
ti = [(NTV
v,NTV
v,[NTV]
vs) | (NTV
v, [NTV]
vs) <- [(NTV, NTV)] -> [(NTV, [NTV])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
groupList ([(NTV, NTV)] -> [(NTV, [NTV])]) -> [(NTV, NTV)] -> [(NTV, [NTV])]
forall a b. (a -> b) -> a -> b
$ TrivInfo -> [(NTV, NTV)]
ntEdges TrivInfo
ti]

ntEdges :: TrivInfo -> [(NTV, NTV)]
ntEdges :: TrivInfo -> [(NTV, NTV)]
ntEdges (NonTrivSorts
nts, KVarMap
kvm) = [(NTV, NTV)]
es [(NTV, NTV)] -> [(NTV, NTV)] -> [(NTV, NTV)]
forall a. [a] -> [a] -> [a]
++ [(NTV
v, NTV
u) | (NTV
u, NTV
v) <- [(NTV, NTV)]
es]
  where
    es :: [(NTV, NTV)]
es = [(NTV
NTV, Sort -> NTV
S Sort
s) | Sort
s       <- NonTrivSorts -> [Sort]
forall a. HashSet a -> [a]
S.toList NonTrivSorts
nts         ]
      [(NTV, NTV)] -> [(NTV, NTV)] -> [(NTV, NTV)]
forall a. [a] -> [a] -> [a]
++ [(KVar -> NTV
K KVar
k, Sort -> NTV
S Sort
s) | (KVar
k, [Sort]
ss) <- KVarMap -> [(KVar, [Sort])]
forall k v. HashMap k v -> [(k, v)]
M.toList KVarMap
kvm, Sort
s <- [Sort]
ss]

type NTG = [(NTV, NTV, [NTV])]

data NTV = NTV
         | K !KVar
         | S !Sort
         deriving (NTV -> NTV -> Bool
(NTV -> NTV -> Bool) -> (NTV -> NTV -> Bool) -> Eq NTV
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NTV -> NTV -> Bool
$c/= :: NTV -> NTV -> Bool
== :: NTV -> NTV -> Bool
$c== :: NTV -> NTV -> Bool
Eq, Eq NTV
Eq NTV
-> (NTV -> NTV -> Ordering)
-> (NTV -> NTV -> Bool)
-> (NTV -> NTV -> Bool)
-> (NTV -> NTV -> Bool)
-> (NTV -> NTV -> Bool)
-> (NTV -> NTV -> NTV)
-> (NTV -> NTV -> NTV)
-> Ord NTV
NTV -> NTV -> Bool
NTV -> NTV -> Ordering
NTV -> NTV -> NTV
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NTV -> NTV -> NTV
$cmin :: NTV -> NTV -> NTV
max :: NTV -> NTV -> NTV
$cmax :: NTV -> NTV -> NTV
>= :: NTV -> NTV -> Bool
$c>= :: NTV -> NTV -> Bool
> :: NTV -> NTV -> Bool
$c> :: NTV -> NTV -> Bool
<= :: NTV -> NTV -> Bool
$c<= :: NTV -> NTV -> Bool
< :: NTV -> NTV -> Bool
$c< :: NTV -> NTV -> Bool
compare :: NTV -> NTV -> Ordering
$ccompare :: NTV -> NTV -> Ordering
$cp1Ord :: Eq NTV
Ord, Vertex -> NTV -> ShowS
[NTV] -> ShowS
NTV -> FilePath
(Vertex -> NTV -> ShowS)
-> (NTV -> FilePath) -> ([NTV] -> ShowS) -> Show NTV
forall a.
(Vertex -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [NTV] -> ShowS
$cshowList :: [NTV] -> ShowS
show :: NTV -> FilePath
$cshow :: NTV -> FilePath
showsPrec :: Vertex -> NTV -> ShowS
$cshowsPrec :: Vertex -> NTV -> ShowS
Show, (forall x. NTV -> Rep NTV x)
-> (forall x. Rep NTV x -> NTV) -> Generic NTV
forall x. Rep NTV x -> NTV
forall x. NTV -> Rep NTV x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NTV x -> NTV
$cfrom :: forall x. NTV -> Rep NTV x
Generic)

instance Hashable NTV

--------------------------------------------------------------------
trivInfo :: FInfo a -> TrivInfo
--------------------------------------------------------------------
trivInfo :: FInfo a -> TrivInfo
trivInfo FInfo a
fi = [SubC a] -> TrivInfo -> TrivInfo
forall a. [SubC a] -> TrivInfo -> TrivInfo
updTISubCs (HashMap SubcId (SubC a) -> [SubC a]
forall k v. HashMap k v -> [v]
M.elems (HashMap SubcId (SubC a) -> [SubC a])
-> HashMap SubcId (SubC a) -> [SubC a]
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi)
            (TrivInfo -> TrivInfo)
-> (TrivInfo -> TrivInfo) -> TrivInfo -> TrivInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindEnv -> TrivInfo -> TrivInfo
updTIBinds (FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi)
            (TrivInfo -> TrivInfo) -> TrivInfo -> TrivInfo
forall a b. (a -> b) -> a -> b
$ (NonTrivSorts
forall a. HashSet a
S.empty, KVarMap
forall k v. HashMap k v
M.empty)

updTISubCs :: [SubC a] -> TrivInfo -> TrivInfo
updTISubCs :: [SubC a] -> TrivInfo -> TrivInfo
updTISubCs [SubC a]
cs TrivInfo
ti = (TrivInfo -> SubC a -> TrivInfo)
-> TrivInfo -> [SubC a] -> TrivInfo
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((SubC a -> TrivInfo -> TrivInfo) -> TrivInfo -> SubC a -> TrivInfo
forall a b c. (a -> b -> c) -> b -> a -> c
flip SubC a -> TrivInfo -> TrivInfo
forall a. SubC a -> TrivInfo -> TrivInfo
updTISubC) TrivInfo
ti [SubC a]
cs

updTISubC :: SubC a -> TrivInfo -> TrivInfo
updTISubC :: SubC a -> TrivInfo -> TrivInfo
updTISubC SubC a
c = Polarity -> SortedReft -> TrivInfo -> TrivInfo
updTI Polarity
Lhs (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c) (TrivInfo -> TrivInfo)
-> (TrivInfo -> TrivInfo) -> TrivInfo -> TrivInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polarity -> SortedReft -> TrivInfo -> TrivInfo
updTI Polarity
Rhs (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)

updTIBinds :: BindEnv -> TrivInfo -> TrivInfo
updTIBinds :: BindEnv -> TrivInfo -> TrivInfo
updTIBinds BindEnv
be TrivInfo
ti = (TrivInfo -> SortedReft -> TrivInfo)
-> TrivInfo -> [SortedReft] -> TrivInfo
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((SortedReft -> TrivInfo -> TrivInfo)
-> TrivInfo -> SortedReft -> TrivInfo
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Polarity -> SortedReft -> TrivInfo -> TrivInfo
updTI Polarity
Lhs)) TrivInfo
ti [SortedReft]
ts
  where
    ts :: [SortedReft]
ts           = [SortedReft
t | (Vertex
_,Symbol
_,SortedReft
t) <- BindEnv -> [(Vertex, Symbol, SortedReft)]
bindEnvToList BindEnv
be]

--------------------------------------------------------------------
updTI :: Polarity -> SortedReft -> TrivInfo -> TrivInfo
--------------------------------------------------------------------
updTI :: Polarity -> SortedReft -> TrivInfo -> TrivInfo
updTI Polarity
p (RR Sort
t Reft
r) = Sort -> [KVar] -> TrivInfo -> TrivInfo
addKVs Sort
t (Reft -> [KVar]
forall t. Visitable t => t -> [KVar]
kvars Reft
r) (TrivInfo -> TrivInfo)
-> (TrivInfo -> TrivInfo) -> TrivInfo -> TrivInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polarity -> Reft -> Sort -> TrivInfo -> TrivInfo
addNTS Polarity
p Reft
r Sort
t

addNTS :: Polarity -> Reft -> Sort -> TrivInfo -> TrivInfo
addNTS :: Polarity -> Reft -> Sort -> TrivInfo -> TrivInfo
addNTS Polarity
p Reft
r Sort
t TrivInfo
ti
  | Polarity -> Reft -> Bool
isNTR Polarity
p Reft
r = Sort -> TrivInfo -> TrivInfo
addSort Sort
t TrivInfo
ti
  | Bool
otherwise = TrivInfo
ti

addKVs :: Sort -> [KVar] -> TrivInfo -> TrivInfo
addKVs :: Sort -> [KVar] -> TrivInfo -> TrivInfo
addKVs Sort
t [KVar]
ks TrivInfo
ti     = (TrivInfo -> KVar -> TrivInfo) -> TrivInfo -> [KVar] -> TrivInfo
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' TrivInfo -> KVar -> TrivInfo
forall k a.
(Eq k, Hashable k) =>
(a, HashMap k [Sort]) -> k -> (a, HashMap k [Sort])
addK TrivInfo
ti [KVar]
ks
  where
    addK :: (a, HashMap k [Sort]) -> k -> (a, HashMap k [Sort])
addK (a
ts, HashMap k [Sort]
m) k
k = (a
ts, k -> Sort -> HashMap k [Sort] -> HashMap k [Sort]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k [v] -> HashMap k [v]
inserts k
k Sort
t HashMap k [Sort]
m)

addSort :: Sort -> TrivInfo -> TrivInfo
addSort :: Sort -> TrivInfo -> TrivInfo
addSort Sort
t (NonTrivSorts
ts, KVarMap
m) = (Sort -> NonTrivSorts -> NonTrivSorts
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert Sort
t NonTrivSorts
ts, KVarMap
m)

--------------------------------------------------------------------
isNTR :: Polarity -> Reft -> Bool
--------------------------------------------------------------------
isNTR :: Polarity -> Reft -> Bool
isNTR Polarity
Rhs = Bool -> Bool
not (Bool -> Bool) -> (Reft -> Bool) -> Reft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Bool
trivR
isNTR Polarity
Lhs = Bool -> Bool
not (Bool -> Bool) -> (Reft -> Bool) -> Reft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Bool
trivOrSingR

trivR :: Reft -> Bool
trivR :: Reft -> Bool
trivR = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
trivP ([Expr] -> Bool) -> (Reft -> [Expr]) -> Reft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts (Expr -> [Expr]) -> (Reft -> Expr) -> Reft -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred

trivOrSingR :: Reft -> Bool
trivOrSingR :: Reft -> Bool
trivOrSingR (Reft (Symbol
v, Expr
p)) = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
trivOrSingP ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
conjuncts Expr
p
  where
    trivOrSingP :: Expr -> Bool
trivOrSingP Expr
p         = Expr -> Bool
trivP Expr
p Bool -> Bool -> Bool
|| Symbol -> Expr -> Bool
singP Symbol
v Expr
p

trivP :: Expr -> Bool
trivP :: Expr -> Bool
trivP (PKVar {}) = Bool
True
trivP Expr
p          = Expr -> Bool
isTautoPred Expr
p

singP :: Symbol -> Expr -> Bool
singP :: Symbol -> Expr -> Bool
singP Symbol
v (PAtom Brel
Eq (EVar Symbol
x) Expr
_)
  | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x                    = Bool
True
singP Symbol
v (PAtom Brel
Eq Expr
_ (EVar Symbol
x))
  | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x                    = Bool
True
singP Symbol
_ Expr
_                     = Bool
False

-------------------------------------------------------------------------
simplifyFInfo :: NonTrivSorts -> FInfo a -> FInfo a
-------------------------------------------------------------------------
simplifyFInfo :: NonTrivSorts -> FInfo a -> FInfo a
simplifyFInfo NonTrivSorts
tm FInfo a
fi = FInfo a
fi {
     cm :: HashMap SubcId (SubC a)
cm   = NonTrivSorts -> HashMap SubcId (SubC a) -> HashMap SubcId (SubC a)
forall k a.
(Eq k, Hashable k) =>
NonTrivSorts -> HashMap k (SubC a) -> HashMap k (SubC a)
simplifySubCs   NonTrivSorts
tm (HashMap SubcId (SubC a) -> HashMap SubcId (SubC a))
-> HashMap SubcId (SubC a) -> HashMap SubcId (SubC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap SubcId (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi
   , ws :: HashMap KVar (WfC a)
ws   = NonTrivSorts -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall a.
NonTrivSorts -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
simplifyWfCs    NonTrivSorts
tm (HashMap KVar (WfC a) -> HashMap KVar (WfC a))
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall a b. (a -> b) -> a -> b
$ FInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
fi
   , bs :: BindEnv
bs   = NonTrivSorts -> BindEnv -> BindEnv
simplifyBindEnv NonTrivSorts
tm (BindEnv -> BindEnv) -> BindEnv -> BindEnv
forall a b. (a -> b) -> a -> b
$ FInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs FInfo a
fi
}

simplifyBindEnv :: NonTrivSorts -> BindEnv -> BindEnv
simplifyBindEnv :: NonTrivSorts -> BindEnv -> BindEnv
simplifyBindEnv NonTrivSorts
tm = (Vertex -> (Symbol, SortedReft) -> (Symbol, SortedReft))
-> BindEnv -> BindEnv
mapBindEnv (\Vertex
_ (Symbol
x, SortedReft
sr) -> (Symbol
x, NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft NonTrivSorts
tm SortedReft
sr))

simplifyWfCs :: NonTrivSorts -> M.HashMap KVar (WfC a) -> M.HashMap KVar (WfC a)
simplifyWfCs :: NonTrivSorts -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
simplifyWfCs NonTrivSorts
tm = (WfC a -> Bool) -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter (NonTrivSorts -> Sort -> Bool
isNonTrivialSort NonTrivSorts
tm (Sort -> Bool) -> (WfC a -> Sort) -> WfC a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort, KVar) -> Sort
forall a b c. (a, b, c) -> b
snd3 ((Symbol, Sort, KVar) -> Sort)
-> (WfC a -> (Symbol, Sort, KVar)) -> WfC a -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft)

simplifySubCs :: (Eq k, Hashable k)
              => NonTrivSorts -> M.HashMap k (SubC a) -> M.HashMap k (SubC a)
simplifySubCs :: NonTrivSorts -> HashMap k (SubC a) -> HashMap k (SubC a)
simplifySubCs NonTrivSorts
ti HashMap k (SubC a)
cm = FilePath -> HashMap k (SubC a) -> HashMap k (SubC a)
forall a. FilePath -> a -> a
trace FilePath
msg HashMap k (SubC a)
cm'
  where
    cm' :: HashMap k (SubC a)
cm' = HashMap k (SubC a) -> HashMap k (SubC a)
forall a. HashMap k (SubC a) -> HashMap k (SubC a)
tx HashMap k (SubC a)
cm
    tx :: HashMap k (SubC a) -> HashMap k (SubC a)
tx  = [(k, SubC a)] -> HashMap k (SubC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(k, SubC a)] -> HashMap k (SubC a))
-> (HashMap k (SubC a) -> [(k, SubC a)])
-> HashMap k (SubC a)
-> HashMap k (SubC a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((k, SubC a) -> Maybe (k, SubC a))
-> [(k, SubC a)] -> [(k, SubC a)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (NonTrivSorts -> (k, SubC a) -> Maybe (k, SubC a)
forall b a. NonTrivSorts -> (b, SubC a) -> Maybe (b, SubC a)
simplifySubC NonTrivSorts
ti) ([(k, SubC a)] -> [(k, SubC a)])
-> (HashMap k (SubC a) -> [(k, SubC a)])
-> HashMap k (SubC a)
-> [(k, SubC a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap k (SubC a) -> [(k, SubC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList
    msg :: FilePath
msg = FilePath -> Vertex -> Vertex -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"simplifySUBC: before = %d, after = %d \n" Vertex
n Vertex
n'
    n :: Vertex
n   = HashMap k (SubC a) -> Vertex
forall k v. HashMap k v -> Vertex
M.size HashMap k (SubC a)
cm
    n' :: Vertex
n'  = HashMap k (SubC a) -> Vertex
forall k v. HashMap k v -> Vertex
M.size HashMap k (SubC a)
cm'

simplifySubC :: NonTrivSorts -> (b, SubC a) -> Maybe (b, SubC a)
simplifySubC :: NonTrivSorts -> (b, SubC a) -> Maybe (b, SubC a)
simplifySubC NonTrivSorts
tm (b
i, SubC a
c)
 | SortedReft -> Bool
forall r. Reftable r => r -> Bool
isNonTrivial SortedReft
srhs' = (b, SubC a) -> Maybe (b, SubC a)
forall a. a -> Maybe a
Just (b
i, SubC a
c { slhs :: SortedReft
slhs = SortedReft
slhs' , srhs :: SortedReft
srhs = SortedReft
srhs' })
 | Bool
otherwise          = Maybe (b, SubC a)
forall a. Maybe a
Nothing
  where
    slhs' :: SortedReft
slhs'             = NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft NonTrivSorts
tm (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c)
    srhs' :: SortedReft
srhs'             = NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft NonTrivSorts
tm (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)

simplifySortedReft :: NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft :: NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft NonTrivSorts
tm SortedReft
sr
  | Bool
nonTrivial = SortedReft
sr
  | Bool
otherwise  = SortedReft
sr { sr_reft :: Reft
sr_reft = Reft
forall a. Monoid a => a
mempty }
  where
    nonTrivial :: Bool
nonTrivial = NonTrivSorts -> Sort -> Bool
isNonTrivialSort NonTrivSorts
tm (SortedReft -> Sort
sr_sort SortedReft
sr)

isNonTrivialSort :: NonTrivSorts -> Sort -> Bool
isNonTrivialSort :: NonTrivSorts -> Sort -> Bool
isNonTrivialSort NonTrivSorts
tm Sort
t = Sort -> NonTrivSorts -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Sort
t NonTrivSorts
tm