-- | 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     (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, allowHO)
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 :: Config -> SInfo a -> SanitizeM (SInfo a)
sanitize Config
cfg =    -- banIllScopedKvars
        --      Misc.fM dropAdtMeasures
        --      >=>
             (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
>=>         SInfo a -> SanitizeM (SInfo a)
forall a. SInfo a -> SanitizeM (SInfo a)
banConstraintFreeVars
         (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)
         (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
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 :: SInfo a -> SInfo a
_dropAdtMeasures SInfo a
si = SInfo a
si { ae :: AxiomEnv
F.ae = [DataDecl] -> AxiomEnv -> AxiomEnv
dropAdtAenv (SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls SInfo a
si) (SInfo a -> AxiomEnv
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 = (Rewrite -> Bool) -> [Rewrite] -> [Rewrite]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Rewrite -> Bool) -> Rewrite -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> Bool
isAdt) (AxiomEnv -> [Rewrite]
F.aenvSimpl AxiomEnv
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 = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> ([DataDecl] -> [Symbol]) -> [DataDecl] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, TheorySymbol) -> Symbol)
-> [(Symbol, TheorySymbol)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, TheorySymbol) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, TheorySymbol)] -> [Symbol])
-> ([DataDecl] -> [(Symbol, TheorySymbol)])
-> [DataDecl]
-> [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 :: SInfo a -> SInfo a
addLiterals SInfo a
si = SInfo a
si { dLits :: SEnv Sort
F.dLits = SEnv Sort -> HashMap Symbol Sort -> SEnv Sort
forall a. SEnv a -> HashMap Symbol a -> SEnv a
F.unionSEnv (SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.dLits SInfo a
si) HashMap Symbol Sort
lits'
                    , gLits :: SEnv Sort
F.gLits = SEnv Sort -> HashMap Symbol Sort -> SEnv Sort
forall a. SEnv a -> HashMap Symbol a -> SEnv a
F.unionSEnv (SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits SInfo a
si) HashMap Symbol Sort
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 ]



cancelCoercion :: F.SInfo a -> F.SInfo a
cancelCoercion :: SInfo a -> SInfo a
cancelCoercion = (Expr -> Expr) -> SInfo a -> SInfo a
forall t. Visitable t => (Expr -> Expr) -> t -> t
mapExpr (Visitor () () -> () -> () -> Expr -> Expr
forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans (Visitor () ()
forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr :: () -> Expr -> Expr
txExpr = () -> Expr -> Expr
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 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t1' Bool -> Bool -> Bool
&& Sort
t2 Sort -> Sort -> Bool
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 :: 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 (Equation -> Equation) -> [Equation] -> [Equation]
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 = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
F.ae SInfo a
si
    eqs :: [Equation]
eqs = (Equation -> Equation) -> [Equation] -> [Equation]
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 = String -> Equation -> Equation
forall a. PPrint a => String -> a -> a
F.notracepp String
"Eliminating" (Equation -> Equation) -> Equation -> Equation
forall a b. (a -> b) -> a -> b
$
                 case Expr
body of
                   F.PAtom Brel
F.Eq Expr
e0 Expr
e1 ->
                     let (Expr
f0, [Symbol]
args0) = Expr -> (Expr, [Symbol])
fapp Expr
e0
                         (Expr
f1, [Symbol]
args1) = String -> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. PPrint a => String -> a -> a
F.notracepp String
"f1" ((Expr, [Symbol]) -> (Expr, [Symbol]))
-> (Expr, [Symbol]) -> (Expr, [Symbol])
forall a b. (a -> b) -> a -> b
$ Expr -> (Expr, [Symbol])
fapp Expr
e1 in
                     if [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
args0 [Symbol] -> [Symbol] -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol]
args
                     then let commonArgs :: [Symbol]
commonArgs = String -> [Symbol] -> [Symbol]
forall a. PPrint a => String -> a -> a
F.notracepp String
"commonArgs" ([Symbol] -> [Symbol])
-> ([(Symbol, Symbol)] -> [Symbol])
-> [(Symbol, Symbol)]
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                           ((Symbol, Symbol) -> Symbol) -> [(Symbol, Symbol)] -> [Symbol]
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)] -> [Symbol])
-> ([(Symbol, Symbol)] -> [(Symbol, Symbol)])
-> [(Symbol, Symbol)]
-> [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)] -> [Symbol]) -> [(Symbol, Symbol)] -> [Symbol]
forall a b. (a -> b) -> a -> b
$
                                           [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
args0 [Symbol]
args1
                              commonLength :: Int
commonLength = [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
commonArgs
                              ([(Symbol, Sort)]
newArgsAndSorts, [(Symbol, Sort)]
elimedArgsAndSorts) =
                                Int -> [(Symbol, Sort)] -> ([(Symbol, Sort)], [(Symbol, Sort)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
commonLength) [(Symbol, Sort)]
argsAndSorts
                              args0' :: [Expr]
args0' = Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse (Int -> [Symbol] -> [Symbol]
forall a. Int -> [a] -> [a]
drop Int
commonLength [Symbol]
args0)
                              args1' :: [Expr]
args1' = Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse (Int -> [Symbol] -> [Symbol]
forall a. Int -> [a] -> [a]
drop Int
commonLength [Symbol]
args1) in
                       Equation
eq { eqArgs :: [(Symbol, Sort)]
F.eqArgs = [(Symbol, Sort)]
newArgsAndSorts
                          , eqSort :: Sort
F.eqSort = (Sort -> Sort -> Sort) -> Sort -> [Sort] -> Sort
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sort -> Sort -> Sort
F.FFunc Sort
sort
                                       ((Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd ((Symbol, Sort) -> Sort) -> [(Symbol, Sort)] -> [Sort]
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 :: [Symbol]
args = (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
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 = String -> Equation -> Equation
forall a. PPrint a => String -> a -> a
F.notracepp String
"Eliminating" (Equation -> Equation) -> Equation -> Equation
forall a b. (a -> b) -> a -> b
$
                  let (Expr
f1, [Symbol]
args1) = Expr -> (Expr, [Symbol])
fapp (Equation -> Expr
F.eqBody Equation
eq) in
                  let commonArgs :: [Symbol]
commonArgs = String -> [Symbol] -> [Symbol]
forall a. PPrint a => String -> a -> a
F.notracepp String
"commonArgs" ([Symbol] -> [Symbol])
-> ([(Symbol, Symbol)] -> [Symbol])
-> [(Symbol, Symbol)]
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                           ((Symbol, Symbol) -> Symbol) -> [(Symbol, Symbol)] -> [Symbol]
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)] -> [Symbol])
-> ([(Symbol, Symbol)] -> [(Symbol, Symbol)])
-> [(Symbol, Symbol)]
-> [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)] -> [Symbol]) -> [(Symbol, Symbol)] -> [Symbol]
forall a b. (a -> b) -> a -> b
$
                                           [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
args0 [Symbol]
args1
                      commonLength :: Int
commonLength = [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
commonArgs
                      ([(Symbol, Sort)]
newArgsAndSorts, [(Symbol, Sort)]
elimedArgsAndSorts) =
                                Int -> [(Symbol, Sort)] -> ([(Symbol, Sort)], [(Symbol, Sort)])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
args Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
commonLength) [(Symbol, Sort)]
argsAndSorts
                      args1' :: [Expr]
args1' = Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse (Int -> [Symbol] -> [Symbol]
forall a. Int -> [a] -> [a]
drop Int
commonLength [Symbol]
args1) in
                  Equation
