-- | Validate and Transform Constraints to Ensure various Invariants -------------------------
--   1. Each binder must be associated with a UNIQUE sort
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards     #-}

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

module Language.Fixpoint.Solver.Sanitize
  ( -- * Transform FInfo to enforce invariants
    sanitize

    -- * Sorts for each Symbol (move elsewhere)
  , symbolEnv

    -- * Remove substitutions K[x := e] where `x` is not in dom(K)
  , dropDeadSubsts
  ) where

import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Visitor
import           Language.Fixpoint.SortCheck     (elaborate, applySorts, isFirstOrder)
-- import           Language.Fixpoint.Defunctionalize
import qualified Language.Fixpoint.Misc                            as Misc
import qualified Language.Fixpoint.Types                           as F
import           Language.Fixpoint.Types.Config (Config)
import qualified Language.Fixpoint.Types.Config as Cfg
import qualified Language.Fixpoint.Types.Errors                    as E
import qualified Language.Fixpoint.Smt.Theories                    as Thy
import           Language.Fixpoint.Graph (kvEdges, CVertex (..))
import qualified Data.HashMap.Strict                               as M
import qualified Data.HashSet                                      as S
import qualified Data.List                                         as L
import qualified Data.Text                                         as T
import           Data.Maybe          (isNothing, mapMaybe, fromMaybe)
import           Control.Monad       ((>=>))
import           Text.PrettyPrint.HughesPJ

type SanitizeM a = Either E.Error a

--------------------------------------------------------------------------------
sanitize :: Config -> F.SInfo a -> SanitizeM (F.SInfo a)
--------------------------------------------------------------------------------
sanitize :: forall a. Config -> SInfo a -> SanitizeM (SInfo a)
sanitize Config
cfg =    -- banIllScopedKvars
        --      Misc.fM dropAdtMeasures
        --      >=>
                     forall a. SInfo a -> SanitizeM (SInfo a)
banIrregularData
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM forall a. SInfo a -> SInfo a
dropFuncSortedShadowedBinders
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM forall a. SInfo a -> SInfo a
sanitizeWfC
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM forall a. SInfo a -> SInfo a
replaceDeadKvars
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM (forall a. SInfo a -> SInfo a
dropDeadSubsts forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SInfo a -> SInfo a
restrictKVarDomain)
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=>         forall a. SInfo a -> SanitizeM (SInfo a)
banMixedRhs
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=>         forall a. SInfo a -> SanitizeM (SInfo a)
banQualifFreeVars
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=>         forall a. SInfo a -> SanitizeM (SInfo a)
banConstraintFreeVars
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM forall a. SInfo a -> SInfo a
addLiterals
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM (forall a. Config -> SInfo a -> SInfo a
eliminateEta Config
cfg)
         forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
Misc.fM forall a. SInfo a -> SInfo a
cancelCoercion


--------------------------------------------------------------------------------
-- | 'dropAdtMeasures' removes all the measure definitions that correspond to
--   constructor, selector or test names for declared datatypes, as these are
--   now "natively" handled by the SMT solver.
--------------------------------------------------------------------------------
_dropAdtMeasures :: F.SInfo a -> F.SInfo a
_dropAdtMeasures :: forall a. SInfo a -> SInfo a
_dropAdtMeasures SInfo a
si = SInfo a
si { ae :: AxiomEnv
F.ae = [DataDecl] -> AxiomEnv -> AxiomEnv
dropAdtAenv (forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls SInfo a
si) (forall (c :: * -> *) a. GInfo c a -> AxiomEnv
F.ae SInfo a
si) }

dropAdtAenv :: [F.DataDecl] -> F.AxiomEnv -> F.AxiomEnv
dropAdtAenv :: [DataDecl] -> AxiomEnv -> AxiomEnv
dropAdtAenv [DataDecl]
ds AxiomEnv
ae = AxiomEnv
ae { aenvSimpl :: [Rewrite]
F.aenvSimpl = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> Bool
isAdt) (AxiomEnv -> [Rewrite]
F.aenvSimpl AxiomEnv
ae) }
  where
    isAdt :: Rewrite -> Bool
isAdt         = (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
adtSyms) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> Symbol
F.smName
    adtSyms :: HashSet Symbol
adtSyms       = [DataDecl] -> HashSet Symbol
adtSymbols [DataDecl]
ds

adtSymbols :: [F.DataDecl] -> S.HashSet F.Symbol
adtSymbols :: [DataDecl] -> HashSet Symbol
adtSymbols = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [(Symbol, TheorySymbol)]
Thy.dataDeclSymbols

--------------------------------------------------------------------------------
-- | `addLiterals` traverses the constraints to find (string) literals that
--   are then added to the `dLits` field.
--------------------------------------------------------------------------------
addLiterals :: F.SInfo a -> F.SInfo a
--------------------------------------------------------------------------------
addLiterals :: forall a. SInfo a -> SInfo a
addLiterals SInfo a
si = SInfo a
si { dLits :: SEnv Sort
F.dLits = forall a. SEnv a -> HashMap Symbol a -> SEnv a
F.unionSEnv (forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.dLits SInfo a
si) HashMap Symbol Sort
lits'
                    , gLits :: SEnv Sort
F.gLits = forall a. SEnv a -> HashMap Symbol a -> SEnv a
F.unionSEnv (forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
si) HashMap Symbol Sort
lits'
                    }
  where
    lits' :: HashMap Symbol Sort
lits'      = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall a. Symbolic a => a -> Symbol
F.symbol SymConst
x, Sort
F.strSort) | SymConst
x <- forall a. SymConsts a => a -> [SymConst]
symConsts SInfo a
si ]



cancelCoercion :: F.SInfo a -> F.SInfo a
cancelCoercion :: forall a. SInfo a -> SInfo a
cancelCoercion = forall t. Visitable t => (Expr -> Expr) -> t -> t
mapExpr (forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans (forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr :: () -> Expr -> Expr
txExpr = forall {p}. p -> Expr -> Expr
go }) () ())
  where
    go :: p -> Expr -> Expr
go p
_ (F.ECoerc Sort
t1 Sort
t2 (F.ECoerc Sort
t2' Sort
t1' Expr
e))
      | Sort
t1 forall a. Eq a => a -> a -> Bool
== Sort
t1' Bool -> Bool -> Bool
&& Sort
t2 forall a. Eq a => a -> a -> Bool
== Sort
t2'
      = Expr
e
    go p
_ Expr
e = Expr
e

--------------------------------------------------------------------------------
-- | `eliminateEta` converts equations of the form f x = g x into f = g
--------------------------------------------------------------------------------
eliminateEta :: Config -> F.SInfo a -> F.SInfo a
--------------------------------------------------------------------------------
eliminateEta :: forall a. Config -> SInfo a -> SInfo a
eliminateEta Config
cfg SInfo a
si
  | Config -> Bool
Cfg.etaElim Config
cfg
  , Config -> Bool
Cfg.oldPLE  Config
cfg
  = SInfo a
