{-# LANGUAGE CPP                        #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE PatternGuards              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE DeriveDataTypeable         #-}

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

-- | This module contains the top-level SOLUTION data types,
--   including various indices used for solving.

module Language.Fixpoint.Types.Solutions (

  -- * Solution tables
    Solution
  , Sol (..)
  , CMap

  -- * Solution elements
  , Hyp, Cube (..), QBind (..)
  , EQual (..)

  -- * Equal elements
  , eQual
  , trueEqual

  , qbExprs

  -- * Solution Candidates (move to SolverMonad?)
  , Cand

  -- * Update
  , update

  -- * Lookup
  , lookupQBind
  , lookup

  -- * Manipulating QBind
  , qb
  , qbPreds
  , qbFilter
  , qbFilterM


  -- * Conversion for client
  , result 

  -- * "Fast" Solver (DEPRECATED as unsound)
  , Index  (..)
  , KIndex (..)
  , BindPred (..)
  , BIndex (..)
  ) where

import           Prelude hiding (lookup)
import           GHC.Generics
import           Control.DeepSeq
import           Data.Hashable
import qualified Data.Maybe                 as Mb
import qualified Data.HashMap.Strict        as M
import qualified Data.List                  as L
import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           Control.Monad (filterM)
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.Sorts
import           Language.Fixpoint.Types.Refinements
import           Language.Fixpoint.Types.Environments
import           Language.Fixpoint.Types.Constraints
import           Language.Fixpoint.Types.Substitutions
import           Text.PrettyPrint.HughesPJ.Compat

--------------------------------------------------------------------------------
-- | Update Solution
--
-- @update s kqs@ sets in @s@ each KVar in @kqs@ to the corresponding QBind.
--
-- Yields a pair @(b, s')@ where @b@ is true if the mapping of any KVar was
-- changed.
--
-- Precondition: @kqs@ contains no duplicate KVars.
--
update :: Sol QBind -> [(KVar, QBind)] -> (Bool, Sol QBind)
--------------------------------------------------------------------------------
update :: Sol QBind -> [(KVar, QBind)] -> (Bool, Sol QBind)
update Sol QBind
s [(KVar, QBind)]
kqs = ((Bool, Sol QBind) -> (KVar, QBind) -> (Bool, Sol QBind))
-> (Bool, Sol QBind) -> [(KVar, QBind)] -> (Bool, Sol QBind)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (Bool, Sol QBind) -> (KVar, QBind) -> (Bool, Sol QBind)
step (Bool
False, Sol QBind
s) [(KVar, QBind)]
kqs
  where
    step :: (Bool, Sol QBind) -> (KVar, QBind) -> (Bool, Sol QBind)
    step :: (Bool, Sol QBind) -> (KVar, QBind) -> (Bool, Sol QBind)
step (Bool
changed, Sol QBind
s) (KVar
k, QBind
qs) = (Bool
changed Bool -> Bool -> Bool
|| Bool
distinctSizes, KVar -> QBind -> Sol QBind -> Sol QBind
forall a. KVar -> a -> Sol a -> Sol a
updateK KVar
k QBind
qs Sol QBind
s)
      where
        oldQs :: QBind
oldQs = Sol QBind -> KVar -> QBind
lookupQBind Sol QBind
s KVar
k
        distinctSizes :: Bool
distinctSizes = QBind -> Int
qbSize QBind
oldQs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= QBind -> Int
qbSize QBind
qs

--------------------------------------------------------------------------------
-- | The `Solution` data type --------------------------------------------------
--------------------------------------------------------------------------------
type Solution  = Sol QBind
newtype QBind  = QB [EQual]   deriving (Int -> QBind -> ShowS
[QBind] -> ShowS
QBind -> [Char]
(Int -> QBind -> ShowS)
-> (QBind -> [Char]) -> ([QBind] -> ShowS) -> Show QBind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QBind -> ShowS
showsPrec :: Int -> QBind -> ShowS
$cshow :: QBind -> [Char]
show :: QBind -> [Char]
$cshowList :: [QBind] -> ShowS
showList :: [QBind] -> ShowS
Show, Typeable QBind
Typeable QBind =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QBind -> c QBind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QBind)
-> (QBind -> Constr)
-> (QBind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QBind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind))
-> ((forall b. Data b => b -> b) -> QBind -> QBind)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r)
-> (forall u. (forall d. Data d => d -> u) -> QBind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QBind -> m QBind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBind -> m QBind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBind -> m QBind)
-> Data QBind
QBind -> Constr
QBind -> DataType
(forall b. Data b => b -> b) -> QBind -> QBind
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
forall u. (forall d. Data d => d -> u) -> QBind -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
$ctoConstr :: QBind -> Constr
toConstr :: QBind -> Constr
$cdataTypeOf :: QBind -> DataType
dataTypeOf :: QBind -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
$cgmapT :: (forall b. Data b => b -> b) -> QBind -> QBind
gmapT :: (forall b. Data b => b -> b) -> QBind -> QBind
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
Data, Typeable, (forall x. QBind -> Rep QBind x)
-> (forall x. Rep QBind x -> QBind) -> Generic QBind
forall x. Rep QBind x -> QBind
forall x. QBind -> Rep QBind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. QBind -> Rep QBind x
from :: forall x. QBind -> Rep QBind x
$cto :: forall x. Rep QBind x -> QBind
to :: forall x. Rep QBind x -> QBind
Generic, QBind -> QBind -> Bool
(QBind -> QBind -> Bool) -> (QBind -> QBind -> Bool) -> Eq QBind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QBind -> QBind -> Bool
== :: QBind -> QBind -> Bool
$c/= :: QBind -> QBind -> Bool
/= :: QBind -> QBind -> Bool
Eq)

