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

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     (ElabParam(..), elaborate, applySorts, isFirstOrder)
-- import           Language.Fixpoint.Defunctionalize
import           Language.Fixpoint.Misc ((==>))
import qualified Language.Fixpoint.Misc                            as Misc
import qualified Language.Fixpoint.Types                           as F
import           Language.Fixpoint.Types.Config (Config, solverFlags)
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.Bifunctor as Bifunctor (first)
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 hiding ((<>))

type SanitizeM a = Either E.Error a

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

--------------------------------------------------------------------------------
-- | '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 { F.ae = dropAdtAenv (F.ddecls si) (F.ae si) }

dropAdtAenv :: [F.DataDecl] -> F.AxiomEnv -> F.AxiomEnv
dropAdtAenv :: [DataDecl] -> AxiomEnv -> AxiomEnv
dropAdtAenv [DataDecl]
ds AxiomEnv
ae = AxiomEnv
ae { F.aenvSimpl = filter (not . isAdt) (F.aenvSimpl ae) }
  where
    isAdt :: Rewrite -> Bool
isAdt         = (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
adtSyms) (Symbol -> Bool) -> (Rewrite -> Symbol) -> Rewrite -> Bool
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 = ListNE Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (ListNE Symbol -> HashSet Symbol)
-> ([DataDecl] -> ListNE Symbol) -> [DataDecl] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, TheorySymbol) -> Symbol)
-> [(Symbol, TheorySymbol)] -> ListNE Symbol
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, TheorySymbol) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, TheorySymbol)] -> ListNE Symbol)
-> ([DataDecl] -> [(Symbol, TheorySymbol)])
-> [DataDecl]
-> ListNE Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> [(Symbol, TheorySymbol)])
-> [DataDecl] -> [(Symbol, TheorySymbol)]
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 { F.dLits = F.unionSEnv (F.dLits si) lits'
                    , F.gLits = F.unionSEnv (F.gLits si) lits'
                    }
  where
    lits' :: HashMap Symbol Sort
lits'      = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (SymConst -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol SymConst
x, Sort
F.strSort) | SymConst
x <- SInfo a -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts SInfo a
si ]

