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

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

module Language.Fixpoint.Types.Solutions (

  -- * Solution tables
    Solution, GSolution
  , Sol (gMap, sEnv, sEbd, sxEnv)
  , updateGMap, updateGMapWithKey
  , sScp
  , CMap

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

  -- * Equal elements
  , eQual
  , trueEqual

  -- * Gradual Solution elements
  , qbToGb, gbToQbs, gbEquals, equalsGb, emptyGMap, qbExprs

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

  -- * Constructor
  , fromList

  -- * Update
  , update
  , updateEbind

  -- * Lookup
  , lookupQBind
  , lookup, glookup

  -- * Manipulating QBind
  , qb
  , qbPreds
  , qbFilter

  , gbFilterM

  -- * Conversion for client
  , result, resultGradual

  -- * "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)
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

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.Theories
import           Language.Fixpoint.Types.Refinements
import           Language.Fixpoint.Types.Environments
import           Language.Fixpoint.Types.Constraints
import           Language.Fixpoint.Types.Substitutions
import           Language.Fixpoint.SortCheck (elaborate)
import           Text.PrettyPrint.HughesPJ.Compat

--------------------------------------------------------------------------------
-- | Update Solution -----------------------------------------------------------
--------------------------------------------------------------------------------
update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
--------------------------------------------------------------------------------
update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
update Sol a QBind
s [KVar]
ks [(KVar, EQual)]
kqs = {- tracepp msg -} ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs, Sol a QBind
s')
  where
    kqss :: [(KVar, QBind)]
kqss        = [KVar] -> [(KVar, EQual)] -> [(KVar, QBind)]
groupKs [KVar]
ks [(KVar, EQual)]
kqs
    ([Bool]
bs, Sol a QBind
s')    = (Sol a QBind -> (KVar, QBind) -> (Bool, Sol a QBind))
-> Sol a QBind -> [(KVar, QBind)] -> ([Bool], Sol a QBind)
forall a b c. (a -> b -> (c, a)) -> a -> [b] -> ([c], a)
folds Sol a QBind -> (KVar, QBind) -> (Bool, Sol a QBind)
forall a. Sol a QBind -> (KVar, QBind) -> (Bool, Sol a QBind)
update1 Sol a QBind
s [(KVar, QBind)]
kqss
    -- msg      = printf "ks = %s, s = %s" (showpp ks) (showpp s)

folds   :: (a -> b -> (c, a)) -> a -> [b] -> ([c], a)
folds :: (a -> b -> (c, a)) -> a -> [b] -> ([c], a)
folds a -> b -> (c, a)
f a
b = (([c], a) -> b -> ([c], a)) -> ([c], a) -> [b] -> ([c], a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ([c], a) -> b -> ([c], a)
step ([], a
b)
  where
     step :: ([c], a) -> b -> ([c], a)
step ([c]
cs, a
acc) b
x = (c
cc -> [c] -> [c]
forall a. a -> [a] -> [a]
:[c]
cs, a
x')
       where
         (c
c, a
x')      = a -> b -> (c, a)
f a
acc b
x

groupKs :: [KVar] -> [(KVar, EQual)] -> [(KVar, QBind)]
groupKs :: [KVar] -> [(KVar, EQual)] -> [(KVar, QBind)]
groupKs [KVar]
ks [(KVar, EQual)]
kqs = [ (KVar
k, [EQual] -> QBind
QB [EQual]
eqs) | (KVar
k, [EQual]
eqs) <- HashMap KVar [EQual] -> [(KVar, [EQual])]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap KVar [EQual] -> [(KVar, [EQual])])
-> HashMap KVar [EQual] -> [(KVar, [EQual])]
forall a b. (a -> b) -> a -> b
$ HashMap KVar [EQual] -> [(KVar, EQual)] -> HashMap KVar [EQual]
forall k v.
(Eq k, Hashable k) =>
HashMap k [v] -> [(k, v)] -> HashMap k [v]
groupBase HashMap KVar [EQual]
m0 [(KVar, EQual)]
kqs ]
  where
    m0 :: HashMap KVar [EQual]
m0         = [(KVar, [EQual])] -> HashMap KVar [EQual]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(KVar, [EQual])] -> HashMap KVar [EQual])
-> [(KVar, [EQual])] -> HashMap KVar [EQual]
forall a b. (a -> b) -> a -> b
$ (,[]) (KVar -> (KVar, [EQual])) -> [KVar] -> [(KVar, [EQual])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [KVar]
ks

update1 :: Sol a QBind -> (KVar, QBind) -> (Bool, Sol a QBind)
update1 :: Sol a QBind -> (KVar, QBind) -> (Bool, Sol a QBind)
update1 Sol a QBind
s (KVar
k, QBind
qs) = (Bool
change, KVar -> QBind -> Sol a QBind -> Sol a QBind
forall a b. KVar -> a -> Sol b a -> Sol b a
updateK KVar
k QBind
qs Sol a QBind
s)
  where
    oldQs :: QBind
oldQs         = Sol a QBind -> KVar -> QBind
forall a. Sol a QBind -> KVar -> QBind
lookupQBind Sol a QBind
s KVar
k
    change :: Bool
change        = 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
type GSolution = Sol (((Symbol, Sort), Expr), GBind) QBind
newtype QBind  = QB [EQual]   deriving (Int -> QBind -> ShowS
[QBind] -> ShowS
QBind -> String
(Int -> QBind -> ShowS)
-> (QBind -> String) -> ([QBind] -> ShowS) -> Show QBind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QBind] -> ShowS
$cshowList :: [QBind] -> ShowS
show :: QBind -> String
$cshow :: QBind -> String
showsPrec :: Int -> QBind -> ShowS
$cshowsPrec :: Int -> QBind -> ShowS
Show, Typeable QBind
DataType
Constr
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 -> DataType
QBind -> Constr
(forall b. Data b => b -> b) -> QBind -> QBind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cQB :: Constr
$tQBind :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> QBind -> m QBind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapQi :: Int -> (forall d. Data d => d -> u) -> QBind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
gmapQ :: (forall d. Data d => d -> u) -> QBind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
gmapT :: (forall b. Data b => b -> b) -> QBind -> QBind
$cgmapT :: (forall b. Data b => b -> b) -> QBind -> QBind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c QBind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
dataTypeOf :: QBind -> DataType
$cdataTypeOf :: QBind -> DataType
toConstr :: QBind -> Constr
$ctoConstr :: QBind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
$cp1Data :: Typeable 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
$cto :: forall x. Rep QBind x -> QBind
$cfrom :: forall x. QBind -> Rep QBind x
Generic, QBind -> QBind -> Bool
(QBind -> QBind -> Bool) -> (QBind -> QBind -> Bool) -> Eq QBind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QBind -> QBind -> Bool
$c/= :: QBind -> QBind -> Bool
== :: QBind -> QBind -> Bool
$c== :: QBind -> QBind -> Bool
Eq)
newtype GBind  = GB [[EQual]] deriving (Int -> GBind -> ShowS
[GBind] -> ShowS
GBind -> String
(Int -> GBind -> ShowS)
-> (GBind -> String) -> ([GBind] -> ShowS) -> Show GBind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GBind] -> ShowS
$cshowList :: [GBind] -> ShowS
show :: GBind -> String
$cshow :: GBind -> String
showsPrec :: Int -> GBind -> ShowS
$cshowsPrec :: Int -> GBind -> ShowS
Show, Typeable GBind
DataType
Constr
Typeable GBind
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> GBind -> c GBind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c GBind)
-> (GBind -> Constr)
-> (GBind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c GBind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind))
-> ((forall b. Data b => b -> b) -> GBind -> GBind)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r)
-> (forall u. (forall d. Data d => d -> u) -> GBind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> GBind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> GBind -> m GBind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GBind -> m GBind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GBind -> m GBind)
-> Data GBind
GBind -> DataType
GBind -> Constr
(forall b. Data b => b -> b) -> GBind -> GBind
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GBind -> c GBind
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GBind
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) -> GBind -> u
forall u. (forall d. Data d => d -> u) -> GBind -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GBind -> m GBind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GBind -> m GBind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GBind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GBind -> c GBind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GBind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind)
$cGB :: Constr
$tGBind :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> GBind -> m GBind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GBind -> m GBind
gmapMp :: (forall d. Data d => d -> m d) -> GBind -> m GBind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GBind -> m GBind
gmapM :: (forall d. Data d => d -> m d) -> GBind -> m GBind
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GBind -> m GBind
gmapQi :: Int -> (forall d. Data d => d -> u) -> GBind -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GBind -> u
gmapQ :: (forall d. Data d => d -> u) -> GBind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GBind -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
gmapT :: (forall b. Data b => b -> b) -> GBind -> GBind
$cgmapT :: (forall b. Data b => b -> b) -> GBind -> GBind
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c GBind)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GBind)
dataTypeOf :: GBind -> DataType
$cdataTypeOf :: GBind -> DataType
toConstr :: GBind -> Constr
$ctoConstr :: GBind -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GBind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GBind
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GBind -> c GBind
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GBind -> c GBind
$cp1Data :: Typeable GBind
Data, Typeable, (forall x. GBind -> Rep GBind x)
-> (forall x. Rep GBind x -> GBind) -> Generic GBind
forall x. Rep GBind x -> GBind
forall x. GBind -> Rep GBind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GBind x -> GBind
$cfrom :: forall x. GBind -> Rep GBind x
Generic)

