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

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

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

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

  -- * Default Visitor
  , defaultVisitor

  -- * Transformers
  , trans

  -- * Accumulators
  , fold

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

  -- * Coercion Substitutions
  , CoSub
  , applyCoSub

  -- * 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




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

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

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

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

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

fold         :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a
fold :: forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> a
fold Visitor a ctx
v ctx
c a
a t
t = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a ctx t.
Visitor a ctx
-> ctx
-> a
-> (Visitor a ctx -> ctx -> t -> State a t)
-> t
-> (t, a)
execVisitM Visitor a ctx
v ctx
c a
a forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit t
t

trans        :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t
trans :: forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans Visitor a ctx
v ctx
c a
_ t
z = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a ctx t.
Visitor a ctx
-> ctx
-> a
-> (Visitor a ctx -> ctx -> t -> State a t)
-> t
-> (t, a)
execVisitM Visitor a ctx
v ctx
c forall a. Monoid a => a
mempty forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit t
z

execVisitM :: Visitor a ctx -> ctx -> a -> (Visitor a ctx -> ctx -> t -> State a t) -> t -> (t, a)
execVisitM :: forall a ctx t.
Visitor a ctx
-> ctx
-> a
-> (Visitor a ctx -> ctx -> t -> State a t)
-> t
-> (t, a)
execVisitM Visitor a ctx
v ctx
c a
a Visitor a ctx -> ctx -> t -> State a t
f t
x = forall s a. State s a -> s -> (a, s)
runState (Visitor a ctx -> ctx -> t -> State a t
f Visitor a ctx
v ctx
c t
x) a
a

type VisitM acc = State acc

accum :: (Monoid a) => a -> VisitM a ()
accum :: forall a. Monoid a => a -> VisitM a ()
accum !a
z = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Monoid a => a -> a -> a
mappend a
z)
  -- do
  -- !cur <- get
  -- put ((mappend $!! z) $!! cur)

class Visitable t where
  visit :: (Monoid a) => Visitor a c -> c -> t -> VisitM a t

instance Visitable Expr where
  visit :: forall a c. Monoid a => Visitor a c -> c -> Expr -> VisitM a Expr
visit = forall a c. Monoid a => Visitor a c -> c -> Expr -> VisitM a Expr
visitExpr

instance Visitable Reft where
  visit :: forall a c. Monoid a => Visitor a c -> c -> Reft -> VisitM a Reft
visit Visitor a c
v c
c (Reft (Symbol
x, Expr
ra)) = (Symbol, Expr) -> Reft
Reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c Expr
ra

instance Visitable SortedReft where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> SortedReft -> VisitM a SortedReft
visit Visitor a c
v c
c (RR Sort
t Reft
r) = Sort -> Reft -> SortedReft
RR Sort
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c Reft
r

instance Visitable (Symbol, SortedReft, a) where
  visit :: forall a c.
Monoid a =>
Visitor a c
-> c -> (Symbol, SortedReft, a) -> VisitM a (Symbol, SortedReft, a)
visit Visitor a c
v c
c (Symbol
sym, SortedReft
sr, a
a) = (Symbol
sym, ,a
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c SortedReft
sr

instance Visitable (BindEnv a) where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> BindEnv a -> VisitM a (BindEnv a)
visit Visitor a c
v c
c = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor 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 Visitable (SimpC a) where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> SimpC a -> VisitM a (SimpC a)
visit Visitor a c
v c
c SimpC a
x = do
    Expr
rhs' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (forall a. SimpC a -> Expr
_crhs SimpC a
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return SimpC a
x { _crhs :: Expr
_crhs = Expr
rhs' }

instance Visitable (SubC a) where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> SubC a -> VisitM a (SubC a)
visit Visitor a c
v c
c SubC a
x = do
    SortedReft
lhs' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (forall a. SubC a -> SortedReft
slhs SubC a
x)
    SortedReft
rhs' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (forall a. SubC a -> SortedReft
srhs SubC a
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return SubC a
x { slhs :: SortedReft
slhs = SortedReft
lhs', srhs :: SortedReft
srhs = SortedReft
rhs' }

instance (Visitable (c a)) => Visitable (GInfo c a) where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> GInfo c a -> VisitM a (GInfo c a)
visit Visitor a c
v c
c GInfo c a
x = do
    HashMap SubcId (c a)
cm' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c) (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm GInfo c a
x)
    BindEnv a
bs' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs GInfo c a
x)
    AxiomEnv