si { ae :: AxiomEnv
F.ae = AxiomEnv
ae' }
  | Config -> Bool
Cfg.etaElim Config
cfg
  = SInfo a
si { ae :: AxiomEnv
F.ae = (AxiomEnv
ae {aenvEqs :: [Equation]
F.aenvEqs = Equation -> Equation
etaElimNEW forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` AxiomEnv -> [Equation]
F.aenvEqs AxiomEnv
ae }) }
  | Bool
otherwise
  = SInfo a
si
  where
    ae' :: AxiomEnv
ae' = AxiomEnv
ae {aenvEqs :: [Equation]
F.aenvEqs = [Equation]
eqs}
    ae :: AxiomEnv
ae = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
F.ae SInfo a
si
    eqs :: [Equation]
eqs = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Equation -> Equation
etaElim (AxiomEnv -> [Equation]
F.aenvEqs AxiomEnv
ae)

    etaElim :: Equation -> Equation
etaElim Equation
eq = forall a. PPrint a => String -> a -> a
F.notracepp String
"Eliminating" forall a b. (a -> b) -> a -> b
$
                 case Expr
body of
                   F.PAtom Brel
F.Eq Expr
e0 Expr
e1 ->
                     let (Expr
f0, ListNE Symbol
args0) = Expr -> (Expr, ListNE Symbol)
fapp Expr
e0
                         (Expr
f1, ListNE Symbol
args1) = forall a. PPrint a => String -> a -> a
F.notracepp String
"f1" forall a b. (a -> b) -> a -> b
$ Expr -> (Expr, ListNE Symbol)
fapp Expr
e1 in
                     if forall a. [a] -> [a]
reverse ListNE Symbol
args0 forall a. Eq a => a -> a -> Bool
== ListNE Symbol
args
                     then let commonArgs :: ListNE Symbol
commonArgs = forall a. PPrint a => String -> a -> a
F.notracepp String
"commonArgs" forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                           forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(==)) forall a b. (a -> b) -> a -> b
$
                                           forall a b. [a] -> [b] -> [(a, b)]
zip ListNE Symbol
args0 ListNE Symbol
args1
                              commonLength :: BindId
commonLength = forall (t :: * -> *) a. Foldable t => t a -> BindId
length ListNE Symbol
commonArgs
                              ([(Symbol, Sort)]
newArgsAndSorts, [(Symbol, Sort)]
elimedArgsAndSorts) =
                                forall a. BindId -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> BindId
length ListNE Symbol
args forall a. Num a => a -> a -> a
- BindId
commonLength) [(Symbol, Sort)]
argsAndSorts
                              args0' :: [Expr]
args0' = forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> [a]
reverse (forall a. BindId -> [a] -> [a]
drop BindId
commonLength ListNE Symbol
args0)
                              args1' :: [Expr]
args1' = forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> [a]
reverse (forall a. BindId -> [a] -> [a]
drop BindId
commonLength ListNE Symbol
args1) in
                       Equation
eq { eqArgs :: [(Symbol, Sort)]
F.eqArgs = [(Symbol, Sort)]
newArgsAndSorts
                          , eqSort :: Sort
F.eqSort = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sort -> Sort -> Sort
F.FFunc Sort
sort
                                       (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
elimedArgsAndSorts)
                          , eqBody :: Expr
F.eqBody = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Expr -> [Expr] -> Expr
F.eApps Expr
f0 [Expr]
args0') (Expr -> [Expr] -> Expr
F.eApps Expr
f1 [Expr]
args1')}
                     else Equation
eq
                   Expr
_ -> Equation
eq
      where argsAndSorts :: [(Symbol, Sort)]
argsAndSorts = Equation -> [(Symbol, Sort)]
F.eqArgs Equation
eq
            args :: ListNE Symbol
args = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
argsAndSorts
            body :: Expr
body = Equation -> Expr
F.eqBody Equation
eq
            sort :: Sort
sort = Equation -> Sort
F.eqSort Equation
eq
    etaElimNEW :: Equation -> Equation
etaElimNEW Equation
eq = forall a. PPrint a => String -> a -> a
F.notracepp String
"Eliminating" forall a b. (a -> b) -> a -> b
$
                  let (Expr
f1, ListNE Symbol
args1) = Expr -> (Expr, ListNE Symbol)
fapp (Equation -> Expr
F.eqBody Equation
eq) in
                  let commonArgs :: ListNE Symbol
commonArgs = forall a. PPrint a => String -> a -> a
F.notracepp String
"commonArgs" forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                           forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                           forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(==)) forall a b. (a -> b) -> a -> b
$
                                           forall a b. [a] -> [b] -> [(a, b)]
zip ListNE Symbol
args0 ListNE Symbol
args1
                      commonLength :: BindId
commonLength = forall (t :: * -> *) a. Foldable t => t a -> BindId
length ListNE Symbol
commonArgs
                      ([(Symbol, Sort)]
newArgsAndSorts, [(Symbol, Sort)]
elimedArgsAndSorts) =
                                forall a. BindId -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> BindId
length ListNE Symbol
args forall a. Num a => a -> a -> a
- BindId
commonLength) [(Symbol, Sort)]
argsAndSorts
                      args1' :: [Expr]
args1' = forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> [a]
reverse (forall a. BindId -> [a] -> [a]
drop BindId
commonLength ListNE Symbol
args1) in
                  Equation
eq { eqArgs :: [(Symbol, Sort)]
F.eqArgs = [(Symbol, Sort)]
newArgsAndSorts
                     , eqSort :: Sort
F.eqSort = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sort -> Sort -> Sort
F.FFunc Sort
sort
                                       (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
elimedArgsAndSorts)
                     , eqBody :: Expr
F.eqBody = Expr -> [Expr] -> Expr
F.eApps Expr
f1 [Expr]
args1'}
      where argsAndSorts :: [(Symbol, Sort)]
argsAndSorts = Equation -> [(Symbol, Sort)]
F.eqArgs Equation
eq
            args :: ListNE Symbol
args  = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
argsAndSorts
            args0 :: ListNE Symbol
args0 = forall a. [a] -> [a]
reverse ListNE Symbol
args
            sort :: Sort
sort  = Equation -> Sort
F.eqSort Equation
eq

    fapp :: F.Expr -> (F.Expr, [F.Symbol])
    fapp :: Expr -> (Expr, ListNE Symbol)
fapp Expr
ee = forall a. a -> Maybe a -> a
fromMaybe (Expr
ee, []) (Expr -> Maybe (Expr, ListNE Symbol)
fapp' Expr
ee)

    fapp' :: F.Expr -> Maybe (F.Expr, [F.Symbol])
    fapp' :: Expr -> Maybe (Expr, ListNE Symbol)
fapp' (F.EApp Expr
e0 (F.EVar Symbol
arg)) = do
      (Expr
fvar, ListNE Symbol
args) <- Expr -> Maybe (Expr, ListNE Symbol)
fapp' Expr
e0
      forall {b}. (Expr, b) -> Maybe (Expr, b)
splitApp (Expr
fvar, Symbol
argforall a. a -> [a] -> [a]
:ListNE Symbol
args)
    fapp' Expr
e = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
e, [])

    theorySymbols :: SEnv TheorySymbol
theorySymbols = forall a. PPrint a => String -> a -> a
F.notracepp String
"theorySymbols" forall a b. (a -> b) -> a -> b
$ [DataDecl] -> SEnv TheorySymbol
Thy.theorySymbols forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls SInfo a
si

    splitApp :: (Expr, b) -> Maybe (Expr, b)
splitApp (Expr
e, b
es)
      | forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => String -> a -> a
F.notracepp (String
"isSmt2App? " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e) forall a b. (a -> b) -> a -> b
$ SEnv TheorySymbol -> Expr -> Maybe BindId
Thy.isSmt2App SEnv TheorySymbol
theorySymbols forall a b. (a -> b) -> a -> b
$ Expr -> Expr
stripCasts Expr
e
      = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
e,b
es)
      | Bool
otherwise
      = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- | See issue liquid-fixpoint issue #230. This checks that whenever we have,
--      G1        |- K.su1
--      G2, K.su2 |- rhs
--   then
--      G1 \cap G2 \subseteq wenv(k)
--------------------------------------------------------------------------------
_banIllScopedKvars :: F.SInfo a ->  SanitizeM (F.SInfo a)
--------------------------------------------------------------------------------
_banIllScopedKvars :: forall a. SInfo a -> SanitizeM (SInfo a)
_banIllScopedKvars SInfo a
si = forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (forall a b. b -> Either a b
Right SInfo a
si) (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(KVar, SubcId, SubcId, IBindEnv)] -> Error
badKs) [(KVar, SubcId, SubcId, IBindEnv)]
errs
  where
    errs :: [(KVar, SubcId, SubcId, IBindEnv)]
errs              = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a.
SInfo a -> KvDefs -> KVar -> [(KVar, SubcId, SubcId, IBindEnv)]
checkIllScope SInfo a
si KvDefs
kDs) [KVar]
ks
    kDs :: KvDefs
kDs               = forall a. SInfo a -> KvDefs
kvarDefUses SInfo a
si
    ks :: [KVar]
ks                = forall a. (a -> Bool) -> [a] -> [a]
filter KVar -> Bool
notKut forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [k]
M.keys (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si)
    notKut :: KVar -> Bool
notKut            = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar -> Kuts -> Bool
`F.ksMember` forall (c :: * -> *) a. GInfo c a -> Kuts
F.kuts SInfo a
si)

badKs :: [(F.KVar, F.SubcId, F.SubcId, F.IBindEnv)] -> F.Error
badKs :: [(KVar, SubcId, SubcId, IBindEnv)] -> Error
badKs = ListNE Error -> Error
E.catErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall k bs.
(PPrint k, PPrint bs) =>
(k, SubcId, SubcId, bs) -> Error
E.errIllScopedKVar

type KvConstrM = M.HashMap F.KVar [Integer]
type KvDefs    = (KvConstrM, KvConstrM)

checkIllScope :: F.SInfo a -> KvDefs -> F.KVar -> [(F.KVar, F.SubcId, F.SubcId, F.IBindEnv)]
checkIllScope :: forall a.
SInfo a -> KvDefs -> KVar -> [(KVar, SubcId, SubcId, IBindEnv)]
checkIllScope SInfo a
si (KvConstrM
inM, KvConstrM
outM) KVar
k = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a.
SInfo a
-> KVar
-> SubcId
-> SubcId
-> Maybe (KVar, SubcId, SubcId, IBindEnv)
isIllScope SInfo a
si KVar
k)) [(SubcId, SubcId)]
ios
  where
    ios :: [(SubcId, SubcId)]
ios                        = [(SubcId
i, SubcId
o) | SubcId
i <- [SubcId]
ins, SubcId
o <- [SubcId]
outs, SubcId
i forall a. Eq a => a -> a -> Bool
/= SubcId
o ]
    ins :: [SubcId]
ins                        = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KvConstrM
inM
    outs :: [SubcId]
outs                       = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KvConstrM
outM

isIllScope :: F.SInfo a -> F.KVar -> F.SubcId -> F.SubcId -> Maybe (F.KVar, F.SubcId, F.SubcId, F.IBindEnv)
isIllScope :: forall a.
SInfo a
-> KVar
-> SubcId
-> SubcId
-> Maybe (KVar, SubcId, SubcId, IBindEnv)
isIllScope SInfo a
si KVar
k SubcId
inI SubcId
outI
  | IBindEnv -> Bool
F.nullIBindEnv IBindEnv
badXs = forall a. Maybe a
Nothing
  | Bool
otherwise            = forall a. a -> Maybe a
Just (KVar
k, SubcId
inI, SubcId
outI, IBindEnv
badXs)
  where
    badXs :: IBindEnv
badXs                = IBindEnv -> IBindEnv -> IBindEnv
F.diffIBindEnv IBindEnv
commonXs IBindEnv
kXs
    kXs :: IBindEnv
kXs                  = {- F.tracepp ("kvarBinds " ++ show k) $ -} forall a. SInfo a -> KVar -> IBindEnv
kvarBinds SInfo a
si KVar
k
    commonXs :: IBindEnv
commonXs             = IBindEnv -> IBindEnv -> IBindEnv
F.intersectionIBindEnv IBindEnv
inXs IBindEnv
outXs
    inXs :: IBindEnv
inXs                 = forall a. SInfo a -> SubcId -> IBindEnv
subcBinds SInfo a
si SubcId
inI
    outXs :: IBindEnv
outXs                = forall a. SInfo a -> SubcId -> IBindEnv
subcBinds SInfo a
si SubcId
outI

subcBinds :: F.SInfo a -> F.SubcId -> F.IBindEnv
subcBinds :: forall a. SInfo a -> SubcId -> IBindEnv
subcBinds SInfo a
si SubcId
i = forall a. SimpC a -> IBindEnv
F._cenv forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
si forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! SubcId
i

kvarBinds :: F.SInfo a -> F.KVar -> F.IBindEnv
kvarBinds :: forall a. SInfo a -> KVar -> IBindEnv
kvarBinds SInfo a
si = forall a. WfC a -> IBindEnv
F.wenv forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.!)

kvarDefUses :: F.SInfo a -> KvDefs
kvarDefUses :: forall a. SInfo a -> KvDefs
kvarDefUses SInfo a
si = (forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(KVar, SubcId)]
ins, forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(KVar, SubcId)]
outs)
  where
    es :: [CEdge]
es         = forall (c :: * -> *) a. TaggedC c a => GInfo c a -> [CEdge]
kvEdges SInfo a
si
    outs :: [(KVar, SubcId)]
outs       = [(KVar
k, SubcId
o) | (KVar KVar
k, Cstr SubcId
o) <- [CEdge]
es ]
    ins :: [(KVar, SubcId)]
ins        = [(KVar
k, SubcId
i) | (Cstr SubcId
i, KVar KVar
k) <- [CEdge]
es ]

--------------------------------------------------------------------------------
-- | `dropDeadSubsts` removes dead `K[x := e]` where `x` NOT in the domain of K.
--------------------------------------------------------------------------------
dropDeadSubsts :: F.SInfo a -> F.SInfo a
dropDeadSubsts :: forall a. SInfo a -> SInfo a
dropDeadSubsts SInfo a
si = forall t. Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts ((Symbol -> Expr -> Bool) -> Subst -> Subst
F.filterSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {p}. KVar -> Symbol -> p -> Bool
f) SInfo a
si
  where
    kvsM :: HashMap KVar (HashSet Symbol)
kvsM          = forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (\KVar
k WfC a
_ -> KVar -> HashSet Symbol
kvDom KVar
k) (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si)
    kvDom :: KVar -> HashSet Symbol
kvDom         = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SInfo a -> KVar -> ListNE Symbol
F.kvarDomain SInfo a
si
    f :: KVar -> Symbol -> p -> Bool
f KVar
k Symbol
x p
_       = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x (forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty KVar
k HashMap KVar (HashSet Symbol)
kvsM)

--------------------------------------------------------------------------------
-- | `restrictKVarDomain` updates the kvar-domains in the wf constraints
--   to a subset of the original binders, where we DELETE the parameters
--   `x` which appear in substitutions of the form `K[x := y]` where `y`
--   is not in the env.
--------------------------------------------------------------------------------
restrictKVarDomain :: F.SInfo a -> F.SInfo a
restrictKVarDomain :: forall a. SInfo a -> SInfo a
restrictKVarDomain SInfo a
si = SInfo a
si { ws :: HashMap KVar (WfC a)
F.ws = forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (forall a. KvDom -> KVar -> WfC a -> WfC a
restrictWf KvDom
kvm) (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si) }
  where
    kvm :: KvDom
kvm               = forall a. SInfo a -> KvDom
safeKvarEnv SInfo a
si

-- | `restrictWf kve k w` restricts the env of `w` to the parameters in `kve k`.
restrictWf :: KvDom -> F.KVar -> F.WfC a -> F.WfC a
restrictWf :: forall a. KvDom -> KVar -> WfC a -> WfC a
restrictWf KvDom
kve KVar
k WfC a
w = WfC a
w { wenv :: IBindEnv
F.wenv = (BindId -> Bool) -> IBindEnv -> IBindEnv
F.filterIBindEnv BindId -> Bool
f (forall a. WfC a -> IBindEnv
F.wenv WfC a
w) }
  where
    f :: BindId -> Bool
f BindId
i            = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member BindId
i HashSet BindId
kis
    kis :: HashSet BindId
kis            = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ BindId
i | (Symbol
_, BindId
i) <- forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv BindId
kEnv ]
    kEnv :: SEnv BindId
kEnv           = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty KVar
k KvDom
kve

-- | `safeKvarEnv` computes the "real" domain of each kvar, which is
--   a SUBSET of the input domain, in which we KILL the parameters
--   `x` which appear in substitutions of the form `K[x := y]`
--   where `y` is not in the env.

type KvDom     = M.HashMap F.KVar (F.SEnv F.BindId)
type KvBads    = M.HashMap F.KVar [F.Symbol]

safeKvarEnv :: F.SInfo a -> KvDom
safeKvarEnv :: forall a. SInfo a -> KvDom
safeKvarEnv SInfo a
si = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (forall a. SInfo a -> KvDom -> SimpC a -> KvDom
dropKvarEnv SInfo a
si) KvDom
env0 [SimpC a]
cs
  where
    cs :: [SimpC a]
cs         = forall k v. HashMap k v -> [v]
M.elems  (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
si)
    env0 :: KvDom
env0       = forall a. SInfo a -> KvDom
initKvarEnv SInfo a
si

dropKvarEnv :: F.SInfo a -> KvDom -> F.SimpC a -> KvDom
dropKvarEnv :: forall a. SInfo a -> KvDom -> SimpC a -> KvDom
dropKvarEnv SInfo a
si KvDom
kve SimpC a
c = forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (KvBads -> KVar -> SEnv BindId -> SEnv BindId
dropBadParams KvBads
kBads) KvDom
kve
  where
    kBads :: KvBads
kBads            = forall a. SInfo a -> SimpC a -> KvBads
badParams SInfo a
si SimpC a
c

dropBadParams :: KvBads -> F.KVar -> F.SEnv F.BindId -> F.SEnv F.BindId
dropBadParams :: KvBads -> KVar -> SEnv BindId -> SEnv BindId
dropBadParams KvBads
kBads KVar
k SEnv BindId
kEnv = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Symbol -> SEnv a -> SEnv a
F.deleteSEnv) SEnv BindId
kEnv ListNE Symbol
xs
  where
    xs :: ListNE Symbol
xs                     = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty KVar
k KvBads
kBads

badParams :: F.SInfo a -> F.SimpC a -> M.HashMap F.KVar [F.Symbol]
badParams :: forall a. SInfo a -> SimpC a -> KvBads
badParams SInfo a
si SimpC a
c = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(KVar, Symbol)]
bads
  where
    bads :: [(KVar, Symbol)]
bads       = [ (KVar
k, Symbol
x) | (Maybe Symbol
v, KVar
k, F.Su HashMap Symbol Expr
su) <- forall a.
[(Symbol, SortedReft)] -> SimpC a -> [(Maybe Symbol, KVar, Subst)]
subcKSubs [(Symbol, SortedReft)]
xsrs SimpC a
c
                          , let vEnv :: HashSet Symbol
vEnv = forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashSet Symbol
sEnv (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
`S.insert` HashSet Symbol
sEnv) Maybe Symbol
v
                          , (Symbol
x, Expr
e)          <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol Expr
su
                          , HashSet Symbol -> Expr -> Bool
badArg HashSet Symbol
vEnv Expr
e
                 ]
    sEnv :: HashSet Symbol
sEnv       = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
xsrs)
    xsrs :: [(Symbol, SortedReft)]
xsrs       = forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si) (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
c)

badArg :: S.HashSet F.Symbol -> F.Expr -> Bool
badArg :: HashSet Symbol -> Expr -> Bool
badArg HashSet Symbol
sEnv (F.EVar Symbol
y) = Bool -> Bool
not (Symbol
y forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
sEnv)
badArg HashSet Symbol
_    Expr
_          = Bool
True

type KSub = (Maybe F.Symbol, F.KVar, F.Subst)

subcKSubs :: [(F.Symbol, F.SortedReft)] -> F.SimpC a -> [KSub]
subcKSubs :: forall a.
[(Symbol, SortedReft)] -> SimpC a -> [(Maybe Symbol, KVar, Subst)]
subcKSubs [(Symbol, SortedReft)]
xsrs SimpC a
c = forall {a}. [(Maybe a, KVar, Subst)]
rhs forall a. [a] -> [a] -> [a]
++ [(Maybe Symbol, KVar, Subst)]
lhs
  where
    lhs :: [(Maybe Symbol, KVar, Subst)]
lhs          = [ (forall a. a -> Maybe a
Just Symbol
v, KVar
k, Subst
su) | (Symbol
_, SortedReft
sr) <- [(Symbol, SortedReft)]
xsrs
                                     , let rs :: [Reft]
rs   = Reft -> [Reft]
F.reftConjuncts (SortedReft -> Reft
F.sr_reft SortedReft
sr)
                                     , F.Reft (Symbol
v, F.PKVar KVar
k Subst
su) <- [Reft]
rs
                   ]
    rhs :: [(Maybe a, KVar, Subst)]
rhs          = [(forall a. Maybe a
Nothing, KVar
k, Subst
su) | F.PKVar KVar
k Subst
su <- [forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC a
c]]


initKvarEnv :: F.SInfo a -> KvDom
initKvarEnv :: forall a. SInfo a -> KvDom
initKvarEnv SInfo a
si = forall a. SInfo a -> WfC a -> SEnv BindId
initEnv SInfo a
si forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si

initEnv :: F.SInfo a -> F.WfC a -> F.SEnv F.BindId
initEnv :: forall a. SInfo a -> WfC a -> SEnv BindId
initEnv SInfo a
si WfC a
w = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [ (BindId -> Symbol
bind BindId
i, BindId
i) | BindId
i <- [BindId]
is ]
  where
    is :: [BindId]
is       = IBindEnv -> [BindId]
F.elemsIBindEnv forall a b. (a -> b) -> a -> b
$ forall a. WfC a -> IBindEnv
F.wenv WfC a
w
    bind :: BindId -> Symbol
bind BindId
i   = forall a b c. (a, b, c) -> a
Misc.fst3 (forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindId
i BindEnv a
be)
    be :: BindEnv a
be       = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si

--------------------------------------------------------------------------------
-- | check that no constraint has free variables (ignores kvars)
--------------------------------------------------------------------------------
banConstraintFreeVars :: F.SInfo a -> SanitizeM (F.SInfo a)
banConstraintFreeVars :: forall a. SInfo a -> SanitizeM (SInfo a)
banConstraintFreeVars SInfo a
fi0 = forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (forall a b. b -> Either a b
Right SInfo a
fi0) (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ListNE (SimpC a, ListNE Symbol) -> Error
badCs) [(SimpC a, ListNE Symbol)]
bads
  where
    fi :: SInfo a
fi      = forall t. Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Expr
F.PTrue) SInfo a
fi0
    bads :: [(SimpC a, ListNE Symbol)]
bads    = [(SimpC a
c, ListNE Symbol
fs) | SimpC a
c <- 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)
F.cm SInfo a
fi, Just ListNE Symbol
fs <- [forall a.
SInfo a -> (Symbol -> Bool) -> SimpC a -> Maybe (ListNE Symbol)
cNoFreeVars SInfo a
fi Symbol -> Bool
k SimpC a
c]]
    k :: Symbol -> Bool
k       = forall a. SInfo a -> Symbol -> Bool
known SInfo a
fi

known :: F.SInfo a -> F.Symbol -> Bool
known :: forall a. SInfo a -> Symbol -> Bool
known SInfo a
fi  = \Symbol
x -> forall a. Symbol -> SEnv a -> Bool
F.memberSEnv Symbol
x SEnv Sort
lits Bool -> Bool -> Bool
|| forall a. Symbol -> SEnv a -> Bool
F.memberSEnv Symbol
x SEnv TheorySymbol
prims
  where
    lits :: SEnv Sort
lits  = forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
fi
    prims :: SEnv TheorySymbol
prims = [DataDecl] -> SEnv TheorySymbol
Thy.theorySymbols forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls forall a b. (a -> b) -> a -> b
$ SInfo a
fi

cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol]
cNoFreeVars :: forall a.
SInfo a -> (Symbol -> Bool) -> SimpC a -> Maybe (ListNE Symbol)
cNoFreeVars SInfo a
fi Symbol -> Bool
known SimpC a
c = if forall a. HashSet a -> Bool
S.null HashSet Symbol
fv then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just (forall a. HashSet a -> [a]
S.toList HashSet Symbol
fv)
  where
    be :: BindEnv a
be   = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi
    ids :: [BindId]
ids  = IBindEnv -> [BindId]
F.elemsIBindEnv forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
c
    cDom :: ListNE Symbol
cDom = [forall a b c. (a, b, c) -> a
Misc.fst3 forall a b. (a -> b) -> a -> b
$ forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindId
i BindEnv a
be | BindId
i <- [BindId]
ids]
    cRng :: ListNE Symbol
cRng = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> HashSet Symbol
F.reftFreeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
F.sr_reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a, b, c) -> b
Misc.snd3 forall a b. (a -> b) -> a -> b
$ forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindId
i BindEnv a
be | BindId
i <- [BindId]
ids]
        forall a. [a] -> [a] -> [a]
++ forall a. Subable a => a -> ListNE Symbol
F.syms (forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC a
c)
    fv :: HashSet Symbol
fv   = (forall a. (Eq a, Hashable a) => [a] -> [a] -> HashSet a
`Misc.nubDiff` ListNE Symbol
cDom) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
known) forall a b. (a -> b) -> a -> b
$ ListNE Symbol
cRng

badCs :: Misc.ListNE (F.SimpC a, [F.Symbol]) -> E.Error
badCs :: forall a. ListNE (SimpC a, ListNE Symbol) -> Error
badCs = ListNE Error -> Error
E.catErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. PPrint a => (SubcId, a) -> Error
E.errFreeVarInConstraint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId)

--------------------------------------------------------------------------------
-- | check that every DataDecl is regular
--------------------------------------------------------------------------------
banIrregularData :: F.SInfo a -> SanitizeM (F.SInfo a)
banIrregularData :: forall a. SInfo a -> SanitizeM (SInfo a)
banIrregularData SInfo a
fi = forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (forall a b. b -> Either a b
Right SInfo a
fi) (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataDecl] -> Error
badDataDecl) [DataDecl]
bads
  where
    bads :: [DataDecl]
bads = [DataDecl] -> [DataDecl]
F.checkRegular (forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls SInfo a
fi )

badDataDecl :: Misc.ListNE F.DataDecl -> E.Error
badDataDecl :: [DataDecl] -> Error
badDataDecl [DataDecl]
ds = ListNE Error -> Error
E.catErrors [ forall x. (Loc x, PPrint x) => x -> Error
E.errBadDataDecl DataDecl
d | DataDecl
d <- [DataDecl]
ds ]

--------------------------------------------------------------------------------
-- | check that no qualifier has free variables
--------------------------------------------------------------------------------
banQualifFreeVars :: F.SInfo a -> SanitizeM (F.SInfo a)
--------------------------------------------------------------------------------
banQualifFreeVars :: forall a. SInfo a -> SanitizeM (SInfo a)
banQualifFreeVars SInfo a
fi = forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (forall a b. b -> Either a b
Right SInfo a
fi) (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Qualifier, ListNE Symbol)] -> Error
badQuals) [(Qualifier, ListNE Symbol)]
bads
  where
    bads :: [(Qualifier, ListNE Symbol)]
bads    = [ (Qualifier
q, ListNE Symbol
xs) | Qualifier
q <- forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
fi, let xs :: ListNE Symbol
xs = forall a. Subable a => a -> ListNE Symbol
free Qualifier
q, Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null ListNE Symbol
xs) ]
    free :: a -> ListNE Symbol
free a
q  = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
isLit) (forall a. Subable a => a -> ListNE Symbol
F.syms a
q)
    isLit :: Symbol -> Bool
isLit Symbol
x = forall a. Symbol -> SEnv a -> Bool
F.memberSEnv Symbol
x (forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
fi)
    -- lits    = fst <$> F.toListSEnv (F.gLits fi)
    -- free q  = S.toList $ F.syms (F.qBody q) `nubDiff` (lits ++ F.prims ++ F.syms (F.qpSym <$> F.qParams q))

badQuals     :: Misc.ListNE (F.Qualifier, Misc.ListNE F.Symbol) -> E.Error
badQuals :: [(Qualifier, ListNE Symbol)] -> Error
badQuals [(Qualifier, ListNE Symbol)]
bqs = ListNE Error -> Error
E.catErrors [ forall q x. (PPrint q, Loc q, PPrint x) => q -> x -> Error
E.errFreeVarInQual Qualifier
q ListNE Symbol
xs | (Qualifier
q, ListNE Symbol
xs) <- [(Qualifier, ListNE Symbol)]
bqs]


--------------------------------------------------------------------------------
-- | check that each constraint has RHS of form [k1,...,kn] or [p]
--------------------------------------------------------------------------------
banMixedRhs :: F.SInfo a -> SanitizeM (F.SInfo a)
--------------------------------------------------------------------------------
banMixedRhs :: forall a. SInfo a -> SanitizeM (SInfo a)
banMixedRhs SInfo a
fi = forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (forall a b. b -> Either a b
Right SInfo a
fi) (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ListNE (SubcId, SimpC a) -> Error
badRhs) [(SubcId, SimpC a)]
bads
  where
    ics :: [(SubcId, SimpC a)]
ics        = forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
fi
    bads :: [(SubcId, SimpC a)]
bads       = [(SubcId
i, SimpC a
c) | (SubcId
i, SimpC a
c) <- [(SubcId, SimpC a)]
ics, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall {c :: * -> *} {a}. TaggedC c a => c a -> Bool
isOk SimpC a
c]
    isOk :: c a -> Bool
isOk c a
c     = forall {c :: * -> *} {a}. TaggedC c a => c a -> Bool
isKvarC c a
c Bool -> Bool -> Bool
|| forall {c :: * -> *} {a}. TaggedC c a => c a -> Bool
isConcC c a
c

badRhs :: Misc.ListNE (Integer, F.SimpC a) -> E.Error
badRhs :: forall a. ListNE (SubcId, SimpC a) -> Error
badRhs = ListNE Error -> Error
E.catErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. (SubcId, SimpC a) -> Error
badRhs1

badRhs1 :: (Integer, F.SimpC a) -> E.Error
badRhs1 :: forall a. (SubcId, SimpC a) -> Error
badRhs1 (SubcId
i, SimpC a
c) = SrcSpan -> Doc -> Error
E.err SrcSpan
E.dummySpan forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ Doc
"Malformed RHS for constraint id" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SubcId
i
                                          , BindId -> Doc -> Doc
nest BindId
4 (forall a. PPrint a => a -> Doc
pprint (forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC a
c)) ]

--------------------------------------------------------------------------------
-- | symbol |-> sort for EVERY variable in the SInfo; 'symbolEnv' can ONLY be
--   called with **sanitized** environments (post the uniqification etc.) or
--   else you get duplicate sorts and other such errors.
--   We do this peculiar dance with `env0` to extract the apply-sorts from the
--   function definitions inside the `AxiomEnv` which cannot be elaborated as
--   it makes it hard to actually find the fundefs within (breaking PLE.)
--------------------------------------------------------------------------------
symbolEnv :: Config -> F.SInfo a -> F.SymEnv
symbolEnv :: forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si = SEnv Sort
-> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
F.symEnv SEnv Sort
sEnv SEnv TheorySymbol
tEnv [DataDecl]
ds SEnv Sort
lits ([Sort]
ts forall a. [a] -> [a] -> [a]
++ [Sort]
ts')
  where
    ts' :: [Sort]
ts'          = forall t. Visitable t => t -> [Sort]
applySorts AxiomEnv
ae'
    ae' :: AxiomEnv
ae'          = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
E.dummySpan String
"symbolEnv") SymEnv
env0 (forall (c :: * -> *) a. GInfo c a -> AxiomEnv
F.ae SInfo a
si)
    env0 :: SymEnv
env0         = SEnv Sort
-> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv
F.symEnv SEnv Sort
sEnv SEnv TheorySymbol
tEnv [DataDecl]
ds SEnv Sort
lits [Sort]
ts
    tEnv :: SEnv TheorySymbol
tEnv         = [DataDecl] -> SEnv TheorySymbol
Thy.theorySymbols [DataDecl]
ds
    ds :: [DataDecl]
ds           = forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls SInfo a
si
    ts :: [Sort]
ts           = forall k. (Eq k, Hashable k) => [k] -> [k]
Misc.hashNub (forall t. Visitable t => t -> [Sort]
applySorts SInfo a
si forall a. [a] -> [a] -> [a]
++ [Sort
t | (Symbol
_, Sort
t) <- forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
sEnv])
    sEnv :: SEnv Sort
sEnv         = (TheorySymbol -> Sort
F.tsSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv TheorySymbol
tEnv) forall a. Monoid a => a -> a -> a
`mappend` forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
xts
    xts :: [(Symbol, Sort)]
xts          = forall (c :: * -> *) a. Config -> GInfo c a -> [(Symbol, Sort)]
symbolSorts Config
cfg SInfo a
si forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
alits
    lits :: SEnv Sort
lits         = forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.dLits SInfo a
si forall a. SEnv a -> SEnv a -> SEnv a
`F.unionSEnv'` forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
alits
    alits :: [(Symbol, Sort)]
alits        = AxiomEnv -> [(Symbol, Sort)]
litsAEnv forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> AxiomEnv
F.ae SInfo a
si

litsAEnv :: F.AxiomEnv -> [(F.Symbol, F.Sort)]
litsAEnv :: AxiomEnv -> [(Symbol, Sort)]
litsAEnv AxiomEnv
ae = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymConsts a => a -> [SymConst]
symConsts AxiomEnv
ae) (forall a. a -> [a]
repeat Sort
F.strSort)

symbolSorts :: Config -> F.GInfo c a -> [(F.Symbol, F.Sort)]
symbolSorts :: forall (c :: * -> *) a. Config -> GInfo c a -> [(Symbol, Sort)]
symbolSorts Config
cfg GInfo c a
fi = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Error -> a
E.die forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a.
Config -> GInfo c a -> SanitizeM [(Symbol, Sort)]
symbolSorts' Config
cfg GInfo c a
fi

symbolSorts' :: Config -> F.GInfo c a -> SanitizeM [(F.Symbol, F.Sort)]
symbolSorts' :: forall (c :: * -> *) a.
Config -> GInfo c a -> SanitizeM [(Symbol, Sort)]
symbolSorts' Config
_cfg GInfo c a
fi  = (SanitizeM [(Symbol, Sort)] -> SanitizeM [(Symbol, Sort)]
normalize forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> SanitizeM [(Symbol, Sort)]
compact forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Symbol, Sort)]
defs forall a. [a] -> [a] -> [a]
++)) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (c :: * -> *) a. GInfo c a -> SanitizeM [(Symbol, Sort)]
bindSorts GInfo c a
fi
  where
    normalize :: SanitizeM [(Symbol, Sort)] -> SanitizeM [(Symbol, Sort)]