qb :: [EQual] -> QBind
qb :: [EQual] -> QBind
qb = [EQual] -> QBind
QB

qbEQuals :: QBind -> [EQual]
qbEQuals :: QBind -> [EQual]
qbEQuals (QB [EQual]
xs) = [EQual]
xs

qbExprs :: QBind -> [Expr]
qbExprs :: QBind -> [ExprV Symbol]
qbExprs (QB [EQual]
xs) = EQual -> ExprV Symbol
eqPred (EQual -> ExprV Symbol) -> [EQual] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [EQual]
xs

qbSize :: QBind -> Int
qbSize :: QBind -> Int
qbSize = [EQual] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([EQual] -> Int) -> (QBind -> [EQual]) -> QBind -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals

qbFilter :: (EQual -> Bool) -> QBind -> QBind
qbFilter :: (EQual -> Bool) -> QBind -> QBind
qbFilter EQual -> Bool
f (QB [EQual]
eqs) = [EQual] -> QBind
QB ((EQual -> Bool) -> [EQual] -> [EQual]
forall a. (a -> Bool) -> [a] -> [a]
filter EQual -> Bool
f [EQual]
eqs)

qbFilterM :: Monad m => (EQual -> m Bool) -> QBind -> m QBind
qbFilterM :: forall (m :: * -> *).
Monad m =>
(EQual -> m Bool) -> QBind -> m QBind
qbFilterM EQual -> m Bool
f (QB [EQual]
eqs) = [EQual] -> QBind
QB ([EQual] -> QBind) -> m [EQual] -> m QBind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EQual -> m Bool) -> [EQual] -> m [EQual]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM EQual -> m Bool
f [EQual]
eqs

instance NFData QBind

instance PPrint QBind where
  pprintTidy :: Tidy -> QBind -> Doc
pprintTidy Tidy
k = Tidy -> [EQual] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ([EQual] -> Doc) -> (QBind -> [EQual]) -> QBind -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals

--------------------------------------------------------------------------------
-- | A `Sol` contains the various indices needed to compute a solution,
--   in particular, to compute `lhsPred` for any given constraint.
--------------------------------------------------------------------------------
data Sol a = Sol
  { forall a. Sol a -> HashMap KVar a
sMap :: !(M.HashMap KVar a)          -- ^ Actual solution (for cut kvar)
  , forall a. Sol a -> HashMap KVar Hyp
sHyp :: !(M.HashMap KVar Hyp)        -- ^ Defining cubes  (for non-cut kvar)
  , forall a. Sol a -> HashMap KVar IBindEnv
sScp :: !(M.HashMap KVar IBindEnv)   -- ^ Set of binders which are in scope for every
                                         -- occurrence of the kvar
  } deriving ((forall x. Sol a -> Rep (Sol a) x)
-> (forall x. Rep (Sol a) x -> Sol a) -> Generic (Sol a)
forall x. Rep (Sol a) x -> Sol a
forall x. Sol a -> Rep (Sol a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Sol a) x -> Sol a
forall a x. Sol a -> Rep (Sol a) x
$cfrom :: forall a x. Sol a -> Rep (Sol a) x
from :: forall x. Sol a -> Rep (Sol a) x
$cto :: forall a x. Rep (Sol a) x -> Sol a
to :: forall x. Rep (Sol a) x -> Sol a
Generic)

deriving instance NFData a => NFData (Sol a)

instance Semigroup (Sol a) where
  Sol a
s1 <> :: Sol a -> Sol a -> Sol a
<> Sol a
s2 = Sol { sMap :: HashMap KVar a
sMap  = Sol a -> HashMap KVar a
forall a. Sol a -> HashMap KVar a
sMap Sol a
s1  HashMap KVar a -> HashMap KVar a -> HashMap KVar a
forall a. Semigroup a => a -> a -> a
<> Sol a -> HashMap KVar a
forall a. Sol a -> HashMap KVar a
sMap Sol a
s2
                 , sHyp :: HashMap KVar Hyp
sHyp  = Sol a -> HashMap KVar Hyp
forall a. Sol a -> HashMap KVar Hyp
sHyp Sol a
s1  HashMap KVar Hyp -> HashMap KVar Hyp -> HashMap KVar Hyp
forall a. Semigroup a => a -> a -> a
<> Sol a -> HashMap KVar Hyp
forall a. Sol a -> HashMap KVar Hyp
sHyp Sol a
s2
                 , sScp :: HashMap KVar IBindEnv
sScp  = Sol a -> HashMap KVar IBindEnv
forall a. Sol a -> HashMap KVar IBindEnv
sScp Sol a
s1  HashMap KVar IBindEnv
-> HashMap KVar IBindEnv -> HashMap KVar IBindEnv
forall a. Semigroup a => a -> a -> a
<> Sol a -> HashMap KVar IBindEnv
forall a. Sol a -> HashMap KVar IBindEnv
sScp Sol a
s2
                 }

instance Monoid (Sol a) where
  mempty :: Sol a
mempty = Sol { sMap :: HashMap KVar a
sMap = HashMap KVar a
forall a. Monoid a => a
mempty
               , sHyp :: HashMap KVar Hyp
sHyp = HashMap KVar Hyp
forall a. Monoid a => a
mempty
               , sScp :: HashMap KVar IBindEnv
sScp = HashMap KVar IBindEnv
forall a. Monoid a => a
mempty
               }
  mappend :: Sol a -> Sol a -> Sol a
mappend = Sol a -> Sol a -> Sol a
forall a. Semigroup a => a -> a -> a
(<>)

instance Functor Sol where
  fmap :: forall a b. (a -> b) -> Sol a -> Sol b
fmap a -> b
f (Sol HashMap KVar a
s HashMap KVar Hyp
m1 HashMap KVar IBindEnv
m2) = HashMap KVar b
-> HashMap KVar Hyp -> HashMap KVar IBindEnv -> Sol b
forall a.
HashMap KVar a
-> HashMap KVar Hyp -> HashMap KVar IBindEnv -> Sol a
Sol (a -> b
f (a -> b) -> HashMap KVar a -> HashMap KVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar a
s) HashMap KVar Hyp
m1 HashMap KVar IBindEnv
m2

instance PPrint a => PPrint (Sol a) where
  pprintTidy :: Tidy -> Sol a -> Doc
