{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE BangPatterns  #-}

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

module Language.Fixpoint.Types.Visitor (
  -- * Visitor
     Folder (..)
  ,  Foldable (..)
  ,  Visitable (..)

  -- * Extracting Symbolic Constants (String Literals)
  ,  SymConsts (..)

  -- * Default Visitor
  , defaultFolder

  -- * Transformers
  , trans

  -- * Accumulators
  , fold

  -- * Clients
  , stripCasts
  , kvarsExpr, eapps
  , size, lamSize
  , envKVars
  , envKVarsN
  , rhsKVars
  , mapKVars, mapKVars', mapGVars', mapKVarSubsts
  , mapExpr, mapExprOnExpr, mapMExpr

  -- * Coercion Substitutions
  , CoSub
  , applyCoSub
  , CoSubV
  , applyCoSubV

  -- * Predicates on Constraints
  , isConcC , isConc, isKvarC

  -- * Sorts
  , foldSort
  , mapSort
  , foldDataDecl
  ) where

-- import           Control.Monad.Trans.State.Strict (State, modify, runState)
-- import           Control.DeepSeq
import           Control.Monad.State.Strict
import qualified Data.HashSet        as S
import qualified Data.HashMap.Strict as M
import qualified Data.List           as L
import           Language.Fixpoint.Types hiding (mapSort)
import qualified Language.Fixpoint.Misc as Misc
import Control.Monad.Reader
import GHC.IO (unsafePerformIO)
import Data.IORef (newIORef, readIORef, IORef, modifyIORef')
import Prelude hiding (Foldable)




data Folder acc ctx = Visitor {
 -- | Context @ctx@ is built in a "top-down" fashion; not "across" siblings
    forall acc ctx. Folder acc ctx -> ctx -> Expr -> ctx
ctxExpr :: ctx -> Expr -> ctx

  -- | Transforms can access current @ctx@
  , forall acc ctx. Folder acc ctx -> ctx -> Expr -> Expr
txExpr  :: ctx -> Expr -> Expr

  -- | Accumulations can access current @ctx@; @acc@ value is monoidal
  , forall acc ctx. Folder acc ctx -> ctx -> Expr -> acc
accExpr :: ctx -> Expr -> acc
  }

---------------------------------------------------------------------------------
defaultFolder :: (Monoid acc) => Folder acc ctx
---------------------------------------------------------------------------------
defaultFolder :: forall acc ctx. Monoid acc => Folder acc ctx
defaultFolder = Visitor
  { ctxExpr :: ctx -> Expr -> ctx
ctxExpr    = ctx -> Expr -> ctx
forall a b. a -> b -> a
const
  , txExpr :: ctx -> Expr -> Expr
txExpr     = \ctx
_ Expr
x -> Expr
x
  , accExpr :: ctx -> Expr -> acc
accExpr    = \ctx
_ Expr
_ -> acc
forall a. Monoid a => a
mempty
  }

------------------------------------------------------------------------

fold         :: (Foldable t, Monoid a) => Folder a ctx -> ctx -> a -> t -> a
fold :: forall t a ctx.
(Foldable t, Monoid a) =>
Folder a ctx -> ctx -> a -> t -> a
fold Folder a ctx
v ctx
c a
a t
t = (t, a) -> a
forall a b. (a, b) -> b
snd ((t, a) -> a) -> (t, a) -> a
forall a b. (a -> b) -> a -> b
$ Folder a ctx
-> ctx
-> a
-> (Folder a ctx -> ctx -> t -> FoldM a t)
-> t
-> (t, a)
forall a ctx t.
Folder a ctx
-> ctx
-> a
-> (Folder a ctx -> ctx -> t -> FoldM a t)
-> t
-> (t, a)
execVisitM Folder a ctx
v ctx
c a
a Folder a ctx -> ctx -> t -> FoldM a t
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> t -> FoldM a t
foldE t
t

-- trans is always passed () () for a and t so we don't need to use the visitor pattern
-- trans        :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t
-- trans !v !c !_ !z = fst $ execVisitM v c mempty visit z

class Visitable t where
  transE :: (Expr -> Expr) -> t -> t

trans :: Visitable t => (Expr -> Expr) -> t -> t
trans :: forall t. Visitable t => (Expr -> Expr) -> t -> t
trans Expr -> Expr
f t
t = (Expr -> Expr) -> t -> t
forall t. Visitable t => (Expr -> Expr) -> t -> t
transE Expr -> Expr
f t
t

instance Visitable Expr where
  transE :: (Expr -> Expr) -> Expr -> Expr
transE Expr -> Expr
f = Expr -> Expr
vE
    where
      vE :: Expr -> Expr
vE Expr
e = Expr -> Expr
step Expr
e' where e' :: Expr
e' = Expr -> Expr
f Expr
e
      step :: Expr -> Expr
step e :: Expr
e@(ESym SymConst
_)       = Expr
e
      step e :: Expr
e@(ECon Constant
_)       = Expr
e
      step e :: Expr
e@(EVar Symbol
_)       = Expr
e
      step (EApp Expr
e1 Expr
e2)       = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
vE Expr
e1) (Expr -> Expr
vE Expr
e2)
      step (ENeg Expr
e)         = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> Expr
vE Expr
e)
      step (EBin Bop
o Expr
e1 Expr
e2)   = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o (Expr -> Expr
vE Expr
e1) (Expr -> Expr
vE Expr
e2)
      step (EIte Expr
p Expr
e1 Expr
e2)   = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte (Expr -> Expr
vE Expr
p) (Expr -> Expr
vE Expr
e1) (Expr -> Expr
vE Expr
e2)
      step (ECst Expr
e Sort
t)       = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst (Expr -> Expr
vE Expr
e) Sort
t
      step (PAnd [Expr]
ps)        = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
vE [Expr]
ps)
      step (POr [Expr]
ps)         = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
vE [Expr]
ps)
      step (PNot Expr
p)         = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> Expr
vE Expr
p)
      step (PImp Expr
p1 Expr
p2)     = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Expr -> Expr
vE Expr
p1) (Expr -> Expr
vE Expr
p2)
      step (PIff Expr
p1 Expr
p2)     = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Expr -> Expr
vE Expr
p1) (Expr -> Expr
vE Expr
p2)
      step (PAtom Brel
r Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Expr -> Expr
vE Expr
e1) (Expr -> Expr
vE Expr
e2)
      step (PAll [(Symbol, Sort)]
xts Expr
p)     = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
xts (Expr -> Expr
vE Expr
p)
      step (ELam (Symbol
x,Sort
t) Expr
e)   = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x,Sort
t) (Expr -> Expr
vE Expr
e)
      step (ECoerc Sort
a Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> Expr
vE Expr
e)
      step (PExist [(Symbol, Sort)]
xts Expr
p)   = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xts (Expr -> Expr
vE Expr
p)
      step (ETApp Expr
e Sort
s)      = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp (Expr -> Expr
vE Expr
e) Sort
s
      step (ETAbs Expr
e Symbol
s)      = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs (Expr -> Expr
vE Expr
e) Symbol
s
      step p :: Expr
p@(PKVar KVar
_ SubstV Symbol
_)    = Expr
p
      step (PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e) = KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i (Expr -> Expr
vE Expr
e)

instance Visitable Reft where
  transE :: (Expr -> Expr) -> Reft -> Reft
transE Expr -> Expr
v (Reft (Symbol
x, Expr
ra)) = (Symbol, Expr) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
x, (Expr -> Expr) -> Expr -> Expr
forall t. Visitable t => (Expr -> Expr) -> t -> t
transE Expr -> Expr
v Expr
ra)

