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

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

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           Control.Monad (void)
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)
import qualified Data.Bifunctor                 as Bifunctor (second)
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 :: forall a.
Fixpoint a =>
Config -> SInfo a -> HashSet KVar -> Solution
init Config
cfg SInfo a
si HashSet KVar
ks_ = forall a b.
SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(Int, EbindSol)]
-> SEnv (Int, Sort)
-> Sol a b
Sol.fromList SymEnv
senv forall a. Monoid a => a
mempty [(KVar, QBind)]
keqs [] forall a. Monoid a => a
mempty [(Int, EbindSol)]
ebs SEnv (Int, Sort)
xEnv
  where
    keqs :: [(KVar, QBind)]
keqs       = forall a b. (a -> b) -> [a] -> [b]
map (forall a.
SInfo a -> QCluster -> SEnv Sort -> WfC a -> (KVar, QBind)
refine SInfo a
si QCluster
qcs SEnv Sort
genv) [WfC a]
ws forall a. a -> Strategy a -> a
`using` forall a. Strategy a -> Strategy [a]
parList 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_        = forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
si
    ws :: [WfC a]
ws         = [ WfC a
w | (KVar
k, WfC a
w) <- forall k v. HashMap k v -> [(k, v)]
M.toList (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si), Bool -> Bool
not (forall a. WfC a -> Bool
isGWfc WfC a
w), KVar
k 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       = forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si
    senv :: SymEnv
senv       = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si
    ebs :: [(Int, EbindSol)]
ebs        = forall a. SInfo a -> [(Int, EbindSol)]
ebindInfo SInfo a
si
    xEnv :: SEnv (Int, Sort)
xEnv       = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [ (Symbol
x, (Int
i, SortedReft -> Sort
F.sr_sort SortedReft
sr)) | (Int
i,(Symbol
x,SortedReft
sr,a
_)) <- forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
F.bindEnvToList (forall (c :: * -> *) a. GInfo c a -> BindEnv a
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 = 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 :: forall a.
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 (forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals SInfo a
fi) SEnv Sort
env QCluster
qs (forall a. WfC a -> (Symbol, Sort, KVar)
F.wrft WfC a
w)
  where
    env :: SEnv Sort
env             = SEnv Sort
wenv forall a. Semigroup a => a -> a -> a
<> SEnv Sort
genv
    wenv :: SEnv Sort
wenv            = SortedReft -> Sort
F.sr_sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi) (forall a. WfC a -> IBindEnv
F.wenv WfC a
w))

instConstants :: F.SInfo a -> F.SEnv F.Sort
instConstants :: forall a. SInfo a -> SEnv Sort
instConstants = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (Symbol, b) -> Bool
notLit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits
  where
    notLit :: (Symbol, b) -> Bool
notLit    = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
F.isLitSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = 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                    = forall r. PrintfType r => String -> r
printf String
"\n\nrefineK: k = %s, eqs = %s" (forall a. PPrint a => a -> String
F.showpp KVar
k) (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [EQual] -> [EQual]
unique forall a b. (a -> b) -> a -> b
$
  [ Qualifier -> [Symbol] -> EQual
Sol.eQual Qualifier
q [Symbol]
xs
      | (QCSig
sig, [Qualifier]
qs) <- 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 = forall k v. HashMap k v -> [v]
M.elems forall a b. (a -> b) -> a -> b
$ 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
_  SEnv Sort
_   Symbol
_ Sort
_ [] = forall a. HasCallStack => String -> a
error String
"Empty qsig in Solution.instKSig"
instKSig Bool
ho SEnv Sort
env Symbol
v Sort
t (QualParam
qp:QCSig
qps) = do
  (TVSubst
su0, Int
i0, QualPattern
qs0) <- forall a.
Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
candidatesP Env
senv [(Int
0, Sort
t, [Symbol
v])] QualParam
qp
  [(Int, QualPattern)]
ixs       <- forall a.
Env
-> [(Int, Sort, a)]
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
matchP Env
senv [(Int, Sort, [Symbol])]
tyss [(Int
i0, QualPattern
qs0)] (TVSubst -> QualParam -> QualParam
applyQPP TVSubst
su0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QCSig
qps)
  -- return     $ F.notracepp msg (reverse ixs)
  [Symbol]
ys        <- forall a.
[(Int, a, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
instSymbol [(Int, Sort, [Symbol])]
tyss (forall a. [a] -> [a]
tail forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [(Int, QualPattern)]
ixs)
  forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
vforall a. a -> [a] -> [a]
:[Symbol]
ys)
  where
    -- msg        = "instKSig " ++ F.showpp qsig
    tyss :: [(Int, Sort, [Symbol])]
tyss       = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i (Sort
t, [Symbol]
ys) -> (Int
i, Sort
t, [Symbol]
ys)) [Int
1..] (Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env)
    senv :: Env
senv       = (forall a. Symbol -> SEnv a -> SESearch a
`F.lookupSEnvWithDistance` SEnv Sort
env)

instSymbol :: [(SortIdx, a, [F.Symbol])] -> [(SortIdx, QualPattern)] -> [[F.Symbol]]
instSymbol :: forall a.
[(Int, a, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
instSymbol [(Int, a, [Symbol])]
tyss = [(Int, QualPattern)] -> [[Symbol]]
go
  where
    m :: HashMap Int [Symbol]
m = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int
i, [Symbol]
ys) | (Int
i,a
_,[Symbol]
ys) <- [(Int, a, [Symbol])]
tyss]
    go :: [(Int, QualPattern)] -> [[Symbol]]
go [] =
      forall (m :: * -> *) a. Monad m => a -> m a
return []
    go ((Int
i,QualPattern
qp):[(Int, QualPattern)]
is) = do
      Symbol
y   <- forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Int
i HashMap Int [Symbol]
m
      QPSubst
qsu <- forall a. Maybe a -> [a]
maybeToList (QualPattern -> Symbol -> Maybe QPSubst
matchSym QualPattern
qp Symbol
y)
      [Symbol]
ys  <- [(Int, QualPattern)] -> [[Symbol]]
go [ (Int
i', QPSubst -> QualPattern -> QualPattern
applyQPSubst QPSubst
qsu  QualPattern
qp') | (Int
i', QualPattern
qp') <- [(Int, QualPattern)]
is]
      forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
yforall 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 = forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (Sort, b) -> Bool
isOk [(Sort, [Symbol])]
tyss
  where
    tyss :: [(Sort, [Symbol])]
tyss      = 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 forall a b. a -> b -> a
const Bool
True else forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe (Tag, [Sort], Sort)
F.functionSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
    xts :: [(Symbol, Sort)]
xts       = forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env


type SortIdx = Int

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

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



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

matchSym :: F.QualPattern -> F.Symbol -> Maybe QPSubst
matchSym :: QualPattern -> Symbol -> Maybe QPSubst
matchSym QualPattern
qp Symbol
y' = case QualPattern
qp of
  F.PatPrefix Symbol
s Int
i -> Int -> Symbol -> QPSubst
JustSub Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> Symbol -> Maybe Symbol
F.stripPrefix Symbol
s Symbol
y
  F.PatSuffix Int
i Symbol
s -> Int -> Symbol -> QPSubst
JustSub Int
i 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       -> forall a. a -> Maybe a
Just QPSubst
NoSub
  F.PatExact Symbol
s    -> if Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
y then forall a. a -> Maybe a
Just QPSubst
NoSub else 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 Int
i Symbol
x) (F.PatPrefix Symbol
s Int
j)
  | Int
i forall a. Eq a => a -> a -> Bool
== Int
j = Symbol -> QualPattern
F.PatExact (Symbol -> Symbol -> Symbol
F.mappendSym Symbol
s Symbol
x)
applyQPSubst (JustSub Int
i Symbol
x) (F.PatSuffix Int
j Symbol
s)
  | Int
i forall a. Eq a => a -> a -> Bool
== Int
j = Symbol -> QualPattern
F.PatExact (Symbol -> Symbol -> Symbol
F.mappendSym Symbol
x Symbol
s)
applyQPSubst QPSubst
_ QualPattern
p
  = QualPattern
p

--------------------------------------------------------------------------------
okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
--------------------------------------------------------------------------------
okInst :: SEnv Sort -> Symbol -> Sort -> EQual -> Bool
okInst SEnv Sort
env Symbol
v Sort
t EQual
eq = 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            = forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
So.checkSorted (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 a
  -> Sol.Solution
  -> F.SimpC a
  -> F.Expr
lhsPred :: forall a.
Loc a =>
IBindEnv -> BindEnv a -> Solution -> SimpC a -> Expr
lhsPred IBindEnv
bindingsInSmt BindEnv a
be Solution
s SimpC a
c = forall a. PPrint a => String -> a -> a
F.notracepp String
_msg forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ExprInfo
apply CombinedEnv a
g Solution
s IBindEnv
bs
  where
    g :: CombinedEnv a
g          = forall a.
Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
CEnv Cid
ci BindEnv a
be IBindEnv
bs (forall a. Loc a => a -> SrcSpan
F.srcSpan SimpC a
c) IBindEnv
bindingsInSmt
    bs :: IBindEnv
bs         = forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
F.senv SimpC a
c
    ci :: Cid
ci         = forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC a
c
    _msg :: String
_msg       = String
"LhsPred for id = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC a
c) forall a. [a] -> [a] -> [a]
++ String
" with SOLUTION = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp Solution
s

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

instance F.Loc (CombinedEnv a) where
  srcSpan :: CombinedEnv a -> SrcSpan
srcSpan = forall a. CombinedEnv a -> SrcSpan
ceSpan

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

apply :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ExprInfo
apply :: forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ExprInfo
apply CombinedEnv ann
g Sol a QBind
s IBindEnv
bs      = ([Expr] -> Expr
F.conj (Expr
pksforall 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)     = forall ann a. CombinedEnv ann -> Sol a QBind -> [KVSub] -> ExprInfo
applyKVars CombinedEnv ann
g {ceBindingsInSmt :: IBindEnv
ceBindingsInSmt = IBindEnv
F.emptyIBindEnv} Sol a QBind
s [KVSub]
ks
    ([Expr]
ps,  [KVSub]
ks, [KVSub]
_)  = forall ann a.
CombinedEnv ann
-> Sol a QBind -> IBindEnv -> ([Expr], [KVSub], [KVSub])
envConcKVars CombinedEnv ann
g Sol a QBind
s IBindEnv
bs


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

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

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

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

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

ebindReft :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> F.Pred
ebindReft :: forall ann a. CombinedEnv ann -> Sol a QBind -> SimpC () -> Expr
ebindReft CombinedEnv ann
g Sol a QBind
s SimpC ()
c = [Expr] -> Expr
F.pAnd [ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ExprInfo
apply CombinedEnv ann
g' Sol a QBind
s IBindEnv
bs, forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC ()
c ]
  where
    g' :: CombinedEnv ann
g'          = CombinedEnv ann
g { ceCid :: Cid
ceCid = forall (c :: * -> *) a. TaggedC c a => c a -> Cid
sid SimpC ()
c, ceIEnv :: IBindEnv
ceIEnv = IBindEnv
bs }
    bs :: IBindEnv
bs          = 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 (Int, Sort) -> IBindEnv -> Int -> Expr -> Expr
exElim SEnv (Int, Sort)
env IBindEnv
ienv Int
xi Expr
p = 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        <- forall a. Subable a => a -> [Symbol]
F.syms Expr
p
                            , (Int
yi, Sort
yt) <- forall a. Maybe a -> [a]
maybeToList (forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
y SEnv (Int, Sort)
env)
                            , Int
xi forall a. Ord a => a -> a -> Bool
< Int
yi
                            , Int
yi Int -> IBindEnv -> Bool
`F.memberIBindEnv` IBindEnv
ienv                  ]

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

applyKVar :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> ExprInfo
applyKVar :: forall ann a. CombinedEnv ann -> Sol a QBind -> KVSub -> ExprInfo
applyKVar CombinedEnv ann
g Sol a QBind
s KVSub
ksu = case 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   -> forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Hyp -> ExprInfo
hypPred CombinedEnv ann
g Sol a QBind
s KVSub
ksu Hyp
cs
  Right QBind
eqs -> ([Expr] -> Expr
F.pAndNoDedup forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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, forall a. Monoid a => a
mempty) -- TODO: don't initialize kvars that have a hyp solution
  where
    msg :: String
msg     = String
"applyKVar: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. CombinedEnv a -> Cid
ceCid CombinedEnv ann
g)

nonCutsResult :: F.BindEnv ann -> Sol.Sol a Sol.QBind -> M.HashMap F.KVar F.Expr
nonCutsResult :: forall ann a. BindEnv ann -> Sol a QBind -> HashMap KVar Expr
nonCutsResult BindEnv ann
be Sol a QBind
s =
  let g :: CombinedEnv ann
g = forall a.
Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
CEnv forall a. Maybe a
Nothing BindEnv ann
be IBindEnv
F.emptyIBindEnv SrcSpan
F.dummySpan IBindEnv
F.emptyIBindEnv
   in forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey (forall {ann}. CombinedEnv ann -> KVar -> Hyp -> Expr
mkNonCutsExpr CombinedEnv ann
g) forall a b. (a -> b) -> a -> b
$ forall b a. Sol b a -> HashMap KVar Hyp
Sol.sHyp Sol a QBind
s
  where
    mkNonCutsExpr :: CombinedEnv ann -> KVar -> Hyp -> Expr
mkNonCutsExpr CombinedEnv ann
g KVar
k Hyp
cs = [Expr] -> Expr
F.pOr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall ann a.
CombinedEnv ann -> Sol a QBind -> KVar -> Cube -> Expr
bareCubePred CombinedEnv ann
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 ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Cube -> F.Expr
bareCubePred :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVar -> Cube -> Expr
bareCubePred CombinedEnv ann
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 ann
g' = forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv  CombinedEnv ann
g IBindEnv
bs
      bs' :: IBindEnv
bs' = forall a. Sol a QBind -> KVar -> IBindEnv -> IBindEnv
delCEnv Sol a QBind
s KVar
k IBindEnv
bs
      yts :: [(Symbol, Sort)]
yts = forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv ann
g IBindEnv
bs'
      sEnv :: SEnv Sort
sEnv = SymEnv -> SEnv Sort
F.seSort (forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s)
      ([(Symbol, Sort)]
xts, Expr
psu) = forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim (forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s) SEnv Sort
sEnv CombinedEnv ann
g' KVar
k Subst
su
      (Expr
p, KInfo
_kI) = forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ExprInfo
apply CombinedEnv ann
g' Sol a QBind
s IBindEnv
bs'
   in [(Symbol, Sort)] -> Expr -> Expr
F.pExist ([(Symbol, Sort)]
xts forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
yts) (Expr
psu Expr -> Expr -> Expr
&.& Expr
p)

hypPred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp  -> ExprInfo
hypPred :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Hyp -> ExprInfo
hypPred CombinedEnv ann
g Sol a QBind
s KVSub
ksu Hyp
hyp = [Expr] -> Expr
F.pOr forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [KInfo] -> KInfo
mconcatPlus forall a b. (a -> b) -> a -> b
$ forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Cube -> ExprInfo
cubePred CombinedEnv ann
g Sol a QBind
s KVSub
ksu 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 :: forall a.
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        = forall a. Elaborate a => Located String -> SymEnv -> a -> a
So.elaborate (forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
sp String
"elabExist") SymEnv
env
    env :: SymEnv
env         = forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s

cubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> ExprInfo
cubePred :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Cube -> ExprInfo
cubePred CombinedEnv ann
g Sol a QBind
s KVSub
ksu Cube
c    = (forall a. PPrint a => String -> a -> a
F.notracepp String
"cubePred" forall a b. (a -> b) -> a -> b
$ 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                = forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv ann
g
    (([(Symbol, Sort)]
xts,Expr
psu,Expr
p), KInfo
kI) = forall ann a.
CombinedEnv ann
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> (([(Symbol, Sort)], Expr, Expr), KInfo)
cubePredExc CombinedEnv ann
g Sol a QBind
s KVSub
ksu Cube
c IBindEnv
bs'
    bs' :: IBindEnv
bs'               = 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 ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> F.IBindEnv
            -> ((Binders, F.Pred, F.Pred), KInfo)

cubePredExc :: forall ann a.
CombinedEnv ann
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> (([(Symbol, Sort)], Expr, Expr), KInfo)
cubePredExc CombinedEnv ann
g Sol a QBind
s KVSub
ksu Cube
c IBindEnv
bs' = (([(Symbol, Sort)], Expr, Expr)
cubeP, KInfo -> Tag -> KInfo
extendKInfo KInfo
kI (Cube -> Tag
Sol.cuTag Cube
c))
  where
    cubeP :: ([(Symbol, Sort)], Expr, Expr)
cubeP           = ([(Symbol, Sort)]
xts, Expr
psu, 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              = forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv ann
g
    yts' :: [(Symbol, Sort)]
yts'            = forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv ann
g IBindEnv
bs'
    g' :: CombinedEnv ann
g'              = forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv  CombinedEnv ann
g IBindEnv
bs
    (Expr
p', KInfo
kI)        = forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ExprInfo
apply CombinedEnv ann
g' Sol a QBind
s IBindEnv
bs'
    ([(Symbol, Sort)]
_  , Expr
psu')     = forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim (forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s) SEnv Sort
sEnv CombinedEnv ann
g' KVar
k Subst
su'
    ([(Symbol, Sort)]
xts, Expr
psu)      = forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim (forall b a. Sol b a -> SymEnv
Sol.sEnv Sol a QBind
s) SEnv Sort
sEnv CombinedEnv ann
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            = 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 forall a b. (a -> b) -> a -> b
$ 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 a -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)
substElim :: forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ([(Symbol, Sort)], Expr)
substElim SymEnv
syEnv SEnv Sort
sEnv CombinedEnv a
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 (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    = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol Expr
m
    env :: SEnv Sort
env    = forall a. CombinedEnv a -> SEnv Sort
combinedSEnv CombinedEnv a
g
    frees :: HashSet Symbol
frees  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. Subable a => a -> [Symbol]
F.syms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Symbol, Expr)]
xes)
    sortOf :: Expr -> [Sort]
sortOf = forall a. Maybe a -> [a]
maybeToList 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     = forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv a
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 = forall a. a -> Maybe a -> a
fromMaybe (forall {a} {a}. PPrint a => a -> a
err Symbol
x) forall a b. (a -> b) -> a -> b
$ forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
x SEnv Sort
sEnv
  where
    err :: a -> a
err a
x            = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Solution.mkSubst: unknown binder " forall a. [a] -> [a] -> [a]
++ 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 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:" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (Sort
tx, Sort
ty) forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (Expr
ex', Expr
ey')
    ex :: Expr
ex          = 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 = forall a. Elaborate a => Located String -> SymEnv -> a -> a
So.elaborate (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

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

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


delCEnv :: Sol.Sol a Sol.QBind -> F.KVar -> F.IBindEnv -> F.IBindEnv
delCEnv :: forall a. 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       = forall k v.
(HasCallStack, Eq k, Hashable k) =>
String -> k -> HashMap k v -> v
Misc.safeLookup String
"delCEnv" KVar
k (forall b a. Sol b a -> HashMap KVar IBindEnv
Sol.sScp Sol a QBind
s)

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

_noKvars :: F.Expr -> Bool
_noKvars :: Expr -> Bool
_noKvars = forall (t :: * -> *) a. Foldable t => t a -> Bool
null 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 -> [Tag]
kiTags  :: [Tag]
                , KInfo -> Int
kiDepth :: !Int
                , KInfo -> Integer
kiCubes :: !Integer
                } deriving (KInfo -> KInfo -> Bool
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
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
Ord, Int -> KInfo -> String -> String
[KInfo] -> String -> String
KInfo -> String
forall a.
(Int -> 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 :: Int -> KInfo -> String -> String
$cshowsPrec :: Int -> KInfo -> String -> String
Show)

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

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

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

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

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

extendKInfo :: KInfo -> F.Tag -> KInfo
extendKInfo :: KInfo -> Tag -> KInfo
extendKInfo KInfo
ki Tag
t = KInfo
ki { kiTags :: [Tag]
kiTags  = [Tag] -> [Tag] -> [Tag]
appendTags [Tag
t] (KInfo -> [Tag]
kiTags  KInfo
ki)
                      , kiDepth :: Int
kiDepth = Int
1  forall a. Num a => a -> a -> a
+            KInfo -> Int
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 :: forall a b c b1 c1.
(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)              = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ 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 :: forall a. SInfo a -> [(Int, EbindSol)]
ebindInfo SInfo a
si = forall {a}. Eq a => [((a, Symbol), SimpC ())] -> [(a, EbindSol)]
group [((Int
bid, Symbol
x), Integer -> SimpC ()
cons Integer
cid) | (Int
bid, Integer
cid, Symbol
x) <- forall a. SInfo a -> [(Int, Integer, Symbol)]
ebindDefs SInfo a
si]
  where cons :: Integer -> SimpC ()
cons Integer
cid = forall (f :: * -> *) a. Functor f => f a -> f ()
void (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 = 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 = forall a b. (a, b) -> a
fst ( forall a b. (a, b) -> a
fst ((a, b), b)
x ) forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst ( 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 -> forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Bifunctor.second ([SimpC ()] -> Symbol -> EbindSol
Sol.EbDef (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((a, Symbol), SimpC ())]
ys)) (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [((a, Symbol), SimpC ())]
ys))
                    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy 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 :: forall a. SInfo a -> [(Int, Integer, Symbol)]
ebindDefs SInfo a
si = [ (Int
bid, Integer
cid, Symbol
x) | (Integer
cid, Symbol
x) <- [(Integer, Symbol)]
cDefs
                               , Int
bid      <- forall a. Maybe a -> [a]
maybeToList (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol Int
ebSyms)]
  where
    ebSyms :: HashMap Symbol Int
ebSyms   = forall a. SInfo a -> HashMap Symbol Int
ebindSyms SInfo a
si
    cDefs :: [(Integer, Symbol)]
cDefs    = forall a. SInfo a -> [(Integer, Symbol)]
cstrDefs  SInfo a
si

ebindSyms :: F.SInfo a -> M.HashMap F.Symbol F.BindId
ebindSyms :: forall a. SInfo a -> HashMap Symbol Int
ebindSyms SInfo a
si = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
xi, Int
bi) | Int
bi        <- forall (c :: * -> *) a. GInfo c a -> Tag
ebinds SInfo a
si
                                     , let (Symbol
xi,SortedReft
_,a
_) = forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv Int
bi BindEnv a
be ]
  where
    be :: BindEnv a
be       = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si

cstrDefs :: F.SInfo a -> [(F.SubcId, F.Symbol)]
cstrDefs :: forall a. SInfo a -> [(Integer, Symbol)]
cstrDefs SInfo a
si = [(Integer
cid, Symbol
x) | (Integer
cid, SimpC a
c) <- forall k v. HashMap k v -> [(k, v)]
M.toList (forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
cm SInfo a
si)
                        , Symbol
x <- forall a. Maybe a -> [a]
maybeToList (forall a. BindEnv a -> SimpC a -> Maybe Symbol
cstrDef BindEnv a
be SimpC a
c) ]
  where
    be :: BindEnv a
be      = forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
si

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