emptyGMap :: GSolution -> GSolution
emptyGMap :: GSolution -> GSolution
emptyGMap GSolution
sol = GSolution
-> ((((Symbol, Sort), Expr), GBind)
    -> (((Symbol, Sort), Expr), GBind))
-> GSolution
forall b a. Sol b a -> (b -> b) -> Sol b a
mapGMap GSolution
sol (\(((Symbol, Sort), Expr)
x,GBind
_) -> (((Symbol, Sort), Expr)
x, [[EQual]] -> GBind
GB []))

updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution
updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution
updateGMapWithKey [(KVar, QBind)]
kqs GSolution
sol = GSolution
sol {gMap :: HashMap KVar (((Symbol, Sort), Expr), GBind)
gMap =  (HashMap KVar (((Symbol, Sort), Expr), GBind)
 -> (KVar, QBind) -> HashMap KVar (((Symbol, Sort), Expr), GBind))
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
-> [(KVar, QBind)]
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\HashMap KVar (((Symbol, Sort), Expr), GBind)
m (KVar
k, (QB [EQual]
eq)) -> ((((Symbol, Sort), Expr), GBind)
 -> (((Symbol, Sort), Expr), GBind))
-> KVar
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust (\(((Symbol, Sort), Expr)
x, GB [[EQual]]
eqs) -> (((Symbol, Sort), Expr)
x, [[EQual]] -> GBind
GB (if [EQual]
eq [EQual] -> [[EQual]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[EQual]]
eqs then [[EQual]]
eqs else [EQual]
eq[EQual] -> [[EQual]] -> [[EQual]]
forall a. a -> [a] -> [a]
:[[EQual]]
eqs))) KVar
k HashMap KVar (((Symbol, Sort), Expr), GBind)
m) (GSolution -> HashMap KVar (((Symbol, Sort), Expr), GBind)
forall b a. Sol b a -> HashMap KVar b
gMap GSolution
sol) [(KVar, QBind)]
kqs }

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 -> [Expr]
qbExprs (QB [EQual]
xs) = EQual -> Expr
eqPred (EQual -> Expr) -> [EQual] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [EQual]
xs