eq { eqArgs :: [(Symbol, Sort)]
F.eqArgs = [(Symbol, Sort)]
newArgsAndSorts
                     , eqSort :: Sort
F.eqSort = (Sort -> Sort -> Sort) -> Sort -> [Sort] -> Sort
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sort -> Sort -> Sort
F.FFunc Sort
sort
                                       ((Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd ((Symbol, Sort) -> Sort) -> [(Symbol, Sort)] -> [Sort]
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 :: [Symbol]
args  = (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
argsAndSorts
            args0 :: [Symbol]
args0 = [Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
args 
            sort :: Sort
sort  = Equation -> Sort
F.eqSort Equation
eq
            
    fapp :: F.Expr -> (F.Expr, [F.Symbol])
    fapp :: Expr -> (Expr, [Symbol])
fapp Expr
ee = (Expr, [Symbol]) -> Maybe (Expr, [Symbol]) -> (Expr, [Symbol])
forall a. a -> Maybe a -> a
fromMaybe (Expr
ee, []) (Expr -> Maybe (Expr, [Symbol])
fapp' Expr
ee)
    
    fapp' :: F.Expr -> Maybe (F.Expr, [F.Symbol])
    fapp' :: Expr -> Maybe (Expr, [Symbol])
fapp' (F.EApp Expr
e0 (F.EVar Symbol
arg)) = do
      (Expr
fvar, [Symbol]
args) <- Expr -> Maybe (Expr, [Symbol])
fapp' Expr
e0
      (Expr, [Symbol]) -> Maybe (Expr, [Symbol])
forall b. (Expr, b) -> Maybe (Expr, b)
splitApp (Expr
fvar, Symbol
argSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
args)
    fapp' Expr
e = (Expr, [Symbol]) -> Maybe (Expr, [Symbol])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
e, [])

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

    splitApp :: (Expr, b) -> Maybe (Expr, b)
splitApp (Expr
e, b
es)
      | Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Int -> Bool) -> Maybe Int -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Maybe Int -> Maybe Int
forall a. PPrint a => String -> a -> a
F.notracepp (String
"isSmt2App? " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e) (Maybe Int -> Maybe Int) -> Maybe Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ SEnv TheorySymbol -> Expr -> Maybe Int
Thy.isSmt2App SEnv TheorySymbol
theorySymbols (Expr -> Maybe Int) -> Expr -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall t. Visitable t => t -> t
stripCasts Expr
e
      = (Expr, b) -> Maybe (Expr, b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
e,b
es)
      | Bool
otherwise
      = Maybe (Expr, b)
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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 :: 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 -> Expr -> Bool) -> Subst -> Subst
F.filterSubst ((Symbol -> Expr -> Bool) -> Subst -> Subst)
-> (KVar -> Symbol -> Expr -> Bool) -> KVar -> Subst -> Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Symbol -> Expr -> 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         = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> (KVar -> [Symbol]) -> KVar -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> KVar -> [Symbol]
forall a. SInfo a -> KVar -> [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 :: SInfo a -> SInfo a
restrictKVarDomain SInfo a
si = SInfo a
si { ws :: HashMap KVar (WfC a)
F.ws = (KVar -> WfC a -> WfC a)
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (KvDom -> KVar -> WfC a -> WfC a
forall a. KvDom -> KVar -> WfC a -> WfC a
restrictWf KvDom
kvm) (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
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 :: KvDom -> KVar -> WfC a -> WfC a
restrictWf KvDom
kve KVar
k WfC a
w = WfC a
w { wenv :: IBindEnv
F.wenv = (Int -> Bool) -> IBindEnv -> IBindEnv
F.filterIBindEnv Int -> Bool
f (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv WfC a
w) }
  where
    f :: Int -> Bool
f Int
i            = Int -> HashSet Int -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Int
i HashSet Int
kis
    kis :: HashSet Int
kis            = [Int] -> HashSet Int
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Int
i | (Symbol
_, Int
i) <- SEnv Int -> [(Symbol, Int)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Int
kEnv ]
    kEnv :: SEnv Int
kEnv           = SEnv Int -> KVar -> KvDom -> SEnv Int
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault SEnv Int
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 :: SInfo a -> KvDom
safeKvarEnv SInfo a
si = (KvDom -> SimpC a -> KvDom) -> KvDom -> [SimpC a] -> KvDom
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 :: SInfo a -> KvDom -> SimpC a -> KvDom
dropKvarEnv SInfo a
si KvDom
kve SimpC a
c = (KVar -> SEnv Int -> SEnv Int) -> KvDom -> KvDom
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (KvBads -> KVar -> SEnv Int -> SEnv Int
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 Int -> SEnv Int
dropBadParams KvBads
kBads KVar
k SEnv Int
kEnv = (SEnv Int -> Symbol -> SEnv Int)
-> SEnv Int -> [Symbol] -> SEnv Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ((Symbol -> SEnv Int -> SEnv Int) -> SEnv Int -> Symbol -> SEnv Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip Symbol -> SEnv Int -> SEnv Int
forall a. Symbol -> SEnv a -> SEnv a
F.deleteSEnv) SEnv Int
kEnv [Symbol]
xs
  where
    xs :: [Symbol]
xs                     = [Symbol] -> KVar -> KvBads -> [Symbol]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [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 :: 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 Expr
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, Expr
e)          <- HashMap Symbol Expr -> [(Symbol, Expr)]
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       = [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)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
xsrs)
    xsrs :: [(Symbol, SortedReft)]
xsrs       = BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
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 -> Expr -> 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
_    Expr
_          = Bool
True

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

subcKSubs :: [(F.Symbol, F.SortedReft)] -> F.SimpC a -> [KSub]
subcKSubs :: [(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 -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC a
c]]


initKvarEnv :: F.SInfo a -> KvDom
initKvarEnv :: SInfo a -> KvDom
initKvarEnv SInfo a
si = SInfo a -> WfC a -> SEnv Int
forall a. SInfo a -> WfC a -> SEnv Int
initEnv SInfo a
si (WfC a -> SEnv Int) -> 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 :: SInfo a -> WfC a -> SEnv Int
initEnv SInfo a
si WfC a
w = [(Symbol, Int)] -> SEnv Int
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [ (Int -> Symbol
bind Int
i, Int
i) | Int
i <- [Int]
is ]
  where
    is :: [Int]
is       = IBindEnv -> [Int]
F.elemsIBindEnv (IBindEnv -> [Int]) -> IBindEnv -> [Int]
forall a b. (a -> b) -> a -> b
$ WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv WfC a
w
    bind :: Int -> Symbol
bind Int
i   = (Symbol, SortedReft) -> Symbol
forall a b. (a, b) -> a
fst (Int -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv Int
i BindEnv
be)
    be :: BindEnv
be       = SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
si

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

known :: F.SInfo a -> F.Symbol -> Bool
known :: SInfo a -> Symbol -> Bool
known 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 = [DataDecl] -> SEnv TheorySymbol
Thy.theorySymbols ([DataDecl] -> SEnv TheorySymbol)
-> (SInfo a -> [DataDecl]) -> SInfo a -> SEnv TheorySymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
F.ddecls (SInfo a -> SEnv TheorySymbol) -> SInfo a -> SEnv TheorySymbol
forall a b. (a -> b) -> a -> b
$ SInfo a
fi

cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol]
cNoFreeVars :: SInfo a -> (Symbol -> Bool) -> SimpC a -> Maybe [Symbol]
cNoFreeVars SInfo a
fi Symbol -> Bool
known SimpC a
c = if HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null HashSet Symbol
fv then Maybe [Symbol]
forall a. Maybe a
Nothing else [Symbol] -> Maybe [Symbol]
forall a. a -> Maybe a
Just (HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
fv)
  where
    be :: BindEnv
be   = SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
fi
    ids :: [Int]
ids  = IBindEnv -> [Int]
F.elemsIBindEnv (IBindEnv -> [Int]) -> IBindEnv -> [Int]
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 :: [Symbol]
cDom = [(Symbol, SortedReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SortedReft) -> Symbol) -> (Symbol, SortedReft) -> Symbol
forall a b. (a -> b) -> a -> b
$ Int -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv Int
i BindEnv
be | Int
i <- [Int]
ids]
    cRng :: [Symbol]
cRng = [[Symbol]] -> [Symbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> [Symbol])
-> ((Symbol, SortedReft) -> HashSet Symbol)
-> (Symbol, SortedReft)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> HashSet Symbol
F.reftFreeVars (Reft -> HashSet Symbol)
-> ((Symbol, SortedReft) -> Reft)
-> (Symbol, SortedReft)
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
F.sr_reft (SortedReft -> Reft)
-> ((Symbol, SortedReft) -> SortedReft)
-> (Symbol, SortedReft)
-> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd ((Symbol, SortedReft) -> [Symbol])
-> (Symbol, SortedReft) -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Int -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv Int
i BindEnv
be | Int
i <- [Int]
ids]
    fv :: HashSet Symbol
fv   = ([Symbol] -> [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> [a] -> HashSet a
`Misc.nubDiff` [Symbol]
cDom) ([Symbol] -> HashSet Symbol)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Bool) -> [Symbol] -> [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
known) ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol]
cRng 

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