ae' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return GInfo c a
x { cm :: HashMap SubcId (c a)
cm = HashMap SubcId (c a)
cm', bs :: BindEnv a
bs = BindEnv a
bs', ae :: AxiomEnv
ae = AxiomEnv
ae' }

instance Visitable AxiomEnv where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> AxiomEnv -> VisitM a AxiomEnv
visit Visitor a c
v c
c AxiomEnv
x = do
    [Equation]
eqs'    <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c) (AxiomEnv -> [Equation]
aenvEqs   AxiomEnv
x)
    [Rewrite]
simpls' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c) (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return AxiomEnv
x { aenvEqs :: [Equation]
aenvEqs = [Equation]
eqs' , aenvSimpl :: [Rewrite]
aenvSimpl = [Rewrite]
simpls'}

instance Visitable Equation where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> Equation -> VisitM a Equation
visit Visitor a c
v c
c Equation
eq = do
    Expr
body' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (Equation -> Expr
eqBody Equation
eq)
    forall (m :: * -> *) a. Monad m => a -> m a
return Equation
eq { eqBody :: Expr
eqBody = Expr
body' }

instance Visitable Rewrite where
  visit :: forall a c.
Monoid a =>
Visitor a c -> c -> Rewrite -> VisitM a Rewrite
visit Visitor a c
v c
c Rewrite
rw = do
    Expr
body' <- forall t a c.
(Visitable t, Monoid a) =>
Visitor a c -> c -> t -> VisitM a t
visit Visitor a c
v c
c (Rewrite -> Expr
smBody Rewrite
rw)
    forall (m :: * -> *) a. Monad m => a -> m a
return Rewrite
rw { smBody :: Expr
smBody = Expr
body' }

---------------------------------------------------------------------------------
visitExpr :: (Monoid a) => Visitor a ctx -> ctx -> Expr -> VisitM a Expr
visitExpr :: forall a c. Monoid a => Visitor a c -> c -> Expr -> VisitM a Expr
visitExpr !Visitor a ctx
v    = ctx -> Expr -> StateT a Identity Expr
vE
  where
    vE :: ctx -> Expr -> StateT a Identity Expr
vE !ctx
c !Expr
e    = do {- SCC "visitExpr.vE.accum" -} forall a. Monoid a => a -> VisitM a ()
accum a
acc
                     {- SCC "visitExpr.vE.step" -}  ctx -> Expr -> StateT a Identity Expr
step ctx
c' Expr
e'
      where !c' :: ctx
c'  = forall acc ctx. Visitor acc ctx -> ctx -> Expr -> ctx
ctxExpr Visitor a ctx
v ctx
c  Expr
e
            !e' :: Expr
e'  = forall acc ctx. Visitor acc ctx -> ctx -> Expr -> Expr
txExpr  Visitor a ctx
v ctx
c' Expr
e
            !acc :: a
acc = forall acc ctx. Visitor acc ctx -> ctx -> Expr -> acc
accExpr Visitor a ctx
v ctx
c' Expr
e
    step :: ctx -> Expr -> StateT a Identity Expr
step ctx
_ e :: Expr
e@(ESym SymConst
_)       = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    step ctx
_ e :: Expr
e@(ECon Constant
_)       = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    step ctx
_ e :: Expr
e@(EVar Symbol
_)       = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    step !ctx
c (EApp Expr
f Expr
e)      = Expr -> Expr -> Expr
EApp        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
f  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step !ctx
c (ENeg Expr
e)        = Expr -> Expr
ENeg        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step !ctx
c (EBin Bop
o Expr
e1 Expr
e2)  = Bop -> Expr -> Expr -> Expr
EBin Bop
o      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e2
    step !ctx
c (EIte Expr
p Expr
e1 Expr
e2)  = Expr -> Expr -> Expr -> Expr
EIte        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e2
    step !ctx
c (ECst Expr
e Sort
t)      = (Expr -> Sort -> Expr
`ECst` Sort
t)  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step !ctx
c (PAnd  [Expr]
ps)      = [Expr] -> Expr
PAnd        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ctx -> Expr -> StateT a Identity Expr
vE ctx
c forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
ps)
    step !ctx
c (POr  [Expr]
ps)       = [Expr] -> Expr
POr         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ctx -> Expr -> StateT a Identity Expr
vE ctx
c forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
ps)
    step !ctx
