{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE PatternGuards     #-}

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

    -- * Update Solution
  , Sol.update

  -- * Lookup Solution
  , lhsPred

  , nonCutsResult
  ) where

import           Control.Parallel.Strategies
import           Control.Arrow (second, (***))
import qualified Data.HashSet                   as S
import qualified Data.HashMap.Strict            as M
import qualified Data.List                      as L
import           Data.Maybe                     (fromMaybe, maybeToList, isNothing)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup                 (Semigroup (..))
#endif

import           Language.Fixpoint.Types.PrettyPrint ()
import           Language.Fixpoint.Types.Visitor      as V
import qualified Language.Fixpoint.SortCheck          as So
import qualified Language.Fixpoint.Misc               as Misc
import           Language.Fixpoint.Types.Config
import qualified Language.Fixpoint.Types              as F
import           Language.Fixpoint.Types                 ((&.&))
import qualified Language.Fixpoint.Types.Solutions    as Sol
import           Language.Fixpoint.Types.Constraints  hiding (ws, bs)
import           Prelude                              hiding (init, lookup)
import           Language.Fixpoint.Solver.Sanitize

-- DEBUG
import Text.Printf (printf)
-- import Debug.Trace (trace)


--------------------------------------------------------------------------------
-- | Initial Solution (from Qualifiers and WF constraints) ---------------------
--------------------------------------------------------------------------------
init :: (F.Fixpoint a) => Config -> F.SInfo a -> S.HashSet F.KVar -> Sol.Solution
--------------------------------------------------------------------------------
init :: Config -> SInfo a -> HashSet KVar -> Solution
init Config
cfg SInfo a
si HashSet KVar
ks_ = SymEnv
-> [(KVar, ())]
-> [(KVar, QBind)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(BindId, EbindSol)]
-> SEnv (BindId, Sort)
-> Solution
forall a b.
SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(BindId, EbindSol)]
-> SEnv (BindId, Sort)
-> Sol a b
Sol.fromList SymEnv
senv [(KVar, ())]
forall a. Monoid a => a
mempty [(KVar, QBind)]
keqs [] HashMap KVar IBindEnv
forall a. Monoid a => a
mempty [(BindId, EbindSol)]
ebs SEnv (BindId, Sort)
xEnv
  where
    keqs :: [(KVar, QBind)]
keqs       = (WfC a -> (KVar, QBind)) -> [WfC a] -> [(KVar, QBind)]
forall a b. (a -> b) -> [a] -> [b]
map (SInfo a -> QCluster -> SEnv Sort -> WfC a -> (KVar, QBind)
forall a.
SInfo a -> QCluster -> SEnv Sort -> WfC a -> (KVar, QBind)
refine SInfo a
si QCluster
qcs SEnv Sort
genv) [WfC a]
ws [(KVar, QBind)] -> Strategy [(KVar, QBind)] -> [(KVar, QBind)]
forall a. a -> Strategy a -> a
`using` Strategy (KVar, QBind) -> Strategy [(KVar, QBind)]
forall a. Strategy a -> Strategy [a]
parList Strategy (KVar, QBind)
forall a. NFData a => Strategy a
rdeepseq
    qcs :: QCluster
qcs        = {- trace ("init-qs-size " ++ show (length ws, length qs_, M.keys qcs_)) $ -} QCluster
qcs_ 
    qcs_ :: QCluster
qcs_       = [Qualifier] -> QCluster
mkQCluster [Qualifier]
qs_
    qs_ :: [Qualifier]
qs_        = SInfo a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
si
    ws :: [WfC a]
ws         = [ WfC a
w | (KVar
k, WfC a
w) <- HashMap KVar (WfC a) -> [(KVar, WfC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si), Bool -> Bool
not (WfC a -> Bool
forall a. WfC a -> Bool
isGWfc WfC a
w), KVar
k KVar -> HashSet KVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet KVar
ks ]
    ks :: HashSet KVar
ks         = {- trace ("init-ks-size" ++ show (S.size ks_)) $ -} HashSet KVar
ks_
    genv :: SEnv Sort
genv       = SInfo a -> SEnv Sort
forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si
    senv :: SymEnv
senv       = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si
    ebs :: [(BindId, EbindSol)]
ebs        = SInfo a -> [(BindId, EbindSol)]
forall a. SInfo a -> [(BindId, EbindSol)]
ebindInfo SInfo a
si
    xEnv :: SEnv (BindId, Sort)
xEnv       = [(Symbol, (BindId, Sort))] -> SEnv (BindId, Sort)
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [ (Symbol
x, (BindId
i, SortedReft -> Sort
F.sr_sort SortedReft
sr)) | (BindId
i,Symbol
x,SortedReft
sr) <- BindEnv -> [(BindId, Symbol, SortedReft)]
F.bindEnvToList (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
si)]

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

type QCluster = M.HashMap QCSig [Qualifier]

type QCSig = [F.QualParam]

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

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

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

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

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


refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)
refineK :: Bool
-> SEnv Sort -> QCluster -> (Symbol, Sort, KVar) -> (KVar, QBind)
refineK Bool
ho SEnv Sort
env QCluster
qs (Symbol
v, Sort
t, KVar
k) = String -> (KVar, QBind) -> (KVar, QBind)
forall a. PPrint a => String -> a -> a
F.notracepp String
_msg (KVar
k, QBind
eqs')
   where
    eqs :: QBind
eqs                     = Bool -> SEnv Sort -> Symbol -> Sort -> QCluster -> QBind
instK Bool
ho SEnv Sort
env Symbol
v Sort
t QCluster
qs
    eqs' :: QBind
eqs'                    = (EQual -> Bool) -> QBind -> QBind
Sol.qbFilter (SEnv Sort -> Symbol -> Sort -> EQual -> Bool
okInst SEnv Sort
env Symbol
v Sort
t) QBind
eqs
    _msg :: String
_msg                    = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"\n\nrefineK: k = %s, eqs = %s" (KVar -> String
forall a. PPrint a => a -> String
F.showpp KVar
k) (QBind -> String
forall a. PPrint a => a -> String
F.showpp QBind
eqs)

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

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

instKSig :: Bool
         -> F.SEnv F.Sort
         -> F.Symbol
         -> F.Sort
         -> QCSig 
         -> [[F.Symbol]]
instKSig :: Bool -> SEnv Sort -> Symbol -> Sort -> QCSig -> [[Symbol]]
instKSig Bool
ho SEnv Sort
env Symbol
v Sort
t QCSig
qsig = do 
  (TVSubst
su0, BindId
i0, QualPattern
qs0) <- Env
-> [(BindId, Sort, [Symbol])]
-> QualParam
-> [(TVSubst, BindId, QualPattern)]
forall a.
Env
-> [(BindId, Sort, a)]
-> QualParam
-> [(TVSubst, BindId, QualPattern)]
candidatesP Env
senv [(BindId
0, Sort
t, [Symbol
v])] QualParam
qp
  [(BindId, QualPattern)]
ixs       <- Env
-> [(BindId, Sort, [Symbol])]
-> [(BindId, QualPattern)]
-> QCSig
-> [[(BindId, QualPattern)]]
forall a.
Env
-> [(BindId, Sort, a)]
-> [(BindId, QualPattern)]
-> QCSig
-> [[(BindId, QualPattern)]]
matchP Env
senv [(BindId, Sort, [Symbol])]
tyss [(BindId
i0, QualPattern
qs0)] (TVSubst -> QualParam -> QualParam
applyQPP TVSubst
su0 (QualParam -> QualParam) -> QCSig -> QCSig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QCSig
qps) 
  -- return     $ F.notracepp msg (reverse ixs)
  [Symbol]
ys        <- [(BindId, Sort, [Symbol])] -> [(BindId, QualPattern)] -> [[Symbol]]
forall a.
[(BindId, a, [Symbol])] -> [(BindId, QualPattern)] -> [[Symbol]]
instSymbol [(BindId, Sort, [Symbol])]
tyss ([(BindId, QualPattern)] -> [(BindId, QualPattern)]
forall a. [a] -> [a]
tail ([(BindId, QualPattern)] -> [(BindId, QualPattern)])
-> [(BindId, QualPattern)] -> [(BindId, QualPattern)]
forall a b. (a -> b) -> a -> b
$ [(BindId, QualPattern)] -> [(BindId, QualPattern)]
forall a. [a] -> [a]
reverse [(BindId, QualPattern)]
ixs) 
  [Symbol] -> [[Symbol]]
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
vSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys)
  where
    -- msg        = "instKSig " ++ F.showpp qsig
    QualParam