normalize       = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> b) -> [a] -> [b]
map (forall a.
(Sort -> Sort)
-> HashMap Symbol a -> (Symbol, Sort) -> (Symbol, Sort)
unShadow forall a. a -> a
txFun HashMap Symbol Sort
dm))
    dm :: HashMap Symbol Sort
dm              = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, Sort)]
defs
    defs :: [(Symbol, Sort)]
defs            = forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits forall a b. (a -> b) -> a -> b
$ GInfo c a
fi
    txFun :: a -> a
txFun           = forall a. a -> a
id

unShadow :: (F.Sort -> F.Sort) -> M.HashMap F.Symbol a -> (F.Symbol, F.Sort) -> (F.Symbol, F.Sort)
unShadow :: forall a.
(Sort -> Sort)
-> HashMap Symbol a -> (Symbol, Sort) -> (Symbol, Sort)
unShadow Sort -> Sort
tx HashMap Symbol a
dm (Symbol
x, Sort
t)
  | forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
x HashMap Symbol a
dm = (Symbol
x, Sort
t)
  | Bool
otherwise     = (Symbol
x, Sort -> Sort
tx Sort
t)

_defuncSort :: F.Sort -> F.Sort
_defuncSort :: Sort -> Sort
_defuncSort F.FFunc{} = Sort
F.funcSort
_defuncSort Sort
t         = Sort
t

