{-# 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 -} ([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), Expr), GBind)
    -> (((Symbol, Sort), Expr), GBind))
-> GSolution
forall b a. Sol b a -> (b -> b) -> Sol b a
mapGMap GSolution
sol (\(((Symbol, Sort), Expr)
x,GBind
_) -> (((Symbol, Sort), Expr)
x, [[EQual]] -> GBind
GB []))

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

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

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

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

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

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

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 Expr
e)   = Doc
"EbSol:" Doc -> Doc -> Doc
<+> Tidy -> Expr -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
e
  pprintTidy Tidy
_ EbindSol
EbIncr    = Doc
"EbIncr"

--------------------------------------------------------------------------------
updateEbind :: Sol a b -> BindId -> Pred -> Sol a b
--------------------------------------------------------------------------------
updateEbind :: forall a b. Sol a b -> Int -> Expr -> Sol a b
updateEbind Sol a b
s Int
i !Expr
e = case Int -> HashMap Int EbindSol -> Maybe EbindSol
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i (Sol a b -> HashMap Int EbindSol
forall b a. Sol b a -> HashMap Int EbindSol
sEbd Sol a b
s) of
  Maybe EbindSol
Nothing         -> [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 Expr
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]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show Expr
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 Expr
result Sol a QBind
s = Sol a Expr -> HashMap KVar Expr
forall b a. Sol b a -> HashMap KVar a
sMap (Sol a Expr -> HashMap KVar Expr)
-> Sol a Expr -> HashMap KVar Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAnd ([Expr] -> Expr) -> (QBind -> [Expr]) -> QBind -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EQual -> Expr) -> [EQual] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EQual -> Expr
eqPred ([EQual] -> [Expr]) -> (QBind -> [EQual]) -> QBind -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QBind -> [EQual]
qbEQuals (QBind -> Expr) -> Sol a QBind -> Sol a Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sol a QBind
s


--------------------------------------------------------------------------------
resultGradual :: GSolution -> M.HashMap KVar (Expr, [Expr])
--------------------------------------------------------------------------------
resultGradual :: GSolution -> HashMap KVar (Expr, [Expr])
resultGradual GSolution
s = ((((Symbol, Sort), Expr), GBind) -> (Expr, [Expr]))
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
-> HashMap KVar (Expr, [Expr])
forall 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), Expr), GBind) -> (Expr, [Expr])
forall {a} {a}. ((a, a), GBind) -> (a, [Expr])
go' (GSolution -> HashMap KVar (((Symbol, Sort), Expr), GBind)
forall b a. Sol b a -> HashMap KVar b
gMap GSolution
s)
  where
    go' :: ((a, a), GBind) -> (a, [Expr])
go' ((a
_,a
e), GB [[EQual]]
eqss)
     = (a
e, [[Expr] -> Expr
PAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (EQual -> Expr) -> [EQual] -> [Expr]
forall 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
-> [(Int, EbindSol)]
-> SEnv (Int, Sort)
-> Sol a b
fromList SymEnv
env [(KVar, a)]
kGs [(KVar, b)]
kXs [(KVar, Hyp)]
kYs HashMap KVar IBindEnv
z [(Int, EbindSol)]
ebs SEnv (Int, Sort)
xbs
        = SymEnv
-> HashMap KVar b
-> HashMap KVar a
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol a b
forall b a.
SymEnv
-> HashMap KVar a
-> HashMap KVar b
-> HashMap KVar Hyp
-> HashMap KVar IBindEnv
-> HashMap Int EbindSol
-> SEnv (Int, Sort)
-> Sol b a
Sol SymEnv
env HashMap KVar b
kXm HashMap KVar a
kGm HashMap KVar Hyp
kYm HashMap KVar IBindEnv
z HashMap Int EbindSol
ebm SEnv (Int, Sort)
xbs
  where
    kXm :: HashMap KVar b
kXm = [(KVar, b)] -> HashMap KVar b
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, b)]
kXs
    kYm :: HashMap KVar Hyp
kYm = [(KVar, Hyp)] -> HashMap KVar Hyp
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, Hyp)]
kYs
    kGm :: HashMap KVar a
kGm = [(KVar, a)] -> HashMap KVar a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(KVar, a)]
kGs
    ebm :: HashMap Int EbindSol