pprintTidy Tidy
k Sol a
s = [Doc] -> Doc
vcat [ Doc
"sMap :=" Doc -> Doc -> Doc
<+> Tidy -> HashMap KVar a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Sol a -> HashMap KVar a
forall a. Sol a -> HashMap KVar a
sMap Sol a
s) ]

--------------------------------------------------------------------------------
-- | A `Cube` is a single constraint defining a KVar ---------------------------
--------------------------------------------------------------------------------
type Hyp      = ListNE Cube

data Cube = Cube
  { Cube -> IBindEnv
cuBinds :: IBindEnv  -- ^ Binders       from defining Env
  , Cube -> Subst
cuSubst :: Subst     -- ^ Substitutions from cstrs    Rhs
  , Cube -> SubcId
cuId    :: SubcId    -- ^ Id            of   defining Cstr
  , Cube -> Tag
cuTag   :: Tag       -- ^ Tag           of   defining Cstr (DEBUG)
  } deriving ((forall x. Cube -> Rep Cube x)
-> (forall x. Rep Cube x -> Cube) -> Generic Cube
forall x. Rep Cube x -> Cube
forall x. Cube -> Rep Cube x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Cube -> Rep Cube x
from :: forall x. Cube -> Rep Cube x
$cto :: forall x. Rep Cube x -> Cube
to :: forall x. Rep Cube x -> Cube
Generic, Cube -> ()
(Cube -> ()) -> NFData Cube
forall a. (a -> ()) -> NFData a
$crnf :: Cube -> ()
rnf :: Cube -> ()
NFData)

instance PPrint Cube where
  pprintTidy :: Tidy -> Cube -> Doc
pprintTidy Tidy
_ Cube
c = Doc
"Cube" Doc -> Doc -> Doc
<+> SubcId -> Doc
forall a. PPrint a => a -> Doc
pprint (Cube -> SubcId
cuId Cube
c)

instance Show Cube where
  show :: Cube -> [Char]
