{-# 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              #-}

{-# 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, GSolution
  , Sol (gMap, sEnv, sEbd, sxEnv)
  , updateGMap, updateGMapWithKey
  , sHyp
  , 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)
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 :: forall a.
Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
update Sol a QBind
s [KVar]
ks [(KVar, EQual)]
kqs = {- tracepp msg -} (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')    = forall a b c. (a -> b -> (c, a)) -> a -> [b] -> ([c], a)
folds 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 :: forall a b c. (a -> b -> (c, a)) -> a -> [b] -> ([c], a)
folds a -> b -> (c, a)
f a
b = 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
cforall 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) <- forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ 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         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ (,[]) 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 :: forall a. Sol a QBind -> (KVar, QBind) -> (Bool, Sol a QBind)
update1 Sol a QBind
s (KVar
k, QBind
qs) = (Bool
change, forall a b. KVar -> a -> Sol b a -> Sol b a
updateK KVar
k QBind
qs Sol a QBind
s)
  where
    oldQs :: QBind
oldQs         = forall a. Sol a QBind -> KVar -> QBind
lookupQBind Sol a QBind
s KVar
k
    change :: Bool
change        = QBind -> BindId
qbSize QBind
oldQs forall a. Eq a => a -> a -> Bool
/= QBind -> BindId
qbSize QBind
qs


--------------------------------------------------------------------------------
-- | The `Solution` data type --------------------------------------------------
--------------------------------------------------------------------------------
type Solution  = Sol () QBind
type GSolution = Sol (((Symbol, Sort), Expr), GBind) QBind
newtype QBind  = QB [EQual]   deriving (BindId -> QBind -> ShowS
[QBind] -> ShowS
QBind -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [QBind] -> ShowS
$cshowList :: [QBind] -> ShowS
show :: QBind -> [Char]
$cshow :: QBind -> [Char]
showsPrec :: BindId -> QBind -> ShowS
$cshowsPrec :: BindId -> QBind -> ShowS
Show, Typeable QBind
QBind -> DataType
QBind -> Constr
(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. BindId -> (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. BindId -> (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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. BindId -> (forall d. Data d => d -> u) -> QBind -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> QBind -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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
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 (BindId -> GBind -> ShowS
[GBind] -> ShowS
GBind -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [GBind] -> ShowS
$cshowList :: [GBind] -> ShowS
show :: GBind -> [Char]
$cshow :: GBind -> [Char]
showsPrec :: BindId -> GBind -> ShowS
$cshowsPrec :: BindId -> GBind -> ShowS
Show, Typeable GBind
GBind -> DataType
GBind -> Constr
(forall b. Data b => b -> b) -> GBind -> 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. BindId -> (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. BindId -> (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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. BindId -> (forall d. Data d => d -> u) -> GBind -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> GBind -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> GBind -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GBind -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 = 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\HashMap KVar (((Symbol, Sort), Expr), GBind)
m (KVar
k, QB [EQual]
eq) -> 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[EQual]]
eqs then [[EQual]]
eqs else [EQual]
eqforall a. a -> [a] -> [a]
:[[EQual]]
eqs))) KVar
k HashMap KVar (((Symbol, Sort), Expr), GBind)
m) (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 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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 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 :: forall (m :: * -> *).
Monad m =>
([EQual] -> m Bool) -> GBind -> m GBind
gbFilterM [EQual] -> m Bool
f (GB [[EQual]]
eqs) = [[EQual]] -> GBind
GB forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [EQual] -> m Bool
f [[EQual]]
eqs

qbSize :: QBind -> Int
qbSize :: QBind -> BindId
qbSize = forall (t :: * -> *) a. Foldable t => t a -> BindId
length 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 (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 = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k 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 (BindId -> EbindSol -> ShowS
[EbindSol] -> ShowS
EbindSol -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [EbindSol] -> ShowS
$cshowList :: [EbindSol] -> ShowS
show :: EbindSol -> [Char]
$cshow :: EbindSol -> [Char]
showsPrec :: BindId -> EbindSol -> ShowS
$cshowsPrec :: BindId -> EbindSol -> ShowS
Show, 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 -> ()
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
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k [SimpC ()]
i Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
x
  pprintTidy Tidy
k (EbSol Expr
e)   = Doc
"EbSol:" Doc -> Doc -> 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 :: forall a b. Sol a b -> BindId -> Expr -> Sol a b
updateEbind Sol a b
s BindId
i !Expr
e = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup BindId
i (forall b a. Sol b a -> HashMap BindId EbindSol
sEbd Sol a b
s) of
  Maybe EbindSol
Nothing         -> forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"updateEBind: Unknown ebind " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show BindId
i
  Just (EbSol Expr
e0) -> forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"updateEBind: Re-assigning ebind " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show BindId
i forall a. [a] -> [a] -> [a]
++ [Char]
" with solution: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Expr
e0
  Just EbindSol
_          -> Sol a b
s { sEbd :: HashMap BindId EbindSol
sEbd = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert BindId
i (Expr -> EbindSol
EbSol Expr
e) (forall b a. Sol b a -> HashMap BindId 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
  { forall b a. Sol b a -> SymEnv
sEnv :: !SymEnv                      -- ^ Environment used to elaborate solutions
  , forall b a. Sol b a -> HashMap KVar a
sMap :: !(M.HashMap KVar a)          -- ^ Actual solution (for cut kvar)
  , forall b a. Sol b a -> HashMap KVar b
gMap :: !(M.HashMap KVar b)          -- ^ Solution for gradual variables
  , forall b a. Sol b a -> HashMap KVar Hyp
sHyp :: !(M.HashMap KVar Hyp)        -- ^ Defining cubes  (for non-cut kvar)
  , forall b a. Sol b a -> HashMap KVar IBindEnv
sScp :: !(M.HashMap KVar IBindEnv)   -- ^ Set of allowed binders for kvar
  , forall b a. Sol b a -> HashMap BindId EbindSol
sEbd :: !(M.HashMap BindId EbindSol) -- ^ EbindSol for each existential binder
  , forall b a. Sol b a -> SEnv (BindId, Sort)
sxEnv :: !(SEnv (BindId, Sort))      --   TODO: merge with sEnv? used for sorts of ebinds to solve ebinds in lhsPred
  } deriving (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 :: forall b a. 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 :: forall b a. 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 = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map b -> b
f (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 { sEnv :: SymEnv
sEnv  = forall b a. Sol b a -> SymEnv
sEnv Sol a b
s1  forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> SymEnv
sEnv Sol a b
s2
                 , sMap :: HashMap KVar b
sMap  = forall b a. Sol b a -> HashMap KVar a
sMap Sol a b
s1  forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> HashMap KVar a
sMap Sol a b
s2
                 , gMap :: HashMap KVar a
gMap  = forall b a. Sol b a -> HashMap KVar b
gMap Sol a b
s1  forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> HashMap KVar b
gMap Sol a b
s2
                 , sHyp :: HashMap KVar Hyp
sHyp  = forall b a. Sol b a -> HashMap KVar Hyp
sHyp Sol a b
s1  forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> HashMap KVar Hyp
sHyp Sol a b
s2
                 , sScp :: HashMap KVar IBindEnv
sScp  = forall b a. Sol b a -> HashMap KVar IBindEnv
sScp Sol a b
s1  forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> HashMap KVar IBindEnv
sScp Sol a b
s2
                 , sEbd :: HashMap BindId EbindSol
sEbd  = forall b a. Sol b a -> HashMap BindId EbindSol
sEbd Sol a b
s1  forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> HashMap BindId EbindSol
sEbd Sol a b
s2
                 , sxEnv :: SEnv (BindId, Sort)
sxEnv = forall b a. Sol b a -> SEnv (BindId, Sort)
sxEnv Sol a b
s1 forall a. Semigroup a => a -> a -> a
<> forall b a. Sol b a -> SEnv (BindId, Sort)
sxEnv Sol a b
s2
                 }

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

instance Functor (Sol a) where
  fmap :: forall a b. (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 BindId EbindSol
m4 SEnv (BindId, Sort)
m5) = forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap BindId EbindSol
-> SEnv (BindId, Sort)
-> Sol b a
Sol SymEnv
e (a -> b
f 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 BindId EbindSol
m4 SEnv (BindId, 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
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall b a. Sol b a -> HashMap KVar a
sMap Sol a b
s)
                        , Doc
"sEbd :=" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (forall b a. Sol b a -> HashMap BindId 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. 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 -> ()
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
<+> forall a. PPrint a => a -> Doc
pprint (Cube -> SubcId
cuId Cube
c)

instance Show Cube where
  show :: Cube -> [Char]
show = forall a. PPrint a => a -> [Char]
showpp
--------------------------------------------------------------------------------
result :: Sol a QBind -> M.HashMap KVar Expr
--------------------------------------------------------------------------------
result :: forall a. Sol a QBind -> HashMap KVar Expr
result Sol a QBind
s = forall b a. Sol b a -> HashMap KVar a
sMap forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> Expr
eqPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {a}. ((a, a), GBind) -> (a, [Expr])
go' (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 forall a b. (a -> b) -> a -> b
$ 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 :: forall a b.
SymEnv
-> [(KVar, a)]
-> [(KVar, b)]
-> [(KVar, Hyp)]
-> HashMap KVar IBindEnv
-> [(BindId, EbindSol)]
-> SEnv (BindId, Sort)
-> Sol a b
fromList SymEnv
env [(KVar, a)]
kGs [(KVar, b)]
kXs [(KVar, Hyp)]
kYs HashMap KVar IBindEnv
z [(BindId, EbindSol)]
ebs SEnv (BindId, Sort)
xbs
        = forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap BindId EbindSol
-> SEnv (BindId, Sort)
-> Sol b a
Sol SymEnv
env HashMap KVar b
kXm HashMap KVar a
kGm HashMap KVar Hyp
kYm HashMap KVar IBindEnv
z HashMap BindId EbindSol
ebm SEnv (BindId, Sort)
xbs
  where
    kXm :: HashMap KVar b
kXm = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, b)]
kXs
    kYm :: HashMap KVar Hyp
kYm = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, Hyp)]
kYs
    kGm :: HashMap KVar a
kGm = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, a)]
kGs
    ebm :: HashMap BindId EbindSol
ebm = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(BindId, EbindSol)]
ebs

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

--------------------------------------------------------------------------------
-- | Read / Write Solution at KVar ---------------------------------------------
--------------------------------------------------------------------------------
lookupQBind :: Sol a QBind -> KVar -> QBind
--------------------------------------------------------------------------------
lookupQBind :: forall a. Sol a QBind -> KVar -> QBind
lookupQBind Sol a QBind
s KVar
k = {- tracepp _msg $ -} forall a. a -> Maybe a -> a
Mb.fromMaybe ([EQual] -> QBind
QB []) (forall b. Sol b QBind -> KVar -> Maybe QBind
lookupElab Sol a QBind
s KVar
k)
  where
    _msg :: [Char]
_msg        = [Char]
"lookupQB: k = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
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 <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k (forall b a. Sol b a -> HashMap KVar b
gMap GSolution
s)
  = forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right (((Symbol, Sort), Expr), GBind)
gbs)
  | Just Hyp
cs  <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k (forall b a. Sol b a -> HashMap KVar Hyp
sHyp GSolution
s) -- non-cut variable, return its cubes
  = forall a b. a -> Either a b
Left Hyp
cs
  | Just QBind
eqs <- forall b. Sol b QBind -> KVar -> Maybe QBind
lookupElab GSolution
s KVar
k
  = forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left QBind
eqs)                 -- TODO: don't initialize kvars that have a hyp solution
  | Bool
otherwise
  = forall a. (?callStack::CallStack) => [Char] -> a
errorstar forall a b. (a -> b) -> a -> b
$ [Char]
"solLookup: Unknown kvar " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show KVar
k



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

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

--------------------------------------------------------------------------------
updateK :: KVar -> a -> Sol b a -> Sol b a
--------------------------------------------------------------------------------
updateK :: forall a b. 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 = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert KVar
k a
qs (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
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, BindId -> EQual -> ShowS
[EQual] -> ShowS
EQual -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [EQual] -> ShowS
$cshowList :: [EQual] -> ShowS
show :: EQual -> [Char]
$cshow :: EQual -> [Char]
showsPrec :: BindId -> EQual -> ShowS
$cshowsPrec :: BindId -> EQual -> ShowS
Show, Typeable EQual
EQual -> DataType
EQual -> Constr
(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. BindId -> (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. BindId -> (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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. BindId -> (forall d. Data d => d -> u) -> EQual -> u
$cgmapQi :: forall u. BindId -> (forall d. Data d => d -> u) -> EQual -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> EQual -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EQual -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 = forall a. Loc a => a -> SrcSpan
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 forall a. Monoid a => a
mempty []

instance PPrint EQual where
  pprintTidy :: Tidy -> EQual -> Doc
pprintTidy Tidy
k = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k 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      = forall a. Subable a => Subst -> a -> a
subst Subst
su forall a b. (a -> b) -> a -> b
$  Qualifier -> Expr
qBody Qualifier
q
    su :: Subst
su     = [(Symbol, Expr)] -> Subst
mkSubst  forall a b. (a -> b) -> a -> b
$  forall a b.
(?callStack::CallStack) =>
[Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"eQual" [Symbol]
qxs [Expr]
es
    es :: [Expr]
es     = forall a. Symbolic a => a -> Expr
eVar    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
    qxs :: [Symbol]
qxs    = QualParam -> Symbol
qpSym   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 -> BindId
kiBIndex :: !BindId
                     , KIndex -> BindId
kiPos    :: !Int
                     , KIndex -> KVar
kiKVar   :: !KVar
                     }
              deriving (KIndex -> KIndex -> Bool
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
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
Ord, BindId -> KIndex -> ShowS
[KIndex] -> ShowS
KIndex -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [KIndex] -> ShowS
$cshowList :: [KIndex] -> ShowS
show :: KIndex -> [Char]
$cshow :: KIndex -> [Char]
showsPrec :: BindId -> KIndex -> ShowS
$cshowsPrec :: BindId -> KIndex -> ShowS
Show, 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
_ = 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
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
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
Ord, BindId -> BIndex -> ShowS
[BIndex] -> ShowS
BIndex -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [BIndex] -> ShowS
$cshowList :: [BIndex] -> ShowS
show :: BIndex -> [Char]
$cshow :: BIndex -> [Char]
showsPrec :: BindId -> BIndex -> ShowS
$cshowsPrec :: BindId -> BIndex -> ShowS
Show, 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
_ = 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 (BindId -> BindPred -> ShowS
[BindPred] -> ShowS
BindPred -> [Char]
forall a.
(BindId -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [BindPred] -> ShowS
$cshowList :: [BindPred] -> ShowS
show :: BindPred -> [Char]
$cshow :: BindPred -> [Char]
showsPrec :: BindId -> BindPred -> ShowS
$cshowsPrec :: BindId -> BindPred -> ShowS
Show)

instance PPrint BindPred where
  pprintTidy :: Tidy -> BindPred -> Doc
pprintTidy Tidy
_ = 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 -> BindId |-> 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