{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wwarn #-}

module Language.Fixpoint.Solver.Solution
  ( -- * Create Initial Solution
    init

    -- * Update Solution
  , Sol.update

    -- * Apply Solution
  , applyInSortedReft
  , CombinedEnv(..)

    -- * Lookup Solution
  , lhsPred

  , nonCutsResult

    -- * Exported for Testing
  , simplifyKVar
  , alphaEq
  ) where

import           Control.Arrow (second, (***))
import           Control.Monad                  (guard, mplus)
import           Control.Monad.Reader
import qualified Data.HashSet                   as S
import qualified Data.HashMap.Strict            as M
import qualified Data.List                      as List
import           Data.Maybe                     (maybeToList, isJust, isNothing)
import           Language.Fixpoint.Types.PrettyPrint ()
import           Language.Fixpoint.Types.Visitor      as V
import           Language.Fixpoint.SortCheck          (ElabM)
import qualified Language.Fixpoint.SortCheck          as So
import qualified Language.Fixpoint.Misc               as Misc
import           Language.Fixpoint.Types.Config
import qualified Language.Fixpoint.Types              as F
import qualified Language.Fixpoint.Types.Solutions    as Sol
import           Language.Fixpoint.Types.Constraints  hiding (ws, bs)
import           Prelude                              hiding (init, lookup)


--------------------------------------------------------------------------------
-- | Initial Solution (from Qualifiers and WF constraints) ---------------------
--------------------------------------------------------------------------------
init :: (F.Fixpoint a) => Config -> F.SInfo a -> S.HashSet F.KVar -> M.HashMap F.KVar Sol.QBind
--------------------------------------------------------------------------------
init :: forall a.
Fixpoint a =>
Config -> SInfo a -> HashSet KVar -> HashMap KVar QBind
init Config
cfg SInfo a
si HashSet KVar
ks =
    Reader ElabFlags (HashMap KVar QBind)
-> ElabFlags -> HashMap KVar QBind
forall r a. Reader r a -> r -> a
runReader ((WfC a -> ReaderT ElabFlags Identity QBind)
-> HashMap KVar (WfC a) -> Reader ElabFlags (HashMap KVar QBind)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap KVar a -> f (HashMap KVar b)
traverse (SInfo a
-> QCluster
-> SEnv Sort
-> WfC a
-> ReaderT ElabFlags Identity QBind
forall a.
SInfo a
-> QCluster
-> SEnv Sort
-> WfC a
-> ReaderT ElabFlags Identity QBind
refine SInfo a
si QCluster
qcs SEnv Sort
genv) HashMap KVar (WfC a)
ws) (Config -> ElabFlags
solverFlags Config
cfg)
  where
    qcs :: QCluster
qcs = [Qualifier] -> QCluster
mkQCluster (SInfo a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
si)
    ws :: HashMap KVar (WfC a)
ws = HashMap KVar (WfC a) -> HashMap KVar () -> HashMap KVar (WfC a)
forall k v w. Eq k => HashMap k v -> HashMap k w -> HashMap k v
M.intersection (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si) (HashSet KVar -> HashMap KVar ()
forall a. HashSet a -> HashMap a ()
S.toMap HashSet KVar
ks)
    genv :: SEnv Sort
genv = Config -> SInfo a -> SEnv Sort
forall a. Fixpoint a => Config -> SInfo a -> SEnv Sort
initQualifierEnv Config
cfg SInfo a
si

initQualifierEnv :: (F.Fixpoint a) => Config -> F.SInfo a -> F.SEnv F.Sort
initQualifierEnv :: forall a. Fixpoint a => Config -> SInfo a -> SEnv Sort
initQualifierEnv Config
cfg SInfo a
si
  | Bool
scraping  = Config -> SInfo a -> SEnv Sort
forall (c :: * -> *) a. Config -> GInfo c a -> SEnv Sort
So.globalEnv Config
cfg SInfo a
si SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SInfo a -> SEnv Sort
forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si
  | Bool
otherwise = SInfo a -> SEnv Sort
forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si
  where
    scraping :: Bool
scraping = Config -> Scrape
scrape Config
cfg Scrape -> Scrape -> Bool
forall a. Eq a => a -> a -> Bool
/= Scrape
No

--------------------------------------------------------------------------------
-- | [NOTE:qual-cluster] It is wasteful to perform instantiation *individually*
--   on each qualifier, as many qualifiers have "equivalent" parameters, and
--   so have the "same" instances in an environment. To exploit this structure,
--
--   1. Group the [Qualifier] into a QCluster
--   2. Refactor instK to use QCluster
--------------------------------------------------------------------------------

type QCluster = M.HashMap QCSig [Qualifier]

type QCSig = [F.QualParam]

mkQCluster :: [Qualifier] -> QCluster
mkQCluster :: [Qualifier] -> QCluster
mkQCluster = (Qualifier -> QCSig) -> [Qualifier] -> QCluster
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> HashMap k [a]
Misc.groupMap Qualifier -> QCSig
qualSig

qualSig :: Qualifier -> QCSig
qualSig :: Qualifier -> QCSig
qualSig Qualifier
q = [ QualParam
p { F.qpSym = F.dummyName }  | QualParam
p <- Qualifier -> QCSig
forall v. QualifierV v -> QCSig
F.qParams Qualifier
q ]

--------------------------------------------------------------------------------

refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> ElabM Sol.QBind
refine :: forall a.
SInfo a
-> QCluster
-> SEnv Sort
-> WfC a
-> ReaderT ElabFlags Identity QBind
refine SInfo a
info QCluster
qs SEnv Sort
genv WfC a
w = Bool
-> SEnv Sort
-> QCluster
-> (Symbol, Sort, KVar)
-> ReaderT ElabFlags Identity QBind
refineK (SInfo a -> Bool
forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals SInfo a
info) SEnv Sort
env QCluster
qs (WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
F.wrft WfC a
w)
  where
    env :: SEnv Sort
env             = SEnv Sort
wenvSort SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SEnv Sort
genv
    wenvSort :: SEnv Sort
wenvSort        = SortedReft -> Sort
F.sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
info) (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv WfC a
w))

instConstants :: F.SInfo a -> F.SEnv F.Sort
instConstants :: forall a. SInfo a -> SEnv Sort
instConstants = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv ([(Symbol, Sort)] -> SEnv Sort)
-> (SInfo a -> [(Symbol, Sort)]) -> SInfo a -> SEnv Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, Sort) -> Bool
forall {b}. (Symbol, b) -> Bool
notLit ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> (SInfo a -> [(Symbol, Sort)]) -> SInfo a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (SInfo a -> SEnv Sort) -> SInfo a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits
  where
    notLit :: (Symbol, b) -> Bool