c (PNot Expr
p)        = Expr -> Expr
PNot        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p
    step !ctx
c (PImp Expr
p1 Expr
p2)    = Expr -> Expr -> Expr
PImp        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p2
    step !ctx
c (PIff Expr
p1 Expr
p2)    = Expr -> Expr -> Expr
PIff        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p2
    step !ctx
c (PAtom Brel
r Expr
e1 Expr
e2) = Brel -> Expr -> Expr -> Expr
PAtom Brel
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e2
    step !ctx
c (PAll [(Symbol, Sort)]
xts Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
PAll   [(Symbol, Sort)]
xts  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p
    step !ctx
c (ELam (Symbol
x,Sort
t) Expr
e)  = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x,Sort
t)  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step !ctx
c (ECoerc Sort
a Sort
t Expr
e)  = Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step !ctx
c (PExist [(Symbol, Sort)]
xts Expr
p)  = [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xts  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
p
    step !ctx
c (ETApp Expr
e Sort
s)     = (Expr -> Sort -> Expr
`ETApp` Sort
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step !ctx
c (ETAbs Expr
e Symbol
s)     = (Expr -> Symbol -> Expr
`ETAbs` Symbol
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity Expr
vE ctx
c Expr
e
    step ctx
_  p :: Expr
p@(PKVar KVar
_ Subst
_)   = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
p
    step !ctx
c (PGrad KVar
k Subst
su GradInfo
i Expr
e) = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx -> Expr -> StateT a Identity 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 = forall t. Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapKVars' 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, Subst) -> Maybe Expr) -> t -> t
mapKVars' (KVar, Subst) -> Maybe Expr
f            = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans forall {ctx}. Visitor () ctx
kvVis () ()
  where
    kvVis :: Visitor () ctx
kvVis              = forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr :: ctx -> Expr -> Expr
txExpr = forall {p}. p -> Expr -> Expr
txK }
    txK :: p -> Expr -> Expr
txK p
_ (PKVar KVar
k Subst
su)
      | Just Expr
p' <- (KVar, Subst) -> Maybe Expr
f (KVar
k, Subst
su) = forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p'
    txK p
_ (PGrad KVar
k Subst
su GradInfo
_ Expr
_)
      | Just Expr
p' <- (KVar, Subst) -> Maybe Expr
f (KVar
k, Subst
su) = forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p'
    txK p
_ Expr
p            = Expr
p



mapGVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapGVars' :: forall t. Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapGVars' (KVar, Subst) -> Maybe Expr
f            = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans forall {ctx}. Visitor () ctx
kvVis () ()
  where
    kvVis :: Visitor () ctx
kvVis              = forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr :: ctx -> Expr -> Expr
txExpr = forall {p}. p -> Expr -> Expr
txK }
    txK :: p -> Expr -> Expr
txK p
_ (PGrad KVar
k Subst
su GradInfo
_ Expr
_)
      | Just Expr
p' <- (KVar, Subst) -> Maybe Expr
f (KVar
k, Subst
su) = forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p'
    txK p
_ Expr
p            = Expr
p

mapExpr :: Visitable t => (Expr -> Expr) -> t -> t
mapExpr :: forall t. Visitable t => (Expr -> Expr) -> t -> t
mapExpr Expr -> Expr
f = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans (forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor {txExpr :: () -> Expr -> Expr
txExpr = forall a b. a -> b -> a
const 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 forall a b. (a -> b) -> a -> b
$ case Expr
e0 of
      EApp Expr
f Expr
e -> Expr -> Expr -> Expr
EApp (Expr -> Expr
go Expr
f) (Expr -> Expr
go Expr
e)
      ENeg Expr
e -> Expr -> Expr
ENeg (Expr -> Expr
go Expr
e)
      EBin Bop
o Expr
e1 Expr
e2 ->  Bop -> Expr -> Expr -> Expr
EBin Bop
o (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
      EIte Expr
p Expr
e1 Expr
e2 -> Expr -> Expr -> Expr -> Expr
EIte (Expr -> Expr
go Expr
p) (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
      ECst Expr
e Sort
t -> Expr -> Sort -> Expr
ECst (Expr -> Expr
go Expr
e) Sort
t
      PAnd [Expr]
ps -> [Expr] -> Expr
PAnd (forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
go [Expr]
ps)
      POr [Expr]
ps -> [Expr] -> Expr
POr (forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
go [Expr]
ps)
      PNot Expr
p -> Expr -> Expr
PNot (Expr -> Expr
go Expr
p)
      PImp Expr
p1 Expr
p2 -> Expr -> Expr -> Expr
PImp (Expr -> Expr
go Expr
p1) (Expr -> Expr
go Expr
p2)
      PIff Expr
p1 Expr
p2 -> Expr -> Expr -> Expr
PIff (Expr -> Expr
go Expr
p1) (Expr -> Expr
go Expr
p2)
      PAtom Brel
r Expr
e1 Expr
e2 -> Brel -> Expr -> Expr -> Expr
PAtom Brel
r (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
      PAll [(Symbol, Sort)]
xts Expr
p -> [(Symbol, Sort)] -> Expr -> Expr
PAll [(Symbol, Sort)]
xts (Expr -> Expr
go Expr
p)
      ELam (Symbol
x,Sort
t) Expr
e -> (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x,Sort
t) (Expr -> Expr
go Expr
e)
      ECoerc Sort
a Sort
t Expr
e -> Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t (Expr -> Expr
go Expr
e)
      PExist [(Symbol, Sort)]
xts Expr
p -> [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xts (Expr -> Expr
go Expr
p)
      ETApp Expr
e Sort
s -> Expr -> Sort -> Expr
ETApp (Expr -> Expr
go Expr
e) Sort
s
      ETAbs Expr
e Symbol
s -> Expr -> Symbol -> Expr
ETAbs (Expr -> Expr
go Expr
e) Symbol
s
      PGrad KVar
k Subst
su GradInfo
i Expr
e -> KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i (Expr -> Expr
go 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


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
_ Subst
_)   = Expr -> m Expr
f Expr
e
    go (PGrad KVar
k Subst
s GradInfo
i Expr
e) = Expr -> m Expr
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
s GradInfo
i 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
ENeg 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
PNot 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
`ECst` Sort
t) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
PAll   [(Symbol, Sort)]
xts 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x,Sort
t) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xts 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
`ETApp` Sort
s) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Symbol -> Expr
`ETAbs` Symbol
s) 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
EApp        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
g  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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Bop -> Expr -> Expr -> Expr
EBin Bop
o      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
e1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
PImp        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
p1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
PIff        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
p1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Brel -> Expr -> Expr -> Expr
PAtom Brel
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
e1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr -> Expr
EIte        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Expr -> m Expr
go Expr
p  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> m Expr
go Expr
e1 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
PAnd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> m Expr
go forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
ps)
    go (POr [Expr]
ps)        = Expr -> m Expr
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
POr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> m Expr
go forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
ps)

mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts :: forall t. Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts KVar -> Subst -> Subst
f          = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> t
trans forall {ctx}. Visitor () ctx
kvVis () ()
  where
    kvVis :: Visitor () ctx
kvVis                = forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor { txExpr :: ctx -> Expr -> Expr
txExpr = forall {p}. p -> Expr -> Expr
txK }
    txK :: p -> Expr -> Expr
txK p
_ (PKVar KVar
k Subst
su)   = KVar -> Subst -> Expr
PKVar KVar
k (KVar -> Subst -> Subst
f KVar
k Subst
su)
    txK p
_ (PGrad KVar
k Subst
su GradInfo
i Expr
e) = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k (KVar -> Subst -> Subst
f KVar
k Subst
su) GradInfo
i Expr
e
    txK p
_ 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 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 = forall a. Semigroup a => a -> a -> a
(<>)

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


lamSize :: Visitable t => t -> Integer
lamSize :: forall t. Visitable t => t -> SubcId
lamSize t
t    = SubcId
n
  where
    MInt SubcId
n = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> a
fold forall {ctx}. Visitor MInt ctx
szV () forall a. Monoid a => a
mempty t
t
    szV :: Visitor MInt ctx
szV    = (forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor :: Visitor MInt t) { accExpr :: ctx -> Expr -> MInt
accExpr = forall {p}. p -> Expr -> MInt
accum }
    accum :: p -> Expr -> MInt
accum p
_ (ELam (Symbol, Sort)
_ Expr
_) = SubcId -> MInt
MInt SubcId
1
    accum p
_ Expr
_          = SubcId -> MInt
MInt SubcId
0

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

{-# SCC kvarsExpr #-}
kvarsExpr :: Expr -> [KVar]
kvarsExpr :: Expr -> [KVar]
kvarsExpr = [KVar] -> Expr -> [KVar]
go []
  where
    go :: [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e0 = case Expr
e0 of
      ESym SymConst
_ -> [KVar]
acc
      ECon Constant
_ -> [KVar]
acc
      EVar Symbol
_ -> [KVar]
acc
      PKVar KVar
k Subst
_ -> KVar
k forall a. a -> [a] -> [a]
: [KVar]
acc
      PGrad KVar
k Subst
_ GradInfo
_ Expr
_ -> KVar
k forall a. a -> [a] -> [a]
: [KVar]
acc
      ENeg Expr
e -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e
      PNot Expr
p -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
p
      ECst Expr
e Sort
_t -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e
      PAll [(Symbol, Sort)]
_xts Expr
p -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
p
      ELam (Symbol, Sort)
_b Expr
e -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e
      ECoerc Sort
_a Sort
_t Expr
e -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e
      PExist [(Symbol, Sort)]
_xts Expr
p -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
p
      ETApp Expr
e Sort
_s -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e
      ETAbs Expr
e Symbol
_s -> [KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e
      EApp Expr
g Expr
e -> [KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e) Expr
g
      EBin Bop
_o Expr
e1 Expr
e2 -> [KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e2) Expr
e1
      PImp Expr
p1 Expr
p2 -> [KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
p2) Expr
p1
      PIff Expr
p1 Expr
p2 -> [KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
p2) Expr
p1
      PAtom Brel
_r Expr
e1 Expr
e2 -> [KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e2) Expr
e1
      EIte Expr
p Expr
e1 Expr
e2 -> [KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go ([KVar] -> Expr -> [KVar]
go [KVar]
acc Expr
e2) Expr
e1) Expr
p
      PAnd [Expr]
ps -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip [KVar] -> Expr -> [KVar]
go) [KVar]
acc [Expr]
ps
      POr [Expr]
ps -> forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip [KVar] -> Expr -> [KVar]
go) [KVar]
acc [Expr]
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) <- forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> [(Symbol, SortedReft)]
clhs BindEnv a
be c a
c]
  where
    squish :: [[KVar]] -> [KVar]
