{-# 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
  , qbFilterM
  , 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           Control.Monad.Reader
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.Config  as Cfg
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 (ElabM, ElabParam(..), 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 -} ([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 :: forall a b c. (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 b a. (b -> a -> b) -> b -> [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
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 :: forall a. 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 -> [Char]
(Int -> QBind -> ShowS)
-> (QBind -> [Char]) -> ([QBind] -> ShowS) -> Show QBind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> QBind -> ShowS
showsPrec :: Int -> QBind -> ShowS
$cshow :: QBind -> [Char]
show :: QBind -> [Char]
$cshowList :: [QBind] -> ShowS
showList :: [QBind] -> ShowS
Show, Typeable QBind
Typeable QBind =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> QBind -> c QBind)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QBind)
-> (QBind -> Constr)
-> (QBind -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QBind))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind))
-> ((forall b. Data b => b -> b) -> QBind -> QBind)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r)
-> (forall u. (forall d. Data d => d -> u) -> QBind -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QBind -> m QBind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBind -> m QBind)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QBind -> m QBind)
-> Data QBind
QBind -> Constr
QBind -> DataType
(forall b. Data b => b -> b) -> QBind -> QBind
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
forall u. (forall d. Data d => d -> u) -> QBind -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QBind -> c QBind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QBind
$ctoConstr :: QBind -> Constr
toConstr :: QBind -> Constr
$cdataTypeOf :: QBind -> DataType
dataTypeOf :: QBind -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QBind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QBind)
$cgmapT :: (forall b. Data b => b -> b) -> QBind -> QBind
gmapT :: (forall b. Data b => b -> b) -> QBind -> QBind
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QBind -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> QBind -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QBind -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QBind -> m QBind
Data, Typeable, (forall x. QBind -> Rep QBind x)
-> (forall x. Rep QBind x -> QBind) -> Generic QBind
forall x. Rep QBind x -> QBind
forall x. QBind -> Rep QBind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. QBind -> Rep QBind x
from :: forall x. QBind -> Rep QBind x
$cto :: forall x. Rep QBind x -> QBind
to :: forall x. Rep QBind x -> QBind
Generic, QBind -> QBind -> Bool
(QBind -> QBind -> Bool) -> (QBind -> QBind -> Bool) -> Eq QBind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QBind -> QBind -> Bool
== :: QBind -> QBind -> Bool
$c/= :: QBind -> QBind -> Bool
/= :: QBind -> QBind -> Bool
Eq)
newtype GBind  = GB [[EQual]] deriving (Int -> GBind -> ShowS
[GBind] -> ShowS
GBind -> [Char]
(Int -> GBind -> ShowS)
-> (GBind -> [Char]) -> ([GBind] -> ShowS) -> Show GBind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GBind -> ShowS
showsPrec :: Int -> GBind -> ShowS
$cshow :: GBind -> [Char]
show :: GBind -> [Char]
$cshowList :: [GBind] -> ShowS
showList :: [GBind] -> ShowS
Show, Typeable GBind
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 -> Constr
GBind -> DataType
(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. 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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GBind -> c GBind
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GBind -> c GBind
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GBind
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GBind
$ctoConstr :: GBind -> Constr
toConstr :: GBind -> Constr
$cdataTypeOf :: GBind -> DataType
dataTypeOf :: GBind -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GBind)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GBind)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GBind)
$cgmapT :: (forall b. Data b => b -> b) -> GBind -> GBind
gmapT :: (forall b. Data b => b -> b) -> GBind -> GBind
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GBind -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GBind -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> GBind -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GBind -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GBind -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GBind -> m GBind
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GBind -> m 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
$cfrom :: forall x. GBind -> Rep GBind x
from :: forall x. GBind -> Rep GBind x
$cto :: forall x. Rep GBind x -> GBind
to :: forall x. Rep GBind x -> GBind
Generic)

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

updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution
updateGMapWithKey :: [(KVar, QBind)] -> GSolution -> GSolution
updateGMapWithKey [(KVar, QBind)]
kqs GSolution
sol = GSolution
sol {gMap = L.foldl' (\HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
m (KVar
k, QB [EQual]
eq) -> ((((Symbol, Sort), ExprV Symbol), GBind)
 -> (((Symbol, Sort), ExprV Symbol), GBind))
-> KVar
-> HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
-> HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust (\(((Symbol, Sort), ExprV Symbol)
x, GB [[EQual]]
eqs) -> (((Symbol, Sort), ExprV Symbol)
x, [[EQual]] -> GBind
GB (if [EQual]
eq [EQual] -> [[EQual]] -> Bool
forall a. Eq a => a -> [a] -> 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), ExprV Symbol), GBind)
m) (gMap sol) 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 -> [ExprV Symbol]
qbExprs (QB [EQual]
xs) = EQual -> ExprV Symbol
eqPred (EQual -> ExprV Symbol) -> [EQual] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [EQual]
xs

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 :: forall (m :: * -> *).
Monad m =>
([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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([EQual] -> Int) -> (QBind -> [EQual]) -> QBind -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals

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

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

instance NFData QBind
instance 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 -> [Char]
(Int -> EbindSol -> ShowS)
-> (EbindSol -> [Char]) -> ([EbindSol] -> ShowS) -> Show EbindSol
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EbindSol -> ShowS
showsPrec :: Int -> EbindSol -> ShowS
$cshow :: EbindSol -> [Char]
show :: EbindSol -> [Char]
$cshowList :: [EbindSol] -> ShowS
showList :: [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
$cfrom :: forall x. EbindSol -> Rep EbindSol x
from :: forall x. EbindSol -> Rep EbindSol x
$cto :: forall x. Rep EbindSol x -> EbindSol
to :: forall x. Rep EbindSol x -> EbindSol
Generic, EbindSol -> ()
(EbindSol -> ()) -> NFData EbindSol
forall a. (a -> ()) -> NFData a
$crnf :: EbindSol -> ()
rnf :: 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 ExprV Symbol
e)   = Doc
"EbSol:" Doc -> Doc -> Doc
<+> Tidy -> ExprV Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ExprV Symbol
e
  pprintTidy Tidy
_ EbindSol
EbIncr    = Doc
"EbIncr"

--------------------------------------------------------------------------------
updateEbind :: Sol a b -> BindId -> Pred -> Sol a b
--------------------------------------------------------------------------------
updateEbind :: forall a b. Sol a b -> Int -> ExprV Symbol -> Sol a b
updateEbind Sol a b
s Int
i !ExprV Symbol
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         -> [Char] -> Sol a b
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Sol a b) -> [Char] -> Sol a b
forall a b. (a -> b) -> a -> b
$ [Char]
"updateEBind: Unknown ebind " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
  Just (EbSol ExprV Symbol
e0) -> [Char] -> Sol a b
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Sol a b) -> [Char] -> Sol a b
forall a b. (a -> b) -> a -> b
$ [Char]
"updateEBind: Re-assigning ebind " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" with solution: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ExprV Symbol -> [Char]
forall a. Show a => a -> [Char]
show ExprV Symbol
e0
  Just EbindSol
_          -> Sol a b
s { sEbd = M.insert i (EbSol e) (sEbd 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 Int EbindSol
sEbd :: !(M.HashMap BindId EbindSol) -- ^ EbindSol for each existential binder
  , forall b a. 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
$cfrom :: forall b a x. Sol b a -> Rep (Sol b a) x
from :: forall x. Sol b a -> Rep (Sol b a) x
$cto :: forall b a x. Rep (Sol b a) x -> Sol b a
to :: forall x. Rep (Sol b a) x -> Sol b a
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 = 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 = M.map f (gMap 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  = 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 { 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 :: 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 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
$cfrom :: forall x. Cube -> Rep Cube x
from :: forall x. Cube -> Rep Cube x
$cto :: forall x. Rep Cube x -> Cube
to :: forall x. Rep Cube x -> Cube
Generic, Cube -> ()
(Cube -> ()) -> NFData Cube
forall a. (a -> ()) -> NFData a
$crnf :: Cube -> ()
rnf :: Cube -> ()
NFData)

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

instance Show Cube where
  show :: Cube -> [Char]
show = Cube -> [Char]
forall a. PPrint a => a -> [Char]
showpp
--------------------------------------------------------------------------------
result :: Sol a QBind -> M.HashMap KVar Expr
--------------------------------------------------------------------------------
result :: forall a. Sol a QBind -> HashMap KVar (ExprV Symbol)
result Sol a QBind
s = Sol a (ExprV Symbol) -> HashMap KVar (ExprV Symbol)
forall b a. Sol b a -> HashMap KVar a
sMap (Sol a (ExprV Symbol) -> HashMap KVar (ExprV Symbol))
-> Sol a (ExprV Symbol) -> HashMap KVar (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([ExprV Symbol] -> ExprV Symbol)
-> (QBind -> [ExprV Symbol]) -> QBind -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EQual -> ExprV Symbol) -> [EQual] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> ExprV Symbol
eqPred ([EQual] -> [ExprV Symbol])
-> (QBind -> [EQual]) -> QBind -> [ExprV Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals (QBind -> ExprV Symbol) -> Sol a QBind -> Sol a (ExprV Symbol)
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 (ExprV Symbol, [ExprV Symbol])
resultGradual GSolution
s = ((((Symbol, Sort), ExprV Symbol), GBind)
 -> (ExprV Symbol, [ExprV Symbol]))
-> HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
-> HashMap KVar (ExprV Symbol, [ExprV Symbol])
forall a b. (a -> b) -> HashMap KVar a -> HashMap KVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Symbol, Sort), ExprV Symbol), GBind)
-> (ExprV Symbol, [ExprV Symbol])
forall {a} {a}. ((a, a), GBind) -> (a, [ExprV Symbol])
go' (GSolution -> HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
forall b a. Sol b a -> HashMap KVar b
gMap GSolution
s)
  where
    go' :: ((a, a), GBind) -> (a, [ExprV Symbol])