notLit    = Bool -> Bool
not (Bool -> Bool) -> ((Symbol, b) -> Bool) -> (Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
F.isLitSymbol (Symbol -> Bool) -> ((Symbol, b) -> Symbol) -> (Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst


refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> ElabM Sol.QBind
refineK :: Bool
-> SEnv Sort
-> QCluster
-> (Symbol, Sort, KVar)
-> ReaderT ElabFlags Identity QBind
refineK Bool
ho SEnv Sort
env QCluster
qs (Symbol
v, Sort
t, KVar
_k) = (EQual -> ReaderT ElabFlags Identity Bool)
-> QBind -> ReaderT ElabFlags Identity QBind
forall (m :: * -> *).
Monad m =>
(EQual -> m Bool) -> QBind -> m QBind
Sol.qbFilterM (SEnv Sort
-> Symbol -> Sort -> EQual -> ReaderT ElabFlags Identity Bool
okInst SEnv Sort
env Symbol
v Sort
t) QBind
eqs
   where
    eqs :: QBind
eqs = Bool -> SEnv Sort -> Symbol -> Sort -> QCluster -> QBind
instK Bool
ho SEnv Sort
env Symbol
v Sort
t QCluster
qs

--------------------------------------------------------------------------------
instK :: Bool
      -> F.SEnv F.Sort
      -> F.Symbol
      -> F.Sort
      -> QCluster
      -> Sol.QBind
--------------------------------------------------------------------------------
instK :: Bool -> SEnv Sort -> Symbol -> Sort -> QCluster -> QBind
instK Bool
ho SEnv Sort
env Symbol
v Sort
t QCluster
qc = [EQual] -> QBind
Sol.qb ([EQual] -> QBind) -> ([EQual] -> [EQual]) -> [EQual] -> QBind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [EQual] -> [EQual]
unique ([EQual] -> QBind) -> [EQual] -> QBind
forall a b. (a -> b) -> a -> b
$
  [ Qualifier -> [Symbol] -> EQual
Sol.eQual Qualifier
q [Symbol]
xs
      | (QCSig
sig, [Qualifier]
qs) <- QCluster -> [(QCSig, [Qualifier])]
forall k v. HashMap k v -> [(k, v)]
M.toList QCluster
qc
      , [Symbol]
xs        <- Bool -> SEnv Sort -> Symbol -> Sort -> QCSig -> [[Symbol]]
instKSig Bool
ho SEnv Sort
env Symbol
v Sort
t QCSig
sig
      , Qualifier
q         <- [Qualifier]
qs
  ]

unique :: [Sol.EQual] -> [Sol.EQual]
unique :: [EQual] -> [EQual]
unique [EQual]
qs = HashMap Expr EQual -> [EQual]
forall k v. HashMap k v -> [v]
M.elems (HashMap Expr EQual -> [EQual]) -> HashMap Expr EQual -> [EQual]
forall a b. (a -> b) -> a -> b
$ [(Expr, EQual)] -> HashMap Expr EQual
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [ (EQual -> Expr
Sol.eqPred EQual
q, EQual
q) | EQual
q <- [EQual]
qs ]

instKSig :: Bool
         -> F.SEnv F.Sort
         -> F.Symbol
         -> F.Sort
         -> QCSig
         -> [[F.Symbol]]
instKSig :: Bool -> SEnv Sort -> Symbol -> Sort -> QCSig -> [[Symbol]]
instKSig Bool
_  SEnv Sort
_   Symbol
_ Sort
_ [] = [Char] -> [[Symbol]]
forall a. HasCallStack => [Char] -> a
error [Char]
"Empty qsig in Solution.instKSig"
instKSig Bool
ho SEnv Sort
env Symbol
v Sort
sort' (QualParam
qp:QCSig
qps) = do
  (TVSubst
su0, Int
i0, QualPattern
qs0) <- Env
-> [(Int, Sort, [Symbol])]
-> QualParam
-> [(TVSubst, Int, QualPattern)]
forall a.
Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
candidatesP Env
symToSrch [(Int
0, Sort
sort', [Symbol
v])] QualParam
qp
  [(Int, QualPattern)]
ixs       <- Env
-> [(Int, Sort, [Symbol])]
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
forall a.
Env
-> [(Int, Sort, a)]
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
matchP Env
symToSrch [(Int, Sort, [Symbol])]
tyss [(Int
i0, QualPattern
qs0)] (TVSubst -> QualParam -> QualParam
applyQPP TVSubst
su0 (QualParam -> QualParam) -> QCSig -> QCSig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QCSig
qps)
  [Symbol]
