{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleInstances #-}
{-# 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           Control.Monad (void)
import           Control.Monad.Reader
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           Language.Fixpoint.SortCheck          (ElabM)
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_ = SymEnv
-> [(KVar, ())]
-> [(KVar, QBind)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(Int, EbindSol)]
-> SEnv (Int, Sort)
-> Solution
forall a b.
SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(Int, EbindSol)]
-> SEnv (Int, Sort)
-> Sol a b
Sol.fromList SymEnv
symEnv [(KVar, ())]
forall a. Monoid a => a
mempty [(KVar, QBind)]
keqs [] HashMap KVar IBindEnv
forall a. Monoid a => a
mempty [(Int, EbindSol)]
ebs SEnv (Int, Sort)
xEnv
  where
    keqs :: [(KVar, QBind)]
keqs       = Reader ElabFlags [(KVar, QBind)] -> ElabFlags -> [(KVar, QBind)]
forall r a. Reader r a -> r -> a
runReader ((WfC a -> ReaderT ElabFlags Identity (KVar, QBind))
-> [WfC a] -> Reader ElabFlags [(KVar, QBind)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (SInfo a
-> QCluster
-> SEnv Sort
-> WfC a
-> ReaderT ElabFlags Identity (KVar, QBind)
forall a.
SInfo a
-> QCluster
-> SEnv Sort
-> WfC a
-> ReaderT ElabFlags Identity (KVar, QBind)
refine SInfo a
si QCluster
qcs SEnv Sort
genv) [WfC a]
ws) (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver Config
cfg) [(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
    symEnv :: SymEnv
symEnv     = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si
    ebs :: [(Int, EbindSol)]
ebs        = SInfo a -> [(Int, EbindSol)]
forall a. SInfo a -> [(Int, EbindSol)]
ebindInfo SInfo a
si
    xEnv :: SEnv (Int, Sort)
xEnv       = [(Symbol, (Int, Sort))] -> SEnv (Int, Sort)
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
_)) <- BindEnv a -> [(Int, (Symbol, SortedReft, a))]
forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
F.bindEnvToList (SInfo a -> BindEnv a
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 = (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 { F.qpSym = F.dummyName }  | QualParam
p <- Qualifier -> QCSig
forall v. QualifierV v -> QCSig
F.qParams Qualifier
q ]

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

refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> ElabM (F.KVar, Sol.QBind)
refine :: forall a.
SInfo a
-> QCluster
-> SEnv Sort
-> WfC a
-> ReaderT ElabFlags Identity (KVar, QBind)
refine SInfo a
info QCluster
qs SEnv Sort
genv WfC a
w = Bool
-> SEnv Sort
-> QCluster
-> (Symbol, Sort, KVar)
-> ReaderT ElabFlags Identity (KVar, QBind)
refineK (SInfo a -> Bool
forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals SInfo a
info) 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
wenvSort SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SEnv Sort
genv
    wenvSort :: SEnv Sort
wenvSort        = 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 a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
info) (WfC a -> IBindEnv
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 = [(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) -> ElabM (F.KVar, Sol.QBind)
refineK :: Bool
-> SEnv Sort
-> QCluster
-> (Symbol, Sort, KVar)
-> ReaderT ElabFlags Identity (KVar, QBind)
refineK Bool
ho SEnv Sort
env QCluster
qs (Symbol
v, Sort
t, KVar
k) =
  do QBind
eqs' <- (EQual -> ReaderT ElabFlags Identity Bool)
-> QBind -> ReaderT ElabFlags Identity QBind
forall (m :: * -> *).
Monad m =>
(EQual -> m Bool) -> QBind -> m QBind
Sol.qbFilterM (SEnv Sort
-> Symbol -> Sort -> EQual -> ReaderT ElabFlags Identity Bool
okInst SEnv Sort
env Symbol
v Sort
t) QBind
eqs
     (KVar, QBind) -> ReaderT ElabFlags Identity (KVar, QBind)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((KVar, QBind) -> ReaderT ElabFlags Identity (KVar, QBind))
-> (KVar, QBind) -> ReaderT ElabFlags Identity (KVar, QBind)
forall a b. (a -> b) -> a -> b
$ 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

    _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
_  SEnv Sort
_   Symbol
_ Sort
_ [] = String -> [[Symbol]]
forall a. HasCallStack => String -> a
error String
"Empty qsig in Solution.instKSig"
instKSig Bool
ho SEnv Sort
env Symbol
v Sort
sort' (QualParam
qp:QCSig
qps) = do
  (TVSubst
su0, Int
i0, QualPattern
qs0) <- Env
-> [(Int, Sort, [Symbol])]
-> QualParam
-> [(TVSubst, Int, QualPattern)]
forall a.
Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
candidatesP Env
symToSrch [(Int
0, Sort
sort', [Symbol
v])] QualParam
qp
  [(Int, QualPattern)]
ixs       <- Env
-> [(Int, Sort, [Symbol])]
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
forall a.
Env
-> [(Int, Sort, a)]
-> [(Int, QualPattern)]
-> QCSig
-> [[(Int, QualPattern)]]
matchP Env
symToSrch [(Int, Sort, [Symbol])]
tyss [(Int
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)
  [Symbol]
ys        <- [(Int, Sort, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
forall a.
[(Int, a, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
instSymbol [(Int, Sort, [Symbol])]
tyss ([(Int, QualPattern)] -> [(Int, QualPattern)]
forall a. HasCallStack => [a] -> [a]
tail ([(Int, QualPattern)] -> [(Int, QualPattern)])
-> [(Int, QualPattern)] -> [(Int, QualPattern)]
forall a b. (a -> b) -> a -> b
$ [(Int, QualPattern)] -> [(Int, QualPattern)]
forall a. [a] -> [a]
reverse [(Int, QualPattern)]
ixs)
  [Symbol] -> [[Symbol]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
vSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys)
  where
    tyss :: [(Int, Sort, [Symbol])]
tyss       = (Int -> (Sort, [Symbol]) -> (Int, Sort, [Symbol]))
-> Tag -> [(Sort, [Symbol])] -> [(Int, Sort, [Symbol])]
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)
    symToSrch :: Env
symToSrch  = (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 :: forall a.
[(Int, a, [Symbol])] -> [(Int, QualPattern)] -> [[Symbol]]
instSymbol [(Int, a, [Symbol])]
tyss = [(Int, QualPattern)] -> [[Symbol]]
go
  where
    m :: HashMap Int [Symbol]
m = [(Int, [Symbol])] -> HashMap Int [Symbol]
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 [] =
      [Symbol] -> [[Symbol]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    go ((Int
i,QualPattern
qp):[(Int, QualPattern)]
is) = do
      Symbol
y   <- [Symbol] -> Int -> HashMap Int [Symbol] -> [Symbol]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] Int
i HashMap Int [Symbol]
m
      QPSubst
qsu <- Maybe QPSubst -> [QPSubst]
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]
      [Symbol] -> [[Symbol]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
ySymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
ys)

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 (Tag, [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Tag, [Sort], Sort) -> Bool)
-> ((Sort, b) -> Maybe (Tag, [Sort], Sort)) -> (Sort, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe (Tag, [Sort], Sort)
F.functionSort (Sort -> Maybe (Tag, [Sort], Sort))
-> ((Sort, b) -> Sort) -> (Sort, b) -> Maybe (Tag, [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 :: 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)(Int, QualPattern) -> [(Int, QualPattern)] -> [(Int, QualPattern)]
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) <- Env
-> [(Int, Sort, a)] -> QualParam -> [(TVSubst, Int, QualPattern)]
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 (QualParam -> QualParam) -> QCSig -> QCSig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QCSig
qps)
    go [(Int, QualPattern)]
is []         = [(Int, QualPattern)] -> [[(Int, QualPattern)]]
forall a. a -> [a]
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 = So.apply     su  (qpSort 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          <- 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 Int
i -> Int -> Symbol -> QPSubst
JustSub Int
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 Int
i Symbol
s -> Int -> Symbol -> QPSubst
JustSub Int
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.unKArgSymbol 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 Int -> Int -> Bool
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 Int -> Int -> Bool
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 -> ElabM Bool
--------------------------------------------------------------------------------
okInst :: SEnv Sort
-> Symbol -> Sort -> EQual -> ReaderT ElabFlags Identity Bool
okInst SEnv Sort
env Symbol
v Sort
t EQual
eq =
  do Maybe Doc
tc <- SrcSpan -> SEnv Sort -> SortedReft -> ElabM (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv Sort -> a -> ElabM (Maybe Doc)
So.checkSorted (EQual -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan EQual
eq) SEnv Sort
env SortedReft
sr
     Bool -> ReaderT ElabFlags Identity Bool
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> ReaderT ElabFlags Identity Bool)
-> Bool -> ReaderT ElabFlags Identity Bool
forall a b. (a -> b) -> a -> b
$ 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
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
v, Expr
p))
    p :: Expr
p             = EQual -> Expr
Sol.eqPred EQual
eq

    -- _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
  -> ElabM F.Expr
lhsPred :: forall a.
Loc a =>
IBindEnv -> BindEnv a -> Solution -> SimpC a -> ElabM Expr
lhsPred IBindEnv
bindingsInSmt BindEnv a
be Solution
s SimpC a
c =
  do ExprInfo
ap <- CombinedEnv a -> Solution -> IBindEnv -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
apply CombinedEnv a
g Solution
s IBindEnv
bs
     Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ 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
$ ExprInfo -> Expr
forall a b. (a, b) -> a
fst ExprInfo
ap
  where
    g :: CombinedEnv a
g          = Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
forall a.
Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
CEnv Cid
ci BindEnv a
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 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 = CombinedEnv a -> 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 -> ElabM ExprInfo
apply :: forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
apply CombinedEnv ann
g Sol a QBind
s IBindEnv
bs      =
  -- Clear the "known" bindings for applyKVars, since it depends on
  -- using the fully expanded representation of the predicates to bind their
  -- variables with quantifiers.
  do ([Expr]
ps,  [KVSub]
ks, [KVSub]
_) <- CombinedEnv ann
-> Sol a QBind -> IBindEnv -> ElabM ([Expr], [KVSub], [KVSub])
forall ann a.
CombinedEnv ann
-> Sol a QBind -> IBindEnv -> ElabM ([Expr], [KVSub], [KVSub])
envConcKVars CombinedEnv ann
g Sol a QBind
s IBindEnv
bs
     (Expr
pks, KInfo
kI) <- CombinedEnv ann -> Sol a QBind -> [KVSub] -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> [KVSub] -> ElabM ExprInfo
applyKVars CombinedEnv ann
g {ceBindingsInSmt = F.emptyIBindEnv} Sol a QBind
s [KVSub]
ks
     ExprInfo -> ElabM ExprInfo
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Expr] -> Expr
F.conj (Expr
pksExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
ps), KInfo
kI)   -- see [NOTE: pAnd-SLOW]


envConcKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ElabM ([F.Expr], [F.KVSub], [F.KVSub])
envConcKVars :: forall ann a.
CombinedEnv ann
-> Sol a QBind -> IBindEnv -> ElabM ([Expr], [KVSub], [KVSub])
envConcKVars CombinedEnv ann
g Sol a QBind
s IBindEnv
bs =
  do [(Symbol, SortedReft)]
xrs <- (Int -> ReaderT ElabFlags Identity (Symbol, SortedReft))
-> Tag -> ReaderT ElabFlags Identity [(Symbol, SortedReft)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (CombinedEnv ann
-> Sol a QBind
-> Int
-> ReaderT ElabFlags Identity (Symbol, SortedReft)
forall ann a.
CombinedEnv ann
-> Sol a QBind
-> Int
-> ReaderT ElabFlags Identity (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv ann
g Sol a QBind
s) Tag
is
     let ([[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 ]
     ([Expr], [KVSub], [KVSub]) -> ElabM ([Expr], [KVSub], [KVSub])
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([[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
    is :: Tag
is = IBindEnv -> Tag
F.elemsIBindEnv IBindEnv
bs

lookupBindEnvExt :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> ElabM (F.Symbol, F.SortedReft)
lookupBindEnvExt :: forall ann a.
CombinedEnv ann
-> Sol a QBind
-> Int
-> ReaderT ElabFlags Identity (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv ann
g Sol a QBind
s Int
i =
  do Maybe Expr
msol <- CombinedEnv ann -> Sol a QBind -> Int -> ElabM (Maybe Expr)
forall ann a.
CombinedEnv ann -> Sol a QBind -> Int -> ElabM (Maybe Expr)
ebSol (CombinedEnv ann
g {ceBindingsInSmt = F.emptyIBindEnv}) Sol a QBind
s Int
i
     (Symbol, SortedReft)
-> ReaderT ElabFlags Identity (Symbol, SortedReft)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbol
x, case Maybe Expr
msol of
                Just Expr
p -> SortedReft
sr { F.sr_reft = F.Reft (x, p) }
                Maybe Expr
Nothing -> if Int -> IBindEnv -> Bool
F.memberIBindEnv Int
i (CombinedEnv ann -> IBindEnv
forall a. CombinedEnv a -> IBindEnv
ceBindingsInSmt CombinedEnv ann
g)
                              then SortedReft
sr { F.sr_reft = F.Reft (x, F.EVar (F.bindSymbol (fromIntegral i)))}
                              else SortedReft
sr)
   where
      (Symbol
x, SortedReft
sr, ann
_)              = Int -> BindEnv ann -> (Symbol, SortedReft, ann)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv Int
i (CombinedEnv ann -> BindEnv ann
forall a. CombinedEnv a -> BindEnv a
ceBEnv CombinedEnv ann
g)

ebSol :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> ElabM (Maybe F.Expr)
ebSol :: forall ann a.
CombinedEnv ann -> Sol a QBind -> Int -> ElabM (Maybe Expr)
ebSol CombinedEnv ann
g Sol a QBind
sol Int
bindId = case Int -> HashMap Int EbindSol -> Maybe EbindSol
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
bindId HashMap Int EbindSol
sebds of
  Just (Sol.EbSol Expr
p)    -> Maybe Expr -> ElabM (Maybe Expr)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Expr -> ElabM (Maybe Expr))
-> Maybe Expr -> ElabM (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
p
  Just (Sol.EbDef [SimpC ()]
cs Symbol
_) ->
    do let cSol :: SimpC () -> ElabM 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 ann -> Cid
forall a. CombinedEnv a -> Cid
ceCid CombinedEnv ann
g
                       then Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
forall v. ExprV v
F.PFalse
                       else do Expr
p <- CombinedEnv ann -> Sol a QBind -> SimpC () -> ElabM Expr
forall ann a.
CombinedEnv ann -> Sol a QBind -> SimpC () -> ElabM Expr
ebindReft CombinedEnv ann
g Sol a QBind
s' SimpC ()
c
                               Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ SEnv (Int, Sort) -> IBindEnv -> Int -> Expr -> Expr
exElim (Sol a QBind -> SEnv (Int, Sort)
forall b a. Sol b a -> SEnv (Int, Sort)
Sol.sxEnv Sol a QBind
s') (SimpC () -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC ()
c) Int
bindId Expr
p
       [Expr]
exps <- (SimpC () -> ElabM Expr)
-> [SimpC ()] -> ReaderT ElabFlags Identity [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse SimpC () -> ElabM Expr
cSol [SimpC ()]
cs
       Maybe Expr -> ElabM (Maybe Expr)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Expr -> ElabM (Maybe Expr))
-> Maybe Expr -> ElabM (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
F.PAnd [Expr]
exps
  Maybe EbindSol
_                     -> Maybe Expr -> ElabM (Maybe Expr)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
forall a. Maybe a
Nothing
  where
    sebds :: HashMap Int EbindSol
sebds = Sol a QBind -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
Sol.sEbd Sol a QBind
sol
    s' :: Sol a QBind
s' = Sol a QBind
sol { Sol.sEbd = M.insert bindId Sol.EbIncr sebds }

ebindReft :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> ElabM F.Pred
ebindReft :: forall ann a.
CombinedEnv ann -> Sol a QBind -> SimpC () -> ElabM Expr
ebindReft CombinedEnv ann
g Sol a QBind
s SimpC ()
c =
  do ExprInfo
a <- CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
apply CombinedEnv ann
g' Sol a QBind
s IBindEnv
bs
     Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [ ExprInfo -> Expr
forall a b. (a, b) -> a
fst ExprInfo
a , SimpC () -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
F.crhs SimpC ()
c ]
  where
    g' :: CombinedEnv ann
g'          = CombinedEnv ann
g { ceCid = sid c, ceIEnv = 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 (Int, Sort) -> IBindEnv -> Int -> Expr -> Expr
exElim SEnv (Int, Sort)
env IBindEnv
ienv Int
xi Expr
p = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
F.notracepp String
msg ([(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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
                            , (Int
yi, Sort
yt) <- Maybe (Int, Sort) -> [(Int, Sort)]
forall a. Maybe a -> [a]
maybeToList (Symbol -> SEnv (Int, Sort) -> Maybe (Int, Sort)
forall a. Symbol -> SEnv a -> Maybe a
F.lookupSEnv Symbol
y SEnv (Int, Sort)
env)
                            , Int
xi Int -> Int -> Bool
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] -> ElabM ExprInfo
applyKVars :: forall ann a.
CombinedEnv ann -> Sol a QBind -> [KVSub] -> ElabM ExprInfo
applyKVars CombinedEnv ann
g Sol a QBind
s [KVSub]
ks =
  (KVSub -> ElabM ExprInfo)
-> ([Expr] -> Expr)
-> ([KInfo] -> KInfo)
-> [KVSub]
-> ElabM ExprInfo
forall (m :: * -> *) a b c b1 c1.
Monad m =>
(a -> m (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> m (b1, c1)
mrExprInfosM (CombinedEnv ann -> Sol a QBind -> KVSub -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> ElabM ExprInfo
applyKVar CombinedEnv ann
g Sol a QBind
s) [Expr] -> Expr
F.pAndNoDedup [KInfo] -> KInfo
forall a. Monoid a => [a] -> a
mconcat [KVSub]
ks

applyKVar :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> ElabM ExprInfo
applyKVar :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> ElabM ExprInfo
applyKVar CombinedEnv ann
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 ann -> Sol a QBind -> KVSub -> Hyp -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Hyp -> ElabM ExprInfo
hypPred CombinedEnv ann
g Sol a QBind
s KVSub
ksu Hyp
cs
  Right QBind
eqs -> do [(Expr, EQual)]
qbp <- String -> Sol a QBind -> Subst -> QBind -> ElabM [(Expr, EQual)]
forall a.
String -> Sol a QBind -> Subst -> QBind -> ElabM [(Expr, EQual)]
Sol.qbPreds String
msg Sol a QBind
s (KVSub -> Subst
F.ksuSubst KVSub
ksu) QBind
eqs
                  ExprInfo -> ElabM ExprInfo
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([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
<$> [(Expr, EQual)]
qbp, 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 ann -> Cid
forall a. CombinedEnv a -> Cid
ceCid CombinedEnv ann
g)

mkNonCutsExpr :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Hyp -> ElabM F.Expr
mkNonCutsExpr :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVar -> Hyp -> ElabM Expr
mkNonCutsExpr CombinedEnv ann
ce Sol a QBind
s KVar
k Hyp
cs = do [Expr]
bcps <- (Cube -> ElabM Expr) -> Hyp -> ReaderT ElabFlags Identity [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (CombinedEnv ann -> Sol a QBind -> KVar -> Cube -> ElabM Expr
forall ann a.
CombinedEnv ann -> Sol a QBind -> KVar -> Cube -> ElabM Expr
bareCubePred CombinedEnv ann
ce Sol a QBind
s KVar
k) Hyp
cs
                             Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pOr [Expr]
bcps

nonCutsResult :: F.BindEnv ann -> Sol.Sol a Sol.QBind -> ElabM (M.HashMap F.KVar F.Expr)
nonCutsResult :: forall ann a.
BindEnv ann -> Sol a QBind -> ElabM (HashMap KVar Expr)
nonCutsResult BindEnv ann
be Sol a QBind
s = (KVar -> Hyp -> ElabM Expr)
-> HashMap KVar Hyp -> ElabM (HashMap KVar Expr)
forall (f :: * -> *) k v1 v2.
Applicative f =>
(k -> v1 -> f v2) -> HashMap k v1 -> f (HashMap k v2)
M.traverseWithKey (CombinedEnv ann -> Sol a QBind -> KVar -> Hyp -> ElabM Expr
forall ann a.
CombinedEnv ann -> Sol a QBind -> KVar -> Hyp -> ElabM Expr
mkNonCutsExpr CombinedEnv ann
g Sol a QBind
s) (HashMap KVar Hyp -> ElabM (HashMap KVar Expr))
-> HashMap KVar Hyp -> ElabM (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
    g :: CombinedEnv ann
g = Cid
-> BindEnv ann
-> IBindEnv
-> SrcSpan
-> IBindEnv
-> CombinedEnv ann
forall a.
Cid
-> BindEnv a -> IBindEnv -> SrcSpan -> IBindEnv -> CombinedEnv a
CEnv Cid
forall a. Maybe a
Nothing BindEnv ann
be IBindEnv
F.emptyIBindEnv SrcSpan
F.dummySpan IBindEnv
F.emptyIBindEnv


-- | 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 -> ElabM F.Expr
bareCubePred :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVar -> Cube -> ElabM Expr
bareCubePred CombinedEnv ann
g Sol a QBind
s KVar
k Cube
c =
  do ([(Symbol, Sort)]
xts, Expr
psu) <- SymEnv
-> SEnv Sort
-> CombinedEnv ann
-> KVar
-> Subst
-> ElabM ([(Symbol, Sort)], Expr)
forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ElabM ([(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 ann
g' KVar
k Subst
su
     (Expr
p, KInfo
_kI) <- CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
apply CombinedEnv ann
g' Sol a QBind
s IBindEnv
bs'
     Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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)
  where
    bs :: IBindEnv
bs = Cube -> IBindEnv
Sol.cuBinds Cube
c
    su :: Subst
su = Cube -> Subst
Sol.cuSubst Cube
c
    g' :: CombinedEnv ann
g' = CombinedEnv ann -> IBindEnv -> CombinedEnv ann
forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv  CombinedEnv ann
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 ann -> IBindEnv -> [(Symbol, Sort)]
forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv ann
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)

hypPred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp -> ElabM ExprInfo
hypPred :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Hyp -> ElabM ExprInfo
hypPred CombinedEnv ann
g Sol a QBind
s KVSub
ksu Hyp
hyp =
  do [ExprInfo]
cs <- (Cube -> ElabM ExprInfo)
-> Hyp -> ReaderT ElabFlags Identity [ExprInfo]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (CombinedEnv ann -> Sol a QBind -> KVSub -> Cube -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Cube -> ElabM ExprInfo
cubePred CombinedEnv ann
g Sol a QBind
s KVSub
ksu) Hyp
hyp
     ExprInfo -> ElabM ExprInfo
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExprInfo -> ElabM ExprInfo) -> ExprInfo -> ElabM ExprInfo
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pOr ([Expr] -> Expr)
-> ([KInfo] -> KInfo) -> ([Expr], [KInfo]) -> ExprInfo
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [KInfo] -> KInfo
mconcatPlus (([Expr], [KInfo]) -> ExprInfo) -> ([Expr], [KInfo]) -> ExprInfo
forall a b. (a -> b) -> a -> b
$ [ExprInfo] -> ([Expr], [KInfo])
forall a b. [(a, b)] -> ([a], [b])
unzip [ExprInfo]
cs

{- | `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 -> ElabM F.Expr
elabExist :: forall a.
SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> ElabM Expr
elabExist SrcSpan
sp Sol a QBind
s [(Symbol, Sort)]
xts Expr
p =
  do ElabFlags
ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     let elab :: Sort -> Sort
elab = ElabParam -> Sort -> Sort
forall a. Elaborate a => ElabParam -> a -> a
So.elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
So.ElabParam ElabFlags
ef (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
sp String
"elabExist") SymEnv
env)
     let xts' :: [(Symbol, Sort)]
xts' = [ (Symbol
x, Sort -> Sort
elab Sort
t) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts]
     Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
F.pExist [(Symbol, Sort)]
xts' Expr
p
  where
    env :: SymEnv
env = Sol a QBind -> SymEnv
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 -> ElabM ExprInfo
cubePred :: forall ann a.
CombinedEnv ann -> Sol a QBind -> KVSub -> Cube -> ElabM ExprInfo
cubePred CombinedEnv ann
g Sol a QBind
s KVSub
ksu Cube
c    =
  do (([(Symbol, Sort)]
xts,Expr
psu,Expr
p), KInfo
kI) <- CombinedEnv ann
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> ElabM (([(Symbol, Sort)], Expr, Expr), KInfo)
forall ann a.
CombinedEnv ann
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> ElabM (([(Symbol, Sort)], Expr, Expr), KInfo)
cubePredExc CombinedEnv ann
g Sol a QBind
s KVSub
ksu Cube
c IBindEnv
bs'
     Expr
e <- String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
F.notracepp String
"cubePred" (Expr -> Expr) -> ElabM Expr -> ElabM Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> ElabM Expr
forall a.
SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> ElabM Expr
elabExist SrcSpan
sp Sol a QBind
s [(Symbol, Sort)]
xts (Expr
psu Expr -> Expr -> Expr
&.& Expr
p)
     ExprInfo -> ElabM ExprInfo
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
e , KInfo
kI)
  where
    sp :: SrcSpan
sp  = CombinedEnv ann -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv ann
g
    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 ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> F.IBindEnv
            -> ElabM ((Binders, F.Pred, F.Pred), KInfo)
cubePredExc :: forall ann a.
CombinedEnv ann
-> Sol a QBind
-> KVSub
-> Cube
-> IBindEnv
-> ElabM (([(Symbol, Sort)], Expr, Expr), KInfo)
cubePredExc CombinedEnv ann
g Sol a QBind
s KVSub
ksu Cube
c IBindEnv
bs' =
  do ([(Symbol, Sort)]
xts, Expr
psu)  <- SymEnv
-> SEnv Sort
-> CombinedEnv ann
-> KVar
-> Subst
-> ElabM ([(Symbol, Sort)], Expr)
forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ElabM ([(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 ann
g  KVar
k Subst
su
     ([(Symbol, Sort)]
_  , Expr
psu') <- SymEnv
-> SEnv Sort
-> CombinedEnv ann
-> KVar
-> Subst
-> ElabM ([(Symbol, Sort)], Expr)
forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ElabM ([(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 ann
g' KVar
k Subst
su'
     (Expr
p', KInfo
kI)    <- CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
forall ann a.
CombinedEnv ann -> Sol a QBind -> IBindEnv -> ElabM ExprInfo
apply CombinedEnv ann
g' Sol a QBind
s IBindEnv
bs'
     Expr
cubeE       <- SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> ElabM Expr
forall a.
SrcSpan -> Sol a QBind -> [(Symbol, Sort)] -> Expr -> ElabM Expr
elabExist SrcSpan
sp Sol a QBind
s [(Symbol, Sort)]
yts' ([Expr] -> Expr
F.pAndNoDedup [Expr
p', Expr
psu'])
     let cubeP :: ([(Symbol, Sort)], Expr, Expr)
cubeP = ([(Symbol, Sort)]
xts, Expr
psu, Expr
cubeE)
     (([(Symbol, Sort)], Expr, Expr), KInfo)
-> ElabM (([(Symbol, Sort)], Expr, Expr), KInfo)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([(Symbol, Sort)], Expr, Expr)
cubeP, KInfo -> Tag -> KInfo
extendKInfo KInfo
kI (Cube -> Tag
Sol.cuTag Cube
c))
  where

    sp :: SrcSpan
sp              = CombinedEnv ann -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv ann
g
    yts' :: [(Symbol, Sort)]
yts'            = CombinedEnv ann -> IBindEnv -> [(Symbol, Sort)]
forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv ann
g IBindEnv
bs'
    g' :: CombinedEnv ann
g'              = CombinedEnv ann -> IBindEnv -> CombinedEnv ann
forall a. CombinedEnv a -> IBindEnv -> CombinedEnv a
addCEnv  CombinedEnv ann
g IBindEnv
bs
    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 a -> F.KVar -> F.Subst -> ElabM ([(F.Symbol, F.Sort)], F.Pred)
substElim :: forall a.
SymEnv
-> SEnv Sort
-> CombinedEnv a
-> KVar
-> Subst
-> ElabM ([(Symbol, Sort)], Expr)
substElim SymEnv
syEnv SEnv Sort
sEnv CombinedEnv a
g KVar
_ (F.Su HashMap Symbol Expr
m) =
    do [Expr]
p <- ((Symbol, Expr, Sort) -> ElabM Expr)
-> [(Symbol, Expr, Sort)] -> ReaderT ElabFlags Identity [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Symbol
x, Expr
e ,Sort
t) -> SrcSpan -> SymEnv -> Symbol -> Sort -> Expr -> Sort -> ElabM Expr
mkSubst SrcSpan
sp SymEnv
syEnv Symbol
x (SEnv Sort -> Symbol -> Sort
substSort SEnv Sort
sEnv Symbol
x) Expr
e Sort
t) [(Symbol, Expr, Sort)]
xets
       ([(Symbol, Sort)], Expr) -> ElabM ([(Symbol, Sort)], Expr)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Symbol, Sort)]
xts, [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd [Expr]
p)
  where
    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)]
    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 a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan CombinedEnv a
g
    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 a -> SEnv Sort
forall a. CombinedEnv a -> SEnv Sort
combinedSEnv CombinedEnv a
g

substSort :: F.SEnv F.Sort -> F.Symbol -> F.Sort
substSort :: SEnv Sort -> Symbol -> Sort
substSort SEnv Sort
sEnv Symbol
sym = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Symbol -> Sort
forall {a} {a}. PPrint a => a -> a
err Symbol
sym) (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
sym 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.substSort: 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 -> ElabM F.Expr
mkSubst :: SrcSpan -> SymEnv -> Symbol -> Sort -> Expr -> Sort -> ElabM 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 -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EEq Expr
ex Expr
ey
  | Bool
otherwise   = do Expr
ex' <- SrcSpan -> SymEnv -> Expr -> Sort -> ElabM Expr
elabToInt SrcSpan
sp SymEnv
env Expr
ex Sort
tx
                     Expr
ey' <- SrcSpan -> SymEnv -> Expr -> Sort -> ElabM Expr
elabToInt SrcSpan
sp SymEnv
env Expr
ey Sort
ty
                     Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ {- F.tracepp _msg $ -} Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
F.EEq Expr
ex' Expr
ey'
  where
    -- _msg        = "mkSubst-DIFF: tx = " ++ F.showpp tx ++ " ty = " ++ F.showpp ty
    --                                     ++ " ex' = " ++ F.showpp ex' ++ " ey' = " ++ F.showpp ey'
    ex :: Expr
ex          = Symbol -> Expr
forall a. Expression a => a -> Expr
F.expr Symbol
x

elabToInt :: F.SrcSpan -> F.SymEnv -> F.Expr -> F.Sort -> ElabM F.Expr
elabToInt :: SrcSpan -> SymEnv -> Expr -> Sort -> ElabM Expr
elabToInt SrcSpan
sp SymEnv
env Expr
e Sort
s =
  do ElabFlags
ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     Expr -> ElabM Expr
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ElabM Expr) -> Expr -> ElabM Expr
forall a b. (a -> b) -> a -> b
$ ElabParam -> Expr -> Expr
forall a. Elaborate a => ElabParam -> a -> a
So.elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
So.ElabParam ElabFlags
ef (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

combinedSEnv :: CombinedEnv a -> F.SEnv F.Sort
combinedSEnv :: forall a. CombinedEnv a -> SEnv Sort
combinedSEnv CombinedEnv a
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 a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs BindEnv a
be IBindEnv
bs)
  where
    be :: BindEnv a
be         = CombinedEnv a -> BindEnv a
forall a. CombinedEnv a -> BindEnv a
ceBEnv CombinedEnv a
g
    bs :: IBindEnv
bs         = CombinedEnv a -> IBindEnv
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 = F.unionIBindEnv (ceIEnv g) 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       = 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 a -> F.IBindEnv -> [(F.Symbol, F.Sort)]
symSorts :: forall a. CombinedEnv a -> IBindEnv -> [(Symbol, Sort)]
symSorts CombinedEnv a
g IBindEnv
bs = (SortedReft -> Sort) -> (Symbol, SortedReft) -> (Symbol, Sort)
forall b c d. (b -> c) -> (d, b) -> (d, c)
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 a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (CombinedEnv a -> BindEnv a
forall a. CombinedEnv a -> BindEnv a
ceBEnv CombinedEnv a
g) IBindEnv
bs

_noKvars :: F.Expr -> Bool
_noKvars :: Expr -> Bool
_noKvars = [KVar] -> Bool
forall a. [a] -> 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]
forall v. ExprV v -> [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
(KInfo -> KInfo -> Bool) -> (KInfo -> KInfo -> Bool) -> Eq KInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KInfo -> KInfo -> Bool
== :: KInfo -> KInfo -> Bool
$c/= :: KInfo -> KInfo -> Bool
/= :: 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
$ccompare :: KInfo -> KInfo -> Ordering
compare :: KInfo -> KInfo -> Ordering
$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
>= :: KInfo -> KInfo -> Bool
$cmax :: KInfo -> KInfo -> KInfo
max :: KInfo -> KInfo -> KInfo
$cmin :: KInfo -> KInfo -> KInfo
min :: KInfo -> KInfo -> KInfo
Ord, Int -> KInfo -> String -> String
[KInfo] -> String -> String
KInfo -> String
(Int -> KInfo -> String -> String)
-> (KInfo -> String) -> ([KInfo] -> String -> String) -> Show KInfo
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> KInfo -> String -> String
showsPrec :: Int -> KInfo -> String -> String
$cshow :: KInfo -> String
show :: KInfo -> String
$cshowList :: [KInfo] -> String -> String
showList :: [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     = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max        (KInfo -> Int
kiDepth KInfo
ki) (KInfo -> Int
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  = [Tag] -> Int -> Integer -> KInfo
KI [] Int
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 = kiCubes ki + kiCubes ki'}

mconcatPlus :: [KInfo] -> KInfo
mconcatPlus :: [KInfo] -> KInfo
mconcatPlus = (KInfo -> KInfo -> KInfo) -> KInfo -> [KInfo] -> KInfo
forall a b. (a -> b -> b) -> b -> [a] -> b
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 :: [Tag] -> [Tag] -> [Tag]
appendTags [Tag]
ts [Tag]
ts' = [Tag] -> [Tag]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Tag]
ts [Tag] -> [Tag] -> [Tag]
forall a. [a] -> [a] -> [a]
++ [Tag]
ts')

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

mrExprInfosM :: Monad m => (a -> m (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> m (b1, c1)
mrExprInfosM :: forall (m :: * -> *) a b c b1 c1.
Monad m =>
(a -> m (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> m (b1, c1)
mrExprInfosM a -> m (b, c)
mF [b] -> b1
erF [c] -> c1
irF [a]
xs =
  do [(b, c)]
bcs <- (a -> m (b, c)) -> [a] -> m [(b, c)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse a -> m (b, c)
mF [a]
xs
     let ([b]
es, [c]
is) = [(b, c)] -> ([b], [c])
forall a b. [(a, b)] -> ([a], [b])
unzip [(b, c)]
bcs
     (b1, c1) -> m (b1, c1)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([b] -> b1
erF [b]
es, [c] -> c1
irF [c]
is)

--------------------------------------------------------------------------------
-- | `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 = [((Int, Symbol), SimpC ())] -> [(Int, EbindSol)]
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) <- SInfo a -> [(Int, Integer, Symbol)]
forall a. SInfo a -> [(Int, Integer, Symbol)]
ebindDefs SInfo a
si]
  where cons :: Integer -> SimpC ()
cons Integer
cid = SimpC a -> SimpC ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (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 -> (Symbol -> EbindSol) -> (a, Symbol) -> (a, EbindSol)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
Bifunctor.second ([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), 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. HasCallStack => [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 :: 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      <- Maybe Int -> Tag
forall a. Maybe a -> [a]
maybeToList (Symbol -> HashMap Symbol Int -> Maybe Int
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   = SInfo a -> HashMap Symbol Int
forall a. SInfo a -> HashMap Symbol Int
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 :: forall a. SInfo a -> HashMap Symbol Int
ebindSyms SInfo a
si = [(Symbol, Int)] -> HashMap Symbol Int
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
xi, Int
bi) | Int
bi        <- SInfo a -> Tag
forall (c :: * -> *) a. GInfo c a -> Tag
ebinds SInfo a
si
                                     , let (Symbol
xi,SortedReft
_,a
_) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv Int
bi BindEnv a
be ]
  where
    be :: BindEnv a
be       = SInfo a -> BindEnv a
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) <- 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 a -> SimpC a -> Maybe Symbol
forall a. BindEnv a -> SimpC a -> Maybe Symbol
cstrDef BindEnv a
be SimpC a
c) ]
  where
    be :: BindEnv a
be      = SInfo a -> BindEnv a
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 = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x
  | Bool
otherwise            = Maybe Symbol
forall a. Maybe a
Nothing
  where
    (Symbol
v,SortedReft
_,a
_)              = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
F.lookupBindEnv (SimpC a -> Int
forall a. SimpC a -> Int
cbind SimpC a
c) BindEnv a
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]
++ Tag -> String
forall a. Show a => a -> String
show (SimpC a -> Tag
forall (c :: * -> *) a. TaggedC c a => c a -> Tag
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)