--------------------------------------------------------------------------------
-- | `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 { F.ae = ae' }
  | Config -> Bool
Cfg.etaElim Config
cfg
  = SInfo a
si { F.ae = (ae {F.aenvEqs = etaElimNEW `fmap` F.aenvEqs ae }) }
  | Bool
otherwise
  = SInfo a
si
  where
    ae' :: AxiomEnv
ae' = AxiomEnv
ae {F.aenvEqs = eqs}
    ae :: AxiomEnv
ae = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
F.ae SInfo a
si
    eqs :: [EquationV Symbol]
eqs = (EquationV Symbol -> EquationV Symbol)
-> [EquationV Symbol] -> [EquationV Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EquationV Symbol -> EquationV Symbol
etaElim (AxiomEnv -> [EquationV Symbol]
F.aenvEqs AxiomEnv
ae)

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

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

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

    thySyms :: SEnv TheorySymbol
thySyms = Config -> SInfo a -> SEnv TheorySymbol
forall (c :: * -> *) a. Config -> GInfo c a -> SEnv TheorySymbol
theoryEnv Config
cfg SInfo a
si

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

theoryEnv :: Config -> F.GInfo c a -> F.SEnv F.TheorySymbol
theoryEnv :: forall (c :: * -> *) a. Config -> GInfo c a -> SEnv TheorySymbol
theoryEnv Config
cfg GInfo c a
si
  =  SMTSolver -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
Thy.theorySymbols (Config -> SMTSolver
Cfg.solver Config
cfg)
  SEnv TheorySymbol -> SEnv TheorySymbol -> SEnv TheorySymbol
forall a. Semigroup a => a -> a -> a
<> [EquationV Symbol] -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
Thy.theorySymbols (GInfo c a -> [EquationV Symbol]
forall (c :: * -> *) a. GInfo c a -> [EquationV Symbol]
F.defns GInfo c a
si)
  SEnv TheorySymbol -> SEnv TheorySymbol -> SEnv TheorySymbol
forall a. Semigroup a => a -> a -> a
<> [DataDecl] -> SEnv TheorySymbol
forall a. TheorySymbols a => a -> SEnv TheorySymbol
Thy.theorySymbols (GInfo c a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls GInfo c a
si)

--------------------------------------------------------------------------------
-- | 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 = SanitizeM (SInfo a)
-> ([(KVar, SubcId, SubcId, IBindEnv)] -> SanitizeM (SInfo a))
-> [(KVar, SubcId, SubcId, IBindEnv)]
-> SanitizeM (SInfo a)
forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (SInfo a -> SanitizeM (SInfo a)
forall a b. b -> Either a b
Right SInfo a
si) (Error -> SanitizeM (SInfo a)
forall a b. a -> Either a b
Left (Error -> SanitizeM (SInfo a))
-> ([(KVar, SubcId, SubcId, IBindEnv)] -> Error)
-> [(KVar, SubcId, SubcId, IBindEnv)]
-> SanitizeM (SInfo a)
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              = (KVar -> [(KVar, SubcId, SubcId, IBindEnv)])
-> [KVar] -> [(KVar, SubcId, SubcId, IBindEnv)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SInfo a -> KvDefs -> KVar -> [(KVar, SubcId, SubcId, IBindEnv)]
forall a.
SInfo a -> KvDefs -> KVar -> [(KVar, SubcId, SubcId, IBindEnv)]
checkIllScope SInfo a
si KvDefs
kDs) [KVar]
ks
    kDs :: KvDefs
kDs               = SInfo a -> KvDefs
forall a. SInfo a -> KvDefs
kvarDefUses SInfo a
si
    ks :: [KVar]
ks                = (KVar -> Bool) -> [KVar] -> [KVar]
forall a. (a -> Bool) -> [a] -> [a]
filter KVar -> Bool
notKut ([KVar] -> [KVar]) -> [KVar] -> [KVar]
forall a b. (a -> b) -> a -> b
$ HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si)
    notKut :: KVar -> Bool
notKut            = Bool -> Bool
not (Bool -> Bool) -> (KVar -> Bool) -> KVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar -> Kuts -> Bool
`F.ksMember` SInfo a -> Kuts
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 (ListNE Error -> Error)
-> ([(KVar, SubcId, SubcId, IBindEnv)] -> ListNE Error)
-> [(KVar, SubcId, SubcId, IBindEnv)]
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((KVar, SubcId, SubcId, IBindEnv) -> Error)
-> [(KVar, SubcId, SubcId, IBindEnv)] -> ListNE Error
forall a b. (a -> b) -> [a] -> [b]
map (KVar, SubcId, SubcId, IBindEnv) -> Error
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 = ((SubcId, SubcId) -> Maybe (KVar, SubcId, SubcId, IBindEnv))
-> [(SubcId, SubcId)] -> [(KVar, SubcId, SubcId, IBindEnv)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((SubcId -> SubcId -> Maybe (KVar, SubcId, SubcId, IBindEnv))
-> (SubcId, SubcId) -> Maybe (KVar, SubcId, SubcId, IBindEnv)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SInfo a
-> KVar
-> SubcId
-> SubcId
-> Maybe (KVar, SubcId, SubcId, IBindEnv)
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 SubcId -> SubcId -> Bool
forall a. Eq a => a -> a -> Bool
/= SubcId
o ]
    ins :: [SubcId]
ins                        = [SubcId] -> KVar -> KvConstrM -> [SubcId]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] KVar
k KvConstrM
inM
    outs :: [SubcId]
outs                       = [SubcId] -> KVar -> KvConstrM -> [SubcId]
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 = Maybe (KVar, SubcId, SubcId, IBindEnv)
forall a. Maybe a
Nothing
  | Bool
otherwise            = (KVar, SubcId, SubcId, IBindEnv)
-> Maybe (KVar, SubcId, SubcId, IBindEnv)
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) $ -} SInfo a -> KVar -> IBindEnv
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                 = SInfo a -> SubcId -> IBindEnv
forall a. SInfo a -> SubcId -> IBindEnv
subcBinds SInfo a
si SubcId
inI
    outXs :: IBindEnv
outXs                = SInfo a -> SubcId -> IBindEnv
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 = SimpC a -> IBindEnv
forall a. SimpC a -> IBindEnv
F._cenv (SimpC a -> IBindEnv) -> SimpC a -> IBindEnv
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
si HashMap SubcId (SimpC a) -> SubcId -> SimpC a
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 = WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv (WfC a -> IBindEnv) -> (KVar -> WfC a) -> KVar -> IBindEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si HashMap KVar (WfC a) -> KVar -> WfC a
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 = ([(KVar, SubcId)] -> KvConstrM
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(KVar, SubcId)]
ins, [(KVar, SubcId)] -> KvConstrM
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(KVar, SubcId)]
outs)
  where
    es :: [CEdge]
es         = SInfo a -> [CEdge]
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 = (KVar -> Subst -> Subst) -> SInfo a -> SInfo a
forall t. Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts ((Symbol -> ExprV Symbol -> Bool) -> Subst -> Subst
F.filterSubst ((Symbol -> ExprV Symbol -> Bool) -> Subst -> Subst)
-> (KVar -> Symbol -> ExprV Symbol -> Bool)
-> KVar
-> Subst
-> Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Symbol -> ExprV Symbol -> Bool
forall {p}. KVar -> Symbol -> p -> Bool
f) SInfo a
si
  where
    kvsM :: HashMap KVar (HashSet Symbol)
kvsM          = (KVar -> WfC a -> HashSet Symbol)
-> HashMap KVar (WfC a) -> HashMap KVar (HashSet Symbol)
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) (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si)
    kvDom :: KVar -> HashSet Symbol
kvDom         = ListNE Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (ListNE Symbol -> HashSet Symbol)
-> (KVar -> ListNE Symbol) -> KVar -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> KVar -> ListNE Symbol
forall a. SInfo a -> KVar -> ListNE Symbol
F.kvarDomain SInfo a
si
    f :: KVar -> Symbol -> p -> Bool
f KVar
k Symbol
x p
_       = Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x (HashSet Symbol
-> KVar -> HashMap KVar (HashSet Symbol) -> HashSet Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault HashSet Symbol
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 { F.ws = M.mapWithKey (restrictWf kvm) (F.ws si) }
  where
    kvm :: KvDom
kvm               = SInfo a -> KvDom
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 { F.wenv = F.filterIBindEnv f (F.wenv w) }
  where
    f :: BindId -> Bool
f BindId
i            = BindId -> HashSet BindId -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member BindId
i HashSet BindId
kis
    kis :: HashSet BindId
kis            = [BindId] -> HashSet BindId
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ BindId
i | (Symbol
_, BindId
i) <- SEnv BindId -> [(Symbol, BindId)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv BindId
kEnv ]
    kEnv :: SEnv BindId
kEnv           = SEnv BindId -> KVar -> KvDom -> SEnv BindId
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault SEnv BindId
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 = (KvDom -> SimpC a -> KvDom) -> KvDom -> [SimpC a] -> KvDom
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (SInfo a -> KvDom -> SimpC a -> KvDom
forall a. SInfo a -> KvDom -> SimpC a -> KvDom
dropKvarEnv SInfo a
si) KvDom
env0 [SimpC a]
cs
  where
    cs :: [SimpC a]
cs         = HashMap SubcId (SimpC a) -> [SimpC a]
forall k v. HashMap k v -> [v]
M.elems  (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
si)
    env0 :: KvDom
env0       = SInfo a -> KvDom
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 = (KVar -> SEnv BindId -> SEnv BindId) -> KvDom -> KvDom
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            = SInfo a -> SimpC a -> KvBads
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 = (SEnv BindId -> Symbol -> SEnv BindId)
-> SEnv BindId -> ListNE Symbol -> SEnv BindId
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ((Symbol -> SEnv BindId -> SEnv BindId)
-> SEnv BindId -> Symbol -> SEnv BindId
forall a b c. (a -> b -> c) -> b -> a -> c
flip Symbol -> SEnv BindId -> SEnv BindId
forall a. Symbol -> SEnv a -> SEnv a
F.deleteSEnv) SEnv BindId
kEnv ListNE Symbol
xs
  where
    xs :: ListNE Symbol
xs                     = ListNE Symbol -> KVar -> KvBads -> ListNE Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault ListNE Symbol
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 = [(KVar, Symbol)] -> KvBads
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 (ExprV Symbol)
su) <- [(Symbol, SortedReft)] -> SimpC a -> [(Maybe Symbol, KVar, Subst)]
forall a.
[(Symbol, SortedReft)] -> SimpC a -> [(Maybe Symbol, KVar, Subst)]
subcKSubs [(Symbol, SortedReft)]
xsrs SimpC a
c
                          , let vEnv :: HashSet Symbol
vEnv = HashSet Symbol
-> (Symbol -> HashSet Symbol) -> Maybe Symbol -> HashSet Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashSet Symbol
sEnv (Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
`S.insert` HashSet Symbol
sEnv) Maybe Symbol
v
                          , (Symbol
x, ExprV Symbol
e)          <- HashMap Symbol (ExprV Symbol) -> [(Symbol, ExprV Symbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol (ExprV Symbol)
su
                          , HashSet Symbol -> ExprV Symbol -> Bool
badArg HashSet Symbol
vEnv ExprV Symbol
e
                 ]
    sEnv :: HashSet Symbol
sEnv       = ListNE Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Symbol, SortedReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SortedReft) -> Symbol)
-> [(Symbol, SortedReft)] -> ListNE Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
xsrs)
    xsrs :: [(Symbol, SortedReft)]
xsrs       = 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
si) (SimpC a -> IBindEnv
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 -> ExprV Symbol -> Bool
badArg HashSet Symbol
sEnv (F.EVar Symbol
y) = Bool -> Bool
not (Symbol
y Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
sEnv)
badArg HashSet Symbol
_    ExprV Symbol
_          = 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 = [(Maybe Symbol, KVar, Subst)]
forall {a}. [(Maybe a, KVar, Subst)]
rhs [(Maybe Symbol, KVar, Subst)]
-> [(Maybe Symbol, KVar, Subst)] -> [(Maybe Symbol, KVar, Subst)]
forall a. [a] -> [a] -> [a]
++ [(Maybe Symbol, KVar, Subst)]
lhs
  where
    lhs :: [(Maybe Symbol, KVar, Subst)]
lhs          = [ (Symbol -> Maybe Symbol
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          = [(Maybe a
forall a. Maybe a
Nothing, KVar
k, Subst
su) | F.PKVar KVar
k Subst
su <- [SimpC a -> ExprV Symbol
forall (c :: * -> *) a. TaggedC c a => c a -> ExprV Symbol
F.crhs SimpC a
c]]


initKvarEnv :: F.SInfo a -> KvDom
initKvarEnv :: forall a. SInfo a -> KvDom
initKvarEnv SInfo a
si = SInfo a -> WfC a -> SEnv BindId
forall a. SInfo a -> WfC a -> SEnv BindId
initEnv SInfo a
si (WfC a -> SEnv BindId) -> HashMap KVar (WfC a) -> KvDom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInfo a -> HashMap KVar (WfC a)
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 = [(Symbol, BindId)] -> SEnv BindId
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 (IBindEnv -> [BindId]) -> IBindEnv -> [BindId]
forall a b. (a -> b) -> a -> b
$ WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv WfC a
w
    bind :: BindId -> Symbol
bind BindId
i   = (Symbol, SortedReft, a) -> Symbol
forall a b c. (a, b, c) -> a
Misc.fst3 (BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindId
i BindEnv a
be)
    be :: BindEnv a
be       = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si

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

known :: Config -> F.SInfo a -> F.Symbol -> Bool
known :: forall a. Config -> SInfo a -> Symbol -> Bool
known Config
cfg SInfo a
fi  = \Symbol
x -> Symbol -> SEnv Sort -> Bool
forall a. Symbol -> SEnv a -> Bool
F.memberSEnv Symbol
x SEnv Sort
lits Bool -> Bool -> Bool
|| Symbol -> SEnv TheorySymbol -> Bool
forall a. Symbol -> SEnv a -> Bool
F.memberSEnv Symbol
x SEnv TheorySymbol
prims
  where
    lits :: SEnv Sort
lits  = SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
fi
    prims :: SEnv TheorySymbol
prims = Config -> SInfo a -> SEnv TheorySymbol
forall (c :: * -> *) a. Config -> GInfo c a -> SEnv TheorySymbol
theoryEnv Config
cfg 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
knownSym SimpC a
c = if HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null HashSet Symbol
fv then Maybe (ListNE Symbol)
forall a. Maybe a
Nothing else ListNE Symbol -> Maybe (ListNE Symbol)
forall a. a -> Maybe a
Just (HashSet Symbol -> ListNE Symbol
forall a. HashSet a -> [a]
S.toList HashSet Symbol
fv)
  where
    be :: BindEnv a
be   = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi
    ids :: [BindId]
ids  = IBindEnv -> [BindId]
F.elemsIBindEnv (IBindEnv -> [BindId]) -> IBindEnv -> [BindId]
forall a b. (a -> b) -> a -> b
$ SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
c
    cDom :: ListNE Symbol
cDom = [(Symbol, SortedReft, a) -> Symbol
forall a b c. (a, b, c) -> a
Misc.fst3 ((Symbol, SortedReft, a) -> Symbol)
-> (Symbol, SortedReft, a) -> Symbol
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindId
i BindEnv a
be | BindId
i <- [BindId]
ids]
    cRng :: ListNE Symbol
cRng = [ListNE Symbol] -> ListNE Symbol
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [HashSet Symbol -> ListNE Symbol
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> ListNE Symbol)
-> ((Symbol, SortedReft, a) -> HashSet Symbol)
-> (Symbol, SortedReft, a)
-> ListNE Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> HashSet Symbol
F.reftFreeVars (Reft -> HashSet Symbol)
-> ((Symbol, SortedReft, a) -> Reft)
-> (Symbol, SortedReft, a)
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
F.sr_reft (SortedReft -> Reft)
-> ((Symbol, SortedReft, a) -> SortedReft)
-> (Symbol, SortedReft, a)
-> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft, a) -> SortedReft
forall a b c. (a, b, c) -> b
Misc.snd3 ((Symbol, SortedReft, a) -> ListNE Symbol)
-> (Symbol, SortedReft, a) -> ListNE Symbol
forall a b. (a -> b) -> a -> b
$ BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv BindId
i BindEnv a
be | BindId
i <- [BindId]
ids]
        ListNE Symbol -> ListNE Symbol -> ListNE Symbol
forall a. [a] -> [a] -> [a]
++ ExprV Symbol -> ListNE Symbol
forall a. Subable a => a -> ListNE Symbol
F.syms (SimpC a -> ExprV Symbol
forall (c :: * -> *) a. TaggedC c a => c a -> ExprV Symbol
F.crhs SimpC a
c)
    fv :: HashSet Symbol
fv   = (ListNE Symbol -> ListNE Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> [a] -> HashSet a
`Misc.nubDiff` ListNE Symbol
cDom) (ListNE Symbol -> HashSet Symbol)
-> (ListNE Symbol -> ListNE Symbol)
-> ListNE Symbol
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Bool) -> ListNE Symbol -> ListNE Symbol
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
knownSym) (ListNE Symbol -> HashSet Symbol)
-> ListNE Symbol -> HashSet Symbol
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 (ListNE Error -> Error)
-> (ListNE (SimpC a, ListNE Symbol) -> ListNE Error)
-> ListNE (SimpC a, ListNE Symbol)
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SimpC a, ListNE Symbol) -> Error)
-> ListNE (SimpC a, ListNE Symbol) -> ListNE Error
forall a b. (a -> b) -> [a] -> [b]
map ((SubcId, ListNE Symbol) -> Error
forall a. PPrint a => (SubcId, a) -> Error
E.errFreeVarInConstraint ((SubcId, ListNE Symbol) -> Error)
-> ((SimpC a, ListNE Symbol) -> (SubcId, ListNE Symbol))
-> (SimpC a, ListNE Symbol)
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpC a -> SubcId)
-> (SimpC a, ListNE Symbol) -> (SubcId, ListNE Symbol)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
Bifunctor.first SimpC a -> SubcId
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 = SanitizeM (SInfo a)
-> ([DataDecl] -> SanitizeM (SInfo a))
-> [DataDecl]
-> SanitizeM (SInfo a)
forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (SInfo a -> SanitizeM (SInfo a)
forall a b. b -> Either a b
Right SInfo a
fi) (Error -> SanitizeM (SInfo a)
forall a b. a -> Either a b
Left (Error -> SanitizeM (SInfo a))
-> ([DataDecl] -> Error) -> [DataDecl] -> SanitizeM (SInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataDecl] -> Error
badDataDecl) [DataDecl]
bads
  where
    bads :: [DataDecl]
bads = [DataDecl] -> [DataDecl]
F.checkRegular (SInfo a -> [DataDecl]
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 [ DataDecl -> Error
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 = SanitizeM (SInfo a)
-> ([(Qualifier, ListNE Symbol)] -> SanitizeM (SInfo a))
-> [(Qualifier, ListNE Symbol)]
-> SanitizeM (SInfo a)
forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (SInfo a -> SanitizeM (SInfo a)
forall a b. b -> Either a b
Right SInfo a
fi) (Error -> SanitizeM (SInfo a)
forall a b. a -> Either a b
Left (Error -> SanitizeM (SInfo a))
-> ([(Qualifier, ListNE Symbol)] -> Error)
-> [(Qualifier, ListNE Symbol)]
-> SanitizeM (SInfo a)
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 <- SInfo a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
fi, let xs :: ListNE Symbol
xs = Qualifier -> ListNE Symbol
forall a. Subable a => a -> ListNE Symbol
free Qualifier
q, Bool -> Bool
not (ListNE Symbol -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ListNE Symbol
xs) ]
    free :: a -> ListNE Symbol
free a
q  = (Symbol -> Bool) -> ListNE Symbol -> ListNE Symbol
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
isLit) (a -> ListNE Symbol
forall a. Subable a => a -> ListNE Symbol
F.syms a
q)
    isLit :: Symbol -> Bool
isLit Symbol
x = Symbol -> SEnv Sort -> Bool
forall a. Symbol -> SEnv a -> Bool
F.memberSEnv Symbol
x (SInfo a -> SEnv Sort
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 [ Qualifier -> ListNE Symbol -> Error
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 = SanitizeM (SInfo a)
-> ([(SubcId, SimpC a)] -> SanitizeM (SInfo a))
-> [(SubcId, SimpC a)]
-> SanitizeM (SInfo a)
forall b a. b -> ([a] -> b) -> [a] -> b
Misc.applyNonNull (SInfo a -> SanitizeM (SInfo a)
forall a b. b -> Either a b
Right SInfo a
fi) (Error -> SanitizeM (SInfo a)
forall a b. a -> Either a b
Left (Error -> SanitizeM (SInfo a))
-> ([(SubcId, SimpC a)] -> Error)
-> [(SubcId, SimpC a)]
-> SanitizeM (SInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SubcId, SimpC a)] -> Error
forall a. ListNE (SubcId, SimpC a) -> Error
badRhs) [(SubcId, SimpC a)]
bads
  where
    ics :: [(SubcId, SimpC a)]
ics        = HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)])
-> HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap SubcId (SimpC a)
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SimpC a -> Bool
forall {c :: * -> *} {a}. TaggedC c a => c a -> Bool
isOk SimpC a
c]
    isOk :: c a -> Bool
isOk c a
c     = c a -> Bool
forall {c :: * -> *} {a}. TaggedC c a => c a -> Bool
isKvarC c a
c Bool -> Bool -> Bool
|| c a -> 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 (ListNE Error -> Error)
-> (ListNE (SubcId, SimpC a) -> ListNE Error)
-> ListNE (SubcId, SimpC a)
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SubcId, SimpC a) -> Error)
-> ListNE (SubcId, SimpC a) -> ListNE Error
forall a b. (a -> b) -> [a] -> [b]
map (SubcId, SimpC a) -> Error
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 (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ Doc
"Malformed RHS for constraint id" Doc -> Doc -> Doc
<+> SubcId -> Doc
forall a. PPrint a => a -> Doc
pprint SubcId
i
                                          , BindId -> Doc -> Doc
nest BindId
4 (ExprV Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (SimpC a -> ExprV Symbol
forall (c :: * -> *) a. TaggedC c a => c a -> ExprV Symbol
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
thyEnv [DataDecl]
ds SEnv Sort
lits ([Sort]
ts [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort]
ts')
  where
    ts' :: [Sort]
ts'          = AxiomEnv -> [Sort]
forall t. Foldable t => t -> [Sort]
applySorts AxiomEnv
ae'
    ae' :: AxiomEnv
ae'          = ElabParam -> AxiomEnv -> AxiomEnv
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam ElabFlags
ef (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
E.dummySpan String
"symbolEnv") SymEnv
env0) (SInfo a -> AxiomEnv
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
thyEnv [DataDecl]
ds SEnv Sort
lits [Sort]
ts
    thyEnv :: SEnv TheorySymbol
thyEnv       = Config -> SInfo a -> SEnv TheorySymbol
forall (c :: * -> *) a. Config -> GInfo c a -> SEnv TheorySymbol
theoryEnv Config
cfg SInfo a
si
    ds :: [DataDecl]
ds           = SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls SInfo a
si
    ts :: [Sort]
ts           = [Sort] -> [Sort]
forall k. Ord k => [k] -> [k]
Misc.setNub (SInfo a -> [Sort]
forall t. Foldable t => t -> [Sort]
applySorts SInfo a
si [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort
t | (Symbol
_, Sort
t) <- SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
sEnv])
    sEnv :: SEnv Sort
sEnv         = ElabFlags -> SEnv Sort -> SEnv Sort
F.coerceSortEnv ElabFlags
ef (SEnv Sort -> SEnv Sort) -> SEnv Sort -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ (TheorySymbol -> Sort
F.tsSort (TheorySymbol -> Sort) -> SEnv TheorySymbol -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv TheorySymbol
thyEnv) SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Monoid a => a -> a -> a
`mappend` [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
xts
    slv :: SMTSolver
slv          = Config -> SMTSolver
Cfg.solver Config
cfg
    ef :: ElabFlags
ef           = SMTSolver -> ElabFlags
solverFlags SMTSolver
slv
    xts :: [(Symbol, Sort)]
xts          = Config -> SInfo a -> [(Symbol, Sort)]
forall (c :: * -> *) a. Config -> GInfo c a -> [(Symbol, Sort)]
symbolSorts Config
cfg SInfo a
si [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
alits
    lits :: SEnv Sort
lits         = SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.dLits SInfo a
si SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. SEnv a -> SEnv a -> SEnv a
`F.unionSEnv'` [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [(Symbol, Sort)]
alits
    alits :: [(Symbol, Sort)]