squish    = forall a. HashSet a -> [a]
S.toList  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    kvs :: SortedReft -> [KVar]
kvs       = Expr -> [KVar]
kvarsExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred 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, Int)]
envKVarsN BindEnv a
be c a
c = [[KVar]] -> [(KVar, Int)]
tally [ SortedReft -> [KVar]
kvs SortedReft
sr |  (Symbol
_, SortedReft
sr) <- forall (c :: * -> *) a.
TaggedC c a =>
BindEnv a -> c a -> [(Symbol, SortedReft)]
clhs BindEnv a
be c a
c]
  where
    tally :: [[KVar]] -> [(KVar, Int)]
tally      = forall k. (Eq k, Hashable k) => [k] -> [(k, Int)]
Misc.count forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    kvs :: SortedReft -> [KVar]
kvs        = Expr -> [KVar]
kvarsExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred 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]
kvarsExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isKvar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isConc forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [KVar]
kvarsExpr

stripCasts :: Expr -> Expr
stripCasts :: Expr -> Expr
stripCasts = (Expr -> Expr) -> Expr -> Expr
mapExprOnExpr Expr -> Expr
go
  where
    go :: Expr -> Expr
go (ECst Expr
e Sort
_) = Expr
e
    go Expr
e          = Expr
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
fE
  where
    fE :: Expr -> Expr
