{-# 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
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 :: forall a. Fixpoint a => Config -> FInfo a -> IO (Result a)
nontrivsorts Config
cfg FInfo a
fi = do
  let fi' :: FInfo a
fi' = forall a. Config -> FInfo a -> FInfo a
simplify' Config
cfg FInfo a
fi
  forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> FilePath -> IO ()
writeFInfo Config
cfg FInfo a
fi' forall a b. (a -> b) -> a -> b
$ Ext -> Config -> FilePath
queryFile Ext
Out Config
cfg
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall a. NonTrivSorts -> FInfo a -> FInfo a
simplifyFInfo (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FInfo a -> TrivInfo
trivInfo

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

ntGraph :: TrivInfo -> NTG
ntGraph :: TrivInfo -> NTG
ntGraph TrivInfo
ti = [(NTV
v,NTV
v,[NTV]
vs) | (NTV
v, [NTV]
vs) <- forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
groupList 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 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       <- forall a. HashSet a -> [a]
S.toList NonTrivSorts
nts         ]
      forall a. [a] -> [a] -> [a]
++ [(KVar -> NTV
K KVar
k, Sort -> NTV
S Sort
s) | (KVar
k, [Sort]
ss) <- 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
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
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
Ord, Vertex -> NTV -> ShowS
[NTV] -> ShowS
NTV -> FilePath
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. 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 :: forall a. FInfo a -> TrivInfo
trivInfo FInfo a
fi = forall a. [SubC a] -> TrivInfo -> TrivInfo
updTISubCs (forall k v. HashMap k v -> [v]
M.elems forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi)
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. BindEnv a -> TrivInfo -> TrivInfo
updTIBinds (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi)
            forall a b. (a -> b) -> a -> b
$ (forall a. HashSet a
S.empty, 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 (forall a. SubC a -> SortedReft
slhs SubC a
c) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Polarity -> SortedReft -> TrivInfo -> TrivInfo
updTI Polarity
Rhs (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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (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
_)) <- 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 (Expr -> [KVar]
kvarsExpr forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred Reft
r) 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     = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' 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, 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) = (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Bool
trivR
isNTR Polarity
Lhs = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Bool
trivOrSingR

trivR :: Reft -> Bool
trivR :: Reft -> Bool
trivR = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
trivP forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts 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)) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
trivOrSingP 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 forall a. Eq a => a -> a -> Bool
== Symbol
x                    = Bool
True
singP Symbol
v (PAtom Brel
Eq Expr
_ (EVar Symbol
x))
  | Symbol
v forall a. Eq a => a -> a -> Bool
== Symbol
x                    = Bool
True
singP Symbol
_ Expr
_                     = 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 :: HashMap SubcId (SubC a)
cm   = forall k a.
(Eq k, Hashable k) =>
NonTrivSorts -> HashMap k (SubC a) -> HashMap k (SubC a)
simplifySubCs   NonTrivSorts
tm forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm FInfo a
fi
   , ws :: HashMap KVar (WfC a)
ws   = forall a.
NonTrivSorts -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
simplifyWfCs    NonTrivSorts
tm forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws FInfo a
fi
   , bs :: BindEnv a
bs   = forall a. NonTrivSorts -> BindEnv a -> BindEnv a
simplifyBindEnv NonTrivSorts
tm forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs FInfo a
fi
}

simplifyBindEnv :: NonTrivSorts -> BindEnv a -> BindEnv a
simplifyBindEnv :: forall a. NonTrivSorts -> BindEnv a -> BindEnv a
simplifyBindEnv NonTrivSorts
tm = 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 = forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter (NonTrivSorts -> Sort -> Bool
isNonTrivialSort NonTrivSorts
tm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> b
snd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. FilePath -> a -> a
trace FilePath
msg HashMap k (SubC a)
cm'
  where
    cm' :: HashMap k (SubC a)
cm' = 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  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall b a. NonTrivSorts -> (b, SubC a) -> Maybe (b, SubC a)
simplifySubC NonTrivSorts
ti) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList
    msg :: FilePath
msg = forall r. PrintfType r => FilePath -> r
printf FilePath
"simplifySUBC: before = %d, after = %d \n" Vertex
n Vertex
n'
    n :: Vertex
n   = forall k v. HashMap k v -> Vertex
M.size HashMap k (SubC a)
cm
    n' :: Vertex
n'  = 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)
 | forall r. Reftable r => r -> Bool
isNonTrivial SortedReft
srhs' = forall a. a -> Maybe a
Just (b
i, SubC a
c { slhs :: SortedReft
slhs = SortedReft
slhs' , srhs :: SortedReft
srhs = SortedReft
srhs' })
 | Bool
otherwise          = forall a. Maybe a
Nothing
  where
    slhs' :: SortedReft
slhs'             = NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft NonTrivSorts
tm (forall a. SubC a -> SortedReft
slhs SubC a
c)
    srhs' :: SortedReft
srhs'             = NonTrivSorts -> SortedReft -> SortedReft
simplifySortedReft NonTrivSorts
tm (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 = 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 = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Sort
t NonTrivSorts
tm