compact :: [(F.Symbol, F.Sort)] -> Either E.Error [(F.Symbol, F.Sort)]
compact :: [(Symbol, Sort)] -> SanitizeM [(Symbol, Sort)]
compact [(Symbol, Sort)]
xts
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, [Sort])]
bad  = forall a b. b -> Either a b
Right [(Symbol
x, Sort
t) | (Symbol
x, [Sort
t]) <- [(Symbol, [Sort])]
ok ]
  | Bool
otherwise = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [(Symbol, [(Sort, [BindId])])] -> Error
dupBindErrors forall {a}. [(Symbol, [(Sort, [a])])]
bad'
  where
    bad' :: [(Symbol, [(Sort, [a])])]
bad'      = [(Symbol
x, (, []) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts) | (Symbol
x, [Sort]
ts) <- [(Symbol, [Sort])]
bad]
    ([(Symbol, [Sort])]
bad, [(Symbol, [Sort])]
ok) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition forall x t. (x, [t]) -> Bool
multiSorted forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> [(Symbol, [Sort])]
binds forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)]
xts
    binds :: [(Symbol, Sort)] -> [(Symbol, [Sort])]
binds     = forall k v. HashMap k v -> [(k, v)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map forall a. Ord a => [a] -> [a]
Misc.sortNub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group

--------------------------------------------------------------------------------
bindSorts  :: F.GInfo c a -> Either E.Error [(F.Symbol, F.Sort)]
--------------------------------------------------------------------------------
bindSorts :: forall (c :: * -> *) a. GInfo c a -> SanitizeM [(Symbol, Sort)]
bindSorts GInfo c a
fi
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, [(Sort, [BindId])])]
bad   = forall a b. b -> Either a b
Right [ (Symbol
x, Sort
t) | (Symbol
x, [(Sort
t, [BindId]
_)]) <- [(Symbol, [(Sort, [BindId])])]
ok ]
  | Bool