--------------------------------------------------------------------------------
-- | check that no qualifier has free variables
--------------------------------------------------------------------------------
banQualifFreeVars :: F.SInfo a -> SanitizeM (F.SInfo a)
--------------------------------------------------------------------------------
banQualifFreeVars :: SInfo a -> SanitizeM (SInfo a)
banQualifFreeVars SInfo a
fi = SanitizeM (SInfo a)
-> ([(Qualifier, [Symbol])] -> SanitizeM (SInfo a))
-> [(Qualifier, [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, [Symbol])] -> Error)
-> [(Qualifier, [Symbol])]
-> SanitizeM (SInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Qualifier, [Symbol])] -> Error
badQuals) [(Qualifier, [Symbol])]
bads
  where
    bads :: [(Qualifier, [Symbol])]
bads    = [ (Qualifier
q, [Symbol]
xs) | Qualifier
q <- SInfo a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
fi, let xs :: [Symbol]
xs = Qualifier -> [Symbol]
forall a. Subable a => a -> [Symbol]
free Qualifier
q, Bool -> Bool
not ([Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol]
xs) ]
    free :: a -> [Symbol]
free a
q  = (Symbol -> Bool) -> [Symbol] -> [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 -> [Symbol]
forall a. Subable a => a -> [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, [Symbol])] -> Error
badQuals [(Qualifier, [Symbol])]
bqs = ListNE Error -> Error
E.catErrors [ Qualifier -> [Symbol] -> Error
forall q x. (PPrint q, Loc q, PPrint x) => q -> x -> Error
E.errFreeVarInQual Qualifier
q [Symbol]
xs | (Qualifier
q, [Symbol]
xs) <- [(Qualifier, [Symbol])]
bqs]