qp : QCSig
qps   = QCSig
qsig
    tyss :: [(BindId, Sort, [Symbol])]
tyss       = (BindId -> (Sort, [Symbol]) -> (BindId, Sort, [Symbol]))
-> [BindId] -> [(Sort, [Symbol])] -> [(BindId, Sort, [Symbol])]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\BindId
i (Sort
t, [Symbol]
ys) -> (BindId
i, Sort
t, [Symbol]
ys)) [BindId
1..] (Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env)
    senv :: Env
senv       = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`F.lookupSEnvWithDistance` SEnv Sort
env)

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

-- instKQ :: Bool
--        -> F.SEnv F.Sort
--        -> F.Symbol
--        -> F.Sort
--        -> F.Qualifier
--        -> [Sol.EQual]
-- instKQ ho env v t q = do 
--   (su0, qsu0, v0) <- candidates senv [(t, [v])] qp
--   xs              <- match senv tyss [v0] (applyQP su0 qsu0 <$> qps) 
--   return           $ Sol.eQual q (F.notracepp msg (reverse xs))
--   where
--     msg        = "instKQ " ++ F.showpp (F.qName q) ++ F.showpp (F.qParams q)
--     qp : qps   = F.qParams q
--     tyss       = instCands ho env
--     senv       = (`F.lookupSEnvWithDistance` env)

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


type SortIdx = Int

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

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

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

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

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


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

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

data QPSubst = NoSub | JustSub Int F.Symbol  

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

--------------------------------------------------------------------------------
okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
--------------------------------------------------------------------------------
okInst :: SEnv Sort -> Symbol -> Sort -> EQual -> Bool
okInst SEnv Sort
env Symbol
v Sort
t EQual
eq = Maybe Doc -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Doc
tc
  where
    sr :: SortedReft
sr            = Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr
p))
    p :: Expr
p             = EQual -> Expr
Sol.eqPred EQual
eq
    tc :: Maybe Doc
tc            = SrcSpan -> SEnv Sort -> SortedReft -> Maybe Doc
forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
So.checkSorted (EQual -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan EQual
eq) SEnv Sort
env SortedReft
sr 
    -- _msg          = printf "okInst: t = %s, eq = %s, env = %s" (F.showpp t) (F.showpp eq) (F.showpp env)


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

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

instance F.Loc CombinedEnv where 
  srcSpan :: CombinedEnv -> SrcSpan
srcSpan = CombinedEnv -> SrcSpan
ceSpan

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

apply :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ExprInfo
apply :: CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
apply CombinedEnv
g Sol a QBind
s IBindEnv
bs      = ([Expr] -> Expr
F.conj (Expr
pksExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
ps), KInfo
kI)   -- see [NOTE: pAnd-SLOW]
  where
    -- Clear the "known" bindings for applyKVars, since it depends on
    -- using the fully expanded representation of the predicates to bind their
    -- variables with quantifiers.
    (Expr
pks, KInfo
kI)     = CombinedEnv -> Sol a QBind -> [KVSub] -> (Expr, KInfo)
forall a. CombinedEnv -> Sol a QBind -> [KVSub] -> (Expr, KInfo)
applyKVars CombinedEnv
g {ceBindingsInSmt :: IBindEnv
ceBindingsInSmt = IBindEnv
F.emptyIBindEnv} Sol a QBind
s [KVSub]
ks
    ([Expr]
ps,  [KVSub]
ks, [KVSub]
_)  = CombinedEnv
-> Sol a QBind -> IBindEnv -> ([Expr], [KVSub], [KVSub])
forall a.
CombinedEnv
-> Sol a QBind -> IBindEnv -> ([Expr], [KVSub], [KVSub])
envConcKVars CombinedEnv
g Sol a QBind
s IBindEnv
bs