instance Visitable SortedReft where
  transE :: (Expr -> Expr) -> SortedReft -> SortedReft
transE Expr -> Expr
v (RR Sort
t Reft
r) = Sort -> Reft -> SortedReft
RR Sort
t ((Expr -> Expr) -> Reft -> Reft
forall t. Visitable t => (Expr -> Expr) -> t -> t
transE Expr -> Expr
v Reft
r)

instance Visitable (Symbol, SortedReft, a) where
  transE :: (Expr -> Expr)
-> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a)
transE Expr -> Expr
f (Symbol
sym, SortedReft
sr, a
a) = (Symbol
sym, (Expr -> Expr) -> SortedReft -> SortedReft
forall t. Visitable t => (Expr -> Expr) -> t -> t
transE Expr -> Expr
f SortedReft
sr, a
a)

instance Visitable (BindEnv a) where
  transE :: (Expr -> Expr) -> BindEnv a -> BindEnv a
transE Expr -> Expr
v BindEnv a
be = BindEnv a
be { beBinds = M.map (transE v) (beBinds be) }

instance (Visitable (c a)) => Visitable (GInfo c a) where
  transE :: (Expr -> Expr) -> GInfo c a -> GInfo c a
transE Expr -> Expr
f GInfo c a
x = GInfo c a
x {
    cm = transE f <$> cm x
    , bs = transE f (bs x)
    , ae = transE f (ae x)
    }

instance Visitable (SimpC a) where
  transE :: (Expr -> Expr) -> SimpC a -> SimpC a
transE Expr -> Expr
v SimpC a
x = SimpC a
x {
    _crhs = transE v (_crhs x)
  }

instance Visitable (SubC a) where
  transE :: (Expr -> Expr) -> SubC a -> SubC a
transE Expr -> Expr
v SubC a
x = SubC a
x {
    slhs = transE v (slhs x),
    srhs = transE v (srhs x)
  }

instance Visitable AxiomEnv where
  transE :: (Expr -> Expr) -> AxiomEnv -> AxiomEnv
transE Expr -> Expr
v AxiomEnv
x = AxiomEnv
x {
    aenvEqs = transE v <$> aenvEqs x,
    aenvSimpl = transE v <$> aenvSimpl x
  }
    
instance Visitable Equation where
  transE :: (Expr -> Expr) -> Equation -> Equation
transE Expr -> Expr
v Equation
eq = Equation
eq {
    eqBody = transE v (eqBody eq)
  }

instance Visitable Rewrite where
  transE :: (Expr -> Expr) -> Rewrite -> Rewrite
transE Expr -> Expr
v Rewrite
rw = Rewrite
rw {
    smBody = transE v (smBody rw)
  }

execVisitM :: Folder a ctx -> ctx -> a -> (Folder a ctx -> ctx -> t -> FoldM a t) -> t -> (t, a)
execVisitM :: forall a ctx t.
Folder a ctx
-> ctx
-> a
-> (Folder a ctx -> ctx -> t -> FoldM a t)
-> t
-> (t, a)
execVisitM !Folder a ctx
v !ctx
c !a
a !Folder a ctx -> ctx -> t -> FoldM a t
f !t
x = IO (t, a) -> (t, a)
forall a. IO a -> a
unsafePerformIO (IO (t, a) -> (t, a)) -> IO (t, a) -> (t, a)
forall a b. (a -> b) -> a -> b
$ do
  IORef a
rn <- a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef a
a
  t
result <- FoldM a t -> IORef a -> IO t
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Folder a ctx -> ctx -> t -> FoldM a t
f Folder a ctx
v ctx
c t
x) IORef a
rn
  a
finalAcc <- IORef a -> IO a
forall a. IORef a -> IO a
readIORef IORef a
rn
  (t, a) -> IO (t, a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (t
result, a
finalAcc) 

type FoldM acc = ReaderT (IORef acc) IO

accum :: (Monoid a) => a -> FoldM a ()
accum :: forall a. Monoid a => a -> FoldM a ()
accum !a
z = do 
  IORef a
ref <- ReaderT (IORef a) IO (IORef a)
forall r (m :: * -> *). MonadReader r m => m r
ask
  IO () -> FoldM a ()
forall a. IO a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> FoldM a ()) -> IO () -> FoldM a ()
forall a b. (a -> b) -> a -> b
$ IORef a -> (a -> a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef a
ref (a -> a -> a
forall a. Monoid a => a -> a -> a
mappend a
z)

class Foldable t where
  foldE :: (Monoid a) => Folder a c -> c -> t -> FoldM a t

instance Foldable Expr where
  foldE :: forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldE = Folder a c -> c -> Expr -> FoldM a Expr
forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldExpr

instance Foldable Reft where
  foldE :: forall a c. Monoid a => Folder a c -> c -> Reft -> FoldM a Reft
foldE Folder a c
v c
c (Reft (Symbol
x, Expr
ra)) = (Symbol, Expr) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft ((Symbol, Expr) -> Reft)
-> (Expr -> (Symbol, Expr)) -> Expr -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x, ) (Expr -> Reft)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Reft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Folder a c -> c -> Expr -> ReaderT (IORef a) IO Expr
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldE Folder a c
v c
c Expr
ra

instance Foldable SortedReft where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> SortedReft -> FoldM a SortedReft
foldE Folder a c
v c
c (RR Sort
t Reft
r) = Sort -> Reft -> SortedReft
RR Sort
t (Reft -> SortedReft)
-> ReaderT (IORef a) IO Reft -> ReaderT (IORef a) IO SortedReft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Folder a c -> c -> Reft -> ReaderT (IORef a) IO Reft
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> Reft -> FoldM a Reft
foldE Folder a c
v c
c Reft
r

instance Foldable (Symbol, SortedReft, a) where
  foldE :: forall a c.