otherwise  = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [(Symbol, [(Sort, [BindId])])] -> Error
dupBindErrors [ (Symbol
x, [(Sort, [BindId])]
ts) | (Symbol
x, [(Sort, [BindId])]
ts) <- [(Symbol, [(Sort, [BindId])])]
bad]
  where
    ([(Symbol, [(Sort, [BindId])])]
bad, [(Symbol, [(Sort, [BindId])])]
ok)  = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition forall x t. (x, [t]) -> Bool
multiSorted forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {c :: * -> *} {a}.
GInfo c a -> [(Symbol, [(Sort, [BindId])])]
binds forall a b. (a -> b) -> a -> b
$ GInfo c a
fi
    binds :: GInfo c a -> [(Symbol, [(Sort, [BindId])])]
binds      = forall a. BindEnv a -> [(Symbol, [(Sort, [BindId])])]
symBinds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs


multiSorted :: (x, [t]) -> Bool
multiSorted :: forall x t. (x, [t]) -> Bool
multiSorted = (BindId
1 forall a. Ord a => a -> a -> Bool
<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> BindId
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd

dupBindErrors :: [(F.Symbol, [(F.Sort, [F.BindId] )])] -> E.Error
dupBindErrors :: [(Symbol, [(Sort, [BindId])])] -> Error
dupBindErrors = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Error -> Error -> Error
E.catError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (PPrint a, PPrint a) => (a, a) -> Error
dbe
  where
   dbe :: (a, a) -> Error
dbe (a
x, a
y) = SrcSpan -> Doc -> Error
E.err SrcSpan
E.dummySpan forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ Doc
"Multiple sorts for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
x
                                         , BindId -> Doc -> Doc
nest BindId
4 (forall a. PPrint a => a -> Doc
pprint a
y) ]