qbToGb :: QBind -> GBind
qbToGb :: QBind -> GBind
qbToGb (QB [EQual]
xs) = [[EQual]] -> GBind
GB ([[EQual]] -> GBind) -> [[EQual]] -> GBind
forall a b. (a -> b) -> a -> b
$ (EQual -> [EQual]) -> [EQual] -> [[EQual]]
forall a b. (a -> b) -> [a] -> [b]
map (EQual -> [EQual] -> [EQual]
forall a. a -> [a] -> [a]
:[]) [EQual]
xs

gbToQbs :: GBind -> [QBind]
gbToQbs :: GBind -> [QBind]
gbToQbs (GB [])  = [[EQual] -> QBind
QB [EQual
trueEqual]]
gbToQbs (GB [[EQual]]
ess) = [EQual] -> QBind
QB ([EQual] -> QBind) -> [[EQual]] -> [QBind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[EQual]]
ess

gbEquals :: GBind -> [[EQual]]
gbEquals :: GBind -> [[EQual]]
gbEquals (GB [[EQual]]
eqs) = [[EQual]]
eqs

equalsGb :: [[EQual]] -> GBind
equalsGb :: [[EQual]] -> GBind
equalsGb = [[EQual]] -> GBind
GB

gbFilterM :: Monad m => ([EQual] -> m Bool) -> GBind -> m GBind
gbFilterM :: ([EQual] -> m Bool) -> GBind -> m GBind
gbFilterM [EQual] -> m Bool
f (GB [[EQual]]
eqs) = [[EQual]] -> GBind
GB ([[EQual]] -> GBind) -> m [[EQual]] -> m GBind
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

qbSize :: QBind -> Int
qbSize :: QBind -> Int
qbSize = [EQual] -> 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)

instance NFData QBind
instance NFData GBind

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