fE (ECoerc Sort
s Sort
t Expr
e) = Sort -> Sort -> Expr -> Expr
ECoerc  (Sort -> Sort
txS Sort
s) (Sort -> Sort
txS Sort
t) Expr
e
    fE (ELam (Symbol
x,Sort
t) Expr
e) = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort -> Sort
txS Sort
t)         Expr
e
    fE (ECst Expr
e Sort
t)     = Expr -> Sort -> Expr
ECst Expr
e (Sort -> Sort
txS Sort
t)
    fE Expr
e              = Expr
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             = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (Symbol -> Sort
FObj Symbol
a) Symbol
a CoSub
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) = 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)  = 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 Int
_ 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 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 Int
i Sort
t)    = Int -> Sort -> Sort
FAbs Int
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 Int
i Sort
t)    = Int -> Sort -> Sort
FAbs Int
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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' a -> Sort -> a
f a
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> [Sort]
dataDeclSorts

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

dataCtorSorts :: DataCtor -> [Sort]
dataCtorSorts :: DataCtor -> [Sort]
dataCtorSorts = forall a b. (a -> b) -> [a] -> [b]
map DataField -> Sort
dfSort 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. SymConsts a => a -> [SymConst]
symConsts [a]
xs

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

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

instance SymConsts Rewrite where
  symConsts :: Rewrite -> [SymConst]