show = Cube -> [Char]
forall a. PPrint a => a -> [Char]
showpp
--------------------------------------------------------------------------------
result :: Sol QBind -> M.HashMap KVar Expr
--------------------------------------------------------------------------------
result :: Sol QBind -> HashMap KVar (ExprV Symbol)
result Sol QBind
s = [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([ExprV Symbol] -> ExprV Symbol)
-> (QBind -> [ExprV Symbol]) -> QBind -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EQual -> ExprV Symbol) -> [EQual] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> ExprV Symbol
eqPred ([EQual] -> [ExprV Symbol])
-> (QBind -> [EQual]) -> QBind -> [ExprV Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals (QBind -> ExprV Symbol)
-> HashMap KVar QBind -> HashMap KVar (ExprV Symbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sol QBind -> HashMap KVar QBind
forall a. Sol a -> HashMap KVar a
sMap Sol QBind
s


--------------------------------------------------------------------------------
qbPreds :: Subst -> QBind -> [(Pred, EQual)]
--------------------------------------------------------------------------------
qbPreds :: Subst -> QBind -> [(ExprV Symbol, EQual)]
qbPreds Subst
su (QB [EQual]
eqs) =  [ (Subst -> ExprV Symbol -> ExprV Symbol
forall a. (Subable a, ?callStack::CallStack) => Subst -> a -> a
subst Subst
su (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ EQual -> ExprV Symbol
eqPred EQual
eq, EQual
eq) | EQual
eq <- [EQual]
eqs ]

--------------------------------------------------------------------------------
-- | Read / Write Solution at KVar ---------------------------------------------
--------------------------------------------------------------------------------
lookupQBind :: Sol QBind -> KVar -> QBind
--------------------------------------------------------------------------------
lookupQBind :: Sol QBind -> KVar -> QBind
lookupQBind Sol QBind
s KVar
k = {- tracepp _msg $ -} QBind -> Maybe QBind -> QBind
forall a. a -> Maybe a -> a
Mb.fromMaybe ([EQual] -> QBind
QB []) (Sol QBind -> KVar -> Maybe QBind
lookupElab Sol QBind
s KVar
k)
  where
    _msg :: [Char]
_msg        = [Char]
"lookupQB: k = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ KVar -> [Char]
forall a. Show a => a -> [Char]
show KVar
k

--------------------------------------------------------------------------------
lookup :: Sol QBind -> KVar -> Either Hyp QBind
--------------------------------------------------------------------------------
lookup :: Sol QBind -> KVar -> Either Hyp QBind
lookup Sol QBind
s KVar
k
  | Just Hyp
cs  <- KVar -> HashMap KVar Hyp -> Maybe Hyp
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup KVar
k (Sol QBind -> HashMap KVar Hyp
forall a. Sol a -> HashMap KVar Hyp
sHyp Sol QBind
s) -- non-cut variable, return its cubes
  = Hyp -> Either Hyp QBind
forall a b. a -> Either a b
Left Hyp
cs
  | Just QBind
eqs <- Sol QBind -> KVar -> Maybe QBind
lookupElab Sol QBind
s KVar
k
  = QBind -> Either Hyp QBind
forall a b. b -> Either a b
Right QBind
eqs                 -- TODO: don't initialize kvars that have a hyp solution
  | Bool
otherwise
  = [Char] -> Either Hyp QBind
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Either Hyp QBind) -> [Char] -> Either Hyp QBind
forall a b. (a -> b) -> a -> b
$ [Char]
"solLookup: Unknown kvar " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ KVar -> [Char]
forall a. Show a => a -> [Char]
show KVar
k

lookupElab :: Sol QBind -> KVar -> Maybe QBind
lookupElab :: Sol QBind -> KVar -> Maybe QBind
lookupElab Sol QBind
s KVar
k = KVar -> HashMap KVar QBind -> Maybe QBind
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup KVar
k (Sol QBind -> HashMap KVar QBind
forall a. Sol a -> HashMap KVar a
sMap Sol QBind
s)

--------------------------------------------------------------------------------
updateK :: KVar -> a -> Sol a -> Sol a
--------------------------------------------------------------------------------
updateK :: forall a. KVar -> a -> Sol a -> Sol a
updateK KVar
k a
qs Sol a
s = Sol a
s { sMap = M.insert k qs (sMap s)
--                 , sBot = M.delete k    (sBot s)
                   }


--------------------------------------------------------------------------------
-- | A `Cand` is an association list indexed by predicates
--------------------------------------------------------------------------------
type Cand a   = [(Expr, a)]


--------------------------------------------------------------------------------
-- | Instantiated Qualifiers ---------------------------------------------------
--------------------------------------------------------------------------------
data EQual = EQL
  { EQual -> Qualifier
eqQual :: !Qualifier
  , EQual -> ExprV Symbol
eqPred  :: !Expr      -- ^ predicate obtained by instantiating the qualifier
  , EQual -> [ExprV Symbol]
_eqArgs :: ![Expr]    -- ^ actual arguments used to instantiate the qualifier
  } deriving (EQual -> EQual -> Bool
(EQual -> EQual -> Bool) -> (EQual -> EQual -> Bool) -> Eq EQual
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EQual -> EQual -> Bool
== :: EQual -> EQual -> Bool
$c/= :: EQual -> EQual -> Bool
/= :: EQual -> EQual -> Bool
Eq, Int -> EQual -> ShowS
[EQual] -> ShowS
EQual -> [Char]
(Int -> EQual -> ShowS)
-> (EQual -> [Char]) -> ([EQual] -> ShowS) -> Show EQual
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EQual -> ShowS
showsPrec :: Int -> EQual -> ShowS
$cshow :: EQual -> [Char]
show :: EQual -> [Char]
$cshowList :: [EQual] -> ShowS
showList :: [EQual] -> ShowS
Show, Typeable EQual
Typeable EQual =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EQual -> c EQual)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EQual)
-> (EQual -> Constr)
-> (EQual -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EQual))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual))
-> ((forall b. Data b => b -> b) -> EQual -> EQual)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r)
-> (forall u. (forall d. Data d => d -> u) -> EQual -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> EQual -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EQual -> m EQual)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EQual -> m EQual)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EQual -> m EQual)
-> Data EQual
EQual -> Constr
EQual -> DataType
(forall b. Data b => b -> b) -> EQual -> EQual
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> EQual -> u
forall u. (forall d. Data d => d -> u) -> EQual -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EQual
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EQual -> c EQual
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EQual)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EQual -> c EQual
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EQual -> c EQual
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EQual
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EQual
$ctoConstr :: EQual -> Constr
toConstr :: EQual -> Constr
$cdataTypeOf :: EQual -> DataType
dataTypeOf :: EQual -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EQual)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EQual)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual)
$cgmapT :: (forall b. Data b => b -> b) -> EQual -> EQual
gmapT :: (forall b. Data b => b -> b) -> EQual -> EQual
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EQual -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> EQual -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EQual -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EQual -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
Data, Typeable, (forall x. EQual -> Rep EQual x)
-> (forall x. Rep EQual x -> EQual) -> Generic EQual
forall x. Rep EQual x -> EQual
forall x. EQual -> Rep EQual x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. EQual -> Rep EQual x
from :: forall x. EQual -> Rep EQual x
$cto :: forall x. Rep EQual x -> EQual
to :: forall x. Rep EQual x -> EQual
Generic)