--------------------------------------------------------------------------------
-- | An `EbindSol` contains the relevant information for an existential-binder;
--   (See tests/pos/ebind-*.fq for examples.) This is either 
--   1. the constraint whose HEAD is a singleton that defines the binder, OR 
--   2. the solved out TERM that we should use in place of the ebind at USES.
--------------------------------------------------------------------------------
data EbindSol
  = EbDef [SimpC ()] Symbol -- ^ The constraint whose HEAD "defines" the Ebind
                             -- and the @Symbol@ for that EBind
  | EbSol Expr             -- ^ The solved out term that should be used at USES.
  | EbIncr                 -- ^ EBinds not to be solved for (because they're currently being solved for)
   deriving (Int -> EbindSol -> ShowS
[EbindSol] -> ShowS
EbindSol -> String
(Int -> EbindSol -> ShowS)
-> (EbindSol -> String) -> ([EbindSol] -> ShowS) -> Show EbindSol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EbindSol] -> ShowS
$cshowList :: [EbindSol] -> ShowS
show :: EbindSol -> String
$cshow :: EbindSol -> String
showsPrec :: Int -> EbindSol -> ShowS
$cshowsPrec :: Int -> EbindSol -> ShowS
Show, (forall x. EbindSol -> Rep EbindSol x)
-> (forall x. Rep EbindSol x -> EbindSol) -> Generic EbindSol
forall x. Rep EbindSol x -> EbindSol
forall x. EbindSol -> Rep EbindSol x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep EbindSol x -> EbindSol
$cfrom :: forall x. EbindSol -> Rep EbindSol x
Generic, EbindSol -> ()
(EbindSol -> ()) -> NFData EbindSol
forall a. (a -> ()) -> NFData a
rnf :: EbindSol -> ()
$crnf :: EbindSol -> ()
NFData)

instance PPrint EbindSol where 
  pprintTidy :: Tidy -> EbindSol -> Doc
pprintTidy Tidy
k (EbDef [SimpC ()]
i Symbol
x) = Doc
"EbDef:" Doc -> Doc -> Doc
<+> Tidy -> [SimpC ()] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [SimpC ()]
i Doc -> Doc -> Doc
<+> Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
x
  pprintTidy Tidy
k (EbSol Expr
e)   = Doc
"EbSol:" Doc -> Doc -> Doc
<+> Tidy -> Expr -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
e
  pprintTidy Tidy
_ (EbindSol
EbIncr)    = Doc
"EbIncr"

--------------------------------------------------------------------------------
updateEbind :: Sol a b -> BindId -> Pred -> Sol a b 
--------------------------------------------------------------------------------
updateEbind :: Sol a b -> Int -> Expr -> Sol a b
updateEbind Sol a b
s Int
i !Expr
e = case Int -> HashMap Int EbindSol -> Maybe EbindSol
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i (Sol a b -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
sEbd Sol a b
s) of 
  Maybe EbindSol
Nothing         -> String -> Sol a b
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> Sol a b) -> String -> Sol a b
forall a b. (a -> b) -> a -> b
$ String
"updateEBind: Unknown ebind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  Just (EbSol Expr
e0) -> String -> Sol a b
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> Sol a b) -> String -> Sol a b
forall a b. (a -> b) -> a -> b
$ String
"updateEBind: Re-assigning ebind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with solution: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e0 
  Just EbindSol
_          -> Sol a b
s { sEbd :: HashMap Int EbindSol
sEbd = Int -> EbindSol -> HashMap Int EbindSol -> HashMap Int EbindSol
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Int
i (Expr -> EbindSol
EbSol Expr
e) (Sol a b -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
sEbd Sol a b
s) }
    
