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

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

    -- * Update Solution
  , Sol.update

  -- * Lookup Solution
  , lhsPred
  ) where

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

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

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


--------------------------------------------------------------------------------
-- | Initial Solution (from Qualifiers and WF constraints) ---------------------
--------------------------------------------------------------------------------
init :: (F.Fixpoint a) => Config -> F.SInfo a -> S.HashSet F.KVar -> Sol.Solution
--------------------------------------------------------------------------------
init :: Config -> SInfo a -> HashSet KVar -> Solution
init Config
cfg SInfo a
si HashSet KVar
ks = SymEnv
-> [(KVar, ())]
-> [(KVar, QBind)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(BindId, EbindSol)]
-> SEnv (BindId, Sort)
-> Solution
forall a b.
SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(BindId, EbindSol)]
-> SEnv (BindId, Sort)
-> Sol a b
Sol.fromList SymEnv
senv [(KVar, ())]
forall a. Monoid a => a
mempty [(KVar, QBind)]
keqs [] HashMap KVar IBindEnv
forall a. Monoid a => a
mempty [(BindId, EbindSol)]
ebs SEnv (BindId, Sort)
xEnv
  where
    keqs :: [(KVar, QBind)]
keqs       = (WfC a -> (KVar, QBind)) -> [WfC a] -> [(KVar, QBind)]
forall a b. (a -> b) -> [a] -> [b]
map (SInfo a -> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, QBind)
forall a.
SInfo a -> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, QBind)
refine SInfo a
si [Qualifier]
qs SEnv Sort
genv) [WfC a]
ws [(KVar, QBind)] -> Strategy [(KVar, QBind)] -> [(KVar, QBind)]
forall a. a -> Strategy a -> a
`using` Strategy (KVar, QBind) -> Strategy [(KVar, QBind)]
forall a. Strategy a -> Strategy [a]
parList Strategy (KVar, QBind)
forall a. NFData a => Strategy a
rdeepseq
    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]
    genv :: SEnv Sort
genv       = SInfo a -> SEnv Sort
forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si
    senv :: SymEnv
senv       = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si
    ebs :: [(BindId, EbindSol)]
ebs        = SInfo a -> [(BindId, EbindSol)]
forall a. SInfo a -> [(BindId, EbindSol)]
ebindInfo SInfo a
si
    xEnv :: SEnv (BindId, Sort)
xEnv       = [(Symbol, (BindId, Sort))] -> SEnv (BindId, Sort)
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv [ (Symbol
x, (BindId
i, SortedReft -> Sort
F.sr_sort SortedReft
sr)) | (BindId
i,Symbol
x,SortedReft
sr) <- BindEnv -> [(BindId, Symbol, SortedReft)]
F.bindEnvToList (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
si)]

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

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


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

--------------------------------------------------------------------------------
instK :: Bool
      -> F.SEnv F.Sort
      -> F.Symbol
      -> F.Sort
      -> [F.Qualifier]
      -> Sol.QBind
--------------------------------------------------------------------------------
instK :: Bool -> SEnv Sort -> Symbol -> Sort -> [Qualifier] -> QBind
instK Bool
ho SEnv Sort
env Symbol
v Sort
t = [EQual] -> QBind
Sol.qb ([EQual] -> QBind)
-> ([Qualifier] -> [EQual]) -> [Qualifier] -> QBind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [EQual] -> [EQual]
unique ([EQual] -> [EQual])
-> ([Qualifier] -> [EQual]) -> [Qualifier] -> [EQual]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Qualifier -> [EQual]) -> [Qualifier] -> [EQual]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> SEnv Sort -> Symbol -> Sort -> Qualifier -> [EQual]
instKQ Bool
ho SEnv Sort
env Symbol
v Sort
t)
  where
    unique :: [EQual] -> [EQual]
unique       = (EQual -> EQual -> Bool) -> [EQual] -> [EQual]
forall a. (a -> a -> Bool) -> [a] -> [a]
L.nubBy (((Expr -> Bool) -> (EQual -> Expr) -> EQual -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Expr
Sol.eqPred) ((Expr -> Bool) -> EQual -> Bool)
-> (EQual -> Expr -> Bool) -> EQual -> EQual -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Expr -> Expr -> Bool) -> (EQual -> Expr) -> EQual -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Expr
Sol.eqPred)

instKQ :: Bool
       -> F.SEnv F.Sort
       -> F.Symbol
       -> F.Sort
       -> F.Qualifier
       -> [Sol.EQual]