envConcKVars :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ([F.Expr], [F.KVSub], [F.KVSub])
envConcKVars :: CombinedEnv
-> Sol a QBind -> IBindEnv -> ([Expr], [KVSub], [KVSub])
envConcKVars CombinedEnv
g Sol a QBind
s IBindEnv
bs = ([[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Expr]]
pss, [[KVSub]] -> [KVSub]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[KVSub]]
kss, (KVSub -> KVSub -> Bool) -> [KVSub] -> [KVSub]
forall a. (a -> a -> Bool) -> [a] -> [a]
L.nubBy (\KVSub
x KVSub
y -> KVSub -> KVar
F.ksuKVar KVSub
x KVar -> KVar -> Bool
forall a. Eq a => a -> a -> Bool
== KVSub -> KVar
F.ksuKVar KVSub
y) ([KVSub] -> [KVSub]) -> [KVSub] -> [KVSub]
forall a b. (a -> b) -> a -> b
$ [[KVSub]] -> [KVSub]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[KVSub]]
gss)
  where
    ([[Expr]]
pss, [[KVSub]]
kss, [[KVSub]]
gss) = [([Expr], [KVSub], [KVSub])] -> ([[Expr]], [[KVSub]], [[KVSub]])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [ String -> ([Expr], [KVSub], [KVSub]) -> ([Expr], [KVSub], [KVSub])
forall a. PPrint a => String -> a -> a
F.notracepp (String
"sortedReftConcKVars" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SortedReft -> String
forall a. PPrint a => a -> String
F.showpp SortedReft
sr) (([Expr], [KVSub], [KVSub]) -> ([Expr], [KVSub], [KVSub]))
-> ([Expr], [KVSub], [KVSub]) -> ([Expr], [KVSub], [KVSub])
forall a b. (a -> b) -> a -> b
$ Symbol -> SortedReft -> ([Expr], [KVSub], [KVSub])
F.sortedReftConcKVars Symbol
x SortedReft
sr | (Symbol
x, SortedReft
sr) <- [(Symbol, SortedReft)]
xrs ]
    xrs :: [(Symbol, SortedReft)]
xrs             = CombinedEnv -> Sol a QBind -> BindId -> (Symbol, SortedReft)
forall a.
CombinedEnv -> Sol a QBind -> BindId -> (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv
g Sol a QBind
s (BindId -> (Symbol, SortedReft))
-> [BindId] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BindId]
is
    is :: [BindId]
is              = IBindEnv -> [BindId]
F.elemsIBindEnv IBindEnv
bs

lookupBindEnvExt :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.BindId -> (F.Symbol, F.SortedReft)
lookupBindEnvExt :: CombinedEnv -> Sol a QBind -> BindId -> (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv
g Sol a QBind
s BindId
i
  | Just Expr
p <- CombinedEnv -> Sol a QBind -> BindId -> Maybe Expr
forall a. CombinedEnv -> Sol a QBind -> BindId -> Maybe Expr
ebSol CombinedEnv
g {ceBindingsInSmt :: IBindEnv
ceBindingsInSmt = IBindEnv
F.emptyIBindEnv} Sol a QBind
s BindId
i = (Symbol
x, SortedReft
sr { sr_reft :: Reft
F.sr_reft = (Symbol, Expr) -> Reft
F.Reft (Symbol
x, Expr
p) })
  | BindId -> IBindEnv -> Bool
F.memberIBindEnv BindId
i (CombinedEnv -> IBindEnv
ceBindingsInSmt CombinedEnv
g) =
      (Symbol
x, SortedReft
sr { sr_reft :: Reft
F.sr_reft = (Symbol, Expr) -> Reft
F.Reft (Symbol
x, Symbol -> Expr
F.EVar (Integer -> Symbol
F.bindSymbol (BindId -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral BindId
i)))})
  | Bool
otherwise             = (Symbol
x, SortedReft
sr)
   where 
      (Symbol
x, SortedReft
sr)              = BindId -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv BindId
i (CombinedEnv -> BindEnv
ceBEnv CombinedEnv
g) 

ebSol :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.BindId -> Maybe F.Expr
ebSol :: CombinedEnv -> Sol a QBind -> BindId -> Maybe Expr
ebSol CombinedEnv
g Sol a QBind
s BindId
i = case  BindId -> HashMap BindId EbindSol -> Maybe EbindSol
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup BindId
i HashMap BindId EbindSol
sebds of
  Just (Sol.EbSol Expr
p)    -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
p
  Just (Sol.EbDef [SimpC ()]
cs Symbol
_) -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
F.PAnd (SimpC () -> Expr
cSol (SimpC () -> Expr) -> [SimpC ()] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SimpC ()]
cs)
  Maybe EbindSol
_                     -> Maybe Expr
forall a. Maybe a
Nothing
  where
    sebds :: HashMap BindId EbindSol
sebds = Sol a QBind -> HashMap BindId EbindSol
forall b a. Sol b a -> HashMap BindId EbindSol
Sol.sEbd Sol a QBind
s

    ebReft :: Sol a QBind -> (BindId, SimpC ()) -> Expr
ebReft Sol a QBind
s (BindId
i,SimpC ()
c) = SEnv (BindId, Sort) -> IBindEnv -> BindId -> Expr -> Expr
exElim (Sol a QBind -> SEnv (BindId, Sort)
forall b a. Sol b a -> SEnv (BindId, Sort)
Sol.sxEnv Sol a QBind
s) (SimpC () -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC ()
c) BindId
i (CombinedEnv -> Sol a QBind -> SimpC () -> Expr
forall a. CombinedEnv -> Sol a QBind -> SimpC () -> Expr
ebindReft CombinedEnv
g Sol a QBind
s SimpC ()
c)
    cSol :: SimpC () -> Expr
cSol SimpC ()
c = if SimpC () -> Cid
forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC ()
c Cid -> Cid -> Bool
forall a. Eq a => a -> a -> Bool
== CombinedEnv -> Cid
ceCid CombinedEnv
g 
                then Expr
F.PFalse
                else Sol a QBind -> (BindId, SimpC ()) -> Expr
forall a. Sol a QBind -> (BindId, SimpC ()) -> Expr
ebReft Sol a QBind
s' (BindId
i, SimpC ()
c)

    s' :: Sol a QBind
s' = Sol a QBind
s { sEbd :: HashMap BindId EbindSol
Sol.sEbd = BindId
-> EbindSol -> HashMap BindId EbindSol -> HashMap BindId EbindSol
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert BindId
i EbindSol
Sol.EbIncr HashMap BindId EbindSol
sebds }

ebindReft :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.SimpC () -> F.Pred
ebindReft :: CombinedEnv -> Sol a QBind -> SimpC () -> Expr
ebindReft CombinedEnv
g Sol a QBind
s SimpC ()
c = [Expr] -> Expr
F.pAnd [ (Expr, KInfo) -> Expr
forall a b. (a, b) -> a
fst ((Expr, KInfo) -> Expr) -> (Expr, KInfo) -> Expr
forall a b. (a -> b) -> a -> b
$ CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
forall a. CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
apply CombinedEnv
g' Sol a QBind
s IBindEnv
bs, SimpC () -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC ()
c ]
  where
    g' :: CombinedEnv