Monoid a =>
Folder a c
-> c -> (Symbol, SortedReft, a) -> FoldM a (Symbol, SortedReft, a)
foldE Folder a c
v c
c (Symbol
sym, SortedReft
sr, a
a) = (Symbol
sym, ,a
a) (SortedReft -> (Symbol, SortedReft, a))
-> ReaderT (IORef a) IO SortedReft
-> ReaderT (IORef a) IO (Symbol, SortedReft, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Folder a c -> c -> SortedReft -> ReaderT (IORef a) IO SortedReft
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> SortedReft -> FoldM a SortedReft
foldE Folder a c
v c
c SortedReft
sr

instance Foldable (BindEnv a) where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> BindEnv a -> FoldM a (BindEnv a)
foldE Folder a c
v c
c = ((Symbol, SortedReft, a)
 -> ReaderT (IORef a) IO (Symbol, SortedReft, a))
-> BindEnv a -> ReaderT (IORef a) IO (BindEnv a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SizedEnv a -> m (SizedEnv b)
mapM (Folder a c
-> c
-> (Symbol, SortedReft, a)
-> ReaderT (IORef a) IO (Symbol, SortedReft, a)
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c
-> c -> (Symbol, SortedReft, a) -> FoldM a (Symbol, SortedReft, a)
foldE Folder a c
v c
c)

---------------------------------------------------------------------------------
-- WARNING: these instances were written for mapKVars over GInfos only;
-- check that they behave as expected before using with other clients.
instance Foldable (SimpC a) where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> SimpC a -> FoldM a (SimpC a)
foldE Folder a c
v c
c SimpC a
x = do
    Expr
rhs' <- Folder a c -> c -> Expr -> FoldM a Expr
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldE Folder a c
v c
c (SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
x)
    SimpC a -> FoldM a (SimpC a)
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SimpC a
x { _crhs = rhs' }

instance Foldable (SubC a) where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> SubC a -> FoldM a (SubC a)
foldE Folder a c
v c
c SubC a
x = do
    SortedReft
lhs' <- Folder a c -> c -> SortedReft -> FoldM a SortedReft
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> SortedReft -> FoldM a SortedReft
foldE Folder a c
v c
c (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
x)
    SortedReft
rhs' <- Folder a c -> c -> SortedReft -> FoldM a SortedReft
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> SortedReft -> FoldM a SortedReft
foldE Folder a c
v c
c (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
x)
    SubC a -> FoldM a (SubC a)
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SubC a
x { slhs = lhs', srhs = rhs' }

instance (Foldable (c a)) => Foldable (GInfo c a) where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> GInfo c a -> FoldM a (GInfo c a)
foldE Folder a c
v c
c GInfo c a
x = do
    HashMap SubcId (c a)
cm' <- (c a -> ReaderT (IORef a) IO (c a))
-> HashMap SubcId (c a)
-> ReaderT (IORef a) IO (HashMap SubcId (c a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap SubcId a -> m (HashMap SubcId b)
mapM (Folder a c -> c -> c a -> ReaderT (IORef a) IO (c a)
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> c a -> FoldM a (c a)
foldE Folder a c
v c
c) (GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm GInfo c a
x)
    BindEnv a
bs' <- Folder a c -> c -> BindEnv a -> FoldM a (BindEnv a)
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> BindEnv a -> FoldM a (BindEnv a)
foldE Folder a c
v c
c (GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
x)
    AxiomEnv
ae' <- Folder a c -> c -> AxiomEnv -> FoldM a AxiomEnv
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> AxiomEnv -> FoldM a AxiomEnv
foldE Folder a c
v c
c (GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
x)
    GInfo c a -> FoldM a (GInfo c a)
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return GInfo c a
x { cm = cm', bs = bs', ae = ae' }

instance Foldable AxiomEnv where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> AxiomEnv -> FoldM a AxiomEnv
foldE Folder a c
v c
c AxiomEnv
x = do
    [Equation]
eqs'    <- (Equation -> ReaderT (IORef a) IO Equation)
-> [Equation] -> ReaderT (IORef a) IO [Equation]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Folder a c -> c -> Equation -> ReaderT (IORef a) IO Equation
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> Equation -> FoldM a Equation
foldE Folder a c
v c
c) (AxiomEnv -> [Equation]
aenvEqs   AxiomEnv
x)
    [Rewrite]
simpls' <- (Rewrite -> ReaderT (IORef a) IO Rewrite)
-> [Rewrite] -> ReaderT (IORef a) IO [Rewrite]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Folder a c -> c -> Rewrite -> ReaderT (IORef a) IO Rewrite
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c.
Monoid a =>
Folder a c -> c -> Rewrite -> FoldM a Rewrite
foldE Folder a c
v c
c) (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
x)
    AxiomEnv -> FoldM a AxiomEnv
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return AxiomEnv
x { aenvEqs = eqs' , aenvSimpl = simpls'}

instance Foldable Equation where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> Equation -> FoldM a Equation
foldE Folder a c
v c
c Equation
eq = do
    Expr
body' <- Folder a c -> c -> Expr -> FoldM a Expr
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldE Folder a c
v c
c (Equation -> Expr
forall v. EquationV v -> ExprV v
eqBody Equation
eq)
    Equation -> FoldM a Equation
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Equation
eq { eqBody = body' }

instance Foldable Rewrite where
  foldE :: forall a c.
Monoid a =>
Folder a c -> c -> Rewrite -> FoldM a Rewrite
foldE Folder a c
v c
c Rewrite
rw = do
    Expr
body' <- Folder a c -> c -> Expr -> FoldM a Expr
forall t a c.
(Foldable t, Monoid a) =>
Folder a c -> c -> t -> FoldM a t
forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldE Folder a c
v c
c (Rewrite -> Expr
smBody Rewrite
rw)
    Rewrite -> FoldM a Rewrite
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Rewrite
rw { smBody = body' }

---------------------------------------------------------------------------------
foldExpr :: (Monoid a) => Folder a ctx -> ctx -> Expr -> FoldM a Expr
foldExpr :: forall a c. Monoid a => Folder a c -> c -> Expr -> FoldM a Expr
foldExpr !Folder a ctx
v    = ctx -> Expr -> ReaderT (IORef a) IO Expr
vE
  where
    vE :: ctx -> Expr -> ReaderT (IORef a) IO Expr
vE !ctx
c !Expr
e    = do {- SCC "visitExpr.vE.accum" -} a -> FoldM a ()
forall a. Monoid a => a -> FoldM a ()
accum a
acc
                     {- SCC "visitExpr.vE.step" -}  ctx -> Expr -> ReaderT (IORef a) IO Expr
step ctx
c' Expr
e'
      where !c' :: ctx
c'  = Folder a ctx -> ctx -> Expr -> ctx
forall acc ctx. Folder acc ctx -> ctx -> Expr -> ctx
ctxExpr Folder a ctx
v ctx
c  Expr
e
            !e' :: Expr
e'  = Folder a ctx -> ctx -> Expr -> Expr
forall acc ctx. Folder acc ctx -> ctx -> Expr -> Expr
txExpr  Folder a ctx
v ctx
c' Expr
e
            !acc :: a
acc = Folder a ctx -> ctx -> Expr -> a
forall acc ctx. Folder acc ctx -> ctx -> Expr -> acc
accExpr Folder a ctx
v ctx
c' Expr
e
    step :: ctx -> Expr -> ReaderT (IORef a) IO Expr
step ctx
_ e :: Expr
e@(ESym SymConst
_)       = Expr -> ReaderT (IORef a) IO Expr
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    step ctx
_ e :: Expr
e@(ECon Constant
_)       = Expr -> ReaderT (IORef a) IO Expr
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    step ctx
_ e :: Expr
e@(EVar Symbol
_)       = Expr -> ReaderT (IORef a) IO Expr
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    step !ctx
c (EApp Expr
f Expr
e)      = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp        (Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
f  ReaderT (IORef a) IO (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step !ctx
c (ENeg Expr
e)        = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg        (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step !ctx
c (EBin Bop
o Expr
e1 Expr
e2)  = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o      (Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e1 ReaderT (IORef a) IO (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e2
    step !ctx
c (EIte Expr
p Expr
e1 Expr
e2)  = Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte        (Expr -> Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr
-> ReaderT (IORef a) IO (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p  ReaderT (IORef a) IO (Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO (Expr -> Expr)
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e1 ReaderT (IORef a) IO (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e2
    step !ctx
c (ECst Expr
e Sort
t)      = (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
t)  (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step !ctx
c (PAnd  [Expr]
ps)      = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd        ([Expr] -> Expr)
-> ReaderT (IORef a) IO [Expr] -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c (Expr -> ReaderT (IORef a) IO Expr)
-> [Expr] -> ReaderT (IORef a) IO [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
ps)
    step !ctx
c (POr  [Expr]
ps)       = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr         ([Expr] -> Expr)
-> ReaderT (IORef a) IO [Expr] -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c (Expr -> ReaderT (IORef a) IO Expr)
-> [Expr] -> ReaderT (IORef a) IO [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
ps)
    step !ctx
c (PNot Expr
p)        = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot        (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p
    step !ctx
c (PImp Expr
p1 Expr
p2)    = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp        (Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p1 ReaderT (IORef a) IO (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p2
    step !ctx
c (PIff Expr
p1 Expr
p2)    = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff        (Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p1 ReaderT (IORef a) IO (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p2
    step !ctx
c (PAtom Brel
r Expr
e1 Expr
e2) = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r     (Expr -> Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e1 ReaderT (IORef a) IO (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall a b.
ReaderT (IORef a) IO (a -> b)
-> ReaderT (IORef a) IO a -> ReaderT (IORef a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e2
    step !ctx
c (PAll [(Symbol, Sort)]
xts Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll   [(Symbol, Sort)]
xts  (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p
    step !ctx
c (ELam (Symbol
x,Sort
t) Expr
e)  = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x,Sort
t)  (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step !ctx
c (ECoerc Sort
a Sort
t Expr
e)  = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t  (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step !ctx
c (PExist [(Symbol, Sort)]
xts Expr
p)  = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xts  (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
p
    step !ctx
c (ETApp Expr
e Sort
s)     = (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ETApp` Sort
s) (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step !ctx
c (ETAbs Expr
e Symbol
s)     = (Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
`ETAbs` Symbol
s) (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e
    step ctx
_  p :: Expr
p@(PKVar KVar
_ SubstV Symbol
_)   = Expr -> ReaderT (IORef a) IO Expr
forall a. a -> ReaderT (IORef a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
p
    step !ctx
c (PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e) = KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i (Expr -> Expr)
-> ReaderT (IORef a) IO Expr -> ReaderT (IORef a) IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> ReaderT (IORef a) IO Expr
vE ctx
c Expr
e

mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars :: forall t. Visitable t => (KVar -> Maybe Expr) -> t -> t
mapKVars KVar -> Maybe Expr
f = ((KVar, SubstV Symbol) -> Maybe Expr) -> t -> t
forall t.
Visitable t =>
((KVar, SubstV Symbol) -> Maybe Expr) -> t -> t
mapKVars' (KVar, SubstV Symbol) -> Maybe Expr
forall {b}. (KVar, b) -> Maybe Expr
f'
  where
    f' :: (KVar, b) -> Maybe Expr
f' (KVar
kv', b
_) = KVar -> Maybe Expr
f KVar
kv'

mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapKVars' :: forall t.
Visitable t =>
((KVar, SubstV Symbol) -> Maybe Expr) -> t -> t
mapKVars' (KVar, SubstV Symbol) -> Maybe Expr
f = (Expr -> Expr) -> t -> t
forall t. Visitable t => (Expr -> Expr) -> t -> t
trans Expr -> Expr
txK
  where
    txK :: Expr -> Expr
txK (PKVar KVar
k SubstV Symbol
su)
      | Just Expr
p' <- (KVar, SubstV Symbol) -> Maybe Expr
f (KVar
k, SubstV Symbol
su) = SubstV Symbol -> Expr -> Expr
forall a. Subable a => SubstV Symbol -> a -> a
subst SubstV Symbol
su Expr
p'
    txK (PGrad KVar
k SubstV Symbol
su GradInfo
_ Expr
_)
      | Just Expr
p' <- (KVar, SubstV Symbol) -> Maybe Expr
f (KVar
k, SubstV Symbol
su) = SubstV Symbol -> Expr -> Expr
forall a. Subable a => SubstV Symbol -> a -> a
subst SubstV Symbol
su Expr
p'
    txK Expr
p = Expr
p



mapGVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapGVars' :: forall t.
Visitable t =>
((KVar, SubstV Symbol) -> Maybe Expr) -> t -> t
mapGVars' (KVar, SubstV Symbol) -> Maybe Expr
f            = (Expr -> Expr) -> t -> t
forall t. Visitable t => (Expr -> Expr) -> t -> t
trans Expr -> Expr
txK
  where
    txK :: Expr -> Expr
txK (PGrad KVar
k SubstV Symbol
su GradInfo
_ Expr
_)
      | Just Expr
p' <- (KVar, SubstV Symbol) -> Maybe Expr
f (KVar
k, SubstV Symbol
su) = SubstV Symbol -> Expr -> Expr
forall a. Subable a => SubstV Symbol -> a -> a
subst SubstV Symbol
su Expr
p'
    txK Expr
p            = Expr
p

mapExpr :: Visitable t => (Expr -> Expr) -> t -> t
mapExpr :: forall t. Visitable t => (Expr -> Expr) -> t -> t
mapExpr Expr -> Expr
f = (Expr -> Expr) -> t -> t
forall t. Visitable t => (Expr -> Expr) -> t -> t
trans Expr -> Expr
f

-- | Specialized and faster version of mapExpr for expressions
mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
f = Expr -> Expr
go
  where
    go :: Expr -> Expr
go !Expr
e0 = Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$! case Expr
e0 of
      EApp Expr
f Expr
e ->
        let !f' :: Expr
f' = Expr -> Expr
go Expr
f
            !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp Expr
f' Expr
e'
      ENeg Expr
e ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg Expr
e'
      EBin Bop
o Expr
e1 Expr
e2 ->
        let !e1' :: Expr
e1' = Expr -> Expr
go Expr
e1
            !e2' :: Expr
e2' = Expr -> Expr
go Expr
e2
        in Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o Expr
e1' Expr
e2'
      EIte Expr
p Expr
e1 Expr
e2 ->
        let !p' :: Expr
p' = Expr -> Expr
go Expr
p
            !e1' :: Expr
e1' = Expr -> Expr
go Expr
e1
            !e2' :: Expr
e2' = Expr -> Expr
go Expr
e2
        in Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte Expr
p' Expr
e1' Expr
e2'
      ECst Expr
e Sort
t ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e' Sort
t
      PAnd [Expr]
ps ->
        let !ps' :: [Expr]
ps' = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
go [Expr]
ps
        in [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd [Expr]
ps'
      POr [Expr]
ps ->
        let !ps' :: [Expr]
ps' = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
go [Expr]
ps
        in [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr [Expr]
ps'
      PNot Expr
p ->
        let !p' :: Expr
p' = Expr -> Expr
go Expr
p
        in Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
p'
      PImp Expr
p1 Expr
p2 ->
        let !p1' :: Expr
p1' = Expr -> Expr
go Expr
p1
            !p2' :: Expr
p2' = Expr -> Expr
go Expr
p2
        in Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp Expr
p1' Expr
p2'
      PIff Expr
p1 Expr
p2 ->
        let !p1' :: Expr
p1' = Expr -> Expr
go Expr
p1
            !p2' :: Expr
p2' = Expr -> Expr
go Expr
p2
        in Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff Expr
p1' Expr
p2'
      PAtom Brel
r Expr
e1 Expr
e2 ->
        let !e1' :: Expr
e1' = Expr -> Expr
go Expr
e1
            !e2' :: Expr
e2' = Expr -> Expr
go Expr
e2
        in Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r Expr
e1' Expr
e2'
      PAll [(Symbol, Sort)]
xts Expr
p ->
        let !p' :: Expr
p' = Expr -> Expr
go Expr
p
        in [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
xts Expr
p'
      ELam (Symbol
x,Sort
t) Expr
e ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x,Sort
t) Expr
e'
      ECoerc Sort
a Sort
t Expr
e ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t Expr
e'
      PExist [(Symbol, Sort)]
xts Expr
p ->
        let !p' :: Expr
p' = Expr -> Expr
go Expr
p
        in [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xts Expr
p'
      ETApp Expr
e Sort
s ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp Expr
e' Sort
s
      ETAbs Expr
e Symbol
s ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs Expr
e' Symbol
s
      PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e ->
        let !e' :: Expr
e' = Expr -> Expr
go Expr
e
        in KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e'
      e :: Expr
e@PKVar{} -> Expr
e
      e :: Expr
e@EVar{} -> Expr
e
      e :: Expr
e@ESym{} -> Expr
e
      e :: Expr
e@ECon{} -> Expr
e

-- mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr
-- mapExprOnExpr f = go
--   where
--     go !e0 = f $! case e0 of
--       EApp f e -> EApp !(go f) !(go e)
--       ENeg e -> ENeg (go e)
--       EBin o e1 e2 ->  EBin o (go e1) (go e2)
--       EIte p e1 e2 -> EIte (go p) (go e1) (go e2)
--       ECst e t -> ECst (go e) t
--       PAnd ps -> PAnd (map go ps)
--       POr ps -> POr (map go ps)
--       PNot p -> PNot (go p)
--       PImp p1 p2 -> PImp (go p1) (go p2)
--       PIff p1 p2 -> PIff (go p1) (go p2)
--       PAtom r e1 e2 -> PAtom r (go e1) (go e2)
--       PAll xts p -> PAll xts (go p)
--       ELam (x,t) e -> ELam (x,t) (go e)
--       ECoerc a t e -> ECoerc a t (go e)
--       PExist xts p -> PExist xts (go p)
--       ETApp e s -> ETApp (go e) s
--       ETAbs e s -> ETAbs (go e) s
--       PGrad k su i e -> PGrad k su i (go e)
--       e@PKVar{} -> e
--       e@EVar{} -> e
--       e@ESym{} -> e
--       e@ECon{} -> e


mapMExpr :: (Monad m) => (Expr -> m Expr) -> Expr -> m Expr
mapMExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
mapMExpr Expr -> m Expr
f = Expr -> m Expr
go
  where
    go :: Expr -> m Expr
go e :: Expr
e@(ESym SymConst
_)      = Expr -> m Expr
f Expr
e
    go e :: Expr
e@(ECon Constant
_)      = Expr -> m Expr
f Expr
e
    go e :: Expr
e@(EVar Symbol
_)      = Expr -> m Expr
f Expr
e
    go e :: Expr
e@(PKVar KVar
_ SubstV Symbol
_)   = Expr -> m Expr
f Expr
e
    go (PGrad KVar
k SubstV Symbol
s GradInfo
i Expr
e) = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
s GradInfo
i (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (ENeg Expr
e)        = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (PNot Expr
p)        = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
p
    go (ECst Expr
e Sort
t)      = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
t) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (PAll [(Symbol, Sort)]
xts Expr
p)    = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll   [(Symbol, Sort)]
xts (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
p
    go (ELam (Symbol
x,Sort
t) Expr
e)  = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x,Sort
t) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (ECoerc Sort
a Sort
t Expr
e)  = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (PExist [(Symbol, Sort)]
xts Expr
p)  = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xts (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
p
    go (ETApp Expr
e Sort
s)     = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ETApp` Sort
s) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (ETAbs Expr
e Symbol
s)     = Expr -> m Expr
f (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
`ETAbs` Symbol
s) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> m Expr
go Expr
e
    go (EApp Expr
g Expr
e)      = Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp        (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
g  m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
e           )
    go (EBin Bop
o Expr
e1 Expr
e2)  = Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o      (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
e1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
e2          )
    go (PImp Expr
p1 Expr
p2)    = Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp        (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
p1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
p2          )
    go (PIff Expr
p1 Expr
p2)    = Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff        (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
p1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
p2          )
    go (PAtom Brel
r Expr
e1 Expr
e2) = Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r     (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
e1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
e2          )
    go (EIte Expr
p Expr
e1 Expr
e2)  = Expr -> m Expr
f (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte        (Expr -> Expr -> Expr -> Expr)
-> m Expr -> m (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
p  m (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
e1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
e2)
    go (PAnd [Expr]
ps)       = Expr -> m Expr
f (Expr -> m Expr) -> ([Expr] -> Expr) -> [Expr] -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ([Expr] -> m Expr) -> m [Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> m Expr
go (Expr -> m Expr) -> [Expr] -> m [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
ps)
    go (POr [Expr]
ps)        = Expr -> m Expr
f (Expr -> m Expr) -> ([Expr] -> Expr) -> [Expr] -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr ([Expr] -> m Expr) -> m [Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> m Expr
go (Expr -> m Expr) -> [Expr] -> m [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
ps)

mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts :: forall t.
Visitable t =>
(KVar -> SubstV Symbol -> SubstV Symbol) -> t -> t
mapKVarSubsts KVar -> SubstV Symbol -> SubstV Symbol
f          = (Expr -> Expr) -> t -> t
forall t. Visitable t => (Expr -> Expr) -> t -> t
trans Expr -> Expr
txK
  where
    txK :: Expr -> Expr
txK (PKVar KVar
k SubstV Symbol
su)   = KVar -> SubstV Symbol -> Expr
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (KVar -> SubstV Symbol -> SubstV Symbol
f KVar
k SubstV Symbol
su)
    txK (PGrad KVar
k SubstV Symbol
su GradInfo
i Expr
e) = KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k (KVar -> SubstV Symbol -> SubstV Symbol
f KVar
k SubstV Symbol
su) GradInfo
i Expr
e
    txK Expr
p              = Expr
p

newtype MInt = MInt Integer -- deriving (Eq, NFData)

instance Semigroup MInt where
  MInt SubcId
m <> :: MInt -> MInt -> MInt
<> MInt SubcId
n = SubcId -> MInt
MInt (SubcId
m SubcId -> SubcId -> SubcId
forall a. Num a => a -> a -> a
+ SubcId
n)

instance Monoid MInt where
  mempty :: MInt
mempty  = SubcId -> MInt
MInt SubcId
0
  mappend :: MInt -> MInt -> MInt
  mappend :: MInt -> MInt -> MInt
mappend = MInt -> MInt -> MInt
forall a. Semigroup a => a -> a -> a
(<>)

size :: Foldable t => t -> Integer
size :: forall t. Foldable t => t -> SubcId
size t
t    = SubcId
n
  where
    MInt SubcId
n = Folder MInt () -> () -> MInt -> t -> MInt
forall t a ctx.
(Foldable t, Monoid a) =>
Folder a ctx -> ctx -> a -> t -> a
fold Folder MInt ()
forall {ctx}. Folder MInt ctx
szV () MInt
forall a. Monoid a => a
mempty t
t
    szV :: Folder MInt ctx
szV    = (Folder MInt t
forall {ctx}. Folder MInt ctx
forall acc ctx. Monoid acc => Folder acc ctx
defaultFolder :: Folder MInt t) { accExpr = \ ctx
_ Expr
_ -> SubcId -> MInt
MInt SubcId
1 }


lamSize :: Foldable t => t -> Integer
lamSize :: forall t. Foldable t => t -> SubcId
lamSize t
t    = SubcId
n
  where
    MInt SubcId
n = Folder MInt () -> () -> MInt -> t -> MInt
forall t a ctx.
(Foldable t, Monoid a) =>
Folder a ctx -> ctx -> a -> t -> a
fold Folder MInt ()
forall {ctx}. Folder MInt ctx
szV () MInt
forall a. Monoid a => a
mempty t
t
    szV :: Folder MInt ctx
szV    = (Folder MInt t
forall {ctx}. Folder MInt ctx
forall acc ctx. Monoid acc => Folder acc ctx
defaultFolder :: Folder MInt t) { accExpr = accum }
    accum :: p -> ExprV v -> MInt
accum p
_ (ELam (Symbol, Sort)
_ ExprV v
_) = SubcId -> MInt
MInt SubcId
1
    accum p
_ ExprV v
_          = SubcId -> MInt
MInt SubcId
0

eapps :: Foldable t => t -> [Expr]
eapps :: forall t. Foldable t => t -> [Expr]
eapps                 = Folder [Expr] () -> () -> [Expr] -> t -> [Expr]
forall t a ctx.
(Foldable t, Monoid a) =>
Folder a ctx -> ctx -> a -> t -> a
fold Folder [Expr] ()
forall {ctx}. Folder [Expr] ctx
eappVis () []
  where
    eappVis :: Folder [Expr] ctx
eappVis              = (Folder [KVar] t
forall {t}. Folder [KVar] t
forall acc ctx. Monoid acc => Folder acc ctx
defaultFolder :: Folder [KVar] t) { accExpr = eapp' }
    eapp' :: p -> ExprV v -> [ExprV v]
eapp' p
_ e :: ExprV v
e@(EApp ExprV v
_ ExprV v
_) = [ExprV v
e]
    eapp' p
_ ExprV v
_            = []

{-# SCC kvarsExpr #-}
kvarsExpr :: ExprV v -> [KVar]
kvarsExpr :: forall v. ExprV v -> [KVar]
kvarsExpr = [KVar] -> ExprV v -> [KVar]
forall {v}. [KVar] -> ExprV v -> [KVar]
go []
  where
    go :: [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e0 = case ExprV v
e0 of
      ESym SymConst
_ -> [KVar]
acc
      ECon Constant
_ -> [KVar]
acc
      EVar v
_ -> [KVar]
acc
      PKVar KVar
k SubstV v
_ -> KVar
k KVar -> [KVar] -> [KVar]
forall a. a -> [a] -> [a]
: [KVar]
acc
      PGrad KVar
k SubstV v
_ GradInfo
_ ExprV v
_ -> KVar
k KVar -> [KVar] -> [KVar]
forall a. a -> [a] -> [a]
: [KVar]
acc
      ENeg ExprV v
e -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e
      PNot ExprV v
p -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
p
      ECst ExprV v
e Sort
_t -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e
      PAll [(Symbol, Sort)]
_xts ExprV v
p -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
p
      ELam (Symbol, Sort)
_b ExprV v
e -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e
      ECoerc Sort
_a Sort
_t ExprV v
e -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e
      PExist [(Symbol, Sort)]
_xts ExprV v
p -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
p
      ETApp ExprV v
e Sort
_s -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e
      ETAbs ExprV v
e Symbol
_s -> [KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e
      EApp ExprV v
g ExprV v
e -> [KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e) ExprV v
g
      EBin Bop
_o ExprV v
e1 ExprV v
e2 -> [KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e2) ExprV v
e1
      PImp ExprV v
p1 ExprV v
p2 -> [KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
p2) ExprV v
p1
      PIff ExprV v
p1 ExprV v
p2 -> [KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
p2) ExprV v
p1
      PAtom Brel
_r ExprV v
e1 ExprV v
e2 -> [KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e2) ExprV v
e1
      EIte ExprV v
p ExprV v
e1 ExprV v
e2 -> [KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go ([KVar] -> ExprV v -> [KVar]
go [KVar]
acc ExprV v
e2) ExprV v
e1) ExprV v
p
      PAnd [ExprV v]
ps -> (ExprV v -> [KVar] -> [KVar]) -> [KVar] -> [ExprV v] -> [KVar]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (([KVar] -> ExprV v -> [KVar]) -> ExprV v -> [KVar] -> [KVar]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [KVar] -> ExprV v -> [KVar]
go) [KVar]
acc [ExprV v]
ps
      POr [ExprV v]
ps -> (ExprV v -> [KVar] -> [KVar]) -> [KVar] -> [ExprV v] -> [KVar]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (([KVar] -> ExprV v -> [KVar]) -> ExprV v -> [KVar] -> [KVar]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [KVar] -> ExprV v -> [KVar]
go) [KVar]
acc [ExprV v]
ps

envKVars :: (TaggedC c a) => BindEnv a -> c a -> [KVar]
envKVars :: forall (c :: * -> *) a. TaggedC c a => BindEnv a -> c a -> [KVar]
envKVars BindEnv a
be c a
c = [[KVar]] -> [KVar]
squish [ SortedReft -> [KVar]
kvs SortedReft
sr |  (Symbol
_, SortedReft
sr) <- BindEnv a -> c a -> [(Symbol, SortedReft)]
forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> [(Symbol, SortedReft)]
clhs BindEnv a
be c a
c]
  where
    squish :: [[KVar]] -> [KVar]
squish    = HashSet KVar -> [KVar]
forall a. HashSet a -> [a]
S.toList  (HashSet KVar -> [KVar])
-> ([[KVar]] -> HashSet KVar) -> [[KVar]] -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([KVar] -> HashSet KVar)
-> ([[KVar]] -> [KVar]) -> [[KVar]] -> HashSet KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[KVar]] -> [KVar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    kvs :: SortedReft -> [KVar]
kvs       = Expr -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr (Expr -> [KVar]) -> (SortedReft -> Expr) -> SortedReft -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
forall v. ReftV v -> ExprV v
reftPred (Reft -> Expr) -> (SortedReft -> Reft) -> SortedReft -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft

envKVarsN :: (TaggedC c a) => BindEnv a -> c a -> [(KVar, Int)]
envKVarsN :: forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> [(KVar, BindId)]
envKVarsN BindEnv a
be c a
c = [[KVar]] -> [(KVar, BindId)]
tally [ SortedReft -> [KVar]
kvs SortedReft
sr |  (Symbol
_, SortedReft
sr) <- BindEnv a -> c a -> [(Symbol, SortedReft)]
forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> [(Symbol, SortedReft)]
clhs BindEnv a
be c a
c]
  where
    tally :: [[KVar]] -> [(KVar, BindId)]
tally      = [KVar] -> [(KVar, BindId)]
forall k. (Eq k, Hashable k) => [k] -> [(k, BindId)]
Misc.count ([KVar] -> [(KVar, BindId)])
-> ([[KVar]] -> [KVar]) -> [[KVar]] -> [(KVar, BindId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[KVar]] -> [KVar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    kvs :: SortedReft -> [KVar]
kvs        = Expr -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr (Expr -> [KVar]) -> (SortedReft -> Expr) -> SortedReft -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
forall v. ReftV v -> ExprV v
reftPred (Reft -> Expr) -> (SortedReft -> Reft) -> SortedReft -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft

rhsKVars :: (TaggedC c a) => c a -> [KVar]
rhsKVars :: forall (c :: * -> *) a. TaggedC c a => c a -> [KVar]
rhsKVars = Expr -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr (Expr -> [KVar]) -> (c a -> Expr) -> c a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs -- rhsCs

isKvarC :: (TaggedC c a) => c a -> Bool
isKvarC :: forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isKvarC = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isKvar ([Expr] -> Bool) -> (c a -> [Expr]) -> c a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts (Expr -> [Expr]) -> (c a -> Expr) -> c a -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs

isConcC :: (TaggedC c a) => c a -> Bool
isConcC :: forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isConcC = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isConc ([Expr] -> Bool) -> (c a -> [Expr]) -> c a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts (Expr -> [Expr]) -> (c a -> Expr) -> c a -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs

isKvar :: Expr -> Bool
isKvar :: Expr -> Bool
isKvar PKVar{} = Bool
True
isKvar PGrad{} = Bool
True
isKvar Expr
_       = Bool
False

isConc :: Expr -> Bool
isConc :: Expr -> Bool
isConc = [KVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([KVar] -> Bool) -> (Expr -> [KVar]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [KVar]
forall v. ExprV v -> [KVar]
kvarsExpr

stripCasts :: Expr -> Expr
stripCasts :: Expr -> Expr
stripCasts = (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
forall v. ExprV v -> ExprV v
go
  where
    go :: ExprV v -> ExprV v
go (ECst ExprV v
e Sort
_) = ExprV v
e
    go ExprV v
e          = ExprV v
e

-- stripCasts :: Expr -> Expr
-- stripCasts = mapExpr go
--  where
--    go (ECst e _) = e
--    go e          = e

--------------------------------------------------------------------------------
-- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'
--   to the ty-vars that they should be substituted with. Note the
--   domain and range are both Symbol and not the Int used for real ty-vars.
--------------------------------------------------------------------------------
type CoSub = M.HashMap Symbol Sort

applyCoSub :: CoSub -> Expr -> Expr
applyCoSub :: CoSub -> Expr -> Expr
applyCoSub CoSub
coSub = (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
forall v. ExprV v -> ExprV v
fE
  where
    fE :: ExprV v -> ExprV v
fE (ECoerc Sort
s Sort
t ExprV v
e) = Sort -> Sort -> ExprV v -> ExprV v
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc  (Sort -> Sort
txS Sort
s) (Sort -> Sort
txS Sort
t) ExprV v
e
    fE (ELam (Symbol
x,Sort
t) ExprV v
e) = (Symbol, Sort) -> ExprV v -> ExprV v
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, Sort -> Sort
txS Sort
t)         ExprV v
e
    fE (ECst ExprV v
e Sort
t)     = ExprV v -> Sort -> ExprV v
forall v. ExprV v -> Sort -> ExprV v
ECst ExprV v
e (Sort -> Sort
txS Sort
t)
    fE ExprV v
e              = ExprV v
e
    txS :: Sort -> Sort
txS               = (Sort -> Sort) -> Sort -> Sort
mapSortOnlyOnce Sort -> Sort
fS
    fS :: Sort -> Sort
fS (FObj Symbol
a)       = {- FObj -} Symbol -> Sort
txV Symbol
a
    fS Sort
t              = Sort
t
    txV :: Symbol -> Sort
txV Symbol
a             = Sort -> Symbol -> CoSub -> Sort
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (Symbol -> Sort
FObj Symbol
a) Symbol
a CoSub
coSub


type CoSubV = M.HashMap Sort Sort

applyCoSubV :: CoSubV -> Expr -> Expr
applyCoSubV :: CoSubV -> Expr -> Expr
applyCoSubV CoSubV
coSub = (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
forall v. ExprV v -> ExprV v
fE
  where
    fE :: ExprV v -> ExprV v
fE (ECoerc Sort
s Sort
t ExprV v
e) = Sort -> Sort -> ExprV v -> ExprV v
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc  (Sort -> Sort
txS Sort
s) (Sort -> Sort
txS Sort
t) ExprV v
e
    fE (ELam (Symbol
x,Sort
t) ExprV v
e) = (Symbol, Sort) -> ExprV v -> ExprV v
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, Sort -> Sort
txS Sort
t)         ExprV v
e
    fE (ECst ExprV v
e Sort
t)     = ExprV v -> Sort -> ExprV v
forall v. ExprV v -> Sort -> ExprV v
ECst ExprV v
e (Sort -> Sort
txS Sort
t)
    fE ExprV v
e              = ExprV v
e

    txS :: Sort -> Sort
txS               = (Sort -> Sort) -> Sort -> Sort
mapSortOnlyOnce Sort -> Sort
fS

    fS :: Sort -> Sort
fS Sort
t              = Sort -> Sort -> CoSubV -> Sort
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Sort
t Sort
t CoSubV
coSub

---------------------------------------------------------------------------------
-- | Visitors over @Sort@
---------------------------------------------------------------------------------
foldSort :: (a -> Sort -> a) -> a -> Sort -> a
foldSort :: forall a. (a -> Sort -> a) -> a -> Sort -> a
foldSort a -> Sort -> a
f = a -> Sort -> a
step
  where
    step :: a -> Sort -> a
step a
b Sort
t           = a -> Sort -> a
go (a -> Sort -> a
f a
b Sort
t) Sort
t
    go :: a -> Sort -> a
go a
b (FFunc Sort
t1 Sort
t2) = (a -> Sort -> a) -> a -> [Sort] -> 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' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
    go a
b (FApp Sort
t1 Sort
t2)  = (a -> Sort -> a) -> a -> [Sort] -> 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' a -> Sort -> a
step a
b [Sort
t1, Sort
t2]
    go a
b (FAbs BindId
_ Sort
t)    = a -> Sort -> a
go a
b Sort
t
    go a
b Sort
_             = a
b

-- | Like 'mapSort' but it doesn't substitute on the result
-- of the function.
--
-- > mapSortOnlyOnce [(a,b), (b,c)] a = b
--
-- whereas
--
-- > mapSort [(a,b), (b,c)] a = c
--
mapSortOnlyOnce :: (Sort -> Sort) -> Sort -> Sort
mapSortOnlyOnce :: (Sort -> Sort) -> Sort -> Sort
mapSortOnlyOnce Sort -> Sort
f = Sort -> Sort
step
  where
    step :: Sort -> Sort
step !Sort
x           = Sort -> Sort
f (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Sort -> Sort
go Sort
x
    go :: Sort -> Sort
go (FFunc Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
    go (FApp Sort
t1 Sort
t2)  = Sort -> Sort -> Sort
FApp  (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
    go (FAbs BindId
i Sort
t)    = BindId -> Sort -> Sort
FAbs BindId
i (Sort -> Sort
step Sort
t)
    go !Sort
t             = Sort
t

mapSort :: (Sort -> Sort) -> Sort -> Sort
mapSort :: (Sort -> Sort) -> Sort -> Sort
mapSort Sort -> Sort
f = Sort -> Sort
step
  where
    step :: Sort -> Sort
step !Sort
x           = Sort -> Sort
go (Sort -> Sort
f Sort
x)
    go :: Sort -> Sort
go (FFunc Sort
t1 Sort
t2) = Sort -> Sort -> Sort
FFunc (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
    go (FApp Sort
t1 Sort
t2)  = Sort -> Sort -> Sort
FApp  (Sort -> Sort
step Sort
t1) (Sort -> Sort
step Sort
t2)
    go (FAbs BindId
i Sort
t)    = BindId -> Sort -> Sort
FAbs BindId
i (Sort -> Sort
step Sort
t)
    go !Sort
t             = Sort
t

foldDataDecl :: (a -> Sort -> a) -> a -> DataDecl -> a
foldDataDecl :: forall a. (a -> Sort -> a) -> a -> DataDecl -> a
foldDataDecl a -> Sort -> a
f a
acc = (a -> Sort -> a) -> a -> [Sort] -> 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' a -> Sort -> a
f a
acc ([Sort] -> a) -> (DataDecl -> [Sort]) -> DataDecl -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> [Sort]
dataDeclSorts

dataDeclSorts :: DataDecl -> [Sort]
dataDeclSorts :: DataDecl -> [Sort]
dataDeclSorts = (DataCtor -> [Sort]) -> [DataCtor] -> [Sort]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtor -> [Sort]
dataCtorSorts ([DataCtor] -> [Sort])
-> (DataDecl -> [DataCtor]) -> DataDecl -> [Sort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> [DataCtor]
ddCtors

dataCtorSorts :: DataCtor -> [Sort]
dataCtorSorts :: DataCtor -> [Sort]
dataCtorSorts = (DataField -> Sort) -> [DataField] -> [Sort]
forall a b. (a -> b) -> [a] -> [b]
map DataField -> Sort
dfSort ([DataField] -> [Sort])
-> (DataCtor -> [DataField]) -> DataCtor -> [Sort]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> [DataField]
dcFields
---------------------------------------------------------------
-- | String Constants -----------------------------------------
---------------------------------------------------------------

-- symConstLits    :: FInfo a -> [(Symbol, Sort)]
-- symConstLits fi = [(symbol c, strSort) | c <- symConsts fi]

class SymConsts a where
  symConsts :: a -> [SymConst]


instance SymConsts a => SymConsts [a] where
  symConsts :: [a] -> [SymConst]
symConsts [a]
xs = (a -> [SymConst]) -> [a] -> [SymConst]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts [a]
xs

instance SymConsts AxiomEnv where
  symConsts :: AxiomEnv -> [SymConst]
symConsts AxiomEnv
xs =  [Equation] -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
xs) [SymConst] -> [SymConst] -> [SymConst]
forall a. [a] -> [a] -> [a]
++ [Rewrite] -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
xs)

instance SymConsts Equation where
  symConsts :: Equation -> [SymConst]
symConsts = Expr -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (Expr -> [SymConst])
-> (Equation -> Expr) -> Equation -> [SymConst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> Expr
forall v. EquationV v -> ExprV v
eqBody

instance SymConsts Rewrite where
  symConsts :: Rewrite -> [SymConst]
symConsts = Expr -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (Expr -> [SymConst]) -> (Rewrite -> Expr) -> Rewrite -> [SymConst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> Expr
smBody


-- instance  SymConsts (FInfo a) where
instance (SymConsts (c a)) => SymConsts (GInfo c a) where
  symConsts :: GInfo c a -> [SymConst]
symConsts GInfo c a
fi = [SymConst] -> [SymConst]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([SymConst] -> [SymConst]) -> [SymConst] -> [SymConst]
forall a b. (a -> b) -> a -> b
$ [SymConst]
csLits [SymConst] -> [SymConst] -> [SymConst]
forall a. [a] -> [a] -> [a]
++ [SymConst]
bsLits [SymConst] -> [SymConst] -> [SymConst]
forall a. [a] -> [a] -> [a]
++ [SymConst]
qsLits
    where
      csLits :: [SymConst]
csLits   = (c a -> [SymConst]) -> [c a] -> [SymConst]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap c a -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts ([c a] -> [SymConst]) -> [c a] -> [SymConst]
forall a b. (a -> b) -> a -> b
$ HashMap SubcId (c a) -> [c a]
forall k v. HashMap k v -> [v]
M.elems (HashMap SubcId (c a) -> [c a]) -> HashMap SubcId (c a) -> [c a]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm    GInfo c a
fi
      bsLits :: [SymConst]
bsLits   = BindEnv a -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts                     (BindEnv a -> [SymConst]) -> BindEnv a -> [SymConst]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs    GInfo c a
fi
      qsLits :: [SymConst]
qsLits   = (Qualifier -> [SymConst]) -> [Qualifier] -> [SymConst]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Expr -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (Expr -> [SymConst])
-> (Qualifier -> Expr) -> Qualifier -> [SymConst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qualifier -> Expr
forall v. QualifierV v -> ExprV v
qBody) ([Qualifier] -> [SymConst]) -> [Qualifier] -> [SymConst]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
fi

instance SymConsts (BindEnv a) where
  symConsts :: BindEnv a -> [SymConst]
symConsts    = ((Symbol, SortedReft, a) -> [SymConst])
-> [(Symbol, SortedReft, a)] -> [SymConst]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SortedReft -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (SortedReft -> [SymConst])
-> ((Symbol, SortedReft, a) -> SortedReft)
-> (Symbol, SortedReft, a)
-> [SymConst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft, a) -> SortedReft
forall a b c. (a, b, c) -> b
Misc.snd3) ([(Symbol, SortedReft, a)] -> [SymConst])
-> (BindEnv a -> [(Symbol, SortedReft, a)])
-> BindEnv a
-> [SymConst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap BindId (Symbol, SortedReft, a) -> [(Symbol, SortedReft, a)]
forall k v. HashMap k v -> [v]
M.elems (HashMap BindId (Symbol, SortedReft, a)
 -> [(Symbol, SortedReft, a)])
-> (BindEnv a -> HashMap BindId (Symbol, SortedReft, a))
-> BindEnv a
-> [(Symbol, SortedReft, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindEnv a -> HashMap BindId (Symbol, SortedReft, a)
forall a. SizedEnv a -> BindMap a
beBinds

instance SymConsts (SubC a) where
  symConsts :: SubC a -> [SymConst]
symConsts SubC a
c  = SortedReft -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (SubC a -> SortedReft
forall a. SubC a -> SortedReft
slhs SubC a
c) [SymConst] -> [SymConst] -> [SymConst]
forall a. [a] -> [a] -> [a]
++
                 SortedReft -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (SubC a -> SortedReft
forall a. SubC a -> SortedReft
srhs SubC a
c)

instance SymConsts (SimpC a) where
  symConsts :: SimpC a -> [SymConst]
symConsts SimpC a
c  = Expr -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
c)

instance SymConsts SortedReft where
  symConsts :: SortedReft -> [SymConst]
symConsts = Reft -> [SymConst]
forall a. SymConsts a => a -> [SymConst]
symConsts (Reft -> [SymConst])
-> (SortedReft -> Reft) -> SortedReft -> [SymConst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft

instance SymConsts Reft where
  symConsts :: Reft -> [SymConst]
symConsts (Reft (Symbol
_, Expr
ra)) = Expr -> [SymConst]
forall t. Foldable t => t -> [SymConst]
getSymConsts Expr
ra


instance SymConsts Expr where
  symConsts :: Expr -> [SymConst]
symConsts = Expr -> [SymConst]
forall t. Foldable t => t -> [SymConst]
getSymConsts

getSymConsts :: Foldable t => t -> [SymConst]
getSymConsts :: forall t. Foldable t => t -> [SymConst]
getSymConsts         = Folder [SymConst] () -> () -> [SymConst] -> t -> [SymConst]
forall t a ctx.
(Foldable t, Monoid a) =>
Folder a ctx -> ctx -> a -> t -> a
fold Folder [SymConst] ()
forall {ctx}. Folder [SymConst] ctx
scVis () []
  where
    scVis :: Folder [SymConst] ctx
scVis            = (Folder [SymConst] t
forall {ctx}. Folder [SymConst] ctx
forall acc ctx. Monoid acc => Folder acc ctx
defaultFolder :: Folder [SymConst] t)  { accExpr = sc }
    sc :: p -> ExprV v -> [SymConst]
sc p
_ (ESym SymConst
c)    = [SymConst
c]
    sc p
_ ExprV v
_           = []