alits        = AxiomEnv -> [(Symbol, Sort)]
litsAEnv (AxiomEnv -> [(Symbol, Sort)]) -> AxiomEnv -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ SInfo a -> AxiomEnv
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 = ListNE Symbol -> [Sort] -> [(Symbol, Sort)]
forall a b. [a] -> [b] -> [(a, b)]
zip (SymConst -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (SymConst -> Symbol) -> [SymConst] -> ListNE Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts AxiomEnv
ae) (Sort -> [Sort]
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 = (Error -> [(Symbol, Sort)])
-> ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> Either Error [(Symbol, Sort)]
-> [(Symbol, Sort)]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Error -> [(Symbol, Sort)]
forall a. Error -> a
E.die [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> a
id (Either Error [(Symbol, Sort)] -> [(Symbol, Sort)])
-> Either Error [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ Config -> GInfo c a -> Either Error [(Symbol, Sort)]
forall (c :: * -> *) a.
Config -> GInfo c a -> Either Error [(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 -> Either Error [(Symbol, Sort)]
symbolSorts' Config
_cfg GInfo c a
fi  = (Either Error [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
normalize (Either Error [(Symbol, Sort)] -> Either Error [(Symbol, Sort)])
-> ([(Symbol, Sort)] -> Either Error [(Symbol, Sort)])
-> [(Symbol, Sort)]
-> Either Error [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
compact ([(Symbol, Sort)] -> Either Error [(Symbol, Sort)])
-> ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)]
-> Either Error [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Symbol, Sort)]
defs [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++)) ([(Symbol, Sort)] -> Either Error [(Symbol, Sort)])
-> Either Error [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GInfo c a -> Either Error [(Symbol, Sort)]
forall (c :: * -> *) a. GInfo c a -> Either Error [(Symbol, Sort)]
bindSorts GInfo c a
fi
  where
    normalize :: Either Error [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
normalize       = ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> Either Error [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
forall a b. (a -> b) -> Either Error a -> Either Error b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map ((Sort -> Sort)
-> HashMap Symbol Sort -> (Symbol, Sort) -> (Symbol, Sort)
forall a.
(Sort -> Sort)
-> HashMap Symbol a -> (Symbol, Sort) -> (Symbol, Sort)
unShadow Sort -> Sort
forall a. a -> a
txFun HashMap Symbol Sort
dm))
    dm :: HashMap Symbol Sort
dm              = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, Sort)]
defs
    defs :: [(Symbol, Sort)]
defs            = SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (GInfo c a -> SEnv Sort) -> GInfo c a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits (GInfo c a -> [(Symbol, Sort)]) -> GInfo c a -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ GInfo c a
fi
    txFun :: a -> a
txFun           = a -> a
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)
  | Symbol -> HashMap Symbol a -> Bool
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)] -> Either Error [(Symbol, Sort)]
compact [(Symbol, Sort)]
xts
  | [(Symbol, [Sort])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, [Sort])]