go' ((a
_,a
e), GB [[EQual]]
eqss)
     = (a
e, [[ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (EQual -> ExprV Symbol) -> [EQual] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> ExprV Symbol
eqPred [EQual]
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
-> [(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 -> ElabM [(Pred, EQual)]
--------------------------------------------------------------------------------
qbPreds :: forall a.
[Char]
-> Sol a QBind -> Subst -> QBind -> ElabM [(ExprV Symbol, EQual)]
qbPreds [Char]
msg Sol a QBind
s Subst
su (QB [EQual]
eqs) =
  do ElabFlags
ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     [(ExprV Symbol, EQual)] -> ElabM [(ExprV Symbol, EQual)]
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ (ElabFlags -> EQual -> ExprV Symbol
elabPred ElabFlags
ef EQual
eq, EQual
eq) | EQual
eq <- [EQual]
eqs ]
  where
    elabPred :: ElabFlags -> EQual -> ExprV Symbol
elabPred ElabFlags
ef EQual
eq = ElabParam -> ExprV Symbol -> ExprV Symbol
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam ElabFlags
ef (EQual -> [Char] -> Located [Char]
forall l b. Loc l => l -> b -> Located b
atLoc EQual
eq ([Char] -> Located [Char]) -> [Char] -> Located [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"qbPreds:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
msg) SymEnv
env)
                   (ExprV Symbol -> ExprV Symbol)
-> (EQual -> ExprV Symbol) -> EQual -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su
                   (ExprV Symbol -> ExprV Symbol)
-> (EQual -> ExprV Symbol) -> EQual -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> ExprV Symbol
eqPred
                   (EQual -> ExprV Symbol) -> EQual -> ExprV Symbol
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 :: forall a. 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 :: [Char]
_msg        = [Char]
"lookupQB: k = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ KVar -> [Char]
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), ExprV Symbol), GBind))
glookup GSolution
s KVar
k
  | Just (((Symbol, Sort), ExprV Symbol), GBind)
gbs <- KVar
-> HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
-> Maybe (((Symbol, Sort), ExprV Symbol), GBind)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k (GSolution -> HashMap KVar (((Symbol, Sort), ExprV Symbol), GBind)
forall b a. Sol b a -> HashMap KVar b
gMap GSolution
s)
  = Either QBind (((Symbol, Sort), ExprV Symbol), GBind)
-> Either
     Hyp (Either QBind (((Symbol, Sort), ExprV Symbol), GBind))
forall a b. b -> Either a b
Right ((((Symbol, Sort), ExprV Symbol), GBind)
-> Either QBind (((Symbol, Sort), ExprV Symbol), GBind)
forall a b. b -> Either a b
Right (((Symbol, Sort), ExprV Symbol), 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), ExprV Symbol), 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), ExprV Symbol), GBind)
-> Either
     Hyp (Either QBind (((Symbol, Sort), ExprV Symbol), GBind))
forall a b. b -> Either a b
Right (QBind -> Either QBind (((Symbol, Sort), ExprV Symbol), GBind)
forall a b. a -> Either a b
Left QBind
eqs)                 -- TODO: don't initialize kvars that have a hyp solution
  | Bool
otherwise
  = [Char]
-> Either
     Hyp (Either QBind (((Symbol, Sort), ExprV Symbol), GBind))
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char]
 -> Either
      Hyp (Either QBind (((Symbol, Sort), ExprV Symbol), GBind)))
-> [Char]
-> Either
     Hyp (Either QBind (((Symbol, Sort), ExprV Symbol), GBind))
forall a b. (a -> b) -> a -> b
$ [Char]
"solLookup: Unknown kvar " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ KVar -> [Char]
forall a. Show a => a -> [Char]
show KVar
k



--------------------------------------------------------------------------------
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  <- 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
  = [Char] -> Either Hyp QBind
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Either Hyp QBind) -> [Char] -> Either Hyp QBind
forall a b. (a -> b) -> a -> b
$ [Char]
"solLookup: Unknown kvar " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ KVar -> [Char]
forall a. Show a => a -> [Char]
show KVar
k

lookupElab :: Sol b QBind -> KVar -> Maybe QBind
lookupElab :: forall b. 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 :: 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 = M.insert k qs (sMap s)
--                 , sBot = M.delete k    (sBot s)
                   }


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


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

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

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

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

instance NFData EQual

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

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

instance Hashable KIndex

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

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

instance Hashable BIndex

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

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

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


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

type CMap a  = M.HashMap SubcId a