g'          = CombinedEnv
g { ceCid :: Cid
ceCid = SimpC () -> Cid
forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC ()
c, ceIEnv :: IBindEnv
ceIEnv = IBindEnv
bs } 
    bs :: IBindEnv
bs          = SimpC () -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC ()
c

exElim :: F.SEnv (F.BindId, F.Sort) -> F.IBindEnv -> F.BindId -> F.Pred -> F.Pred
exElim :: SEnv (BindId, Sort) -> IBindEnv -> BindId -> Expr -> Expr
exElim SEnv (BindId, Sort)
env IBindEnv
ienv BindId
xi Expr
p = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
F.notracepp String
msg ([(Symbol, Sort)] -> Expr -> Expr
F.pExist [(Symbol, Sort)]
yts Expr
p)
  where
    msg :: String
msg         = String
"exElim" -- printf "exElim: ix = %d, p = %s" xi (F.showpp p)
    yts :: [(Symbol, Sort)]
yts         = [ (Symbol
y, Sort
yt) | Symbol
y        <- Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms Expr
p
                            , (BindId
yi, Sort
yt) <- Maybe (BindId, Sort) -> [(BindId, Sort)]
forall a. Maybe a -> [a]
maybeToList (Symbol -> SEnv (BindId, Sort) -> Maybe (BindId, Sort)
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
y SEnv (BindId, Sort)
env)
                            , BindId
xi BindId -> BindId -> Bool
forall a. Ord a => a -> a -> Bool
< BindId
yi
                            , BindId
yi BindId -> IBindEnv -> Bool
`F.memberIBindEnv` IBindEnv
ienv                  ]

applyKVars :: CombinedEnv -> Sol.Sol a Sol.QBind -> [F.KVSub] -> ExprInfo
applyKVars :: CombinedEnv -> Sol a QBind -> [KVSub] -> (Expr, KInfo)
applyKVars CombinedEnv
g Sol a QBind
s = (KVSub -> (Expr, KInfo))
-> ([Expr] -> Expr)
-> ([KInfo] -> KInfo)
-> [KVSub]
-> (Expr, KInfo)
forall a b c b1 c1.
(a -> (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> (b1, c1)
mrExprInfos (CombinedEnv -> Sol a QBind -> KVSub -> (Expr, KInfo)
forall a. CombinedEnv -> Sol a QBind -> KVSub -> (Expr, KInfo)
applyKVar CombinedEnv
g Sol a QBind
s) [Expr] -> Expr
F.pAndNoDedup [KInfo] -> KInfo
forall a. Monoid a => [a] -> a
mconcat

applyKVar :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVSub -> ExprInfo
applyKVar :: CombinedEnv -> Sol a QBind -> KVSub -> (Expr, KInfo)
applyKVar CombinedEnv
g Sol a QBind
s KVSub
ksu = case Sol a QBind -> KVar -> Either Hyp QBind
forall a. Sol a QBind -> KVar -> Either Hyp QBind
Sol.lookup Sol a QBind
s (KVSub -> KVar
F.ksuKVar KVSub
ksu) of
  Left Hyp
cs   -> CombinedEnv -> Sol a QBind -> KVSub -> Hyp -> (Expr, KInfo)
forall a.
CombinedEnv -> Sol a QBind -> KVSub -> Hyp -> (Expr, KInfo)
hypPred CombinedEnv
g Sol a QBind
s KVSub
ksu Hyp
cs
  Right QBind
eqs -> ([Expr] -> Expr
F.pAndNoDedup ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr, EQual) -> Expr
forall a b. (a, b) -> a
fst ((Expr, EQual) -> Expr) -> [(Expr, EQual)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Sol a QBind -> Subst -> QBind -> [(Expr, EQual)]
forall a.
String -> Sol a QBind -> Subst -> QBind -> [(Expr, EQual)]
Sol.qbPreds String
msg Sol a QBind
s (KVSub -> Subst
F.ksuSubst KVSub
ksu) QBind
eqs, KInfo
forall a. Monoid a => a
mempty) -- TODO: don't initialize kvars that have a hyp solution
  where
    msg :: String
msg     = String
"applyKVar: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Cid -> String
forall a. Show a => a -> String
show (CombinedEnv -> Cid
ceCid CombinedEnv
g)

nonCutsResult :: F.BindEnv -> Sol.Sol a Sol.QBind -> M.HashMap F.KVar F.Expr
nonCutsResult :: BindEnv -> Sol a QBind -> HashMap KVar Expr
nonCutsResult BindEnv
be Sol a QBind
s =
  let g :: CombinedEnv
g = Cid -> BindEnv -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv
CEnv Cid
forall a. Maybe a
Nothing BindEnv
be IBindEnv
F.emptyIBindEnv SrcSpan
F.dummySpan IBindEnv
F.emptyIBindEnv
   in (KVar -> Hyp -> Expr) -> HashMap KVar Hyp -> HashMap KVar Expr
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (CombinedEnv -> KVar -> Hyp -> Expr
mkNonCutsExpr CombinedEnv
g) (HashMap KVar Hyp -> HashMap KVar Expr)
-> HashMap KVar Hyp -> HashMap KVar Expr
forall a b. (a -> b) -> a -> b
$ Sol a QBind -> HashMap KVar Hyp
forall b a. Sol b a -> HashMap KVar Hyp
Sol.sHyp Sol a QBind
s
  where
    mkNonCutsExpr :: CombinedEnv -> KVar -> Hyp -> Expr
mkNonCutsExpr CombinedEnv
g KVar
k Hyp
cs = [Expr] -> Expr
F.pOr ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (Cube -> Expr) -> Hyp -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (CombinedEnv -> Sol a QBind -> KVar -> Cube -> Expr
forall a. CombinedEnv -> Sol a QBind -> KVar -> Cube -> Expr
bareCubePred CombinedEnv
g Sol a QBind
s KVar
k) Hyp
cs

-- | Produces a predicate from a constraint defining a kvar.
--
-- This is written in imitation of 'cubePred'. However, there are some
-- differences since the result of 'cubePred' is fed to the verification
-- pipeline and @bareCubePred@ is meant for human inspection.
--
-- 1) Only one existential quantifier is introduced at the top of the
--    expression.
-- 2) @bareCubePred@ doesn't elaborate the expression, so it avoids calling
--    'elabExist'. 'apply' is invoked to eliminate other kvars though, and
--    apply will invoke 'elabExist', so 'Liquid.Fixpoint.SortCheck.unElab'
--    might need to be called on the output to remove the elaboration.
-- 3) The expression is created from its defining constraints only, while
--    @cubePred@ does expect the caller to supply the substitution at a
--    particular use of the KVar. Thus @cubePred@ produces a different
--    expression for every use site of the kvar, while here we produce one
--    expression for all the uses.
bareCubePred :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Cube -> F.Expr
bareCubePred :: CombinedEnv -> Sol a QBind -> KVar -> Cube -> Expr
bareCubePred CombinedEnv
g Sol a QBind
s KVar
k Cube
c =
  let bs :: IBindEnv