--------------------------------------------------------------------------------
-- | A `Sol` contains the various indices needed to compute a solution,
--   in particular, to compute `lhsPred` for any given constraint.
--------------------------------------------------------------------------------
data Sol b a = Sol
  { Sol b a -> SymEnv
sEnv :: !SymEnv                      -- ^ Environment used to elaborate solutions
  , Sol b a -> HashMap KVar a
sMap :: !(M.HashMap KVar a)          -- ^ Actual solution (for cut kvar)
  , Sol b a -> HashMap KVar b
gMap :: !(M.HashMap KVar b)          -- ^ Solution for gradual variables
  , Sol b a -> HashMap KVar Hyp
sHyp :: !(M.HashMap KVar Hyp)        -- ^ Defining cubes  (for non-cut kvar)
  , Sol b a -> HashMap KVar IBindEnv
sScp :: !(M.HashMap KVar IBindEnv)   -- ^ Set of allowed binders for kvar
  , Sol b a -> HashMap Int EbindSol
sEbd :: !(M.HashMap BindId EbindSol) -- ^ EbindSol for each existential binder
  , Sol b a -> SEnv (Int, Sort)
sxEnv :: !(SEnv (BindId, Sort))      --   TODO: merge with sEnv? used for sorts of ebinds to solve ebinds in lhsPred
  } deriving ((forall x. Sol b a -> Rep (Sol b a) x)
-> (forall x. Rep (Sol b a) x -> Sol b a) -> Generic (Sol b a)
forall x. Rep (Sol b a) x -> Sol b a
forall x. Sol b a -> Rep (Sol b a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall b a x. Rep (Sol b a) x -> Sol b a
forall b a x. Sol b a -> Rep (Sol b a) x
$cto :: forall b a x. Rep (Sol b a) x -> Sol b a
$cfrom :: forall b a x. Sol b a -> Rep (Sol b a) x
Generic)

deriving instance (NFData b, NFData a) => NFData (Sol b a)

updateGMap :: Sol b a -> M.HashMap KVar b -> Sol b a
updateGMap :: Sol b a -> HashMap KVar b -> Sol b a
updateGMap Sol b a
sol HashMap KVar b
gmap = Sol b a
sol {gMap :: HashMap KVar b
gMap = HashMap KVar b
gmap}

mapGMap :: Sol b a -> (b -> b) -> Sol b a
mapGMap :: Sol b a -> (b -> b) -> Sol b a
mapGMap Sol b a
sol b -> b
f = Sol b a
sol {gMap :: HashMap KVar b
gMap = (b -> b) -> HashMap KVar b -> HashMap KVar b
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map b -> b
f (Sol b a -> HashMap KVar b
forall b a. Sol b a -> HashMap KVar b
gMap Sol b a
sol)}

instance Semigroup (Sol a b) where
  Sol a b
s1 <> :: Sol a b -> Sol a b -> Sol a b
<> Sol a b
s2 = Sol :: forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol b a
Sol { sEnv :: SymEnv
sEnv  = (Sol a b -> SymEnv
forall b a. Sol b a -> SymEnv
sEnv Sol a b
s1)  SymEnv -> SymEnv -> SymEnv
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> SymEnv
forall b a. Sol b a -> SymEnv
sEnv Sol a b
s2)
                 , sMap :: HashMap KVar b
sMap  = (Sol a b -> HashMap KVar b
forall b a. Sol b a -> HashMap KVar a
sMap Sol a b
s1)  HashMap KVar b -> HashMap KVar b -> HashMap KVar b
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> HashMap KVar b
forall b a. Sol b a -> HashMap KVar a
sMap Sol a b
s2)
                 , gMap :: HashMap KVar a
gMap  = (Sol a b -> HashMap KVar a
forall b a. Sol b a -> HashMap KVar b
gMap Sol a b
s1)  HashMap KVar a -> HashMap KVar a -> HashMap KVar a
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> HashMap KVar a
forall b a. Sol b a -> HashMap KVar b
gMap Sol a b
s2)
                 , sHyp :: HashMap KVar Hyp
sHyp  = (Sol a b -> HashMap KVar Hyp
forall b a. Sol b a -> HashMap KVar Hyp
sHyp Sol a b
s1)  HashMap KVar Hyp -> HashMap KVar Hyp -> HashMap KVar Hyp
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> HashMap KVar Hyp
forall b a. Sol b a -> HashMap KVar Hyp
sHyp Sol a b
s2)
                 , sScp :: HashMap KVar IBindEnv
sScp  = (Sol a b -> HashMap KVar IBindEnv
forall b a. Sol b a -> HashMap KVar IBindEnv
sScp Sol a b
s1)  HashMap KVar IBindEnv
-> HashMap KVar IBindEnv -> HashMap KVar IBindEnv
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> HashMap KVar IBindEnv
forall b a. Sol b a -> HashMap KVar IBindEnv
sScp Sol a b
s2)
                 , sEbd :: HashMap Int EbindSol
sEbd  = (Sol a b -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
sEbd Sol a b
s1)  HashMap Int EbindSol
-> HashMap Int EbindSol -> HashMap Int EbindSol
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
sEbd Sol a b
s2) 
                 , sxEnv :: SEnv (Int, Sort)
sxEnv = (Sol a b -> SEnv (Int, Sort)
forall b a. Sol b a -> SEnv (Int, Sort)
sxEnv Sol a b
s1) SEnv (Int, Sort) -> SEnv (Int, Sort) -> SEnv (Int, Sort)
forall a. Semigroup a => a -> a -> a
<> (Sol a b -> SEnv (Int, Sort)
forall b a. Sol b a -> SEnv (Int, Sort)
sxEnv Sol a b
s2) 
                 }

instance Monoid (Sol a b) where
  mempty :: Sol a b
mempty = Sol :: forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol b a
Sol { sEnv :: SymEnv
sEnv = SymEnv
forall a. Monoid a => a
mempty 
               , sMap :: HashMap KVar b
sMap = HashMap KVar b
forall a. Monoid a => a
mempty 
               , gMap :: HashMap KVar a
gMap = 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 
               , sEbd :: HashMap Int EbindSol
sEbd = HashMap Int EbindSol
forall a. Monoid a => a
mempty
               , sxEnv :: SEnv (Int, Sort)
sxEnv = SEnv (Int, Sort)
forall a. Monoid a => a
mempty
               }
  mappend :: Sol a b -> Sol a b -> Sol a b