--------------------------------------------------------------------------------
symBinds  :: F.BindEnv a -> [SymBinds]
--------------------------------------------------------------------------------
symBinds :: forall a. BindEnv a -> [(Symbol, [(Sort, [BindId])])]
symBinds  = {- THIS KILLS ELEM: tracepp "symBinds" . -}
            forall k v. HashMap k v -> [(k, v)]
M.toList
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group
          forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. BindEnv a -> [(Symbol, (Sort, BindId))]
binders

type SymBinds = (F.Symbol, [(F.Sort, [F.BindId])])

binders :: F.BindEnv a -> [(F.Symbol, (F.Sort, F.BindId))]
binders :: forall a. BindEnv a -> [(Symbol, (Sort, BindId))]
binders BindEnv a
be = [(Symbol
x, (SortedReft -> Sort
F.sr_sort SortedReft
t, BindId
i)) | (BindId
i, (Symbol
x, SortedReft
t, a
_)) <- forall a. BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
F.bindEnvToList BindEnv a
be]


--------------------------------------------------------------------------------
-- | Drop func-sorted `bind` that are shadowed by `constant` (if same type, else error)
--------------------------------------------------------------------------------
dropFuncSortedShadowedBinders :: F.SInfo a -> F.SInfo a
--------------------------------------------------------------------------------
dropFuncSortedShadowedBinders :: forall a. SInfo a -> SInfo a
dropFuncSortedShadowedBinders SInfo a
fi = forall a. KeepBindF -> KeepSortF -> SInfo a -> SInfo a
dropBinders KeepBindF
ok (forall a b. a -> b -> a
const Bool
True) SInfo a
fi
  where
    ok :: KeepBindF