ys        <- [(Int, Sort, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
forall a.
[(Int, a, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
instSymbol [(Int, Sort, [Symbol])]
tyss ([(Int, QualPattern)] -> [(Int, QualPattern)]
forall a. HasCallStack => [a] -> [a]
tail ([(Int, QualPattern)] -> [(Int, QualPattern)])
-> [(Int, QualPattern)] -> [(Int, QualPattern)]
forall a b. (a -> b) -> a -> b
$ [(Int, QualPattern)] -> [(Int, QualPattern)]
forall a. [a] -> [a]
reverse [(Int, QualPattern)]
ixs)
  [Symbol] -> [[Symbol]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
vSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys)
  where
    tyss :: [(Int, Sort, [Symbol])]
tyss       = (Int -> (Sort, [Symbol]) -> (Int, Sort, [Symbol]))
-> Tag -> [(Sort, [Symbol])] -> [(Int, Sort, [Symbol])]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i (Sort
t, [Symbol]
ys) -> (Int
i, Sort
t, [Symbol]
ys)) [Int
1..] (Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env)
    symToSrch :: Env
symToSrch  = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`F.lookupSEnvWithDistance` SEnv Sort
env)

instSymbol :: [(SortIdx, a, [F.Symbol])] -> [(SortIdx, QualPattern)] -> [[F.Symbol]]
instSymbol :: forall a.
[(Int, a, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
instSymbol [(Int, a, [Symbol])]
tyss = [(Int, QualPattern)] -> [[Symbol]]
go
  where
    m :: HashMap Int [Symbol]
m = [(Int, [Symbol])] -> HashMap Int [Symbol]
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Int
i, [Symbol]
ys) | (Int
i,a
_,[Symbol]
ys) <- [(Int, a, [Symbol])]
tyss]
    go :: [(Int, QualPattern)] -> [[Symbol]]
go [] =
      [Symbol] -> [[Symbol]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    go ((Int
i,QualPattern
qp):[(Int, QualPattern)]
is) = do
      Symbol
y   <- [Symbol] -> Int -> HashMap Int [Symbol] -> [Symbol]
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault [] Int
i HashMap Int [Symbol]
m
      QPSubst
qsu <- Maybe QPSubst -> [QPSubst]
forall a. Maybe a -> [a]
maybeToList (QualPattern -> Symbol -> Maybe QPSubst
matchSym QualPattern
qp Symbol
y)
      [Symbol]
ys  <- [(Int, QualPattern)] -> [[Symbol]]
go [ (Int
i', QPSubst -> QualPattern -> QualPattern
applyQPSubst QPSubst
qsu  QualPattern
qp') | (Int
i', QualPattern
qp') <- [(Int, QualPattern)]
is]
      [Symbol] -> [[Symbol]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
ySymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys)

instCands :: Bool -> F.SEnv F.Sort -> [(F.Sort, [F.Symbol])]
instCands :: Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env = ((Sort, [Symbol]) -> Bool)
-> [(Sort, [Symbol])] -> [(Sort, [Symbol])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Sort, [Symbol]) -> Bool
forall {b}. (Sort, b) -> Bool
isOk [(Sort, [Symbol])]
tyss
  where
    tyss :: [(Sort, [Symbol])]
tyss      = [(Sort, Symbol)] -> [(Sort, [Symbol])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Sort
t, Symbol
x) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts]
    isOk :: (Sort, b) -> Bool
isOk      = if Bool
ho then Bool -> (Sort, b) -> Bool
forall a b. a -> b -> a
const Bool
True else Maybe (Tag, [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Tag, [Sort], Sort) -> Bool)
-> ((Sort, b) -> Maybe (Tag, [Sort], Sort)) -> (Sort, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe (Tag, [Sort], Sort)
F.functionSort (Sort -> Maybe (Tag, [Sort], Sort))
-> ((Sort, b) -> Sort) -> (Sort, b) -> Maybe (Tag, [Sort], Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort, b) -> Sort
forall a b. (a, b) -> a
fst
    xts :: [(Symbol, Sort)]
xts       = SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env


type SortIdx = Int

matchP :: So.Env -> [(SortIdx, F.Sort, a)] -> [(SortIdx, QualPattern)] -> [F.QualParam] ->
          [[(SortIdx, QualPattern)]]
matchP :: forall a.
Env
-> [(Int, Sort, a)]
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
matchP Env
env [(Int, Sort, a)]
tyss = [(Int, QualPattern)] -> QCSig -> [[(Int, QualPattern)]]
go
  where
    go' :: Int
-> QualPattern
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
go' !Int
i !QualPattern
p ![(Int, QualPattern)]
is !QCSig
qps  = [(Int, QualPattern)] -> QCSig -> [[(Int, QualPattern)]]
go ((Int
i, QualPattern
p)(Int, QualPattern) -> [(Int, QualPattern)] -> [(Int, QualPattern)]
forall a. a -> [a] -> [a]
:[(Int, QualPattern)]
is) QCSig
qps
    go :: [(Int, QualPattern)] -> QCSig -> [[(Int, QualPattern)]]
go [(Int, QualPattern)]
is (QualParam
qp : QCSig
qps) = do (TVSubst
su, Int
i, QualPattern
pat) <- Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
forall a.
Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
candidatesP Env
env [(Int, Sort, a)]
tyss QualParam
qp
                          Int
-> QualPattern
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
go' Int
i QualPattern
pat [(Int, QualPattern)]
is (TVSubst -> QualParam -> QualParam
applyQPP TVSubst
su (QualParam -> QualParam) -> QCSig -> QCSig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QCSig
qps)
    go [(Int, QualPattern)]
is []         = [(Int, QualPattern)] -> [[(Int, QualPattern)]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, QualPattern)]
is

applyQPP :: So.TVSubst -> F.QualParam -> F.QualParam
applyQPP :: TVSubst -> QualParam -> QualParam
applyQPP TVSubst
su QualParam
qp = QualParam
qp
  { qpSort = So.apply     su  (qpSort qp)
  }

-- match :: So.Env -> [(F.Sort, [F.Symbol])] -> [F.Symbol] -> [F.QualParam] -> [[F.Symbol]]
-- match env tyss xs (qp : qps)
--   = do (su, qsu, x) <- candidates env tyss qp
--        match env tyss (x : xs) (applyQP su qsu <$> qps)
-- match _   _   xs []
--   = return xs

-- applyQP :: So.TVSubst -> QPSubst -> F.QualParam -> F.QualParam
-- applyQP su qsu qp = qp
--   { qpSort = So.apply     su  (qpSort qp)
--   , qpPat  = applyQPSubst qsu (qpPat qp)
--   }

--------------------------------------------------------------------------------
candidatesP :: So.Env -> [(SortIdx, F.Sort, a)] -> F.QualParam ->
               [(So.TVSubst, SortIdx, QualPattern)]
--------------------------------------------------------------------------------
candidatesP :: forall a.
Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
candidatesP Env
env [(Int, Sort, a)]
tyss QualParam
x =
    [(TVSubst
su, Int
idx, QualPattern
qPat)
        | (Int
idx, Sort
t,a
_)  <- [(Int, Sort, a)]
tyss
        , TVSubst
su          <- Maybe TVSubst -> [TVSubst]
forall a. Maybe a -> [a]
maybeToList (Bool -> Env -> Sort -> Sort -> Maybe TVSubst
So.unifyFast Bool
mono Env
env Sort
xt Sort
t)
    ]
  where
    xt :: Sort
xt   = QualParam -> Sort
F.qpSort QualParam
x
    qPat :: QualPattern
qPat = QualParam -> QualPattern
F.qpPat  QualParam
x
    mono :: Bool
mono = Sort -> Bool
So.isMono Sort
xt

-- --------------------------------------------------------------------------------
-- candidates :: So.Env -> [(F.Sort, [F.Symbol])] -> F.QualParam
--            -> [(So.TVSubst, QPSubst, F.Symbol)]
-- --------------------------------------------------------------------------------
-- candidates env tyss x = -- traceShow _msg
--     [(su, qsu, y) | (t, ys)  <- tyss
--                   , su       <- maybeToList (So.unifyFast mono env xt t)
--                   , y        <- ys
--                   , qsu      <- maybeToList (matchSym x y)
--     ]
--   where
--     xt   = F.qpSort x
--     mono = So.isMono xt
--     _msg = "candidates tyss :=" ++ F.showpp tyss ++ "tx := " ++ F.showpp xt

matchSym :: F.QualPattern -> F.Symbol -> Maybe QPSubst
matchSym :: QualPattern -> Symbol -> Maybe QPSubst
matchSym QualPattern
qp Symbol
y' = case QualPattern
qp of
  F.PatPrefix Symbol
s Int
i -> Int -> Symbol -> QPSubst
JustSub Int
i (Symbol -> QPSubst) -> Maybe Symbol -> Maybe QPSubst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Symbol -> Maybe Symbol
F.stripPrefix Symbol
s Symbol
y
  F.PatSuffix Int
i Symbol
s -> Int -> Symbol -> QPSubst
JustSub Int
i (Symbol -> QPSubst) -> Maybe Symbol -> Maybe QPSubst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Symbol -> Maybe Symbol
F.stripSuffix Symbol
s Symbol
y
  QualPattern
F.PatNone       -> QPSubst -> Maybe QPSubst
forall a. a -> Maybe a
Just QPSubst
NoSub
  F.PatExact Symbol
s    -> if Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
y then QPSubst -> Maybe QPSubst
forall a. a -> Maybe a
Just QPSubst
NoSub else Maybe QPSubst
forall a. Maybe a
Nothing
  where
    y :: Symbol
y             =  Symbol -> Symbol
F.unKArgSymbol Symbol
y'

data QPSubst = NoSub | JustSub Int F.Symbol

applyQPSubst :: QPSubst -> F.QualPattern -> F.QualPattern
applyQPSubst :: QPSubst -> QualPattern -> QualPattern
applyQPSubst (JustSub Int
i Symbol
x) (F.PatPrefix Symbol
s Int
j)
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = Symbol -> QualPattern
F.PatExact (Symbol -> Symbol -> Symbol
F.mappendSym Symbol
s Symbol
x)
applyQPSubst (JustSub Int
i Symbol
x) (F.PatSuffix Int
j Symbol
s)
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = Symbol -> QualPattern
F.PatExact (Symbol -> Symbol -> Symbol
F.mappendSym Symbol
x Symbol
s)
applyQPSubst QPSubst
_ QualPattern
p
  = QualPattern
p

--------------------------------------------------------------------------------
okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> ElabM Bool
--------------------------------------------------------------------------------
okInst :: SEnv Sort
-> Symbol -> Sort -> EQual -> ReaderT ElabFlags Identity Bool
okInst SEnv Sort
env Symbol
v Sort
t EQual
eq =
  do Maybe Doc
tc <- SrcSpan -> SEnv Sort -> SortedReft -> ElabM (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv Sort -> a -> ElabM (Maybe Doc)
So.checkSorted (EQual -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan EQual
eq) SEnv Sort
env SortedReft
sr
     Bool -> ReaderT ElabFlags Identity Bool
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> ReaderT ElabFlags Identity Bool)
-> Bool -> ReaderT ElabFlags Identity Bool
forall a b. (a -> b) -> a -> b
$ Maybe Doc -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Doc
tc
  where
    sr :: SortedReft
sr            = Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, Expr) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
v, Expr
p))
    p :: Expr
p             = EQual -> Expr
Sol.eqPred EQual
eq

    -- _msg          = printf "okInst: t = %s, eq = %s, env = %s" (F.showpp t) (F.showpp eq) (F.showpp env)