mappend = Sol a b -> Sol a b -> Sol a b
forall a. Semigroup a => a -> a -> a
(<>)

instance Functor (Sol a) where
  fmap :: (a -> b) -> Sol a a -> Sol a b
fmap a -> b
f (Sol SymEnv
e HashMap KVar a
s HashMap KVar a
m1 HashMap KVar Hyp
m2 HashMap KVar IBindEnv
m3 HashMap Int EbindSol
m4 SEnv (Int, Sort)
m5) = SymEnv
-> HashMap KVar b
-> HashMap KVar a
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol a b
forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol b a
Sol SymEnv
e (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 a
m1 HashMap KVar Hyp
m2 HashMap KVar IBindEnv
m3 HashMap Int EbindSol
m4 SEnv (Int, Sort)
m5

instance (PPrint a, PPrint b) => PPrint (Sol a b) where
  pprintTidy :: Tidy -> Sol a b -> Doc
pprintTidy Tidy
k Sol a b
s = [Doc] -> Doc
vcat [ Doc
"sMap :=" Doc -> Doc -> Doc
<+> Tidy -> HashMap KVar b -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Sol a b -> HashMap KVar b
forall b a. Sol b a -> HashMap KVar a
sMap Sol a b
s)
                        , Doc
"sEbd :=" Doc -> Doc -> Doc
<+> Tidy -> HashMap Int EbindSol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Sol a b -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
sEbd Sol a b
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
$cto :: forall x. Rep Cube x -> Cube
$cfrom :: forall x. Cube -> Rep Cube x
Generic, Cube -> ()
(Cube -> ()) -> NFData Cube
forall a. (a -> ()) -> NFData a
rnf :: Cube -> ()
$crnf :: 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 -> String
show = Cube -> String
forall a. PPrint a => a -> String
showpp
--------------------------------------------------------------------------------
result :: Sol a QBind -> M.HashMap KVar Expr
--------------------------------------------------------------------------------
result :: Sol a QBind -> HashMap KVar Expr
result Sol a QBind
s = Sol a Expr -> HashMap KVar Expr
forall b a. Sol b a -> HashMap KVar a
sMap (Sol a Expr -> HashMap KVar Expr)
-> Sol a Expr -> HashMap KVar Expr
forall a b. (a -> b) -> a -> b
$ ([Expr] -> Expr
pAnd ([Expr] -> Expr) -> (QBind -> [Expr]) -> QBind -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EQual -> Expr) -> [EQual] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> Expr
eqPred ([EQual] -> [Expr]) -> (QBind -> [EQual]) -> QBind -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals) (QBind -> Expr) -> Sol a QBind -> Sol a Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sol a QBind
s


--------------------------------------------------------------------------------
resultGradual :: GSolution -> M.HashMap KVar (Expr, [Expr])
--------------------------------------------------------------------------------
resultGradual :: GSolution -> HashMap KVar (Expr, [Expr])
resultGradual GSolution
s = ((((Symbol, Sort), Expr), GBind) -> (Expr, [Expr]))
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
-> HashMap KVar (Expr, [Expr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Symbol, Sort), Expr), GBind) -> (Expr, [Expr])
forall a a. ((a, a), GBind) -> (a, [Expr])
go' (GSolution -> HashMap KVar (((Symbol, Sort), Expr), GBind)
forall b a. Sol b a -> HashMap KVar b
gMap GSolution
s)
  where
    go' :: ((a, a), GBind) -> (a, [Expr])
go' ((a
_,a
e), GB [[EQual]]
eqss)
     = (a
e, [[Expr] -> Expr
PAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (EQual -> Expr) -> [EQual] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> Expr
eqPred [EQual]
eqs | [EQual]
eqs <- [[EQual]]
eqss])


--------------------------------------------------------------------------------
-- | Create a Solution ---------------------------------------------------------
--------------------------------------------------------------------------------
fromList :: SymEnv 
         -> [(KVar, a)] 
         -> [(KVar, b)] 
         -> [(KVar, Hyp)] 
         -> M.HashMap KVar IBindEnv 
         -> [(BindId, EbindSol)]
         -> SEnv (BindId, Sort)
         -> Sol a b
fromList :: SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(Int, EbindSol)]
-> SEnv (Int, Sort)
-> Sol a b
fromList SymEnv
env [(KVar, a)]
kGs [(KVar, b)]
kXs [(KVar, Hyp)]
kYs HashMap KVar IBindEnv
z [(Int, EbindSol)]
ebs SEnv (Int, Sort)
xbs
        = SymEnv
-> HashMap KVar b
-> HashMap KVar a
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol a b
forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol b a
Sol SymEnv
env HashMap KVar b
kXm HashMap KVar a
kGm HashMap KVar Hyp
kYm HashMap KVar IBindEnv
z HashMap Int EbindSol
ebm SEnv (Int, Sort)
xbs
  where
    kXm :: HashMap KVar b