instKQ :: Bool -> SEnv Sort -> Symbol -> Sort -> Qualifier -> [EQual]
instKQ Bool
ho SEnv Sort
env Symbol
v Sort
t Qualifier
q = do 
  (TVSubst
su0, QPSubst
qsu0, Symbol
v0) <- Env
-> [(Sort, [Symbol])] -> QualParam -> [(TVSubst, QPSubst, Symbol)]
candidates Env
senv [(Sort
t, [Symbol
v])] QualParam
qp
  [Symbol]
xs              <- Env -> [(Sort, [Symbol])] -> [Symbol] -> [QualParam] -> [[Symbol]]
match Env
senv [(Sort, [Symbol])]
tyss [Symbol
v0] (TVSubst -> QPSubst -> QualParam -> QualParam
applyQP TVSubst
su0 QPSubst
qsu0 (QualParam -> QualParam) -> [QualParam] -> [QualParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
qps) 
  EQual -> [EQual]
forall (m :: * -> *) a. Monad m => a -> m a
return           (EQual -> [EQual]) -> EQual -> [EQual]
forall a b. (a -> b) -> a -> b
$ Qualifier -> [Symbol] -> EQual
Sol.eQual Qualifier
q (String -> [Symbol] -> [Symbol]
forall a. PPrint a => String -> a -> a
F.notracepp String
msg ([Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
xs))
  where
    msg :: String
msg        = String
"instKQ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp (Qualifier -> Symbol
F.qName Qualifier
q) String -> String -> String
forall a. [a] -> [a] -> [a]
++ [QualParam] -> String
forall a. PPrint a => a -> String
F.showpp (Qualifier -> [QualParam]
F.qParams Qualifier
q)
    QualParam
qp : [QualParam]
qps   = Qualifier -> [QualParam]
F.qParams Qualifier
q
    tyss :: [(Sort, [Symbol])]
tyss       = Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env
    senv :: Env
senv       = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`F.lookupSEnvWithDistance` SEnv Sort
env)

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

match :: So.Env -> [(F.Sort, [F.Symbol])] -> [F.Symbol] -> [F.QualParam] -> [[F.Symbol]]
match :: Env -> [(Sort, [Symbol])] -> [Symbol] -> [QualParam] -> [[Symbol]]
match Env
env [(Sort, [Symbol])]
tyss [Symbol]
xs (QualParam
qp : [QualParam]
qps)
  = do (TVSubst
su, QPSubst
qsu, Symbol
x) <- Env
-> [(Sort, [Symbol])] -> QualParam -> [(TVSubst, QPSubst, Symbol)]
candidates Env
env [(Sort, [Symbol])]
tyss QualParam
qp
       Env -> [(Sort, [Symbol])] -> [Symbol] -> [QualParam] -> [[Symbol]]
match Env
env [(Sort, [Symbol])]
tyss (Symbol
x Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
xs) (TVSubst -> QPSubst -> QualParam -> QualParam
applyQP TVSubst
su QPSubst
qsu (QualParam -> QualParam) -> [QualParam] -> [QualParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [QualParam]
qps)
match Env
_   [(Sort, [Symbol])]
_   [Symbol]
xs []
  = [Symbol] -> [[Symbol]]
forall (m :: * -> *) a. Monad m => a -> m a
return [Symbol]
xs

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

--------------------------------------------------------------------------------
candidates :: So.Env -> [(F.Sort, [F.Symbol])] -> F.QualParam 
           -> [(So.TVSubst, QPSubst, F.Symbol)]
--------------------------------------------------------------------------------
candidates :: Env
-> [(Sort, [Symbol])] -> QualParam -> [(TVSubst, QPSubst, Symbol)]
candidates Env
env [(Sort, [Symbol])]
tyss QualParam
x = -- traceShow _msg
    [(TVSubst
su, QPSubst
qsu, Symbol
y) | (Sort
t, [Symbol]
ys)  <- [(Sort, [Symbol])]
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)
                  , Symbol
y        <- [Symbol]
ys
                  , QPSubst
qsu      <- Maybe QPSubst -> [QPSubst]
forall a. Maybe a -> [a]
maybeToList (QualParam -> Symbol -> Maybe QPSubst
matchSym QualParam
x Symbol
y)                                     
    ]
  where
    xt :: Sort
xt   = QualParam -> Sort
F.qpSort QualParam
x
    mono :: Bool
mono = Sort -> Bool
So.isMono Sort
xt
    _msg :: String
_msg = String
"candidates tyss :=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Sort, [Symbol])] -> String
forall a. PPrint a => a -> String
F.showpp [(Sort, [Symbol])]
tyss String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"tx := " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sort -> String
forall a. PPrint a => a -> String
F.showpp Sort
xt

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


data QPSubst = NoSub | JustSub Int F.Symbol  

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

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


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