--------------------------------------------------------------------------------
-- | check that each constraint has RHS of form [k1,...,kn] or [p]
--------------------------------------------------------------------------------
banMixedRhs :: F.SInfo a -> SanitizeM (F.SInfo a)
--------------------------------------------------------------------------------
banMixedRhs :: 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 :: 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 :: (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
                                          , Int -> Doc -> Doc
nest Int
4 (Expr -> Doc
forall a. PPrint a => a -> Doc
pprint (SimpC a -> Expr
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 :: 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 (SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.dLits SInfo a
si) ([Sort]
ts [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort]
ts')
  where
    ts' :: [Sort]
ts'          = AxiomEnv -> [Sort]
forall t. Visitable t => t -> [Sort]
applySorts AxiomEnv
ae' 
    ae' :: AxiomEnv
ae'          = Located String -> SymEnv -> AxiomEnv -> AxiomEnv
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (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
tEnv [DataDecl]
ds (SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.dLits SInfo a
si) [Sort]
ts
    tEnv :: SEnv TheorySymbol
tEnv         = [DataDecl] -> SEnv TheorySymbol
Thy.theorySymbols [DataDecl]
ds
    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. (Eq k, Hashable k) => [k] -> [k]
Misc.hashNub (SInfo a -> [Sort]
forall t. Visitable 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         = (TheorySymbol -> Sort
F.tsSort (TheorySymbol -> Sort) -> SEnv TheorySymbol -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEnv TheorySymbol
tEnv) 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)
    xts :: [(Symbol, Sort)]
xts          = Config -> SInfo a -> [(Symbol, Sort)]
forall (c :: * -> *) a. Config -> GInfo c a -> [(Symbol, Sort)]
symbolSorts Config
cfg SInfo a
si


symbolSorts :: Config -> F.GInfo c a -> [(F.Symbol, F.Sort)]
symbolSorts :: 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' :: 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 (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
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 :: Sort -> Sort
txFun           
      | Bool
True        = Sort -> Sort
forall a. a -> a
id
      | Config -> Bool
allowHO Config
cfg = Sort -> Sort
forall a. a -> a
id
      | Bool
otherwise   = Sort -> Sort
defuncSort

unShadow :: (F.Sort -> F.Sort) -> M.HashMap F.Symbol a -> (F.Symbol, F.Sort) -> (F.Symbol, F.Sort)
unShadow :: (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 (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, [Int])])] -> Error
dupBindErrors [(Symbol, [(Sort, [Int])])]
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 a. Ord a => [a] -> [a]
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 :: GInfo c a -> Either Error [(Symbol, Sort)]
bindSorts GInfo c a
fi
  | [(Symbol, [(Sort, [Int])])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, [(Sort, [Int])])]
bad   = [(Symbol, Sort)] -> Either Error [(Symbol, Sort)]
forall a b. b -> Either a b
Right [ (Symbol
x, Sort
t) | (Symbol
x, [(Sort
t, [Int]
_)]) <- [(Symbol, [(Sort, [Int])])]
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, [Int])])] -> Error
dupBindErrors [ (Symbol
x, [(Sort, [Int])]
ts) | (Symbol
x, [(Sort, [Int])]
ts) <- [(Symbol, [(Sort, [Int])])]
bad]
  where
    ([(Symbol, [(Sort, [Int])])]
bad, [(Symbol, [(Sort, [Int])])]
ok)  = ((Symbol, [(Sort, [Int])]) -> Bool)
-> [(Symbol, [(Sort, [Int])])]
-> ([(Symbol, [(Sort, [Int])])], [(Symbol, [(Sort, [Int])])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Symbol, [(Sort, [Int])]) -> Bool
forall x t. (x, [t]) -> Bool
multiSorted ([(Symbol, [(Sort, [Int])])]
 -> ([(Symbol, [(Sort, [Int])])], [(Symbol, [(Sort, [Int])])]))
-> (GInfo c a -> [(Symbol, [(Sort, [Int])])])
-> GInfo c a
-> ([(Symbol, [(Sort, [Int])])], [(Symbol, [(Sort, [Int])])])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> [(Symbol, [(Sort, [Int])])]
forall (c :: * -> *) a. GInfo c a -> [(Symbol, [(Sort, [Int])])]
binds (GInfo c a
 -> ([(Symbol, [(Sort, [Int])])], [(Symbol, [(Sort, [Int])])]))
-> GInfo c a
-> ([(Symbol, [(Sort, [Int])])], [(Symbol, [(Sort, [Int])])])
forall a b. (a -> b) -> a -> b
$ GInfo c a
fi
    binds :: GInfo c a -> [(Symbol, [(Sort, [Int])])]
binds      = BindEnv -> [(Symbol, [(Sort, [Int])])]
symBinds (BindEnv -> [(Symbol, [(Sort, [Int])])])
-> (GInfo c a -> BindEnv)
-> GInfo c a
-> [(Symbol, [(Sort, [Int])])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs


multiSorted :: (x, [t]) -> Bool
multiSorted :: (x, [t]) -> Bool
multiSorted = (Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<) (Int -> Bool) -> ((x, [t]) -> Int) -> (x, [t]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [t] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([t] -> Int) -> ((x, [t]) -> [t]) -> (x, [t]) -> Int
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, [Int])])] -> Error
dupBindErrors = (Error -> Error -> Error) -> ListNE Error -> Error
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Error -> Error -> Error
E.catError (ListNE Error -> Error)
-> ([(Symbol, [(Sort, [Int])])] -> ListNE Error)
-> [(Symbol, [(Sort, [Int])])]
-> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, [(Sort, [Int])]) -> Error)
-> [(Symbol, [(Sort, [Int])])] -> ListNE Error
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, [(Sort, [Int])]) -> 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
                                         , Int -> Doc -> Doc