ebm = [(Int, EbindSol)] -> HashMap Int EbindSol
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int, EbindSol)]
ebs

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

--------------------------------------------------------------------------------
-- | Read / Write Solution at KVar ---------------------------------------------
--------------------------------------------------------------------------------
lookupQBind :: Sol a QBind -> KVar -> QBind
--------------------------------------------------------------------------------
lookupQBind :: 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), Expr), GBind))
glookup GSolution
s KVar
k
  | Just (((Symbol, Sort), Expr), GBind)
gbs <- KVar
-> HashMap KVar (((Symbol, Sort), Expr), GBind)
-> Maybe (((Symbol, Sort), Expr), GBind)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k (GSolution -> HashMap KVar (((Symbol, Sort), Expr), GBind)
forall b a. Sol b a -> HashMap KVar b
gMap GSolution
s)
  = Either QBind (((Symbol, Sort), Expr), GBind)
-> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind))
forall a b. b -> Either a b
Right ((((Symbol, Sort), Expr), GBind)
-> Either QBind (((Symbol, Sort), Expr), GBind)
forall a b. b -> Either a b
Right (((Symbol, Sort), Expr), GBind)
gbs)
  | Just Hyp
cs  <- KVar -> HashMap KVar Hyp -> Maybe Hyp
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k (GSolution -> HashMap KVar Hyp
forall b a. Sol b a -> HashMap KVar Hyp
sHyp GSolution
s) -- non-cut variable, return its cubes
  = Hyp -> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind))
forall a b. a -> Either a b
Left Hyp
cs
  | Just QBind
eqs <- GSolution -> KVar -> Maybe QBind
forall b. Sol b QBind -> KVar -> Maybe QBind
lookupElab GSolution
s KVar
k
  = Either QBind (((Symbol, Sort), Expr), GBind)
-> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind))
forall a b. b -> Either a b
Right (QBind -> Either QBind (((Symbol, Sort), Expr), GBind)
forall a b. a -> Either a b
Left QBind
eqs)                 -- TODO: don't initialize kvars that have a hyp solution
  | Bool
otherwise
  = [Char] -> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind))
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char]
 -> Either Hyp (Either QBind (((Symbol, Sort), Expr), GBind)))
-> [Char]
-> Either Hyp (Either QBind (((Symbol, Sort), Expr), 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 -> Expr
eqPred  :: !Expr
  , EQual -> [Expr]
_eqArgs :: ![Expr]
  } deriving (EQual -> EQual -> Bool
(EQual -> EQual -> Bool) -> (EQual -> EQual -> Bool) -> Eq EQual
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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 -> Expr -> [Expr] -> EQual
EQL Qualifier
trueQual Expr
forall a. Monoid a => a
mempty []

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

instance NFData EQual

{- EQL :: q:_ -> p:_ -> ListX F.Expr {q_params q} -> _ @-}
eQual :: Qualifier -> [Symbol] -> EQual
eQual :: Qualifier -> [Symbol] -> EQual
eQual Qualifier
q [Symbol]
xs = {- tracepp "eQual" $ -} Qualifier -> Expr -> [Expr] -> EQual
EQL Qualifier
q Expr
p [Expr]
es
  where
    p :: Expr
p      = Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$  Qualifier -> Expr
qBody Qualifier
q
    su :: Subst
su     = [(Symbol, Expr)] -> Subst
mkSubst  ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$  [Char] -> [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b.
(?callStack::CallStack) =>
[Char] -> [a] -> [b] -> [(a, b)]
safeZip [Char]
"eQual" [Symbol]
qxs [Expr]
es
    es :: [Expr]
es     = Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar    (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
    qxs :: [Symbol]
qxs    = QualParam -> Symbol
qpSym   (QualParam -> Symbol) -> [QualParam] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
qParams Qualifier
q

--------------------------------------------------------------------------------
-- | A KIndex uniquely identifies each *use* of a KVar in an (LHS) binder
--------------------------------------------------------------------------------
data KIndex = KIndex { KIndex -> Int
kiBIndex :: !BindId
                     , KIndex -> Int
kiPos    :: !Int
                     , KIndex -> KVar
kiKVar   :: !KVar
                     }
              deriving (KIndex -> KIndex -> Bool
(KIndex -> KIndex -> Bool)
-> (KIndex -> KIndex -> Bool) -> Eq KIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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 -> Expr
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