bs = Cube -> IBindEnv
Sol.cuBinds Cube
c
      su :: Subst
su = Cube -> Subst
Sol.cuSubst Cube
c
      g' :: CombinedEnv
g' = CombinedEnv -> IBindEnv -> CombinedEnv
addCEnv  CombinedEnv
g IBindEnv
bs
      bs' :: IBindEnv
bs' = Sol a QBind -> KVar -> IBindEnv -> IBindEnv
forall a. Sol a QBind -> KVar -> IBindEnv -> IBindEnv
delCEnv Sol a QBind
s KVar
k IBindEnv
bs
      yts :: [(Symbol, Sort)]
yts = CombinedEnv -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv
g IBindEnv
bs'
      sEnv :: SEnv Sort
sEnv = SymEnv -> SEnv Sort
F.seSort (Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s)
      ([(Symbol, Sort)]
xts, Expr
psu) = SymEnv
-> SEnv Sort
-> CombinedEnv
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim (Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s) SEnv Sort
sEnv CombinedEnv
g' KVar
k Subst
su
      (Expr
p, KInfo
_kI) = CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
forall a. CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
apply CombinedEnv
g' Sol a QBind
s IBindEnv
bs'
   in [(Symbol, Sort)] -> Expr -> Expr
F.pExist ([(Symbol, Sort)]
xts [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
yts) (Expr
psu Expr -> Expr -> Expr
&.& Expr
p)

hypPred :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp  -> ExprInfo
hypPred :: CombinedEnv -> Sol a QBind -> KVSub -> Hyp -> (Expr, KInfo)
hypPred CombinedEnv
g Sol a QBind
s KVSub
ksu Hyp
hyp = [Expr] -> Expr
F.pOr ([Expr] -> Expr)
-> ([KInfo] -> KInfo) -> ([Expr], [KInfo]) -> (Expr, KInfo)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [KInfo] -> KInfo
mconcatPlus (([Expr], [KInfo]) -> (Expr, KInfo))
-> ([Expr], [KInfo]) -> (Expr, KInfo)
forall a b. (a -> b) -> a -> b
$ [(Expr, KInfo)] -> ([Expr], [KInfo])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Expr, KInfo)] -> ([Expr], [KInfo]))
-> [(Expr, KInfo)] -> ([Expr], [KInfo])
forall a b. (a -> b) -> a -> b
$ CombinedEnv -> Sol a QBind -> KVSub -> Cube -> (Expr, KInfo)
forall a.
CombinedEnv -> Sol a QBind -> KVSub -> Cube -> (Expr, KInfo)
cubePred CombinedEnv
g Sol a QBind
s KVSub
ksu (Cube -> (Expr, KInfo)) -> Hyp -> [(Expr, KInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Hyp
hyp

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

        (k . su)

      defined by using cube

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

      in the binder environment `g`.

        bs' := the subset of "extra" binders in [b1...bn] that are *not* in `g`
        p'  := the predicate corresponding to the "extra" binders

 -}

elabExist :: F.SrcSpan -> Sol.Sol a Sol.QBind -> [(F.Symbol, F.Sort)] -> F.Expr -> F.Expr
elabExist :: SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> Expr
elabExist SrcSpan
sp Sol a QBind
s [(Symbol, Sort)]
xts Expr
p = [(Symbol, Sort)] -> Expr -> Expr
F.pExist [(Symbol, Sort)]
xts' Expr
p
  where
    xts' :: [(Symbol, Sort)]
xts'        = [ (Symbol
x, Sort -> Sort
elab Sort
t) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts]
    elab :: Sort -> Sort
elab        = Located String -> SymEnv -> Sort -> Sort
forall a. Elaborate a => Located String -> SymEnv -> a -> a
So.elaborate (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
sp String
"elabExist") SymEnv
env
    env :: SymEnv
env         = Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s

cubePred :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> ExprInfo
cubePred :: CombinedEnv -> Sol a QBind -> KVSub -> Cube -> (Expr, KInfo)
cubePred CombinedEnv
g Sol a QBind
s KVSub
ksu Cube
c    = (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
F.notracepp String
"cubePred" (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> Expr
forall a.
SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> Expr
elabExist SrcSpan
sp Sol a QBind
s [(Symbol, Sort)]
xts (Expr
psu Expr -> Expr -> Expr
&.& Expr
p), KInfo
kI)
  where
    sp :: SrcSpan
sp                = CombinedEnv -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv
g
    (([(Symbol, Sort)]
xts,Expr
psu,Expr
p), KInfo
kI) = CombinedEnv
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> (([(Symbol, Sort)], Expr, Expr), KInfo)
forall a.
CombinedEnv
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> (([(Symbol, Sort)], Expr, Expr), KInfo)
cubePredExc CombinedEnv
g Sol a QBind
s KVSub
ksu Cube
c IBindEnv
bs'
    bs' :: IBindEnv
bs'               = Sol a QBind -> KVar -> IBindEnv -> IBindEnv
forall a. Sol a QBind -> KVar -> IBindEnv -> IBindEnv
delCEnv Sol a QBind
s KVar
k IBindEnv
bs
    bs :: IBindEnv
bs                = Cube -> IBindEnv
Sol.cuBinds Cube
c
    k :: KVar
k                 = KVSub -> KVar
F.ksuKVar KVSub
ksu

type Binders = [(F.Symbol, F.Sort)]

-- | @cubePredExc@ computes the predicate for the subset of binders bs'.
--   The output is a tuple, `(xts, psu, p, kI)` such that the actual predicate
--   we want is `Exists xts. (psu /\ p)`.

cubePredExc :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> F.IBindEnv
            -> ((Binders, F.Pred, F.Pred), KInfo)

cubePredExc :: CombinedEnv
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> (([(Symbol, Sort)], Expr, Expr), KInfo)
cubePredExc CombinedEnv
g Sol a QBind
s KVSub
ksu Cube
c IBindEnv
bs' = (([(Symbol, Sort)], Expr, Expr)
cubeP, KInfo -> [BindId] -> KInfo
extendKInfo KInfo
kI (Cube -> [BindId]
Sol.cuTag Cube
c))
  where
    cubeP :: ([(Symbol, Sort)], Expr, Expr)