ok Symbol
x Sort
t  = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
x HashMap Symbol Sort
defs Bool -> Bool -> Bool
==> (forall (c :: * -> *) a. GInfo c a -> Bool
F.allowHO SInfo a
fi Bool -> Bool -> Bool
|| KeepSortF
isFirstOrder Sort
t)
    defs :: HashMap Symbol Sort
defs    = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
fi

infixl 9 ==>
(==>) :: Bool -> Bool -> Bool
Bool
p ==> :: Bool -> Bool -> Bool
==> Bool
q = Bool -> Bool
not Bool
p Bool -> Bool -> Bool
|| Bool
q

--------------------------------------------------------------------------------
-- | Drop irrelevant binders from WfC Environments
--------------------------------------------------------------------------------
sanitizeWfC :: F.SInfo a -> F.SInfo a
sanitizeWfC :: forall a. SInfo a -> SInfo a
sanitizeWfC SInfo a
si = SInfo a
si { ws :: HashMap KVar (WfC a)
F.ws = HashMap KVar (WfC a)
ws' }
  where
    ws' :: HashMap KVar (WfC a)
ws'        = forall a. [BindId] -> WfC a -> WfC a
deleteWfCBinds [BindId]
drops forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si
    (BindEnv a
_,[BindId]
drops)  = forall a. KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
filterBindEnv KeepBindF
keepF   forall a b. (a -> b) -> a -> b
$  forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si
    keepF :: KeepBindF
keepF      = [KeepBindF] -> KeepBindF
conjKF [forall a. SInfo a -> KeepBindF
nonConstantF SInfo a
si, forall a. SInfo a -> KeepBindF
nonFunctionF SInfo a
si, KeepBindF
_nonDerivedLH]
    -- drops   = F.tracepp "sanitizeWfC: dropping" $ L.sort drops'

conjKF :: [KeepBindF] -> KeepBindF
conjKF :: [KeepBindF] -> KeepBindF
conjKF [KeepBindF]
fs Symbol
x Sort
t = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [KeepBindF
f Symbol
x Sort
t | KeepBindF
f <- [KeepBindF]
fs]

-- | `nonDerivedLH` keeps a bind x if it does not start with `$` which is used
--   typically for names that are automatically "derived" by GHC (and which can)
--   blow up the environments thereby clogging instantiation, etc.
--   NOTE: This is an LH specific hack and should be moved there.

_nonDerivedLH :: KeepBindF
_nonDerivedLH :: KeepBindF
_nonDerivedLH Symbol
x Sort
_ = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Bool
T.isPrefixOf Text
"$" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
last forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Text -> [Text]
T.split (Char
'.' forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText forall a b. (a -> b) -> a -> b
$ Symbol
x

nonConstantF :: F.SInfo a -> KeepBindF
nonConstantF :: forall a. SInfo a -> KeepBindF
nonConstantF SInfo a
si = \Symbol
x Sort
_ -> Bool -> Bool
not (Symbol
x forall a. Symbol -> SEnv a -> Bool
`F.memberSEnv` SEnv Sort
cEnv)
  where
    cEnv :: SEnv Sort
cEnv        = forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
si

nonFunctionF :: F.SInfo a -> KeepBindF
nonFunctionF :: forall a. SInfo a -> KeepBindF
nonFunctionF SInfo a
si
  | forall (c :: * -> *) a. GInfo c a -> Bool
F.allowHO SInfo a
si    = \Symbol
_ Sort
_ -> Bool
True
  | Bool
otherwise       = \Symbol
_ Sort
t -> forall a. Maybe a -> Bool
isNothing (Sort -> Maybe ([BindId], [Sort], Sort)
F.functionSort Sort
t)

--------------------------------------------------------------------------------
-- | Generic API for Deleting Binders from FInfo
--------------------------------------------------------------------------------
dropBinders :: KeepBindF -> KeepSortF -> F.SInfo a -> F.SInfo a
--------------------------------------------------------------------------------
dropBinders :: forall a. KeepBindF -> KeepSortF -> SInfo a -> SInfo a
dropBinders KeepBindF
f KeepSortF
g SInfo a
fi  = SInfo a
fi { bs :: BindEnv a
F.bs    = BindEnv a
bs'
                         , cm :: HashMap SubcId (SimpC a)
F.cm    = HashMap SubcId (SimpC a)
cm'
                         , ws :: HashMap KVar (WfC a)
F.ws    = HashMap KVar (WfC a)
ws'
                         , gLits :: SEnv Sort
F.gLits = SEnv Sort
lits' }
  where
    -- discards        = diss
    (BindEnv a
bs', [BindId]
discards) = forall a. KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
filterBindEnv KeepBindF
f forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi
    cm' :: HashMap SubcId (SimpC a)
cm'             = forall a. [BindId] -> SimpC a -> SimpC a
deleteSubCBinds [BindId]
discards   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
fi
    ws' :: HashMap KVar (WfC a)
ws'             = forall a. [BindId] -> WfC a -> WfC a
deleteWfCBinds  [BindId]
discards   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi
    lits' :: SEnv Sort
lits'           = forall a. (a -> Bool) -> SEnv a -> SEnv a
F.filterSEnv KeepSortF
g (forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
fi)

type KeepBindF = F.Symbol -> F.Sort -> Bool
type KeepSortF = F.Sort -> Bool

deleteSubCBinds :: [F.BindId] -> F.SimpC a -> F.SimpC a
deleteSubCBinds :: forall a. [BindId] -> SimpC a -> SimpC a
deleteSubCBinds [BindId]
bs SimpC a
sc = SimpC a
sc { _cenv :: IBindEnv
F._cenv = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr BindId -> IBindEnv -> IBindEnv
F.deleteIBindEnv (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
sc) [BindId]
bs }

deleteWfCBinds :: [F.BindId] -> F.WfC a -> F.WfC a
deleteWfCBinds :: forall a. [BindId] -> WfC a -> WfC a
deleteWfCBinds [BindId]
bs WfC a
wf = WfC a
wf { wenv :: IBindEnv
F.wenv = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr BindId -> IBindEnv -> IBindEnv
F.deleteIBindEnv (forall a. WfC a -> IBindEnv
F.wenv WfC a
wf) [BindId]
bs }

filterBindEnv :: KeepBindF -> F.BindEnv a -> (F.BindEnv a, [F.BindId])
filterBindEnv :: forall a. KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
filterBindEnv KeepBindF
f BindEnv a
be  = (BindEnv a
keepBindEnv , [BindId]
discard')
  where
    keepBindEnv :: BindEnv a
keepBindEnv     = forall a. [(BindId, (Symbol, SortedReft, a))] -> BindEnv a
F.bindEnvFromList [(BindId
i, (Symbol
x, SortedReft
sr, a
a)) | (BindId
i, (Symbol
x, SortedReft
sr, a
a)) <- [(BindId, (Symbol, SortedReft, a))]
keep]
    ([(BindId, (Symbol, SortedReft, a))]
keep, [(BindId, (Symbol, SortedReft, a))]
discard) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition forall {a} {c}. (a, (Symbol, SortedReft, c)) -> Bool
f' forall a b. (a -> b) -> a -> b
$ forall a. BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
F.bindEnvToList BindEnv a
be
    discard' :: [BindId]
discard'        = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BindId, (Symbol, SortedReft, a))]
discard
    f' :: (a, (Symbol, SortedReft, c)) -> Bool
f' (a
_, (Symbol
x, SortedReft
t, c
_)) = KeepBindF
f Symbol
x (SortedReft -> Sort
F.sr_sort SortedReft
t)


---------------------------------------------------------------------------
-- | Replace KVars that do not have a WfC with PFalse
---------------------------------------------------------------------------
replaceDeadKvars :: F.SInfo a -> F.SInfo a
---------------------------------------------------------------------------
replaceDeadKvars :: forall a. SInfo a -> SInfo a
replaceDeadKvars SInfo a
fi = forall t. Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars KVar -> Maybe Expr
go SInfo a
fi
  where
    go :: KVar -> Maybe Expr
go KVar
k | KVar
k forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`M.member` forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi = forall a. Maybe a
Nothing
         | Bool
otherwise            = forall a. a -> Maybe a
Just Expr
F.PFalse