data CombinedEnv = CEnv 
  { CombinedEnv -> Cid
ceCid  :: !Cid
  , CombinedEnv -> BindEnv
ceBEnv :: !F.BindEnv
  , CombinedEnv -> IBindEnv
ceIEnv :: !F.IBindEnv 
  , CombinedEnv -> SrcSpan
ceSpan :: !F.SrcSpan
  }

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

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

apply :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ExprInfo
apply :: CombinedEnv -> Sol a QBind -> IBindEnv -> (Expr, KInfo)
apply CombinedEnv
g Sol a QBind
s IBindEnv
bs      = (ListNE Expr -> Expr
F.pAnd (Expr
pksExpr -> ListNE Expr -> ListNE Expr
forall a. a -> [a] -> [a]
:ListNE Expr
ps), KInfo
kI)
  where
    (Expr
pks, KInfo
kI)     = CombinedEnv -> Sol a QBind -> [KVSub] -> (Expr, KInfo)
forall a. CombinedEnv -> Sol a QBind -> [KVSub] -> (Expr, KInfo)
applyKVars CombinedEnv
g Sol a QBind
s [KVSub]
ks  
    (ListNE Expr
ps,  [KVSub]
ks, [KVSub]
_)  = CombinedEnv
-> Sol a QBind -> IBindEnv -> (ListNE Expr, [KVSub], [KVSub])
forall a.
CombinedEnv
-> Sol a QBind -> IBindEnv -> (ListNE Expr, [KVSub], [KVSub])
envConcKVars CombinedEnv
g Sol a QBind
s IBindEnv
bs


envConcKVars :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ([F.Expr], [F.KVSub], [F.KVSub])
envConcKVars :: CombinedEnv
-> Sol a QBind -> IBindEnv -> (ListNE Expr, [KVSub], [KVSub])
envConcKVars CombinedEnv
g Sol a QBind
s IBindEnv
bs = ([ListNE Expr] -> ListNE Expr
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ListNE 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
    ([ListNE Expr]
pss, [[KVSub]]
kss, [[KVSub]]
gss) = [(ListNE Expr, [KVSub], [KVSub])]
-> ([ListNE Expr], [[KVSub]], [[KVSub]])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [ String
-> (ListNE Expr, [KVSub], [KVSub])
-> (ListNE 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) ((ListNE Expr, [KVSub], [KVSub])
 -> (ListNE Expr, [KVSub], [KVSub]))
-> (ListNE Expr, [KVSub], [KVSub])
-> (ListNE Expr, [KVSub], [KVSub])
forall a b. (a -> b) -> a -> b
$ Symbol -> SortedReft -> (ListNE Expr, [KVSub], [KVSub])
F.sortedReftConcKVars Symbol
x SortedReft
sr | (Symbol
x, SortedReft
sr) <- [(Symbol, SortedReft)]
xrs ]
    xrs :: [(Symbol, SortedReft)]
xrs             = CombinedEnv -> Sol a QBind -> BindId -> (Symbol, SortedReft)
forall a.
CombinedEnv -> Sol a QBind -> BindId -> (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv
g Sol a QBind
s (BindId -> (Symbol, SortedReft))
-> [BindId] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BindId]
is
    is :: [BindId]
is              = IBindEnv -> [BindId]
F.elemsIBindEnv IBindEnv
bs

lookupBindEnvExt :: CombinedEnv -> Sol.Sol a Sol.QBind -> F.BindId -> (F.Symbol, F.SortedReft)
lookupBindEnvExt :: CombinedEnv -> Sol a QBind -> BindId -> (Symbol, SortedReft)
lookupBindEnvExt CombinedEnv
g Sol a QBind
s BindId
i 
  | Just Expr
p <- CombinedEnv -> Sol a QBind -> BindId -> Maybe Expr
forall a. CombinedEnv -> Sol a QBind -> BindId -> Maybe Expr
ebSol CombinedEnv
g Sol a QBind
s BindId
i = (Symbol
x, SortedReft
sr { sr_reft :: Reft
F.sr_reft = (Symbol, Expr) -> Reft
F.Reft (Symbol
x, Expr
p) }) 
  | Bool
otherwise             = (Symbol
x, SortedReft
sr)
   where 
      (Symbol
x, SortedReft
sr)              = BindId -> BindEnv -> (Symbol, SortedReft)
F.lookupBindEnv BindId
i (CombinedEnv -> BindEnv
ceBEnv CombinedEnv
g) 

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

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

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

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

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

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

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

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

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

        (k . su)

      defined by using cube

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

      in the binder environment `g`.

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

 -}

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

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

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

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

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

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

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

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

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

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

       x1:t1 ... xn:tn

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

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

     Finally, we filter out binders if they are

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

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

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


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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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