bad  = [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
forall a b. b -> Either a b
Right [(Symbol
x, Sort
t) | (Symbol
x, [Sort
t]) <- [(Symbol, [Sort])]
ok ]
  | Bool
otherwise = Error -> Either Error [(Symbol, Sort)]
forall a b. a -> Either a b
Left (Error -> Either Error [(Symbol, Sort)])
-> Error -> Either Error [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, [(Sort, [BindId])])] -> Error
dupBindErrors [(Symbol, [(Sort, [BindId])])]
forall {a}. [(Symbol, [(Sort, [a])])]
bad'
  where
    bad' :: [(Symbol, [(Sort, [a])])]
bad'      = [(Symbol
x, (, []) (Sort -> (Sort, [a])) -> [Sort] -> [(Sort, [a])]
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) = ((Symbol, [Sort]) -> Bool)
-> [(Symbol, [Sort])] -> ([(Symbol, [Sort])], [(Symbol, [Sort])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Symbol, [Sort]) -> Bool
forall x t. (x, [t]) -> Bool
multiSorted ([(Symbol, [Sort])] -> ([(Symbol, [Sort])], [(Symbol, [Sort])]))
-> ([(Symbol, Sort)] -> [(Symbol, [Sort])])
-> [(Symbol, Sort)]
-> ([(Symbol, [Sort])], [(Symbol, [Sort])])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> [(Symbol, [Sort])]
binds ([(Symbol, Sort)] -> ([(Symbol, [Sort])], [(Symbol, [Sort])]))
-> [(Symbol, Sort)] -> ([(Symbol, [Sort])], [(Symbol, [Sort])])
forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)]
xts
    binds :: [(Symbol, Sort)] -> [(Symbol, [Sort])]