cubeP           = ([(Symbol, Sort)]
xts, Expr
psu, SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> Expr
forall a.
SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> Expr
elabExist SrcSpan
sp Sol a QBind
s [(Symbol, Sort)]
yts' ([Expr] -> Expr
F.pAndNoDedup [Expr
p', Expr
psu']) )
    sp :: SrcSpan
sp              = CombinedEnv -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv
g
    yts' :: [(Symbol, Sort)]
yts'            = CombinedEnv -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv
g IBindEnv
bs'
    g' :: CombinedEnv
g'              = CombinedEnv -> IBindEnv -> CombinedEnv
addCEnv  CombinedEnv
g IBindEnv
bs
    (Expr
p', KInfo
kI)        = CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
forall a. CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
apply CombinedEnv
g' Sol a QBind
s IBindEnv
bs'
    ([(Symbol, Sort)]
_  , Expr
psu')     = SymEnv
-> SEnv Sort
-> CombinedEnv
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim (Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s) SEnv Sort
sEnv CombinedEnv
g' KVar
k Subst
su'
    ([(Symbol, Sort)]
xts, Expr
psu)      = SymEnv
-> SEnv Sort
-> CombinedEnv
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim (Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s) SEnv Sort
sEnv CombinedEnv
g  KVar
k Subst
su
    su' :: Subst
su'             = Cube -> Subst
Sol.cuSubst Cube
c
    bs :: IBindEnv
bs              = Cube -> IBindEnv
Sol.cuBinds Cube
c
    k :: KVar
k               = KVSub -> KVar
F.ksuKVar   KVSub
ksu
    su :: Subst
su              = KVSub -> Subst
F.ksuSubst  KVSub
ksu
    sEnv :: SEnv Sort
sEnv            = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv (KVSub -> Symbol
F.ksuVV KVSub
ksu) (KVSub -> Sort
F.ksuSort KVSub
ksu) (SymEnv -> SEnv Sort
F.seSort (SymEnv -> SEnv Sort) -> SymEnv -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s)

-- TODO: SUPER SLOW! Decorate all substitutions with Sorts in a SINGLE pass.

{- | @substElim@ returns the binders that must be existentially quantified,
     and the equality predicate relating the kvar-"parameters" and their
     actual values. i.e. given

        K[x1 := e1]...[xn := en]

     where e1 ... en have types t1 ... tn
     we want to quantify out

       x1:t1 ... xn:tn

     and generate the equality predicate && [x1 ~~ e1, ... , xn ~~ en]
     we use ~~ because the param and value may have different sorts, see:

        tests/pos/kvar-param-poly-00.hs

     Finally, we filter out binders if they are

     1. "free" in e1...en i.e. in the outer environment.
        (Hmm, that shouldn't happen...?)

     2. are binders corresponding to sorts (e.g. `a : num`, currently used
        to hack typeclasses current.)
 -}
substElim :: F.SymEnv -> F.SEnv F.Sort -> CombinedEnv -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)
substElim :: SymEnv
-> SEnv Sort
-> CombinedEnv
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim SymEnv
syEnv SEnv Sort
sEnv CombinedEnv
g KVar
_ (F.Su HashMap Symbol Expr
m) = ([(Symbol, Sort)]
xts, Expr
p)
  where
    p :: Expr
p      = [Expr] -> Expr
F.pAnd [ SrcSpan -> SymEnv -> Symbol -> Sort -> Expr -> Sort -> Expr
mkSubst SrcSpan
sp SymEnv
syEnv Symbol
x (SEnv Sort -> HashSet Symbol -> Symbol -> Sort -> Sort
substSort SEnv Sort
sEnv HashSet Symbol
frees Symbol
x Sort
t) Expr
e Sort
t | (Symbol
x, Expr
e, Sort
t) <- [(Symbol, Expr, Sort)]
xets  ]
    xts :: [(Symbol, Sort)]
xts    = [ (Symbol
x, Sort
t)    | (Symbol
x, Expr
_, Sort
t) <- [(Symbol, Expr, Sort)]
xets, Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
frees) ]
    xets :: [(Symbol, Expr, Sort)]
xets   = [ (Symbol
x, Expr
e, Sort
t) | (Symbol
x, Expr
e)    <- [(Symbol, Expr)]
xes, Sort
t <- Expr -> [Sort]
sortOf Expr
e, Bool -> Bool
not (Sort -> Bool
isClass Sort
t)]
    xes :: [(Symbol, Expr)]
xes    = HashMap Symbol Expr -> [(Symbol, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol Expr
m
    env :: SEnv Sort
env    = CombinedEnv -> SEnv Sort
combinedSEnv CombinedEnv
g
    frees :: HashSet Symbol
frees  = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (((Symbol, Expr) -> [Symbol]) -> [(Symbol, Expr)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms (Expr -> [Symbol])
-> ((Symbol, Expr) -> Expr) -> (Symbol, Expr) -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Expr) -> Expr
forall a b. (a, b) -> b
snd) [(Symbol, Expr)]
xes)
    sortOf :: Expr -> [Sort]
sortOf = Maybe Sort -> [Sort]
forall a. Maybe a -> [a]
maybeToList (Maybe Sort -> [Sort]) -> (Expr -> Maybe Sort) -> Expr -> [Sort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> SEnv Sort -> Expr -> Maybe Sort
So.checkSortExpr SrcSpan
sp SEnv Sort
env
    sp :: SrcSpan
sp     = CombinedEnv -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv
g

substSort :: F.SEnv F.Sort -> S.HashSet F.Symbol -> F.Symbol -> F.Sort -> F.Sort
substSort :: SEnv Sort -> HashSet Symbol -> Symbol -> Sort -> Sort
substSort SEnv Sort
sEnv HashSet Symbol
_frees Symbol
x Sort
_t = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Symbol -> Sort
forall a a. PPrint a => a -> a
err Symbol
x) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
x SEnv Sort
sEnv
  where
    err :: a -> a
err a
x            = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Solution.mkSubst: unknown binder " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. PPrint a => a -> String
F.showpp a
x


-- LH #1091
mkSubst :: F.SrcSpan -> F.SymEnv -> F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr
mkSubst :: SrcSpan -> SymEnv -> Symbol -> Sort -> Expr -> Sort -> Expr
mkSubst SrcSpan
sp SymEnv
env Symbol
x Sort
tx Expr
ey Sort
ty
  | Sort
tx Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
ty    = Expr -> Expr -> Expr
F.EEq Expr
ex Expr
ey
  | Bool
otherwise   = {- F.tracepp _msg -} (Expr -> Expr -> Expr
F.EEq Expr
ex' Expr
ey')
  where
    _msg :: String
_msg         = String
"mkSubst-DIFF:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Sort, Sort) -> String
forall a. PPrint a => a -> String
F.showpp (Sort
tx, Sort
ty) String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> String
forall a. PPrint a => a -> String
F.showpp (Expr
ex', Expr
ey')
    ex :: Expr
ex          = Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
x
    ex' :: Expr
ex'         = SrcSpan -> SymEnv -> Expr -> Sort -> Expr
elabToInt SrcSpan
sp SymEnv
env Expr
ex Sort
tx
    ey' :: Expr
ey'         = SrcSpan -> SymEnv -> Expr -> Sort -> Expr
elabToInt SrcSpan
sp SymEnv
env Expr
ey Sort
ty

elabToInt :: F.SrcSpan -> F.SymEnv -> F.Expr -> F.Sort -> F.Expr
elabToInt :: SrcSpan -> SymEnv -> Expr -> Sort -> Expr
elabToInt SrcSpan
sp SymEnv
env Expr
e Sort
s = Located String -> SymEnv -> Expr -> Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
So.elaborate (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
sp String
"elabToInt") SymEnv
env (SymEnv -> Expr -> Sort -> Expr
So.toInt SymEnv
env Expr
e Sort
s)

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

--badExpr :: CombinedEnv -> F.KVar -> F.Expr -> a
--badExpr g@(i,_,_) k e
  -- = errorstar $ "substSorts has a badExpr: "
              -- ++ show e
              -- ++ " in cid = "
              -- ++ show i
              -- ++ " for kvar " ++ show k
              -- ++ " in env \n"
              -- ++ show (combinedSEnv g)

-- substPred :: F.Subst -> F.Pred
-- substPred (F.Su m) = F.pAnd [ F.PAtom F.Eq (F.eVar x) e | (x, e) <- M.toList m]

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

addCEnv :: CombinedEnv -> F.IBindEnv -> CombinedEnv
addCEnv :: CombinedEnv -> IBindEnv -> CombinedEnv
addCEnv CombinedEnv
g IBindEnv
bs' = CombinedEnv
g { ceIEnv :: IBindEnv
ceIEnv = IBindEnv -> IBindEnv -> IBindEnv
F.unionIBindEnv (CombinedEnv -> IBindEnv
ceIEnv CombinedEnv
g) IBindEnv
bs' }
-- addCEnv (x, be, bs) bs' = (x, be, F.unionIBindEnv bs bs')


delCEnv :: Sol.Sol a Sol.QBind -> F.KVar -> F.IBindEnv -> F.IBindEnv
delCEnv :: Sol a QBind -> KVar -> IBindEnv -> IBindEnv
delCEnv Sol a QBind
s KVar
k IBindEnv
bs = IBindEnv -> IBindEnv -> IBindEnv
F.diffIBindEnv IBindEnv
bs IBindEnv
_kbs
  where
    _kbs :: IBindEnv
_kbs       = String -> KVar -> HashMap KVar IBindEnv -> IBindEnv
forall k v.
(HasCallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
Misc.safeLookup String
"delCEnv" KVar
k (Sol a QBind -> HashMap KVar IBindEnv
forall b a. Sol b a -> HashMap KVar IBindEnv
Sol.sScp Sol a QBind
s)

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

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

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

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

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

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

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

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

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

-- mrExprInfos :: (a -> ExprInfo) -> ([F.Expr] -> F.Expr) -> ([KInfo] -> KInfo) -> [a] -> ExprInfo
mrExprInfos :: (a -> (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> (b1, c1)
mrExprInfos :: (a -> (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> (b1, c1)
mrExprInfos a -> (b, c)
mF [b] -> b1
erF [c] -> c1
irF [a]
xs = ([b] -> b1
erF [b]
es, [c] -> c1
irF [c]
is)
  where
    ([b]
es, [c]
is)              = [(b, c)] -> ([b], [c])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(b, c)] -> ([b], [c])) -> [(b, c)] -> ([b], [c])
forall a b. (a -> b) -> a -> b
$ (a -> (b, c)) -> [a] -> [(b, c)]
forall a b. (a -> b) -> [a] -> [b]
map a -> (b, c)
mF [a]
xs

--------------------------------------------------------------------------------
-- | `ebindInfo` constructs the information about the "ebind-definitions". 
--------------------------------------------------------------------------------
ebindInfo :: F.SInfo a -> [(F.BindId, Sol.EbindSol)]
ebindInfo :: SInfo a -> [(BindId, EbindSol)]
ebindInfo SInfo a
si = [((BindId, Symbol), SimpC ())] -> [(BindId, EbindSol)]
forall a. Eq a => [((a, Symbol), SimpC ())] -> [(a, EbindSol)]
group [((BindId
bid, Symbol
x), Integer -> SimpC ()
cons Integer
cid) | (BindId
bid, Integer
cid, Symbol
x) <- SInfo a -> [(BindId, Integer, Symbol)]
forall a. SInfo a -> [(BindId, Integer, Symbol)]
ebindDefs SInfo a
si]
  where cons :: Integer -> SimpC ()
cons Integer
cid = () -> a -> ()
forall a b. a -> b -> a
const () (a -> ()) -> SimpC a -> SimpC ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Integer -> HashMap Integer (SimpC a) -> SimpC a
forall k v.
(HasCallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
Misc.safeLookup String
"ebindInfo" Integer
cid HashMap Integer (SimpC a)
cs
        cs :: HashMap Integer (SimpC a)
cs = SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
F.cm SInfo a
si
        cmpByFst :: ((a, b), b) -> ((a, b), b) -> Bool
cmpByFst ((a, b), b)
x ((a, b), b)
y = (a, b) -> a
forall a b. (a, b) -> a
fst ( ((a, b), b) -> (a, b)
forall a b. (a, b) -> a
fst ((a, b), b)
x ) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a, b) -> a
forall a b. (a, b) -> a
fst ( ((a, b), b) -> (a, b)
forall a b. (a, b) -> a
fst ((a, b), b)
y )
        group :: [((a, Symbol), SimpC ())] -> [(a, EbindSol)]
group [((a, Symbol), SimpC ())]
xs = (\[((a, Symbol), SimpC ())]
ys -> ( ((a, Symbol) -> a
forall a b. (a, b) -> a
fst ((a, Symbol) -> a) -> (a, Symbol) -> a
forall a b. (a -> b) -> a -> b
$ ((a, Symbol), SimpC ()) -> (a, Symbol)
forall a b. (a, b) -> a
fst (((a, Symbol), SimpC ()) -> (a, Symbol))
-> ((a, Symbol), SimpC ()) -> (a, Symbol)
forall a b. (a -> b) -> a -> b
$ [((a, Symbol), SimpC ())] -> ((a, Symbol), SimpC ())
forall a. [a] -> a
head [((a, Symbol), SimpC ())]
ys)
                           , [SimpC ()] -> Symbol -> EbindSol
Sol.EbDef (((a, Symbol), SimpC ()) -> SimpC ()
forall a b. (a, b) -> b
snd (((a, Symbol), SimpC ()) -> SimpC ())
-> [((a, Symbol), SimpC ())] -> [SimpC ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((a, Symbol), SimpC ())]
ys) ((a, Symbol) -> Symbol
forall a b. (a, b) -> b
snd ((a, Symbol) -> Symbol) -> (a, Symbol) -> Symbol
forall a b. (a -> b) -> a -> b
$ ((a, Symbol), SimpC ()) -> (a, Symbol)
forall a b. (a, b) -> a
fst (((a, Symbol), SimpC ()) -> (a, Symbol))
-> ((a, Symbol), SimpC ()) -> (a, Symbol)
forall a b. (a -> b) -> a -> b
$ [((a, Symbol), SimpC ())] -> ((a, Symbol), SimpC ())
forall a. [a] -> a
head [((a, Symbol), SimpC ())]
ys)))
                    ([((a, Symbol), SimpC ())] -> (a, EbindSol))
-> [[((a, Symbol), SimpC ())]] -> [(a, EbindSol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((a, Symbol), SimpC ()) -> ((a, Symbol), SimpC ()) -> Bool)
-> [((a, Symbol), SimpC ())] -> [[((a, Symbol), SimpC ())]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy ((a, Symbol), SimpC ()) -> ((a, Symbol), SimpC ()) -> Bool
forall a b b b b. Eq a => ((a, b), b) -> ((a, b), b) -> Bool
cmpByFst [((a, Symbol), SimpC ())]
xs

ebindDefs :: F.SInfo a -> [(F.BindId, F.SubcId, F.Symbol)]
ebindDefs :: SInfo a -> [(BindId, Integer, Symbol)]
ebindDefs SInfo a
si = [ (BindId
bid, Integer
cid, Symbol
x) | (Integer
cid, Symbol
x) <- [(Integer, Symbol)]
cDefs
                               , BindId
bid      <- Maybe BindId -> [BindId]
forall a. Maybe a -> [a]
maybeToList (Symbol -> HashMap Symbol BindId -> Maybe BindId
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol BindId
ebSyms)]
  where 
    ebSyms :: HashMap Symbol BindId
ebSyms   = SInfo a -> HashMap Symbol BindId
forall a. SInfo a -> HashMap Symbol BindId
ebindSyms SInfo a
si 
    cDefs :: [(Integer, Symbol)]
cDefs    = SInfo a -> [(Integer, Symbol)]
forall a. SInfo a -> [(Integer, Symbol)]
cstrDefs  SInfo a
si 

ebindSyms :: F.SInfo a -> M.HashMap F.Symbol F.BindId
ebindSyms :: SInfo a -> HashMap Symbol BindId
ebindSyms SInfo a
si = [(Symbol, BindId)] -> HashMap Symbol BindId
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
xi, BindId
bi) | BindId
bi        <- SInfo a -> [BindId]
forall (c :: * -> *) a. GInfo c a -> [BindId]
ebinds SInfo a
si
                                     , let (Symbol
xi,SortedReft
_) = BindId -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv BindId
bi BindEnv
be ] 
  where
    be :: BindEnv
be       = SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
si 
 
cstrDefs :: F.SInfo a -> [(F.SubcId, F.Symbol)]
cstrDefs :: SInfo a -> [(Integer, Symbol)]
cstrDefs SInfo a
si = [(Integer
cid, Symbol
x) | (Integer
cid, SimpC a
c) <- HashMap Integer (SimpC a) -> [(Integer, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (SInfo a -> HashMap Integer (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
                        , Symbol
x <- Maybe Symbol -> [Symbol]
forall a. Maybe a -> [a]
maybeToList (BindEnv -> SimpC a -> Maybe Symbol
forall a. BindEnv -> SimpC a -> Maybe Symbol
cstrDef BindEnv
be SimpC a
c) ]
  where 
    be :: BindEnv
be      = SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
si

cstrDef :: F.BindEnv -> F.SimpC a -> Maybe F.Symbol 
cstrDef :: BindEnv -> SimpC a -> Maybe Symbol
cstrDef BindEnv
be SimpC a
c 
  | Just (F.EVar Symbol
x) <- Maybe Expr
e = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x 
  | Bool
otherwise            = Maybe Symbol
forall a. Maybe a
Nothing 
  where 
    (Symbol
v,SortedReft
_)              = BindId -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv (SimpC a -> BindId
forall a. SimpC a -> BindId
cbind SimpC a
c) BindEnv
be 
    e :: Maybe Expr
e                  = String -> Maybe Expr -> Maybe Expr
forall a. PPrint a => String -> a -> a
F.notracepp String
_msg (Maybe Expr -> Maybe Expr) -> Maybe Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr -> Maybe Expr
F.isSingletonExpr Symbol
v Expr
rhs 
    _msg :: String
_msg                = String
"cstrDef: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [BindId] -> String
forall a. Show a => a -> String
show (SimpC a -> [BindId]
forall (c :: * -> *) a. TaggedC c a => c a -> [BindId]
stag SimpC a
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" crhs = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
F.showpp Expr
rhs 
    rhs :: Expr
rhs                = Expr -> Expr
V.stripCasts (SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
c)