--------------------------------------------------------------------------------
-- | Predicate corresponding to LHS of constraint in current solution
--------------------------------------------------------------------------------
{-# SCC lhsPred #-}
lhsPred
  :: (F.Loc a)
  => Config
  -> F.IBindEnv
  -> F.BindEnv a
  -> Sol.Solution
  -> F.SimpC a
  -> F.Expr
lhsPred :: forall a.
Loc a =>
Config -> IBindEnv -> BindEnv a -> Solution -> SimpC a -> Expr
lhsPred Config
cfg IBindEnv
bindingsInSmt BindEnv a
be Solution
s SimpC a
c =
    let ap :: ExprInfo
ap = Config -> CombinedEnv a -> Solution -> IBindEnv -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> IBindEnv -> ExprInfo
apply Config
cfg CombinedEnv a
g Solution
s IBindEnv
bs
     in [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
_msg (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Expr
forall a b. (a, b) -> a
fst ExprInfo
ap
  where
    g :: CombinedEnv a
g          = Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
forall a.
Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
CEnv Cid
ci BindEnv a
be IBindEnv
bs (SimpC a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan SimpC a
c) IBindEnv
bindingsInSmt
    bs :: IBindEnv
bs         = SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
c
    ci :: Cid
ci         = SimpC a -> Cid
forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC a
c
    _msg :: [Char]
_msg       = [Char]
"LhsPred for id = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Cid -> [Char]
forall a. Show a => a -> [Char]
show (SimpC a -> Cid
forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC a
c) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" with SOLUTION = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Solution -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Solution
s

data CombinedEnv a = CEnv
  { forall a. CombinedEnv a -> Cid
ceCid  :: !Cid
  , forall a. CombinedEnv a -> BindEnv a
ceBEnv :: !(F.BindEnv a)
  , forall a. CombinedEnv a -> IBindEnv
ceIEnv :: !F.IBindEnv
  , forall a. CombinedEnv a -> SrcSpan
ceSpan :: !F.SrcSpan
    -- | These are the bindings that the smt solver knows about and can be
    -- referred as @EVar (bindSymbol <bindId>)@ instead of serializing them
    -- again.
  , forall a. CombinedEnv a -> IBindEnv
ceBindingsInSmt :: !F.IBindEnv
  }

type Cid         = Maybe Integer
type ExprInfo    = (F.Expr, KInfo)

apply :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.IBindEnv -> ExprInfo
apply :: forall ann.
Config -> CombinedEnv ann -> Solution -> IBindEnv -> ExprInfo
apply Config
cfg CombinedEnv ann
g Solution
s IBindEnv
bs =
    -- Clear the "known" bindings for applyKVars, since it depends on
    -- using the fully expanded representation of the predicates to bind their
    -- variables with quantifiers.
    let xrs :: [(Symbol, SortedReft)]
xrs = (Int -> (Symbol, SortedReft)) -> Tag -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> [a] -> [b]
map (CombinedEnv ann -> Int -> (Symbol, SortedReft)
forall ann. CombinedEnv ann -> Int -> (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv ann
g) (IBindEnv -> Tag
F.elemsIBindEnv IBindEnv
bs)
        ([Expr]
ps,  [KVSub]
ks) = [(Symbol, SortedReft)] -> ([Expr], [KVSub])
envConcKVars [(Symbol, SortedReft)]
xrs
        (Expr
pks, KInfo
kI) = Config -> CombinedEnv ann -> Solution -> [KVSub] -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> [KVSub] -> ExprInfo
applyKVars Config
cfg CombinedEnv ann
g {ceBindingsInSmt = F.emptyIBindEnv} Solution
s [KVSub]
ks
     in ([Expr] -> Expr
F.conj (Expr
pksExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
ps), KInfo
kI)   -- see [NOTE: pAnd-SLOW]

-- | @applyInSortedReft@ applies the solution to a single sorted reft
applyInSortedReft
  :: Config
  -> CombinedEnv ann
  -> Sol.Sol Sol.QBind
  -> (F.Symbol, F.SortedReft)
  -> (F.Symbol, F.SortedReft)
applyInSortedReft :: forall ann.
Config
-> CombinedEnv ann
-> Solution
-> (Symbol, SortedReft)
-> (Symbol, SortedReft)
applyInSortedReft Config
cfg CombinedEnv ann
g Solution
s xsr :: (Symbol, SortedReft)
xsr@(Symbol
x, SortedReft
sr) =
    let ([Expr]
ps,  [KVSub]
ks) = [(Symbol, SortedReft)] -> ([Expr], [KVSub])
envConcKVars [(Symbol, SortedReft)
xsr]
        (Expr
pks, KInfo
_) = Config -> CombinedEnv ann -> Solution -> [KVSub] -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> [KVSub] -> ExprInfo
applyKVars Config
cfg CombinedEnv ann
g {ceBindingsInSmt = F.emptyIBindEnv} Solution
s [KVSub]
ks
     in (Symbol
x, SortedReft
sr { F.sr_reft = F.Reft (x, F.conj (pks : ps)) })

-- | Produces conjuncts of each sorted reft in the IBindEnv, separated
-- into concrete conjuncts and kvars.
envConcKVars :: [(F.Symbol, F.SortedReft)] -> ([F.Expr], [F.KVSub])
envConcKVars :: [(Symbol, SortedReft)] -> ([Expr], [KVSub])
envConcKVars [(Symbol, SortedReft)]
xrs =
  let ([[Expr]]
pss, [[KVSub]]
kss) = [([Expr], [KVSub])] -> ([[Expr]], [[KVSub]])
forall a b. [(a, b)] -> ([a], [b])
unzip [ Symbol -> SortedReft -> ([Expr], [KVSub])
F.sortedReftConcKVars Symbol
x SortedReft
sr | (Symbol
x, SortedReft
sr) <- [(Symbol, SortedReft)]
xrs ]
   in ([[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Expr]]
pss, [[KVSub]] -> [KVSub]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[KVSub]]
kss)

lookupBindEnvExt
  :: CombinedEnv ann -> F.BindId -> (F.Symbol, F.SortedReft)
lookupBindEnvExt :: forall ann. CombinedEnv ann -> Int -> (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv ann
g Int
i =
     (,) Symbol
x (SortedReft -> (Symbol, SortedReft))
-> SortedReft -> (Symbol, SortedReft)
forall a b. (a -> b) -> a -> b
$
       if Int -> IBindEnv -> Bool
F.memberIBindEnv Int
i (CombinedEnv ann -> IBindEnv
forall a. CombinedEnv a -> IBindEnv
ceBindingsInSmt CombinedEnv ann
g)
       then SortedReft
sr { F.sr_reft = F.Reft (x, F.EVar (F.bindSymbol (fromIntegral i)))}
       else SortedReft
sr
   where
      (Symbol
x, SortedReft
sr, ann
_)              = Int -> BindEnv ann -> (Symbol, SortedReft, ann)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv Int
i (CombinedEnv ann -> BindEnv ann
forall a. CombinedEnv a -> BindEnv a
ceBEnv CombinedEnv ann
g)

applyKVars :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> [F.KVSub] -> ExprInfo
applyKVars :: forall ann.
Config -> CombinedEnv ann -> Solution -> [KVSub] -> ExprInfo
applyKVars Config
cfg CombinedEnv ann
g Solution
s [KVSub]
ks =
  let bcs :: [ExprInfo]
bcs = (KVSub -> ExprInfo) -> [KVSub] -> [ExprInfo]
forall a b. (a -> b) -> [a] -> [b]
map (Config -> CombinedEnv ann -> Solution -> KVSub -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> KVSub -> ExprInfo
applyKVar Config
cfg CombinedEnv ann
g Solution
s) [KVSub]
ks
      ([Expr]
es, [KInfo]
is) = [ExprInfo] -> ([Expr], [KInfo])
forall a b. [(a, b)] -> ([a], [b])
unzip [ExprInfo]
bcs
   in ([Expr] -> Expr
F.pAndNoDedup [Expr]
es, [KInfo] -> KInfo
forall a. Monoid a => [a] -> a
mconcat [KInfo]
is)

applyKVar :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVSub -> ExprInfo
applyKVar :: forall ann.
Config -> CombinedEnv ann -> Solution -> KVSub -> ExprInfo
applyKVar Config
cfg  CombinedEnv ann
g Solution
s KVSub
ksu = case Solution -> KVar -> Either Hyp QBind
Sol.lookup Solution
s (KVSub -> KVar
F.ksuKVar KVSub
ksu) of
  Left Hyp
cs   -> Config -> CombinedEnv ann -> Solution -> KVSub -> Hyp -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> KVSub -> Hyp -> ExprInfo
hypPred Config
cfg CombinedEnv ann
g Solution
s KVSub
ksu Hyp
cs
  Right QBind
eqs -> let qbp :: [(Expr, EQual)]
qbp = Subst -> QBind -> [(Expr, EQual)]
Sol.qbPreds (KVSub -> Subst
F.ksuSubst KVSub
ksu) QBind
eqs
                in ([Expr] -> Expr
F.pAndNoDedup ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr, EQual) -> Expr
forall a b. (a, b) -> a
fst ((Expr, EQual) -> Expr) -> [(Expr, EQual)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr, EQual)]
qbp, KInfo
forall a. Monoid a => a
mempty) -- TODO: don't initialize kvars that have a hyp solution

mkNonCutsExpr :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVar -> Sol.Hyp -> F.Expr
mkNonCutsExpr :: forall ann.
Config -> CombinedEnv ann -> Solution -> KVar -> Hyp -> Expr
mkNonCutsExpr Config
cfg CombinedEnv ann
ce Solution
s KVar
k Hyp
cs =
  let bcps :: [Expr]
bcps = (Cube -> Expr) -> Hyp -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Config -> CombinedEnv ann -> Solution -> KVar -> Cube -> Expr
forall ann.
Config -> CombinedEnv ann -> Solution -> KVar -> Cube -> Expr
bareCubePred Config
cfg CombinedEnv ann
ce Solution
s KVar
k) Hyp
cs
   in [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pOr [Expr]
bcps

nonCutsResult :: Config -> F.BindEnv ann -> Sol.Sol Sol.QBind -> FixDelayedSolution
nonCutsResult :: forall ann. Config -> BindEnv ann -> Solution -> FixDelayedSolution
nonCutsResult Config
cfg BindEnv ann
be Solution
s = (KVar -> Hyp -> Delayed Expr)
-> HashMap KVar Hyp -> FixDelayedSolution
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (\KVar
k -> Expr -> Delayed Expr
forall a. a -> Delayed a
Delayed (Expr -> Delayed Expr) -> (Hyp -> Expr) -> Hyp -> Delayed Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> CombinedEnv ann -> Solution -> KVar -> Hyp -> Expr
forall ann.
Config -> CombinedEnv ann -> Solution -> KVar -> Hyp -> Expr
mkNonCutsExpr Config
cfg CombinedEnv ann
g Solution
s KVar
k) (HashMap KVar Hyp -> FixDelayedSolution)
-> HashMap KVar Hyp -> FixDelayedSolution
forall a b. (a -> b) -> a -> b
$ Solution -> HashMap KVar Hyp
forall a. Sol a -> HashMap KVar Hyp
Sol.sHyp Solution
s
  where
    g :: CombinedEnv ann
g = Cid
-> BindEnv ann
-> IBindEnv
-> SrcSpan
-> IBindEnv
-> CombinedEnv ann
forall a.
Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
CEnv Cid
forall a. Maybe a
Nothing BindEnv ann
be IBindEnv
F.emptyIBindEnv SrcSpan
F.dummySpan IBindEnv
F.emptyIBindEnv


-- | Produces a predicate from a constraint defining a kvar.
--
-- This is written in imitation of 'cubePred'. However, there are some
-- differences since the result of 'cubePred' is fed to the verification
-- pipeline and @bareCubePred@ is meant for human inspection.
--
-- The expression is created from its defining constraints only, while
-- @cubePred@ does expect the caller to supply the substitution at a
-- particular use of the KVar. Thus @cubePred@ produces a different
-- expression for every use site of the kvar, while here we produce one
-- expression for all the uses.
--
-- Where the cube rhs is @k[params:=xts]@, we keep the parameters free in the
-- final predicate. e.g. @params == xts && exists yts . ...@
-- That is, we only quantify out the `yts` as we want to make
-- explicit what equalities those parameters have in each cube.
--
-- Issue https://github.com/ucsd-progsys/liquid-fixpoint/issues/808 discusses
-- an example where the equalities are essential to keep.

bareCubePred :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVar -> Sol.Cube -> F.Expr
bareCubePred :: forall ann.
Config -> CombinedEnv ann -> Solution -> KVar -> Cube -> Expr
bareCubePred Config
cfg CombinedEnv ann
g Solution
s KVar
k Cube
c =
    let psu :: Expr
psu = [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EEq (Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
x) Expr
e | (Symbol
x, Expr
e) <- HashMap Symbol Expr -> [(Symbol, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol Expr
m ]
        (Expr
p, KInfo
_kI) = Config -> CombinedEnv ann -> Solution -> IBindEnv -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> IBindEnv -> ExprInfo
apply Config
cfg CombinedEnv ann
g' Solution
s IBindEnv
bs
     in [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.pExist [(Symbol, Sort)]
yts (Expr
p Expr -> Expr -> Expr
F.&.& Expr
psu)
  where
    bs :: IBindEnv
bs = Cube -> IBindEnv
Sol.cuBinds Cube
c
    F.Su HashMap Symbol Expr
m = Config -> CombinedEnv ann -> Subst -> Subst
forall ann. Config -> CombinedEnv ann -> Subst -> Subst
dropUnsortedExprs Config
cfg CombinedEnv ann
g' (Cube -> Subst
Sol.cuSubst Cube
c)
    g' :: CombinedEnv ann
g' = CombinedEnv ann -> IBindEnv -> CombinedEnv ann
forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv  CombinedEnv ann
g IBindEnv
bs
    bs' :: IBindEnv
bs' = IBindEnv -> IBindEnv -> IBindEnv
F.diffIBindEnv IBindEnv
bs ([Char] -> KVar -> HashMap KVar IBindEnv -> IBindEnv
forall k v.
(HasCallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
Misc.safeLookup [Char]
"sScp" KVar
k (Solution -> HashMap KVar IBindEnv
forall a. Sol a -> HashMap KVar IBindEnv
Sol.sScp Solution
s))
    yts :: [(Symbol, Sort)]
yts = CombinedEnv ann -> IBindEnv -> [(Symbol, Sort)]
forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv ann
g IBindEnv
bs'

-- | At the moment, the liquid-fixpoint implementation allows for unsorted
-- expressions in substitutions. See the discussion in
-- https://github.com/ucsd-progsys/liquid-fixpoint/issues/800
-- The `explicitKvars` flag is meant for Horn-style constraints, which must
-- have well-formed (expressions) as arguments, and so we *disable* the
-- filtering of unsorted expressions when that flag is set.
dropUnsortedExprs :: Config -> CombinedEnv ann -> F.Subst -> F.Subst
dropUnsortedExprs :: forall ann. Config -> CombinedEnv ann -> Subst -> Subst
dropUnsortedExprs Config
cfg CombinedEnv ann
g su :: Subst
su@(F.Su HashMap Symbol Expr
m)
  | Config -> Bool
explicitKvars Config
cfg = Subst
su
  | Bool
otherwise         = HashMap Symbol Expr -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
F.Su (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$
    (Expr -> Bool) -> HashMap Symbol Expr -> HashMap Symbol Expr
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter
      (\Expr
e -> Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
         Sort
t <- SrcSpan -> SEnv Sort -> Expr -> Maybe Sort
So.checkSortExpr SrcSpan
sp SEnv Sort
env Expr
e
         Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Sort -> Bool
isClass Sort
t))
      )
      HashMap Symbol Expr
m
  where
    sp :: SrcSpan
sp  = CombinedEnv ann -> SrcSpan
forall a. CombinedEnv a -> SrcSpan
ceSpan CombinedEnv ann
g
    env :: SEnv Sort
env = CombinedEnv ann -> SEnv Sort
forall a. CombinedEnv a -> SEnv Sort
combinedSEnv CombinedEnv ann
g

hypPred :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVSub -> Sol.Hyp -> ExprInfo
hypPred :: forall ann.
Config -> CombinedEnv ann -> Solution -> KVSub -> Hyp -> ExprInfo
hypPred Config
cfg CombinedEnv ann
g Solution
s KVSub
ksu Hyp
hyp =
  let cs :: [ExprInfo]
cs = (Cube -> ExprInfo) -> Hyp -> [ExprInfo]
forall a b. (a -> b) -> [a] -> [b]
map (Config -> CombinedEnv ann -> Solution -> KVSub -> Cube -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> KVSub -> Cube -> ExprInfo
cubePred Config
cfg CombinedEnv ann
g Solution
s KVSub
ksu) Hyp
hyp
   in [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pOr ([Expr] -> Expr)
-> ([KInfo] -> KInfo) -> ([Expr], [KInfo]) -> ExprInfo
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [KInfo] -> KInfo
mconcatPlus (([Expr], [KInfo]) -> ExprInfo) -> ([Expr], [KInfo]) -> ExprInfo
forall a b. (a -> b) -> a -> b
$ [ExprInfo] -> ([Expr], [KInfo])
forall a b. [(a, b)] -> ([a], [b])
unzip [ExprInfo]
cs

{- | `cubePred g s k su c` returns the predicate for

        (k . su)

      defined by using cube

        c := [b1,...,bn] |- (k . su')

      in the binder environment `g`. The binders in `sScp s k` are not included
      in the final predicate. They are considered redundant conjuncts as per
      section 2.4 of "Local Refinement Typing", ICFP 2017.
 -}
cubePred :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVSub -> Sol.Cube -> ExprInfo
cubePred :: forall ann.
Config -> CombinedEnv ann -> Solution -> KVSub -> Cube -> ExprInfo
cubePred Config
cfg CombinedEnv ann
g Solution
s KVSub
ksu Cube
c    =
    let (Expr
p, KInfo
kI) = Config
-> CombinedEnv ann -> Solution -> Cube -> IBindEnv -> ExprInfo
forall ann.
Config
-> CombinedEnv ann -> Solution -> Cube -> IBindEnv -> ExprInfo
cubePredExc Config
cfg CombinedEnv ann
g Solution
s Cube
c IBindEnv
bs'
        -- Free variables in p should not colide with those generated by
        -- the rapier substitution. If that were the case, perhaps we would
        -- need to include @combinedSEnv g@ in the scope set.
     in (HashSet Symbol -> Subst -> Expr -> Expr
F.rapierSubstExpr (Subst -> HashSet Symbol
F.substSymbolsSet Subst
su) Subst
su Expr
p, KInfo
kI)
  where
    bs' :: IBindEnv
bs' = IBindEnv -> IBindEnv -> IBindEnv
F.diffIBindEnv IBindEnv
bs ([Char] -> KVar -> HashMap KVar IBindEnv -> IBindEnv
forall k v.
(HasCallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
Misc.safeLookup [Char]
"sScp" KVar
k (Solution -> HashMap KVar IBindEnv
forall a. Sol a -> HashMap KVar IBindEnv
Sol.sScp Solution
s))
    bs :: IBindEnv
bs  = Cube -> IBindEnv
Sol.cuBinds Cube
c
    k :: KVar
k   = KVSub -> KVar
F.ksuKVar KVSub
ksu
    su :: Subst
su = Config -> CombinedEnv ann -> Subst -> Subst
forall ann. Config -> CombinedEnv ann -> Subst -> Subst
dropUnsortedExprs Config
cfg CombinedEnv ann
g (KVSub -> Subst
F.ksuSubst  KVSub
ksu)

-- | @cubePredExc@ computes the predicate for the subset of binders bs'.
--
-- Schematically, the result is
--
-- > Exists (bindsOf bs'). (pAnd (predicatesOf bs'))[Sol.cuSubst c]
--
-- but we also preserve the information about which variables are being
-- substituted:
--
-- > Exists (bindsOf bs'). pAnd (predicatesOf bs') && x1=e1 && ... && xn=en
--
-- where @Sol.cuSubst c = [x1:=e1;...;xn:=en]@.
--
cubePredExc :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> Sol.Cube -> F.IBindEnv
            -> (F.Pred, KInfo)
cubePredExc :: forall ann.
Config
-> CombinedEnv ann -> Solution -> Cube -> IBindEnv -> ExprInfo
cubePredExc Config
cfg CombinedEnv ann
g Solution
s Cube
c IBindEnv
bs' =
    let psu' :: Expr
psu' = [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EEq (Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
x) Expr
e | (Symbol
x, Expr
e) <- HashMap Symbol Expr -> [(Symbol, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol Expr
m ]
        (Expr
p', KInfo
kI) = Config -> CombinedEnv ann -> Solution -> IBindEnv -> ExprInfo
forall ann.
Config -> CombinedEnv ann -> Solution -> IBindEnv -> ExprInfo
apply Config
cfg CombinedEnv ann
g' Solution
s IBindEnv
bs'
        cubeE :: Expr
cubeE = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.pExist [(Symbol, Sort)]
yts' ([Expr] -> Expr
F.pAndNoDedup [Expr
p', Expr
psu'])
     in (Expr
cubeE, KInfo -> Tag -> KInfo
extendKInfo KInfo
kI (Cube -> Tag
Sol.cuTag Cube
c))
  where
    yts' :: [(Symbol, Sort)]
yts' = CombinedEnv ann -> IBindEnv -> [(Symbol, Sort)]
forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv ann
g IBindEnv
bs'
    g' :: CombinedEnv ann
g' = CombinedEnv ann -> IBindEnv -> CombinedEnv ann
forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv  CombinedEnv ann
g IBindEnv
bs
    F.Su HashMap Symbol Expr
m = Config -> CombinedEnv ann -> Subst -> Subst
forall ann. Config -> CombinedEnv ann -> Subst -> Subst
dropUnsortedExprs Config
cfg CombinedEnv ann
g' (Cube -> Subst
Sol.cuSubst Cube
c)
    bs :: IBindEnv
bs = Cube -> IBindEnv
Sol.cuBinds Cube
c

isClass :: F.Sort -> Bool
isClass :: Sort -> Bool
isClass Sort
F.FNum  = Bool
True
isClass Sort
F.FFrac = Bool
True
isClass Sort
_       = Bool
False

combinedSEnv :: CombinedEnv a -> F.SEnv F.Sort
combinedSEnv :: forall a. CombinedEnv a -> SEnv Sort
combinedSEnv CombinedEnv a
g = SortedReft -> Sort
F.sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs BindEnv a
be IBindEnv
bs)
  where
    be :: BindEnv a
be         = CombinedEnv a -> BindEnv a
forall a. CombinedEnv a -> BindEnv a
ceBEnv CombinedEnv a
g
    bs :: IBindEnv
bs         = CombinedEnv a -> IBindEnv
forall a. CombinedEnv a -> IBindEnv
ceIEnv CombinedEnv a
g

addCEnv :: CombinedEnv a -> F.IBindEnv -> CombinedEnv a
addCEnv :: forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv CombinedEnv a
g IBindEnv
bs' = CombinedEnv a
g { ceIEnv = F.unionIBindEnv (ceIEnv g) bs' }

symSorts :: CombinedEnv a -> F.IBindEnv -> [(F.Symbol, F.Sort)]
symSorts :: forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv a
g IBindEnv
bs = (SortedReft -> Sort) -> (Symbol, SortedReft) -> (Symbol, Sort)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second SortedReft -> Sort
F.sr_sort ((Symbol, SortedReft) -> (Symbol, Sort))
-> [(Symbol, SortedReft)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (CombinedEnv a -> BindEnv a
forall a. CombinedEnv a -> BindEnv a
ceBEnv CombinedEnv a
g) IBindEnv
bs

_noKvars :: F.Expr -> Bool
_noKvars :: Expr -> Bool
_noKvars = [KVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([KVar] -> Bool) -> (Expr -> [KVar]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [KVar]
forall v. ExprV v -> [KVar]
V.kvarsExpr

--------------------------------------------------------------------------------
-- | Information about size of formula corresponding to an "eliminated" KVar.
--------------------------------------------------------------------------------
data KInfo = KI { KInfo -> [Tag]
kiTags  :: [Tag]
                , KInfo -> Int
kiDepth :: !Int
                , KInfo -> Integer
kiCubes :: !Integer
                } deriving (KInfo -> KInfo -> Bool
(KInfo -> KInfo -> Bool) -> (KInfo -> KInfo -> Bool) -> Eq KInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KInfo -> KInfo -> Bool
== :: KInfo -> KInfo -> Bool
$c/= :: KInfo -> KInfo -> Bool
/= :: KInfo -> KInfo -> Bool
Eq, Eq KInfo
Eq KInfo =>
(KInfo -> KInfo -> Ordering)
-> (KInfo -> KInfo -> Bool)
-> (KInfo -> KInfo -> Bool)
-> (KInfo -> KInfo -> Bool)
-> (KInfo -> KInfo -> Bool)
-> (KInfo -> KInfo -> KInfo)
-> (KInfo -> KInfo -> KInfo)
-> Ord KInfo
KInfo -> KInfo -> Bool
KInfo -> KInfo -> Ordering
KInfo -> KInfo -> KInfo
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 :: KInfo -> KInfo -> Ordering
compare :: KInfo -> KInfo -> Ordering
$c< :: KInfo -> KInfo -> Bool
< :: KInfo -> KInfo -> Bool
$c<= :: KInfo -> KInfo -> Bool
<= :: KInfo -> KInfo -> Bool
$c> :: KInfo -> KInfo -> Bool
> :: KInfo -> KInfo -> Bool
$c>= :: KInfo -> KInfo -> Bool
>= :: KInfo -> KInfo -> Bool
$cmax :: KInfo -> KInfo -> KInfo
max :: KInfo -> KInfo -> KInfo
$cmin :: KInfo -> KInfo -> KInfo
min :: KInfo -> KInfo -> KInfo
Ord, Int -> KInfo -> [Char] -> [Char]
[KInfo] -> [Char] -> [Char]
KInfo -> [Char]
(Int -> KInfo -> [Char] -> [Char])
-> (KInfo -> [Char]) -> ([KInfo] -> [Char] -> [Char]) -> Show KInfo
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> KInfo -> [Char] -> [Char]
showsPrec :: Int -> KInfo -> [Char] -> [Char]
$cshow :: KInfo -> [Char]
show :: KInfo -> [Char]
$cshowList :: [KInfo] -> [Char] -> [Char]
showList :: [KInfo] -> [Char] -> [Char]
Show)

instance Semigroup KInfo where
  KInfo
ki <> :: KInfo -> KInfo -> KInfo
<> KInfo
ki' = [Tag] -> Int -> Integer -> KInfo
KI [Tag]
ts Int
d Integer
s
    where
      ts :: [Tag]
ts    = [Tag] -> [Tag] -> [Tag]
appendTags (KInfo -> [Tag]
kiTags  KInfo
ki) (KInfo -> [Tag]
kiTags  KInfo
ki')
      d :: Int
d     = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max        (KInfo -> Int
kiDepth KInfo
ki) (KInfo -> Int
kiDepth KInfo
ki')
      s :: Integer
s     = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*)        (KInfo -> Integer
kiCubes KInfo
ki) (KInfo -> Integer
kiCubes KInfo
ki')

instance Monoid KInfo where
  mempty :: KInfo
mempty  = [Tag] -> Int -> Integer -> KInfo
KI [] Int
0 Integer
1
  mappend :: KInfo -> KInfo -> KInfo
mappend = KInfo -> KInfo -> KInfo
forall a. Semigroup a => a -> a -> a
(<>)

mplusKInfo :: KInfo -> KInfo -> KInfo
mplusKInfo :: KInfo -> KInfo -> KInfo
mplusKInfo KInfo
ki KInfo
ki' = (KInfo -> KInfo -> KInfo
forall a. Monoid a => a -> a -> a
mappend KInfo
ki KInfo
ki') { kiCubes = kiCubes ki + kiCubes ki'}

mconcatPlus :: [KInfo] -> KInfo
mconcatPlus :: [KInfo] -> KInfo
mconcatPlus = (KInfo -> KInfo -> KInfo) -> KInfo -> [KInfo] -> KInfo
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr KInfo -> KInfo -> KInfo
mplusKInfo KInfo
forall a. Monoid a => a
mempty

appendTags :: [Tag] -> [Tag] -> [Tag]
appendTags :: [Tag] -> [Tag] -> [Tag]
appendTags [Tag]
ts [Tag]
ts' = [Tag] -> [Tag]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Tag]
ts [Tag] -> [Tag] -> [Tag]
forall a. [a] -> [a] -> [a]
++ [Tag]
ts')

extendKInfo :: KInfo -> F.Tag -> KInfo
extendKInfo :: KInfo -> Tag -> KInfo
extendKInfo KInfo
ki Tag
t = KInfo
ki { kiTags  = appendTags [t] (kiTags  ki)
                      , kiDepth = 1  +            kiDepth ki }

-- | Simplifies existential expressions with unused or inconsequential bindings.
--
-- Simplification is helpful for human readability of solutions. It makes easier
-- reporting errors. Sometimes it can be useful for debugging if run on queries
-- sent to the SMT solver. We don't do that by default because some benchmarks
-- show a slowdown in some cases.
--
-- For instance, in the following example, "x" is not used at all.
--
-- > simplifyKVar "exists x y. y == z && y == C"
-- >   ==
-- > "exists y. y == z && y == C"
--
-- And in the following example, @x@ is used but in a way that doesn't
-- contribute any useful knowledge.
--
-- > simplifyKVar "exists x y. x == C && y == z && y == C"
-- >   ==
-- > "exists y. y == z && y == C"
--
-- Therefore we eliminate variables that appear in equalities via substitutions.
--
-- > simplifyKVar "exists x y. x == C && P && Q y"
-- >   ==
-- > "exists y. (P && Q y)[x:=C]"
--
-- The first parameter is the set of symbols that can appear free in the input
-- expression. At the moment, this only needs to include the free variables that
-- start with the @subst$@ prefix.
--
simplifyKVar :: S.HashSet F.Symbol -> F.Expr -> F.Expr
simplifyKVar :: HashSet Symbol -> Expr -> Expr
simplifyKVar HashSet Symbol
s0 = [Expr] -> Expr
F.conj ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet Symbol -> [Expr] -> [Expr]
dedupByAlphaEq HashSet Symbol
s0 ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
floatPExistConjuncts (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet Symbol -> Expr -> Expr
go HashSet Symbol
s0
  where
    go :: HashSet Symbol -> Expr -> Expr
go HashSet Symbol
s (F.POr [Expr]
es) = [Expr] -> Expr
disj ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map ([Expr] -> Expr
F.conj ([Expr] -> Expr) -> (Expr -> [Expr]) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
floatPExistConjuncts (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet Symbol -> Expr -> Expr
go HashSet Symbol
s) [Expr]
es
    go HashSet Symbol
s (F.PAnd [Expr]
es) = [Expr] -> Expr
F.conj ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> [Expr] -> [Expr]
dedupByAlphaEq HashSet Symbol
forall a. HashSet a
S.empty ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> [Expr]
floatPExistConjuncts (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet Symbol -> Expr -> Expr
go HashSet Symbol
s) [Expr]
es
    go HashSet Symbol
s (F.PExist [(Symbol, Sort)]
bs Expr
e0) =
      let es :: [Expr]
es = (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> [Expr]
floatPExistConjuncts (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet Symbol -> Expr -> Expr
go (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashSet Symbol
s (HashSet Symbol -> HashSet Symbol)
-> HashSet Symbol -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs)) (Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
F.conjuncts Expr
e0)
       in Expr -> Expr
elimExistentialBinds ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.PExist [(Symbol, Sort)]
bs ([Expr] -> Expr
F.conj [Expr]
es))
    go HashSet Symbol
_ Expr
e = Expr
e

    dedupByAlphaEq :: S.HashSet F.Symbol -> [F.Expr] -> [F.Expr]
    dedupByAlphaEq :: HashSet Symbol -> [Expr] -> [Expr]
dedupByAlphaEq HashSet Symbol
s = (Expr -> Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> a -> Bool) -> [a] -> [a]
List.nubBy (\Expr
e1 Expr
e2 -> HashSet Symbol -> Expr -> Expr -> Bool
alphaEq HashSet Symbol
s Expr
e1 Expr
e2)

    disj :: [F.Expr] -> F.Expr
    disj :: [Expr] -> Expr
disj [] = Expr
forall v. ExprV v
F.PFalse
    disj [Expr
e] = Expr
e
    disj [Expr]
es = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.POr [Expr]
es

    elimExistentialBinds :: Expr -> Expr
elimExistentialBinds (F.PExist [(Symbol, Sort)]
bs0 (F.PExist [(Symbol, Sort)]
bs1 Expr
p)) =
      let bs0' :: [(Symbol, Sort)]
bs0' = ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Symbol
x,Sort
_) -> Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs1) [(Symbol, Sort)]
bs0
       in Expr -> Expr
elimExistentialBinds ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.PExist ([(Symbol, Sort)]
bs0' [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
bs1) Expr
p)
    elimExistentialBinds (F.PExist [(Symbol, Sort)]
bs Expr
e0) =
      let es :: [Expr]
es = Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
F.conjuncts Expr
e0
          esv :: [(Maybe (Symbol, Expr), Expr)]
esv = (Expr -> (Maybe (Symbol, Expr), Expr))
-> [Expr] -> [(Maybe (Symbol, Expr), Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ([Symbol] -> Expr -> (Maybe (Symbol, Expr), Expr)
isVarEq (((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs)) [Expr]
es
          -- Eliminating multiple variables at once can be difficult if the
          -- equalities define cyclic dependencies, so we only eliminate one
          -- variable at a time.
          esvElim :: [(Symbol, Expr)]
esvElim = Int -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. Int -> [a] -> [a]
take Int
1 [ (Symbol
x, Expr
v) | (Just (Symbol
x, Expr
v), Expr
_) <- [(Maybe (Symbol, Expr), Expr)]
esv ]
          esvKeep :: [Expr]
esvKeep =
            let ([(Maybe (Symbol, Expr), Expr)]
xs, [(Maybe (Symbol, Expr), Expr)]
ys) = ((Maybe (Symbol, Expr), Expr) -> Bool)
-> [(Maybe (Symbol, Expr), Expr)]
-> ([(Maybe (Symbol, Expr), Expr)], [(Maybe (Symbol, Expr), Expr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Maybe (Symbol, Expr) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Symbol, Expr) -> Bool)
-> ((Maybe (Symbol, Expr), Expr) -> Maybe (Symbol, Expr))
-> (Maybe (Symbol, Expr), Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (Symbol, Expr), Expr) -> Maybe (Symbol, Expr)
forall a b. (a, b) -> a
fst) [(Maybe (Symbol, Expr), Expr)]
esv
             in ((Maybe (Symbol, Expr), Expr) -> Expr)
-> [(Maybe (Symbol, Expr), Expr)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Symbol, Expr), Expr) -> Expr
forall a b. (a, b) -> b
snd ([(Maybe (Symbol, Expr), Expr)]
xs [(Maybe (Symbol, Expr), Expr)]
-> [(Maybe (Symbol, Expr), Expr)] -> [(Maybe (Symbol, Expr), Expr)]
forall a. [a] -> [a] -> [a]
++ Int
-> [(Maybe (Symbol, Expr), Expr)] -> [(Maybe (Symbol, Expr), Expr)]
forall a. Int -> [a] -> [a]
drop Int
1 [(Maybe (Symbol, Expr), Expr)]
ys)
          su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
esvElim
          e' :: Expr
e' = HashSet Symbol -> Subst -> Expr -> Expr
F.rapierSubstExpr (Subst -> HashSet Symbol
F.substSymbolsSet Subst
su) Subst
su (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
F.conj [Expr]
esvKeep
          bs' :: [(Symbol, Sort)]
bs' = ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` Expr -> HashSet Symbol
F.exprSymbolsSet Expr
e') (Symbol -> Bool)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst) [(Symbol, Sort)]
bs
          e'' :: Expr
e'' = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.pExist [(Symbol, Sort)]
bs' Expr
e'
       in
          if [(Symbol, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, Expr)]
esvElim then Expr
e'' else Expr -> Expr
elimExistentialBinds Expr
e''
    elimExistentialBinds Expr
e = Expr
e

    -- | Float out conjuncts from an existential expression that does not
    -- depend on the existentially bound variables.
    floatPExistConjuncts :: F.Expr -> [F.Expr]
    floatPExistConjuncts :: Expr -> [Expr]
floatPExistConjuncts e0 :: Expr
e0@(F.PExist [(Symbol, Sort)]
bs Expr
es0) =
      let es :: [Expr]
es = Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
F.conjuncts Expr
es0
          ([Expr]
floatable, [Expr]
nonFloatable) =
           (Expr -> Bool) -> [Expr] -> ([Expr], [Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (HashSet Symbol -> Expr -> Bool
isFloatableConjunct ([Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList (((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs))) [Expr]
es
       in
          if [Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
floatable then
            [Expr
e0]
          else
            Expr -> Expr
elimExistentialBinds ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.pExist [(Symbol, Sort)]
bs ([Expr] -> Expr
F.conj [Expr]
nonFloatable)) Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
floatable
      where
        isFloatableConjunct :: S.HashSet F.Symbol -> F.Expr -> Bool
        isFloatableConjunct :: HashSet Symbol -> Expr -> Bool
isFloatableConjunct HashSet Symbol
s Expr
e = HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> Bool) -> HashSet Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.intersection (Expr -> HashSet Symbol
F.exprSymbolsSet Expr
e) HashSet Symbol
s
    floatPExistConjuncts Expr
e = [Expr
e]

-- | Determine if two expressions are alpha-equivalent.
--
-- Takes as first parameter the set of variables that might appear free
-- in the expressions to compare.
--
-- Doesn't handle all cases, just enough for simplifying KVars which requires
-- alpha-equivalence checking of existentially quantified expressions.
alphaEq :: S.HashSet F.Symbol -> F.Expr -> F.Expr -> Bool
alphaEq :: HashSet Symbol -> Expr -> Expr -> Bool
alphaEq HashSet Symbol
s0 = HashSet Symbol -> Subst -> Expr -> Expr -> Bool
go HashSet Symbol
s0 ([(Symbol, Expr)] -> Subst
F.mkSubst [])
  where
    go :: S.HashSet F.Symbol -> F.Subst -> F.Expr -> F.Expr -> Bool
    go :: HashSet Symbol -> Subst -> Expr -> Expr -> Bool
go HashSet Symbol
s Subst
su (F.PExist [(Symbol, Sort)]
bs1 Expr
x1) (F.PExist [(Symbol, Sort)]
bs2 Expr
x2) =
      let su' :: Subst
su' =
            (Subst -> (Symbol, Symbol) -> Subst)
-> Subst -> [(Symbol, Symbol)] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl'
              (\Subst
su1 (Symbol
v1, Symbol
v2) -> Subst -> Symbol -> Expr -> Subst
F.extendSubst Subst
su1 Symbol
v1 (Symbol -> Expr
forall v. v -> ExprV v
F.EVar Symbol
v2))
              Subst
su
              ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs1) (((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs2))
       in HashSet Symbol -> Subst -> Expr -> Expr -> Bool
go (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashSet Symbol
s ([Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, Sort)]
bs2)) Subst
su' Expr
x1 Expr
x2
    go HashSet Symbol
s Subst
su (F.PAnd [Expr]
es1) (F.PAnd [Expr]
es2) =
      [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Expr -> Expr -> Bool) -> [Expr] -> [Expr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (HashSet Symbol -> Subst -> Expr -> Expr -> Bool
go HashSet Symbol
s Subst
su) [Expr]
es1 [Expr]
es2)
    go HashSet Symbol
s Subst
su (F.POr [Expr]
es1) (F.POr [Expr]
es2) =
      [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Expr -> Expr -> Bool) -> [Expr] -> [Expr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (HashSet Symbol -> Subst -> Expr -> Expr -> Bool
go HashSet Symbol
s Subst
su) [Expr]
es1 [Expr]
es2)
    go HashSet Symbol
s Subst
su Expr
e1 Expr
e2 =
      HashSet Symbol -> Subst -> Expr -> Expr
F.rapierSubstExpr HashSet Symbol
s Subst
su Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2

-- | Determine if the expression is an equality that sets the value of
-- a variable in the given set.
--
-- @isVarEq fvs e@ yields @(Just (v, e'), e)@ if @v@ is in @fvs@, and @e@ has
-- the form @v == e'@.
isVarEq :: [F.Symbol] -> F.Expr -> (Maybe (F.Symbol, F.Expr), F.Expr)
isVarEq :: [Symbol] -> Expr -> (Maybe (Symbol, Expr), Expr)
isVarEq [Symbol]
fvs Expr
ei0 = case Expr
ei0 of
  F.PAtom Brel
brel Expr
e0 Expr
e1
    | Brel -> Bool
isEqRel Brel
brel ->
      let m :: Maybe (F.Symbol, F.Expr)
          m :: Maybe (Symbol, Expr)
m = do
            (Symbol
v, Expr
ei) <- ((,Expr
e1) (Symbol -> (Symbol, Expr)) -> Maybe Symbol -> Maybe (Symbol, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> [Symbol] -> Maybe Symbol
isVarIn Expr
e0 [Symbol]
fvs) Maybe (Symbol, Expr)
-> Maybe (Symbol, Expr) -> Maybe (Symbol, Expr)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
                       ((,Expr
e0) (Symbol -> (Symbol, Expr)) -> Maybe Symbol -> Maybe (Symbol, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> [Symbol] -> Maybe Symbol
isVarIn Expr
e1 [Symbol]
fvs)
            () <- Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member Symbol
v (Expr -> HashSet Symbol
F.exprSymbolsSet Expr
ei)))
            (Symbol, Expr) -> Maybe (Symbol, Expr)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
v, Expr
ei)
       in (Maybe (Symbol, Expr)
m, Expr
ei0)
  Expr
_ ->
    (Maybe (Symbol, Expr)
forall a. Maybe a
Nothing, Expr
ei0)
  where
    -- | Tells if the binary relation is an equality.
    isEqRel :: F.Brel -> Bool
    isEqRel :: Brel -> Bool
isEqRel Brel
F.Eq = Bool
True
    isEqRel Brel
F.Ueq = Bool
True
    isEqRel Brel
_ = Bool
False

    -- | @isVarIn s fvs@ yields @Just s@ if @s@ is a variable and it is in
    -- @fvs@.
    isVarIn :: F.Expr -> [F.Symbol] -> Maybe F.Symbol
    isVarIn :: Expr -> [Symbol] -> Maybe Symbol
isVarIn (F.EVar Symbol
s) [Symbol]
vs
      | Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
s [Symbol]
vs = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
s
    isVarIn Expr
_ [Symbol]
_vs = Maybe Symbol
forall a. Maybe a
Nothing