binds     = HashMap Symbol [Sort] -> [(Symbol, [Sort])]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Symbol [Sort] -> [(Symbol, [Sort])])
-> ([(Symbol, Sort)] -> HashMap Symbol [Sort])
-> [(Symbol, Sort)]
-> [(Symbol, [Sort])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Sort] -> [Sort])
-> HashMap Symbol [Sort] -> HashMap Symbol [Sort]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map [Sort] -> [Sort]
forall k. Ord k => [k] -> [k]
Misc.sortNub (HashMap Symbol [Sort] -> HashMap Symbol [Sort])
-> ([(Symbol, Sort)] -> HashMap Symbol [Sort])
-> [(Symbol, Sort)]
-> HashMap Symbol [Sort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> HashMap Symbol [Sort]
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 -> Either Error [(Symbol, Sort)]
bindSorts GInfo c a
fi
  | [(Symbol, [(Sort, [BindId])])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, [(Sort, [BindId])])]
bad   = [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
forall a b. b -> Either a b
Right [ (Symbol
x, Sort
t) | (Symbol
x, [(Sort
t, [BindId]
_)]) <- [(Symbol, [(Sort, [BindId])])]
ok ]
  | Bool
otherwise  = Error -> Either Error [(Symbol, Sort)]
forall a b. a -> Either a b
Left (Error -> Either Error [(Symbol, Sort)])
-> Error -> Either Error [(Symbol, Sort)]
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)  = ((Symbol, [(Sort, [BindId])]) -> Bool)
-> [(Symbol, [(Sort, [BindId])])]
-> ([(Symbol, [(Sort, [BindId])])], [(Symbol, [(Sort, [BindId])])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Symbol, [(Sort, [BindId])]) -> Bool
forall x t. (x, [t]) -> Bool
multiSorted ([(Symbol, [(Sort, [BindId])])]
 -> ([(Symbol, [(Sort, [BindId])])],
     [(Symbol, [(Sort, [BindId])])]))
-> (GInfo c a -> [(Symbol, [(Sort, [BindId])])])
-> GInfo c a
-> ([(Symbol, [(Sort, [BindId])])], [(Symbol, [(Sort, [BindId])])])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> [(Symbol, [(Sort, [BindId])])]
forall {c :: * -> *} {a}.
GInfo c a -> [(Symbol, [(Sort, [BindId])])]
binds (GInfo c a
 -> ([(Symbol, [(Sort, [BindId])])],
     [(Symbol, [(Sort, [BindId])])]))
-> GInfo c a
-> ([(Symbol, [(Sort, [BindId])])], [(Symbol, [(Sort, [BindId])])])
forall a b. (a -> b) -> a -> b
$ GInfo c a
fi
    binds :: GInfo c a -> [(Symbol, [(Sort, [BindId])])]
binds      = BindEnv a -> [(Symbol, [(Sort, [BindId])])]
forall a. BindEnv a -> [(Symbol, [(Sort, [BindId])])]
symBinds (BindEnv a -> [(Symbol, [(Sort, [BindId])])])
-> (GInfo c a -> BindEnv a)
-> GInfo c a
-> [(Symbol, [(Sort, [BindId])])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs


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

dupBindErrors :: [(F.Symbol, [(F.Sort, [F.BindId] )])] -> E.Error
dupBindErrors :: [(Symbol, [(Sort, [BindId])])] -> Error
dupBindErrors = (Error -> Error -> Error) -> ListNE Error -> Error
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Error -> Error -> Error
E.catError (ListNE Error -> Error)
-> ([(Symbol, [(Sort, [BindId])])] -> ListNE Error)
-> [(Symbol, [(Sort, [BindId])])]
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, [(Sort, [BindId])]) -> Error)
-> [(Symbol, [(Sort, [BindId])])] -> ListNE Error
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [(Sort, [BindId])]) -> Error
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 (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ Doc
"Multiple sorts for" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x
                                         , BindId -> Doc -> Doc
nest BindId
4 (a -> Doc
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" . -}
            HashMap Symbol [(Sort, [BindId])] -> [(Symbol, [(Sort, [BindId])])]
forall k v. HashMap k v -> [(k, v)]
M.toList
          (HashMap Symbol [(Sort, [BindId])]
 -> [(Symbol, [(Sort, [BindId])])])
-> (BindEnv a -> HashMap Symbol [(Sort, [BindId])])
-> BindEnv a
-> [(Symbol, [(Sort, [BindId])])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Sort, BindId)] -> [(Sort, [BindId])])
-> HashMap Symbol [(Sort, BindId)]
-> HashMap Symbol [(Sort, [BindId])]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map [(Sort, BindId)] -> [(Sort, [BindId])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList
          (HashMap Symbol [(Sort, BindId)]
 -> HashMap Symbol [(Sort, [BindId])])
-> (BindEnv a -> HashMap Symbol [(Sort, BindId)])
-> BindEnv a
-> HashMap Symbol [(Sort, [BindId])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, (Sort, BindId))] -> HashMap Symbol [(Sort, BindId)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group
          ([(Symbol, (Sort, BindId))] -> HashMap Symbol [(Sort, BindId)])
-> (BindEnv a -> [(Symbol, (Sort, BindId))])
-> BindEnv a
-> HashMap Symbol [(Sort, BindId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindEnv a -> [(Symbol, (Sort, BindId))]
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
_)) <- BindEnv a -> [(BindId, (Symbol, SortedReft, 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 = KeepBindF -> KeepSortF -> SInfo a -> SInfo a
forall a. KeepBindF -> KeepSortF -> SInfo a -> SInfo a
dropBinders KeepBindF
ok (Bool -> KeepSortF
forall a b. a -> b -> a
const Bool
True) SInfo a
fi
  where
    ok :: KeepBindF
ok Symbol
x Sort
t  = Symbol -> HashMap Symbol Sort -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
x HashMap Symbol Sort
defs Bool -> Bool -> Bool
==> (SInfo a -> 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    = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, Sort)] -> HashMap Symbol Sort)
-> [(Symbol, Sort)] -> HashMap Symbol Sort
forall a b. (a -> b) -> a -> b
$ SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)]) -> SEnv Sort -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
fi