nest Int
4 (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
y) ]

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

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

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


--------------------------------------------------------------------------------
-- | Drop func-sorted `bind` that are shadowed by `constant` (if same type, else error)
--------------------------------------------------------------------------------
dropFuncSortedShadowedBinders :: F.SInfo a -> F.SInfo a
--------------------------------------------------------------------------------
dropFuncSortedShadowedBinders :: SInfo a -> SInfo a
dropFuncSortedShadowedBinders SInfo a
fi = KeepBindF -> (Sort -> Bool) -> SInfo a -> SInfo a
forall a. KeepBindF -> (Sort -> Bool) -> SInfo a -> SInfo a
dropBinders KeepBindF
ok (Bool -> Sort -> Bool
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
|| Sort -> Bool
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

(==>) :: 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 :: 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'        = [Int] -> WfC a -> WfC a
forall a. [Int] -> WfC a -> WfC a
deleteWfCBinds [Int]
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
_,[Int]
drops)  = KeepBindF -> BindEnv -> (BindEnv, [Int])
filterBindEnv KeepBindF
keepF   (BindEnv -> (BindEnv, [Int])) -> BindEnv -> (BindEnv, [Int])
forall a b. (a -> b) -> a -> b
$  SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
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]
    -- drops   = F.tracepp "sanitizeWfC: dropping" $ L.sort drops'

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. [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 :: 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 :: 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 ([Int], [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isNothing (Sort -> Maybe ([Int], [Sort], Sort)
F.functionSort Sort
t)

--------------------------------------------------------------------------------
-- | Generic API for Deleting Binders from FInfo
--------------------------------------------------------------------------------
dropBinders :: KeepBindF -> KeepSortF -> F.SInfo a -> F.SInfo a
--------------------------------------------------------------------------------
dropBinders :: KeepBindF -> (Sort -> Bool) -> SInfo a -> SInfo a
dropBinders KeepBindF
f Sort -> Bool
g SInfo a
fi  = SInfo a
fi { bs :: BindEnv
F.bs    = BindEnv
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
bs', [Int]
discards) = KeepBindF -> BindEnv -> (BindEnv, [Int])
filterBindEnv KeepBindF
f (BindEnv -> (BindEnv, [Int])) -> BindEnv -> (BindEnv, [Int])
forall a b. (a -> b) -> a -> b
$ SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
fi
    cm' :: HashMap SubcId (SimpC a)
cm'             = [Int] -> SimpC a -> SimpC a
forall a. [Int] -> SimpC a -> SimpC a
deleteSubCBinds [Int]
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'             = [Int] -> WfC a -> WfC a
forall a. [Int] -> WfC a -> WfC a
deleteWfCBinds  [Int]
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'           = (Sort -> Bool) -> SEnv Sort -> SEnv Sort
forall a. (a -> Bool) -> SEnv a -> SEnv a
F.filterSEnv Sort -> Bool
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 :: [Int] -> SimpC a -> SimpC a
deleteSubCBinds [Int]
bs SimpC a
sc = SimpC a
sc { _cenv :: IBindEnv
F._cenv = (Int -> IBindEnv -> IBindEnv) -> IBindEnv -> [Int] -> IBindEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Int -> IBindEnv -> IBindEnv
F.deleteIBindEnv (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
sc) [Int]
bs }

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

filterBindEnv :: KeepBindF -> F.BindEnv -> (F.BindEnv, [F.BindId])
filterBindEnv :: KeepBindF -> BindEnv -> (BindEnv, [Int])
filterBindEnv KeepBindF
f BindEnv
be  = ([(Int, Symbol, SortedReft)] -> BindEnv
F.bindEnvFromList [(Int, Symbol, SortedReft)]
keep, [Int]
discard')
  where
    ([(Int, Symbol, SortedReft)]
keep, [(Int, Symbol, SortedReft)]
discard) = ((Int, Symbol, SortedReft) -> Bool)
-> [(Int, Symbol, SortedReft)]
-> ([(Int, Symbol, SortedReft)], [(Int, Symbol, SortedReft)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Int, Symbol, SortedReft) -> Bool
forall a. (a, Symbol, SortedReft) -> Bool
f' ([(Int, Symbol, SortedReft)]
 -> ([(Int, Symbol, SortedReft)], [(Int, Symbol, SortedReft)]))
-> [(Int, Symbol, SortedReft)]
-> ([(Int, Symbol, SortedReft)], [(Int, Symbol, SortedReft)])
forall a b. (a -> b) -> a -> b
$ BindEnv -> [(Int, Symbol, SortedReft)]
F.bindEnvToList BindEnv
be
    discard' :: [Int]
discard'        = (Int, Symbol, SortedReft) -> Int
forall a b c. (a, b, c) -> a
Misc.fst3     ((Int, Symbol, SortedReft) -> Int)
-> [(Int, Symbol, SortedReft)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, Symbol, SortedReft)]
discard
    f' :: (a, Symbol, SortedReft) -> Bool
f' (a
_, Symbol
x, SortedReft
t)    = 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 :: SInfo a -> SInfo a
replaceDeadKvars SInfo a
fi = (KVar -> Maybe Expr) -> SInfo a -> SInfo a
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 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 Expr
forall a. Maybe a
Nothing
         | Bool
otherwise            = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
F.PFalse