symConsts = forall a. SymConsts a => a -> [SymConst]
symConsts 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 = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ [SymConst]
csLits forall a. [a] -> [a] -> [a]
++ [SymConst]
bsLits forall a. [a] -> [a] -> [a]
++ [SymConst]
qsLits
    where
      csLits :: [SymConst]
csLits   = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. SymConsts a => a -> [SymConst]
symConsts forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [v]
M.elems  forall a b. (a -> b) -> a -> b
$  forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm    GInfo c a
fi
      bsLits :: [SymConst]
bsLits   = forall a. SymConsts a => a -> [SymConst]
symConsts           forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs                GInfo c a
fi
      qsLits :: [SymConst]
qsLits   = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. SymConsts a => a -> [SymConst]
symConsts forall a b. (a -> b) -> a -> b
$ Qualifier -> Expr
qBody   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals GInfo c a
fi

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

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

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

instance SymConsts SortedReft where
  symConsts :: SortedReft -> [SymConst]
symConsts = forall a. SymConsts a => a -> [SymConst]
symConsts 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)) = forall t. Visitable t => t -> [SymConst]
getSymConsts Expr
ra


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

getSymConsts :: Visitable t => t -> [SymConst]
getSymConsts :: forall t. Visitable t => t -> [SymConst]
getSymConsts         = forall t a ctx.
(Visitable t, Monoid a) =>
Visitor a ctx -> ctx -> a -> t -> a
fold forall {ctx}. Visitor [SymConst] ctx
scVis () []
  where
    scVis :: Visitor [SymConst] ctx
scVis            = (forall acc ctx. Monoid acc => Visitor acc ctx
defaultVisitor :: Visitor [SymConst] t)  { accExpr :: ctx -> Expr -> [SymConst]
accExpr = forall {p}. p -> Expr -> [SymConst]
sc }
    sc :: p -> Expr -> [SymConst]
sc p
_ (ESym SymConst
c)    = [SymConst
c]
    sc p
_ Expr
_           = []