{-# LANGUAGE CPP           #-}
{-# LANGUAGE DeriveGeneric #-}

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

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
#if !MIN_VERSION_base(4,20,0)
import           Data.List (foldl')
#endif
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 :: forall a. Fixpoint a => 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 a. a -> IO 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' :: forall a. 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 :: forall a. 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
$c== :: NTV -> NTV -> Bool
== :: NTV -> NTV -> Bool
$c/= :: NTV -> NTV -> Bool
/= :: 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
$ccompare :: NTV -> NTV -> Ordering
compare :: NTV -> NTV -> Ordering
$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
>= :: NTV -> NTV -> Bool
$cmax :: NTV -> NTV -> NTV
max :: NTV -> NTV -> NTV
$cmin :: NTV -> NTV -> NTV
min :: NTV -> NTV -> 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
$cshowsPrec :: Vertex -> NTV -> ShowS
showsPrec :: Vertex -> NTV -> ShowS
$cshow :: NTV -> FilePath
show :: NTV -> FilePath
$cshowList :: [NTV] -> ShowS
showList :: [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
$cfrom :: forall x. NTV -> Rep NTV x
from :: forall x. NTV -> Rep NTV x
$cto :: forall x. Rep NTV x -> NTV
to :: forall x. Rep NTV x -> NTV
Generic)

instance Hashable NTV

--------------------------------------------------------------------
trivInfo :: FInfo a -> TrivInfo
--------------------------------------------------------------------
trivInfo :: forall a. 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 a -> TrivInfo -> TrivInfo
forall a. BindEnv a -> TrivInfo -> TrivInfo
updTIBinds (FInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
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 :: forall a. [SubC a] -> TrivInfo -> TrivInfo
updTISubCs [SubC a]
cs TrivInfo
ti = (TrivInfo -> SubC a -> TrivInfo)
-> TrivInfo -> [SubC a] -> TrivInfo
forall b a. (b -> a -> b) -> b -> [a] -> b
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 :: forall a. 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 a -> TrivInfo -> TrivInfo
updTIBinds :: forall a. BindEnv a -> TrivInfo -> TrivInfo
updTIBinds BindEnv a
be TrivInfo
ti = (TrivInfo -> SortedReft -> TrivInfo)
-> TrivInfo -> [SortedReft] -> TrivInfo
forall b a. (b -> a -> b) -> b -> [a] -> b
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,a
_)) <- BindEnv a -> [(Vertex, (Symbol, SortedReft, a))]
forall a. BindEnv a -> [(Vertex, (Symbol, SortedReft, a))]
bindEnvToList BindEnv a
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 (ExprV Symbol -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr (ExprV Symbol -> [KVar]) -> ExprV Symbol -> [KVar]
forall a b. (a -> b) -> a -> b
$ Reft -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred 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 b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' TrivInfo -> KVar -> TrivInfo
forall {k} {a}.
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 = (ExprV Symbol -> Bool) -> [ExprV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprV Symbol -> Bool
trivP ([ExprV Symbol] -> Bool)
-> (Reft -> [ExprV Symbol]) -> Reft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV Symbol -> [ExprV Symbol]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts (ExprV Symbol -> [ExprV Symbol])
-> (Reft -> ExprV Symbol) -> Reft -> [ExprV Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred

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

trivP :: Expr -> Bool
trivP :: ExprV Symbol -> Bool
trivP PKVar {} = Bool
True
trivP ExprV Symbol
p        = ExprV Symbol -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV Symbol
p

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

-------------------------------------------------------------------------
simplifyFInfo :: NonTrivSorts -> FInfo a -> FInfo a
-------------------------------------------------------------------------
simplifyFInfo :: forall a. NonTrivSorts -> FInfo a -> FInfo a
simplifyFInfo NonTrivSorts
tm FInfo a
fi = FInfo a
fi {
     cm   = simplifySubCs   tm $ cm fi
   , ws   = simplifyWfCs    tm $ ws fi
   , bs   = simplifyBindEnv tm $ bs fi
}

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

simplifyWfCs :: NonTrivSorts -> M.HashMap KVar (WfC a) -> M.HashMap KVar (WfC a)
simplifyWfCs :: forall a.
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 :: forall k a.
(Eq k, Hashable k) =>
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 :: forall b a. NonTrivSorts -> (b, SubC a) -> Maybe (b, SubC a)
simplifySubC NonTrivSorts
tm (b
i, SubC a
c)
 | SortedReft -> Bool
isNonTrivial SortedReft
srhs' = (b, SubC a) -> Maybe (b, SubC a)
forall a. a -> Maybe a
Just (b
i, SubC a
c { slhs = slhs' , srhs = 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 = trueReft }
  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