--------------------------------------------------------------------------------
-- | 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 { F.ws = ws' }
  where
    ws' :: HashMap KVar (WfC a)
ws'        = [BindId] -> WfC a -> WfC a
forall a. [BindId] -> WfC a -> WfC a
deleteWfCBinds [BindId]
drops (WfC a -> WfC a) -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si
    (BindEnv a
_,[BindId]
drops)  = KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
forall a. KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
filterBindEnv KeepBindF
keepF   (BindEnv a -> (BindEnv a, [BindId]))
-> BindEnv a -> (BindEnv a, [BindId])
forall a b. (a -> b) -> a -> b
$  SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si
    keepF :: KeepBindF
keepF      = [KeepBindF] -> KeepBindF
conjKF [SInfo a -> KeepBindF
forall a. SInfo a -> KeepBindF
nonConstantF SInfo a
si, SInfo a -> KeepBindF
forall a. SInfo a -> KeepBindF
nonFunctionF SInfo a
si, KeepBindF
_nonDerivedLH]

conjKF :: [KeepBindF] -> KeepBindF
conjKF :: [KeepBindF] -> KeepBindF
conjKF [KeepBindF]
fs Symbol
x Sort
t = [Bool] -> Bool
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 (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Bool
T.isPrefixOf Text
"$" (Text -> Bool) -> (Symbol -> Text) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
forall a. HasCallStack => [a] -> a
last ([Text] -> Text) -> (Symbol -> [Text]) -> Symbol -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Text -> [Text]
T.split (Char
'.' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==) (Text -> [Text]) -> (Symbol -> Text) -> Symbol -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
F.symbolText (Symbol -> Bool) -> Symbol -> Bool
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 Symbol -> SEnv Sort -> Bool
forall a. Symbol -> SEnv a -> Bool
`F.memberSEnv` SEnv Sort
cEnv)
  where
    cEnv :: SEnv Sort
cEnv        = SInfo a -> SEnv Sort
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
  | SInfo a -> Bool
forall (c :: * -> *) a. GInfo c a -> Bool
F.allowHO SInfo a
si    = \Symbol
_ Sort
_ -> Bool
True
  | Bool
otherwise       = \Symbol
_ Sort
t -> Maybe ([BindId], [Sort], Sort) -> Bool
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 { F.bs    = bs'
                         , F.cm    = cm'
                         , F.ws    = ws'
                         , F.gLits = lits' }
  where
    -- discards        = diss
    (BindEnv a
bs', [BindId]
discards) = KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
forall a. KeepBindF -> BindEnv a -> (BindEnv a, [BindId])
filterBindEnv KeepBindF
f (BindEnv a -> (BindEnv a, [BindId]))
-> BindEnv a -> (BindEnv a, [BindId])
forall a b. (a -> b) -> a -> b
$ SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi
    cm' :: HashMap SubcId (SimpC a)
cm'             = [BindId] -> SimpC a -> SimpC a
forall a. [BindId] -> SimpC a -> SimpC a
deleteSubCBinds [BindId]
discards   (SimpC a -> SimpC a)
-> HashMap SubcId (SimpC a) -> HashMap SubcId (SimpC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm SInfo a
fi
    ws' :: HashMap KVar (WfC a)
ws'             = [BindId] -> WfC a -> WfC a
forall a. [BindId] -> WfC a -> WfC a
deleteWfCBinds  [BindId]
discards   (WfC a -> WfC a) -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi
    lits' :: SEnv Sort
lits'           = KeepSortF -> SEnv Sort -> SEnv Sort
forall a. (a -> Bool) -> SEnv a -> SEnv a
F.filterSEnv KeepSortF
g (SInfo a -> SEnv Sort
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 { F._cenv = foldr F.deleteIBindEnv (F.senv sc) 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 { F.wenv = foldr F.deleteIBindEnv (F.wenv wf) 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     = [(BindId, (Symbol, SortedReft, a))] -> BindEnv a
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) = ((BindId, (Symbol, SortedReft, a)) -> Bool)
-> [(BindId, (Symbol, SortedReft, a))]
-> ([(BindId, (Symbol, SortedReft, a))],
    [(BindId, (Symbol, SortedReft, a))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (BindId, (Symbol, SortedReft, a)) -> Bool
forall {a} {c}. (a, (Symbol, SortedReft, c)) -> Bool
f' ([(BindId, (Symbol, SortedReft, a))]
 -> ([(BindId, (Symbol, SortedReft, a))],
     [(BindId, (Symbol, SortedReft, a))]))
-> [(BindId, (Symbol, SortedReft, a))]
-> ([(BindId, (Symbol, SortedReft, a))],
    [(BindId, (Symbol, SortedReft, a))])
forall a b. (a -> b) -> a -> b
$ BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
forall a. BindEnv a -> [(BindId, (Symbol, SortedReft, a))]
F.bindEnvToList BindEnv a
be
    discard' :: [BindId]
discard'        = (BindId, (Symbol, SortedReft, a)) -> BindId
forall a b. (a, b) -> a
fst ((BindId, (Symbol, SortedReft, a)) -> BindId)
-> [(BindId, (Symbol, SortedReft, a))] -> [BindId]
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 = (KVar -> Maybe (ExprV Symbol)) -> SInfo a -> SInfo a
forall t. Visitable t => (KVar -> Maybe (ExprV Symbol)) -> t -> t
mapKVars KVar -> Maybe (ExprV Symbol)
forall {v}. KVar -> Maybe (ExprV v)
go SInfo a
fi
  where
    go :: KVar -> Maybe (ExprV v)
go KVar
k | KVar
k KVar -> HashMap KVar (WfC a) -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`M.member` SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi = Maybe (ExprV v)
forall a. Maybe a
Nothing
         | Bool
otherwise            = ExprV v -> Maybe (ExprV v)
forall a. a -> Maybe a
Just ExprV v
forall v. ExprV v
F.PFalse