instance Loc EQual where
  srcSpan :: EQual -> SrcSpan
srcSpan = Qualifier -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan (Qualifier -> SrcSpan) -> (EQual -> Qualifier) -> EQual -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Qualifier
eqQual

trueEqual :: EQual
trueEqual :: EQual
trueEqual = Qualifier -> ExprV Symbol -> [ExprV Symbol] -> EQual
EQL Qualifier
trueQual ExprV Symbol
forall v. ExprV v
PTrue []

instance PPrint EQual where
  pprintTidy :: Tidy -> EQual -> Doc
pprintTidy Tidy
k = Tidy -> ExprV Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (ExprV Symbol -> Doc) -> (EQual -> ExprV Symbol) -> EQual -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> ExprV Symbol
eqPred

instance NFData EQual

-- | @eQual q xs@ instantiates @q@ with the arguments in @xs@
eQual :: Qualifier -> [Symbol] -> EQual
eQual :: Qualifier -> [Symbol] -> EQual
eQual Qualifier
q [Symbol]
xs = {- tracepp "eQual" $ -} Qualifier -> ExprV Symbol -> [ExprV Symbol] -> EQual
EQL Qualifier
q ExprV Symbol
p [ExprV Symbol]
es
  where
    p :: ExprV Symbol
p      = Subst -> ExprV Symbol -> ExprV Symbol
forall a. (Subable a, ?callStack::CallStack) => Subst -> a -> a
subst Subst
su (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$  Qualifier -> ExprV Symbol
forall v. QualifierV v -> ExprV v
qBody Qualifier
q
    su :: Subst
su     = [(Symbol, ExprV Symbol)] -> Subst
mkSubst  ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$  [Char] -> [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b.
(?callStack::CallStack) =>
[Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"eQual" [Symbol]
qxs [ExprV Symbol]
es
    es :: [ExprV Symbol]
es     = Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar    (Symbol -> ExprV Symbol) -> [Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
    qxs :: [Symbol]
qxs    = QualParam -> Symbol
qpSym   (QualParam -> Symbol) -> [QualParam] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
forall v. QualifierV v -> [QualParam]
qParams Qualifier
q

--------------------------------------------------------------------------------
-- | A KIndex uniquely identifies each *use* of a KVar in an (LHS) binder
--------------------------------------------------------------------------------
data KIndex = KIndex { KIndex -> Int
kiBIndex :: !BindId
                     , KIndex -> Int
kiPos    :: !Int
                     , KIndex -> KVar
kiKVar   :: !KVar
                     }
              deriving (KIndex -> KIndex -> Bool
(KIndex -> KIndex -> Bool)
-> (KIndex -> KIndex -> Bool) -> Eq KIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KIndex -> KIndex -> Bool
== :: KIndex -> KIndex -> Bool
$c/= :: KIndex -> KIndex -> Bool
/= :: KIndex -> KIndex -> Bool
Eq, Eq KIndex
Eq KIndex =>
(KIndex -> KIndex -> Ordering)
-> (KIndex -> KIndex -> Bool)
-> (KIndex -> KIndex -> Bool)
-> (KIndex -> KIndex -> Bool)
-> (KIndex -> KIndex -> Bool)
-> (KIndex -> KIndex -> KIndex)
-> (KIndex -> KIndex -> KIndex)
-> Ord KIndex
KIndex -> KIndex -> Bool
KIndex -> KIndex -> Ordering
KIndex -> KIndex -> KIndex
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 :: KIndex -> KIndex -> Ordering
compare :: KIndex -> KIndex -> Ordering
$c< :: KIndex -> KIndex -> Bool
< :: KIndex -> KIndex -> Bool
$c<= :: KIndex -> KIndex -> Bool
<= :: KIndex -> KIndex -> Bool
$c> :: KIndex -> KIndex -> Bool
> :: KIndex -> KIndex -> Bool
$c>= :: KIndex -> KIndex -> Bool
>= :: KIndex -> KIndex -> Bool
$cmax :: KIndex -> KIndex -> KIndex
max :: KIndex -> KIndex -> KIndex
$cmin :: KIndex -> KIndex -> KIndex
min :: KIndex -> KIndex -> KIndex
Ord, Int -> KIndex -> ShowS
[KIndex] -> ShowS
KIndex -> [Char]
(Int -> KIndex -> ShowS)
-> (KIndex -> [Char]) -> ([KIndex] -> ShowS) -> Show KIndex
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KIndex -> ShowS
showsPrec :: Int -> KIndex -> ShowS
$cshow :: KIndex -> [Char]
show :: KIndex -> [Char]
$cshowList :: [KIndex] -> ShowS
showList :: [KIndex] -> ShowS
Show, (forall x. KIndex -> Rep KIndex x)
-> (forall x. Rep KIndex x -> KIndex) -> Generic KIndex
forall x. Rep KIndex x -> KIndex
forall x. KIndex -> Rep KIndex x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. KIndex -> Rep KIndex x
from :: forall x. KIndex -> Rep KIndex x
$cto :: forall x. Rep KIndex x -> KIndex
to :: forall x. Rep KIndex x -> KIndex
Generic)

instance Hashable KIndex

instance PPrint KIndex where
  pprintTidy :: Tidy -> KIndex -> Doc
pprintTidy Tidy
_ = KIndex -> Doc
forall a. Show a => a -> Doc
tshow

--------------------------------------------------------------------------------
-- | A BIndex is created for each LHS Bind or RHS constraint
--------------------------------------------------------------------------------
data BIndex    = Root
               | Bind !BindId
               | Cstr !SubcId
                 deriving (BIndex -> BIndex -> Bool
(BIndex -> BIndex -> Bool)
-> (BIndex -> BIndex -> Bool) -> Eq BIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BIndex -> BIndex -> Bool
== :: BIndex -> BIndex -> Bool
$c/= :: BIndex -> BIndex -> Bool
/= :: BIndex -> BIndex -> Bool
Eq, Eq BIndex
Eq BIndex =>
(BIndex -> BIndex -> Ordering)
-> (BIndex -> BIndex -> Bool)
-> (BIndex -> BIndex -> Bool)
-> (BIndex -> BIndex -> Bool)
-> (BIndex -> BIndex -> Bool)
-> (BIndex -> BIndex -> BIndex)
-> (BIndex -> BIndex -> BIndex)
-> Ord BIndex
BIndex -> BIndex -> Bool
BIndex -> BIndex -> Ordering
BIndex -> BIndex -> BIndex
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 :: BIndex -> BIndex -> Ordering
compare :: BIndex -> BIndex -> Ordering
$c< :: BIndex -> BIndex -> Bool
< :: BIndex -> BIndex -> Bool
$c<= :: BIndex -> BIndex -> Bool
<= :: BIndex -> BIndex -> Bool
$c> :: BIndex -> BIndex -> Bool
> :: BIndex -> BIndex -> Bool
$c>= :: BIndex -> BIndex -> Bool
>= :: BIndex -> BIndex -> Bool
$cmax :: BIndex -> BIndex -> BIndex
max :: BIndex -> BIndex -> BIndex
$cmin :: BIndex -> BIndex -> BIndex
min :: BIndex -> BIndex -> BIndex
Ord, Int -> BIndex -> ShowS
[BIndex] -> ShowS
BIndex -> [Char]
(Int -> BIndex -> ShowS)
-> (BIndex -> [Char]) -> ([BIndex] -> ShowS) -> Show BIndex
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BIndex -> ShowS
showsPrec :: Int -> BIndex -> ShowS
$cshow :: BIndex -> [Char]
show :: BIndex -> [Char]
$cshowList :: [BIndex] -> ShowS
showList :: [BIndex] -> ShowS
Show, (forall x. BIndex -> Rep BIndex x)
-> (forall x. Rep BIndex x -> BIndex) -> Generic BIndex
forall x. Rep BIndex x -> BIndex
forall x. BIndex -> Rep BIndex x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BIndex -> Rep BIndex x
from :: forall x. BIndex -> Rep BIndex x
$cto :: forall x. Rep BIndex x -> BIndex
to :: forall x. Rep BIndex x -> BIndex
Generic)

instance Hashable BIndex

instance PPrint BIndex where
  pprintTidy :: Tidy -> BIndex -> Doc
pprintTidy Tidy
_ = BIndex -> Doc
forall a. Show a => a -> Doc
tshow

--------------------------------------------------------------------------------
-- | Each `Bind` corresponds to a conjunction of a `bpConc` and `bpKVars`
--------------------------------------------------------------------------------
data BindPred  = BP
  { BindPred -> ExprV Symbol
bpConc :: !Pred                  -- ^ Concrete predicate (PTrue o)
  , BindPred -> [KIndex]
bpKVar :: ![KIndex]              -- ^ KVar-Subst pairs
  } deriving (Int -> BindPred -> ShowS
[BindPred] -> ShowS
BindPred -> [Char]
(Int -> BindPred -> ShowS)
-> (BindPred -> [Char]) -> ([BindPred] -> ShowS) -> Show BindPred
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BindPred -> ShowS
showsPrec :: Int -> BindPred -> ShowS
$cshow :: BindPred -> [Char]
show :: BindPred -> [Char]
$cshowList :: [BindPred] -> ShowS
showList :: [BindPred] -> ShowS
Show)

instance PPrint BindPred where
  pprintTidy :: Tidy -> BindPred -> Doc
pprintTidy Tidy
_ = BindPred -> Doc
forall a. Show a => a -> Doc
tshow


--------------------------------------------------------------------------------
-- | A Index is a suitably indexed version of the cosntraints that lets us
--   1. CREATE a monolithic "background formula" representing all constraints,
--   2. ASSERT each lhs via bits for the subc-id and formulas for dependent cut KVars
--------------------------------------------------------------------------------
data Index = FastIdx
  { Index -> Int |-> BindPred
bindExpr   :: !(BindId |-> BindPred) -- ^ BindPred for each BindId
  , Index -> KIndex |-> KVSub
kvUse      :: !(KIndex |-> KVSub)    -- ^ Definition of each `KIndex`
  , Index -> HashMap KVar Hyp
kvDef      :: !(KVar   |-> Hyp)      -- ^ Constraints defining each `KVar`
  , Index -> CMap IBindEnv
envBinds   :: !(CMap IBindEnv)       -- ^ Binders of each Subc
  , Index -> CMap [SubcId]
envTx      :: !(CMap [SubcId])       -- ^ Transitive closure oof all dependent binders
  , Index -> SEnv Sort
envSorts   :: !(SEnv Sort)           -- ^ Sorts for all symbols
  -- , bindPrev   :: !(BIndex |-> BIndex)   -- ^ "parent" (immediately dominating) binder
  -- , kvDeps     :: !(CMap [KIndex])       -- ^ List of (Cut) KVars on which a SubC depends
  }

type CMap a  = M.HashMap SubcId a