kXm = [(KVar, b)] -> HashMap KVar b
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, b)]
kXs
    kYm :: HashMap KVar Hyp
kYm = [(KVar, Hyp)] -> HashMap KVar Hyp
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, Hyp)]
kYs
    kGm :: HashMap KVar a
kGm = [(KVar, a)] -> HashMap KVar a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, a)]
kGs
    ebm :: HashMap Int EbindSol
ebm = [(Int, EbindSol)] -> HashMap Int EbindSol
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int, EbindSol)]
ebs

--------------------------------------------------------------------------------
qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]
--------------------------------------------------------------------------------
qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Expr, EQual)]
qbPreds String
msg Sol a QBind
s Subst
su (QB [EQual]
eqs) = [ (EQual -> Expr
elabPred EQual
eq, EQual
eq) | EQual
eq <- [EQual]
eqs ]
  where
    elabPred :: EQual -> Expr
elabPred EQual
eq           = Located String -> SymEnv -> Expr -> Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (EQual -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc EQual
eq (String -> Located String) -> String -> Located String
forall a b. (a -> b) -> a -> b
$ String
"qbPreds:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg) SymEnv
env 
                          (Expr -> Expr) -> (EQual -> Expr) -> EQual -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su 
                          (Expr -> Expr) -> (EQual -> Expr) -> EQual -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Expr
eqPred 
                          (EQual -> Expr) -> EQual -> Expr
forall a b. (a -> b) -> a -> b
$ EQual
eq
    env :: SymEnv
env                   = Sol a QBind -> SymEnv
forall b a. Sol b a -> SymEnv
sEnv Sol a QBind
s

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

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



--------------------------------------------------------------------------------
lookup :: Sol a QBind -> KVar -> Either Hyp QBind
--------------------------------------------------------------------------------
lookup :: Sol a QBind -> KVar -> Either Hyp QBind
lookup Sol a QBind
s KVar
k
  | Just Hyp
cs  <- KVar -> HashMap KVar Hyp -> Maybe Hyp
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k (Sol a QBind -> HashMap KVar Hyp
forall b a. Sol b a -> HashMap KVar Hyp
sHyp Sol a 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 a QBind -> KVar -> Maybe QBind
forall b. Sol b QBind -> KVar -> Maybe QBind
lookupElab Sol a 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
  = String -> Either Hyp QBind
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> Either Hyp QBind) -> String -> Either Hyp QBind
forall a b. (a -> b) -> a -> b
$ String
"solLookup: Unknown kvar " String -> ShowS
forall a. [a] -> [a] -> [a]
++ KVar -> String
forall a. Show a => a -> String
show KVar
k

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

--------------------------------------------------------------------------------
updateK :: KVar -> a -> Sol b a -> Sol b a
--------------------------------------------------------------------------------
updateK :: KVar -> a -> Sol b a -> Sol b a
updateK KVar
k a
qs Sol b a
s = Sol b a
s { sMap :: HashMap KVar a
sMap = KVar -> a -> HashMap KVar a -> HashMap KVar a
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert KVar
k a
qs (Sol b a -> HashMap KVar a
forall b a. Sol b a -> HashMap KVar a
sMap Sol b a
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 -> Expr
eqPred  :: !Expr
  , EQual -> [Expr]
_eqArgs :: ![Expr]
  } deriving (EQual -> EQual -> Bool
(EQual -> EQual -> Bool) -> (EQual -> EQual -> Bool) -> Eq EQual
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EQual -> EQual -> Bool
$c/= :: EQual -> EQual -> Bool
== :: EQual -> EQual -> Bool
$c== :: EQual -> EQual -> Bool
Eq, Int -> EQual -> ShowS
[EQual] -> ShowS
EQual -> String
(Int -> EQual -> ShowS)
-> (EQual -> String) -> ([EQual] -> ShowS) -> Show EQual
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EQual] -> ShowS
$cshowList :: [EQual] -> ShowS
show :: EQual -> String
$cshow :: EQual -> String
showsPrec :: Int -> EQual -> ShowS
$cshowsPrec :: Int -> EQual -> ShowS
Show, Typeable EQual
DataType
Constr
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 -> DataType
EQual -> Constr
(forall b. Data b => b -> b) -> EQual -> EQual
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EQual -> c EQual
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cEQL :: Constr
$tEQual :: DataType
gmapMo :: (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
gmapMp :: (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
gmapM :: (forall d. Data d => d -> m d) -> EQual -> m EQual
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EQual -> m EQual
gmapQi :: Int -> (forall d. Data d => d -> u) -> EQual -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EQual -> u
gmapQ :: (forall d. Data d => d -> u) -> EQual -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EQual -> [u]
gmapQr :: (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
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EQual -> r
gmapT :: (forall b. Data b => b -> b) -> EQual -> EQual
$cgmapT :: (forall b. Data b => b -> b) -> EQual -> EQual
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EQual)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EQual)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EQual)
dataTypeOf :: EQual -> DataType
$cdataTypeOf :: EQual -> DataType
toConstr :: EQual -> Constr
$ctoConstr :: EQual -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EQual
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EQual
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EQual -> c EQual
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EQual -> c EQual
$cp1Data :: Typeable 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
$cto :: forall x. Rep EQual x -> EQual
$cfrom :: forall x. EQual -> Rep EQual x
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 -> Expr -> [Expr] -> EQual
EQL Qualifier
trueQual Expr
forall a. Monoid a => a
mempty []

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

instance NFData EQual

{- EQL :: q:_ -> p:_ -> ListX F.Expr {q_params q} -> _ @-}
eQual :: Qualifier -> [Symbol] -> EQual
eQual :: Qualifier -> [Symbol] -> EQual
eQual Qualifier
q [Symbol]
xs = {- tracepp "eQual" $ -} Qualifier -> Expr -> [Expr] -> EQual
EQL Qualifier
q Expr
p [Expr]
es
  where
    p :: Expr
p      = Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$  Qualifier -> Expr
qBody Qualifier
q
    su :: Subst
su     = [(Symbol, Expr)] -> Subst
mkSubst  ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$  String -> [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b.
(?callStack::CallStack) =>
String -> [a] -> [b] -> [(a, b)]
safeZip String
"eQual" [Symbol]
qxs [Expr]
es
    es :: [Expr]
es     = Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar    (Symbol -> Expr) -> [Symbol] -> [Expr]
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]
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
/= :: KIndex -> KIndex -> Bool
$c/= :: KIndex -> KIndex -> Bool
== :: KIndex -> KIndex -> Bool
$c== :: 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
min :: KIndex -> KIndex -> KIndex
$cmin :: KIndex -> KIndex -> KIndex
max :: KIndex -> KIndex -> KIndex
$cmax :: KIndex -> KIndex -> KIndex
>= :: KIndex -> KIndex -> Bool
$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
compare :: KIndex -> KIndex -> Ordering
$ccompare :: KIndex -> KIndex -> Ordering
$cp1Ord :: Eq KIndex
Ord, Int -> KIndex -> ShowS
[KIndex] -> ShowS
KIndex -> String
(Int -> KIndex -> ShowS)
-> (KIndex -> String) -> ([KIndex] -> ShowS) -> Show KIndex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KIndex] -> ShowS
$cshowList :: [KIndex] -> ShowS
show :: KIndex -> String
$cshow :: KIndex -> String
showsPrec :: Int -> KIndex -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep KIndex x -> KIndex
$cfrom :: forall x. KIndex -> Rep KIndex x
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
/= :: BIndex -> BIndex -> Bool
$c/= :: BIndex -> BIndex -> Bool
== :: BIndex -> BIndex -> Bool
$c== :: 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
min :: BIndex -> BIndex -> BIndex
$cmin :: BIndex -> BIndex -> BIndex
max :: BIndex -> BIndex -> BIndex
$cmax :: BIndex -> BIndex -> BIndex
>= :: BIndex -> BIndex -> Bool
$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
compare :: BIndex -> BIndex -> Ordering
$ccompare :: BIndex -> BIndex -> Ordering
$cp1Ord :: Eq BIndex
Ord, Int -> BIndex -> ShowS
[BIndex] -> ShowS
BIndex -> String
(Int -> BIndex -> ShowS)
-> (BIndex -> String) -> ([BIndex] -> ShowS) -> Show BIndex
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BIndex] -> ShowS
$cshowList :: [BIndex] -> ShowS
show :: BIndex -> String
$cshow :: BIndex -> String
showsPrec :: Int -> BIndex -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep BIndex x -> BIndex
$cfrom :: forall x. BIndex -> Rep BIndex x
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 -> Expr
bpConc :: !Pred                  -- ^ Concrete predicate (PTrue o)
  , BindPred -> [KIndex]
bpKVar :: ![KIndex]              -- ^ KVar-Subst pairs
  } deriving (Int -> BindPred -> ShowS
[BindPred] -> ShowS
BindPred -> String
(Int -> BindPred -> ShowS)
-> (BindPred -> String) -> ([BindPred] -> ShowS) -> Show BindPred
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BindPred] -> ShowS
$cshowList :: [BindPred] -> ShowS
show :: BindPred -> String
$cshow :: BindPred -> String
showsPrec :: Int -> BindPred -> ShowS
$cshowsPrec :: Int -> 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