{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleInstances #-}

{-# OPTIONS_GHC -Wno-orphans   #-}

-- | This module contains the various instances for Subable,
--   which (should) depend on the visitors, and hence cannot
--   be in the same place as the @Term@ definitions.
module Language.Fixpoint.Types.Substitutions (
    mkSubst
  , isEmptySubst
  , substExcept
  , substfExcept
  , subst1Except
  , targetSubstSyms
  , filterSubst
  , catSubst
  , exprSymbolsSet
  , meetReft
  , pprReft
  ) where

import           Data.Maybe
import qualified Data.HashMap.Strict       as M
import qualified Data.HashSet              as S
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.Sorts
import           Language.Fixpoint.Types.Refinements
import           Language.Fixpoint.Misc
import           Text.PrettyPrint.HughesPJ.Compat
import           Text.Printf               (printf)

instance Semigroup Subst where
  <> :: Subst -> Subst -> Subst
(<>) = Subst -> Subst -> Subst
catSubst

instance Monoid Subst where
  mempty :: Subst
mempty  = Subst
emptySubst
  mappend :: Subst -> Subst -> Subst
mappend = Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
(<>)

filterSubst :: (Symbol -> Expr -> Bool) -> Subst -> Subst
filterSubst :: (Symbol -> ExprV Symbol -> Bool) -> Subst -> Subst
filterSubst Symbol -> ExprV Symbol -> Bool
f (Su HashMap Symbol (ExprV Symbol)
m) = HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su ((Symbol -> ExprV Symbol -> Bool)
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey Symbol -> ExprV Symbol -> Bool
f HashMap Symbol (ExprV Symbol)
m)

emptySubst :: Subst
emptySubst :: Subst
emptySubst = HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su HashMap Symbol (ExprV Symbol)
forall k v. HashMap k v
M.empty

catSubst :: Subst -> Subst -> Subst
catSubst :: Subst -> Subst -> Subst
catSubst (Su HashMap Symbol (ExprV Symbol)
s1) θ2 :: Subst
θ2@(Su HashMap Symbol (ExprV Symbol)
s2) = HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$ HashMap Symbol (ExprV Symbol)
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap Symbol (ExprV Symbol)
s1' HashMap Symbol (ExprV Symbol)
s2
  where
    s1' :: HashMap Symbol (ExprV Symbol)
s1'                     = Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
θ2 (ExprV Symbol -> ExprV Symbol)
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Symbol (ExprV Symbol)
s1

mkSubst :: [(Symbol, Expr)] -> Subst
mkSubst :: [(Symbol, ExprV Symbol)] -> Subst
mkSubst = HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> ([(Symbol, ExprV Symbol)] -> HashMap Symbol (ExprV Symbol))
-> [(Symbol, ExprV Symbol)]
-> Subst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, ExprV Symbol)] -> HashMap Symbol (ExprV Symbol)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, ExprV Symbol)] -> HashMap Symbol (ExprV Symbol))
-> ([(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)])
-> [(Symbol, ExprV Symbol)]
-> HashMap Symbol (ExprV Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)]
forall a. [a] -> [a]
reverse ([(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)])
-> ([(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)])
-> [(Symbol, ExprV Symbol)]
-> [(Symbol, ExprV Symbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, ExprV Symbol) -> Bool)
-> [(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, ExprV Symbol) -> Bool
forall {a}. Eq a => (a, ExprV a) -> Bool
notTrivial
  where
    notTrivial :: (a, ExprV a) -> Bool
notTrivial (a
x, EVar a
y) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y
    notTrivial (a, ExprV a)
_           = Bool
True

isEmptySubst :: Subst -> Bool
isEmptySubst :: Subst -> Bool
isEmptySubst (Su HashMap Symbol (ExprV Symbol)
xes) = HashMap Symbol (ExprV Symbol) -> Bool
forall k v. HashMap k v -> Bool
M.null HashMap Symbol (ExprV Symbol)
xes

targetSubstSyms :: Subst -> [Symbol]
targetSubstSyms :: Subst -> [Symbol]
targetSubstSyms (Su HashMap Symbol (ExprV Symbol)
ms) = [ExprV Symbol] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ([ExprV Symbol] -> [Symbol]) -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ HashMap Symbol (ExprV Symbol) -> [ExprV Symbol]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol (ExprV Symbol)
ms



instance Subable () where
  syms :: () -> [Symbol]
syms ()
_      = []
  subst :: Subst -> () -> ()
subst Subst
_ ()  = ()
  substf :: (Symbol -> ExprV Symbol) -> () -> ()
substf Symbol -> ExprV Symbol
_ () = ()
  substa :: (Symbol -> Symbol) -> () -> ()
substa Symbol -> Symbol
_ () = ()

instance (Subable a, Subable b) => Subable (a,b) where
  syms :: (a, b) -> [Symbol]
syms  (a
x, b
y)   = a -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms a
x [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ b -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms b
y
  subst :: Subst -> (a, b) -> (a, b)
subst Subst
su (a
x,b
y) = (Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst Subst
su a
x, Subst -> b -> b
forall a. Subable a => Subst -> a -> a
subst Subst
su b
y)
  substf :: (Symbol -> ExprV Symbol) -> (a, b) -> (a, b)
substf Symbol -> ExprV Symbol
f (a
x,b
y) = ((Symbol -> ExprV Symbol) -> a -> a
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f a
x, (Symbol -> ExprV Symbol) -> b -> b
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f b
y)
  substa :: (Symbol -> Symbol) -> (a, b) -> (a, b)
substa Symbol -> Symbol
f (a
x,b
y) = ((Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f a
x, (Symbol -> Symbol) -> b -> b
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f b
y)

instance Subable a => Subable [a] where
  syms :: [a] -> [Symbol]
syms   = (a -> [Symbol]) -> [a] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms
  subst :: Subst -> [a] -> [a]
subst  = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> [a] -> [a])
-> (Subst -> a -> a) -> Subst -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst
  substf :: (Symbol -> ExprV Symbol) -> [a] -> [a]
substf = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> [a] -> [a])
-> ((Symbol -> ExprV Symbol) -> a -> a)
-> (Symbol -> ExprV Symbol)
-> [a]
-> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> ExprV Symbol) -> a -> a
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> [a] -> [a]
substa = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> [a] -> [a])
-> ((Symbol -> Symbol) -> a -> a)
-> (Symbol -> Symbol)
-> [a]
-> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa

instance Subable a => Subable (Maybe a) where
  syms :: Maybe a -> [Symbol]
syms   = (a -> [Symbol]) -> [a] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap a -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ([a] -> [Symbol]) -> (Maybe a -> [a]) -> Maybe a -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList
  subst :: Subst -> Maybe a -> Maybe a
subst  = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> (Subst -> a -> a) -> Subst -> Maybe a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst
  substf :: (Symbol -> ExprV Symbol) -> Maybe a -> Maybe a
substf = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> ((Symbol -> ExprV Symbol) -> a -> a)
-> (Symbol -> ExprV Symbol)
-> Maybe a
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> ExprV Symbol) -> a -> a
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> Maybe a -> Maybe a
substa = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> ((Symbol -> Symbol) -> a -> a)
-> (Symbol -> Symbol)
-> Maybe a
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa


instance Subable a => Subable (M.HashMap k a) where
  syms :: HashMap k a -> [Symbol]
syms   = [a] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ([a] -> [Symbol])
-> (HashMap k a -> [a]) -> HashMap k a -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap k a -> [a]
forall k v. HashMap k v -> [v]
M.elems
  subst :: Subst -> HashMap k a -> HashMap k a
subst  = (a -> a) -> HashMap k a -> HashMap k a
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((a -> a) -> HashMap k a -> HashMap k a)
-> (Subst -> a -> a) -> Subst -> HashMap k a -> HashMap k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst
  substf :: (Symbol -> ExprV Symbol) -> HashMap k a -> HashMap k a
substf = (a -> a) -> HashMap k a -> HashMap k a
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((a -> a) -> HashMap k a -> HashMap k a)
-> ((Symbol -> ExprV Symbol) -> a -> a)
-> (Symbol -> ExprV Symbol)
-> HashMap k a
-> HashMap k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> ExprV Symbol) -> a -> a
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> HashMap k a -> HashMap k a
substa = (a -> a) -> HashMap k a -> HashMap k a
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((a -> a) -> HashMap k a -> HashMap k a)
-> ((Symbol -> Symbol) -> a -> a)
-> (Symbol -> Symbol)
-> HashMap k a
-> HashMap k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa

subst1Except :: (Subable a) => [Symbol] -> a -> (Symbol, Expr) -> a
subst1Except :: forall a. Subable a => [Symbol] -> a -> (Symbol, ExprV Symbol) -> a
subst1Except [Symbol]
xs a
z su :: (Symbol, ExprV Symbol)
su@(Symbol
x, ExprV Symbol
_)
  | Symbol
x Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs = a
z
  | Bool
otherwise   = a -> (Symbol, ExprV Symbol) -> a
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
subst1 a
z (Symbol, ExprV Symbol)
su

substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
substfExcept :: (Symbol -> ExprV Symbol) -> [Symbol] -> Symbol -> ExprV Symbol
substfExcept Symbol -> ExprV Symbol
f [Symbol]
xs Symbol
y = if Symbol
y Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs then Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
y else Symbol -> ExprV Symbol
f Symbol
y

substExcept  :: Subst -> [Symbol] -> Subst
-- substExcept  (Su m) xs = Su (foldr M.delete m xs)
substExcept :: Subst -> [Symbol] -> Subst
substExcept (Su HashMap Symbol (ExprV Symbol)
xes) [Symbol]
xs = HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> ExprV Symbol -> Bool)
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (Bool -> ExprV Symbol -> Bool
forall a b. a -> b -> a
const (Bool -> ExprV Symbol -> Bool)
-> (Symbol -> Bool) -> Symbol -> ExprV Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs)) HashMap Symbol (ExprV Symbol)
xes

instance Subable Symbol where
  substa :: (Symbol -> Symbol) -> Symbol -> Symbol
substa Symbol -> Symbol
f                 = Symbol -> Symbol
f
  substf :: (Symbol -> ExprV Symbol) -> Symbol -> Symbol
substf Symbol -> ExprV Symbol
f Symbol
x               = Maybe (ExprV Symbol) -> Symbol -> Symbol
subSymbol (ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just (Symbol -> ExprV Symbol
f Symbol
x)) Symbol
x
  subst :: Subst -> Symbol -> Symbol
subst Subst
su Symbol
x               = Maybe (ExprV Symbol) -> Symbol -> Symbol
subSymbol (ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just (ExprV Symbol -> Maybe (ExprV Symbol))
-> ExprV Symbol -> Maybe (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ Subst -> Symbol -> ExprV Symbol
appSubst Subst
su Symbol
x) Symbol
x -- subSymbol (M.lookup x s) x
  syms :: Symbol -> [Symbol]
syms Symbol
x                   = [Symbol
x]

appSubst :: Subst -> Symbol -> Expr
appSubst :: Subst -> Symbol -> ExprV Symbol
appSubst (Su HashMap Symbol (ExprV Symbol)
s) Symbol
x = ExprV Symbol -> Maybe (ExprV Symbol) -> ExprV Symbol
forall a. a -> Maybe a -> a
fromMaybe (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
x) (Symbol -> HashMap Symbol (ExprV Symbol) -> Maybe (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol (ExprV Symbol)
s)

subSymbol :: Maybe Expr -> Symbol -> Symbol
subSymbol :: Maybe (ExprV Symbol) -> Symbol -> Symbol
subSymbol (Just (EVar Symbol
y)) Symbol
_ = Symbol
y
subSymbol Maybe (ExprV Symbol)
Nothing         Symbol
x = Symbol
x
subSymbol Maybe (ExprV Symbol)
a               Symbol
b = String -> Symbol
forall a. (?callStack::CallStack) => String -> a
errorstar (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Cannot substitute symbol %s with expression %s" (Symbol -> String
forall a. Fixpoint a => a -> String
showFix Symbol
b) (Maybe (ExprV Symbol) -> String
forall a. Fixpoint a => a -> String
showFix Maybe (ExprV Symbol)
a))

substfLam :: (Symbol -> Expr) -> (Symbol, Sort) -> Expr -> Expr
substfLam :: (Symbol -> ExprV Symbol)
-> (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
substfLam Symbol -> ExprV Symbol
f s :: (Symbol, Sort)
s@(Symbol
x, Sort
_) ExprV Symbol
e =  (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
s ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf (\Symbol
y -> if Symbol
y Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x then Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
x else Symbol -> ExprV Symbol
f Symbol
y) ExprV Symbol
e)

instance Subable Expr where
  syms :: ExprV Symbol -> [Symbol]
syms                     = ExprV Symbol -> [Symbol]
exprSymbols
  substa :: (Symbol -> Symbol) -> ExprV Symbol -> ExprV Symbol
substa Symbol -> Symbol
f                 = (Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol)
-> (Symbol -> Symbol) -> Symbol -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
f)
  substf :: (Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
substf Symbol -> ExprV Symbol
f (EApp ExprV Symbol
s ExprV Symbol
e)      = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
s) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e)
  substf Symbol -> ExprV Symbol
f (ELam (Symbol, Sort)
x ExprV Symbol
e)      = (Symbol -> ExprV Symbol)
-> (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
substfLam Symbol -> ExprV Symbol
f (Symbol, Sort)
x ExprV Symbol
e
  substf Symbol -> ExprV Symbol
f (ECoerc Sort
a Sort
t ExprV Symbol
e)  = Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e)
  substf Symbol -> ExprV Symbol
f (ENeg ExprV Symbol
e)        = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
ENeg ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e)
  substf Symbol -> ExprV Symbol
f (EBin Bop
op ExprV Symbol
e1 ExprV Symbol
e2) = Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
op ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e1) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e2)
  substf Symbol -> ExprV Symbol
f (EIte ExprV Symbol
p ExprV Symbol
e1 ExprV Symbol
e2)  = ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
p) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e1) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e2)
  substf Symbol -> ExprV Symbol
f (ECst ExprV Symbol
e Sort
so)     = ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e) Sort
so
  substf Symbol -> ExprV Symbol
f (EVar Symbol
x)        = Symbol -> ExprV Symbol
f Symbol
x
  substf Symbol -> ExprV Symbol
f (PAnd [ExprV Symbol]
ps)       = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f) [ExprV Symbol]
ps
  substf Symbol -> ExprV Symbol
f (POr  [ExprV Symbol]
ps)       = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
POr  ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f) [ExprV Symbol]
ps
  substf Symbol -> ExprV Symbol
f (PNot ExprV Symbol
p)        = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
p
  substf Symbol -> ExprV Symbol
f (PImp ExprV Symbol
p1 ExprV Symbol
p2)    = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PImp ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
p1) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
p2)
  substf Symbol -> ExprV Symbol
f (PIff ExprV Symbol
p1 ExprV Symbol
p2)    = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PIff ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
p1) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
p2)
  substf Symbol -> ExprV Symbol
f (PAtom Brel
r ExprV Symbol
e1 ExprV Symbol
e2) = Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e1) ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e2)
  substf Symbol -> ExprV Symbol
f (PKVar KVar
k (Su HashMap Symbol (ExprV Symbol)
su)) = KVar -> Subst -> ExprV Symbol
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol)
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f) HashMap Symbol (ExprV Symbol)
su)
  substf Symbol -> ExprV Symbol
_  (PAll [(Symbol, Sort)]
_ ExprV Symbol
_)     = String -> ExprV Symbol
forall a. (?callStack::CallStack) => String -> a
errorstar String
"substf: FORALL"
  substf Symbol -> ExprV Symbol
f (PGrad KVar
k Subst
su GradInfo
i ExprV Symbol
e)= KVar -> Subst -> GradInfo -> ExprV Symbol -> ExprV Symbol
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k Subst
su GradInfo
i ((Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f ExprV Symbol
e)
  substf Symbol -> ExprV Symbol
_  ExprV Symbol
p              = ExprV Symbol
p


  subst :: Subst -> ExprV Symbol -> ExprV Symbol
subst Subst
su (EApp ExprV Symbol
f ExprV Symbol
e)      = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
f) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e)
  subst Subst
su (ELam (Symbol, Sort)
x ExprV Symbol
e)      = (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
x (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst (Subst -> Symbol -> Subst
removeSubst Subst
su ((Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst (Symbol, Sort)
x)) ExprV Symbol
e)
  subst Subst
su (ECoerc Sort
a Sort
t ExprV Symbol
e)  = Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e)
  subst Subst
su (ENeg ExprV Symbol
e)        = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
ENeg (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e)
  subst Subst
su (EBin Bop
op ExprV Symbol
e1 ExprV Symbol
e2) = Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
op (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e1) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e2)
  subst Subst
su (EIte ExprV Symbol
p ExprV Symbol
e1 ExprV Symbol
e2)  = ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e1) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e2)
  subst Subst
su (ECst ExprV Symbol
e Sort
so)     = ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e) Sort
so
  subst Subst
su (EVar Symbol
x)        = Subst -> Symbol -> ExprV Symbol
appSubst Subst
su Symbol
x
  subst Subst
su (PAnd [ExprV Symbol]
ps)       = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su) [ExprV Symbol]
ps
  subst Subst
su (POr  [ExprV Symbol]
ps)       = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
POr  ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su) [ExprV Symbol]
ps
  subst Subst
su (PNot ExprV Symbol
p)        = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p
  subst Subst
su (PImp ExprV Symbol
p1 ExprV Symbol
p2)    = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p1) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p2)
  subst Subst
su (PIff ExprV Symbol
p1 ExprV Symbol
p2)    = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p1) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p2)
  subst Subst
su (PAtom Brel
r ExprV Symbol
e1 ExprV Symbol
e2) = Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e1) (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e2)
  subst Subst
su (PKVar KVar
k Subst
su')   = KVar -> Subst -> ExprV Symbol
forall v. KVar -> SubstV v -> ExprV v
PKVar KVar
k (Subst -> ExprV Symbol) -> Subst -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Subst
su' Subst -> Subst -> Subst
`catSubst` Subst
su
  subst Subst
su (PGrad KVar
k Subst
su' GradInfo
i ExprV Symbol
e) = KVar -> Subst -> GradInfo -> ExprV Symbol -> ExprV Symbol
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k (Subst
su' Subst -> Subst -> Subst
`catSubst` Subst
su) GradInfo
i (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
e)
  subst Subst
su (PAll [(Symbol, Sort)]
bs ExprV Symbol
p)
          | Subst -> [(Symbol, Sort)] -> Bool
disjoint Subst
su [(Symbol, Sort)]
bs = [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p --(substExcept su (fst <$> bs)) p
          | Bool
otherwise      = String -> ExprV Symbol
forall a. (?callStack::CallStack) => String -> a
errorstar String
"subst: PAll (without disjoint binds)"
  subst Subst
su (PExist [(Symbol, Sort)]
bs ExprV Symbol
p)
          | Subst -> [(Symbol, Sort)] -> Bool
disjoint Subst
su [(Symbol, Sort)]
bs = [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su ExprV Symbol
p --(substExcept su (fst <$> bs)) p
          | Bool
otherwise      = String -> ExprV Symbol
forall a. (?callStack::CallStack) => String -> a
errorstar (String
"subst: EXISTS (without disjoint binds)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([(Symbol, Sort)], Subst, ExprV Symbol) -> String
forall a. Show a => a -> String
show ([(Symbol, Sort)]
bs, Subst
su, ExprV Symbol
p))
  subst Subst
_  ExprV Symbol
p               = ExprV Symbol
p

removeSubst :: Subst -> Symbol -> Subst
removeSubst :: Subst -> Symbol -> Subst
removeSubst (Su HashMap Symbol (ExprV Symbol)
su) Symbol
x = HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$ Symbol
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Symbol
x HashMap Symbol (ExprV Symbol)
su

disjoint :: Subst -> [(Symbol, Sort)] -> Bool
disjoint :: Subst -> [(Symbol, Sort)] -> Bool
disjoint (Su HashMap Symbol (ExprV Symbol)
su) [(Symbol, Sort)]
bs = HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> Bool) -> HashSet Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ HashSet Symbol
suSyms HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.intersection` HashSet Symbol
bsSyms
  where
    suSyms :: HashSet Symbol
suSyms = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [ExprV Symbol] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (HashMap Symbol (ExprV Symbol) -> [ExprV Symbol]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol (ExprV Symbol)
su) [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (HashMap Symbol (ExprV Symbol) -> [Symbol]
forall k v. HashMap k v -> [k]
M.keys HashMap Symbol (ExprV Symbol)
su)
    bsSyms :: HashSet Symbol
bsSyms = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
bs

meetReft :: Reft -> Reft -> Reft
meetReft :: Reft -> Reft -> Reft
meetReft (Reft (Symbol
v, ExprV Symbol
ra)) (Reft (Symbol
v', ExprV Symbol
ra'))
  | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
v'          = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v , [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV Symbol
ra, ExprV Symbol
ra'])
  | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dummySymbol = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v', [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV Symbol
ra', ExprV Symbol
ra ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`subst1`  (Symbol
v , Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v')])
  | Bool
otherwise        = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v , [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV Symbol
ra, ExprV Symbol
ra' ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
`subst1` (Symbol
v', Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v )])

instance Subable Reft where
  syms :: Reft -> [Symbol]
syms (Reft (Symbol
v, ExprV Symbol
ras))      = Symbol
v Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ExprV Symbol
ras
  substa :: (Symbol -> Symbol) -> Reft -> Reft
substa Symbol -> Symbol
f (Reft (Symbol
v, ExprV Symbol
ras))  = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol -> Symbol
f Symbol
v, (Symbol -> Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f ExprV Symbol
ras)
  subst :: Subst -> Reft -> Reft
subst Subst
su (Reft (Symbol
v, ExprV Symbol
ras))  = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst (Subst -> [Symbol] -> Subst
substExcept Subst
su [Symbol
v]) ExprV Symbol
ras)
  substf :: (Symbol -> ExprV Symbol) -> Reft -> Reft
substf Symbol -> ExprV Symbol
f (Reft (Symbol
v, ExprV Symbol
ras))  = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, (Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf ((Symbol -> ExprV Symbol) -> [Symbol] -> Symbol -> ExprV Symbol
substfExcept Symbol -> ExprV Symbol
f [Symbol
v]) ExprV Symbol
ras)
  subst1 :: Reft -> (Symbol, ExprV Symbol) -> Reft
subst1 (Reft (Symbol
v, ExprV Symbol
ras)) (Symbol, ExprV Symbol)
su = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, [Symbol] -> ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => [Symbol] -> a -> (Symbol, ExprV Symbol) -> a
subst1Except [Symbol
v] ExprV Symbol
ras (Symbol, ExprV Symbol)
su)

instance Subable SortedReft where
  syms :: SortedReft -> [Symbol]
syms               = Reft -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (Reft -> [Symbol])
-> (SortedReft -> Reft) -> SortedReft -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
  subst :: Subst -> SortedReft -> SortedReft
subst Subst
su (RR Sort
so Reft
r) = Sort -> Reft -> SortedReft
RR Sort
so (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ Subst -> Reft -> Reft
forall a. Subable a => Subst -> a -> a
subst Subst
su Reft
r
  substf :: (Symbol -> ExprV Symbol) -> SortedReft -> SortedReft
substf Symbol -> ExprV Symbol
f (RR Sort
so Reft
r) = Sort -> Reft -> SortedReft
RR Sort
so (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> ExprV Symbol) -> Reft -> Reft
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
f Reft
r
  substa :: (Symbol -> Symbol) -> SortedReft -> SortedReft
substa Symbol -> Symbol
f (RR Sort
so Reft
r) = Sort -> Reft -> SortedReft
RR Sort
so (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol) -> Reft -> Reft
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f Reft
r

pprReft :: Reft -> Doc -> Doc
pprReft :: Reft -> Doc -> Doc
pprReft (Reft (Symbol
v, ExprV Symbol
p)) Doc
d
  | ExprV Symbol -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV Symbol
p
  = Doc
d
  | Bool
otherwise
  = Doc -> Doc
braces (Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
v Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Doc
d Doc -> Doc -> Doc
<+> String -> Doc
text String
"|" Doc -> Doc -> Doc
<+> [ExprV Symbol] -> Doc
ppRas [ExprV Symbol
p])

-- RJ: this depends on `isTauto` hence, here.
instance (PPrint v, Fixpoint v, Ord v) => PPrint (ReftV v) where
  pprintTidy :: Tidy -> ReftV v -> Doc
pprintTidy Tidy
k ReftV v
r
    | ReftV v -> Bool
forall v. Eq v => ReftV v -> Bool
isTautoReft ReftV v
r        = String -> Doc
text String
"true"
    | Bool
otherwise        = Tidy -> ReftV v -> Doc
forall v. (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc
pprintReft Tidy
k ReftV v
r

instance PPrint SortedReft where
  pprintTidy :: Tidy -> SortedReft -> Doc
pprintTidy Tidy
k (RR Sort
so (Reft (Symbol
v, ExprV Symbol
ras)))
    = Doc -> Doc
braces
    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
v Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
so Doc -> Doc -> Doc
<+> String -> Doc
text String
"|" Doc -> Doc -> Doc
<+> Tidy -> ExprV Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ExprV Symbol
ras

instance Fixpoint Reft where
  toFix :: Reft -> Doc
toFix = Reft -> Doc
pprReftPred

instance Fixpoint SortedReft where
  toFix :: SortedReft -> Doc
toFix (RR Sort
so (Reft (Symbol
v, ExprV Symbol
ra)))
    = Doc -> Doc
braces
    (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
v Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
so Doc -> Doc -> Doc
<+> String -> Doc
text String
"|" Doc -> Doc -> Doc
<+> [ExprV Symbol] -> Doc
forall a. Fixpoint a => a -> Doc
toFix (ExprV Symbol -> [ExprV Symbol]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts ExprV Symbol
ra)
  simplify :: SortedReft -> SortedReft
simplify (RR Sort
so (Reft (Symbol
v, ExprV Symbol
ra))) = Sort -> Reft -> SortedReft
RR (Sort -> Sort
forall a. Fixpoint a => a -> a
simplify Sort
so) ((Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol -> Symbol
forall a. Fixpoint a => a -> a
simplify Symbol
v, ExprV Symbol -> ExprV Symbol
forall a. Fixpoint a => a -> a
simplify ExprV Symbol
ra))

instance Show Reft where
  show :: Reft -> String
show = Reft -> String
forall a. Fixpoint a => a -> String
showFix

instance Show SortedReft where
  show :: SortedReft -> String
show  = SortedReft -> String
forall a. Fixpoint a => a -> String
showFix

pprReftPred :: Reft -> Doc
pprReftPred :: Reft -> Doc
pprReftPred (Reft (Symbol
_, ExprV Symbol
p))
  | ExprV Symbol -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV Symbol
p
  = String -> Doc
text String
"true"
  | Bool
otherwise
  = [ExprV Symbol] -> Doc
ppRas [ExprV Symbol
p]

ppRas :: [Expr] -> Doc
ppRas :: [ExprV Symbol] -> Doc
ppRas = [Doc] -> Doc
cat ([Doc] -> Doc)
-> ([ExprV Symbol] -> [Doc]) -> [ExprV Symbol] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc])
-> ([ExprV Symbol] -> [Doc]) -> [ExprV Symbol] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExprV Symbol -> Doc) -> [ExprV Symbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ExprV Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([ExprV Symbol] -> [Doc])
-> ([ExprV Symbol] -> [ExprV Symbol]) -> [ExprV Symbol] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExprV Symbol] -> [ExprV Symbol]
forall v. [ExprV v] -> [ExprV v]
flattenRefas

--------------------------------------------------------------------------------
-- | TODO: Rewrite using visitor -----------------------------------------------
--------------------------------------------------------------------------------
-- exprSymbols :: Expr -> [Symbol]
-- exprSymbols = go
  -- where
    -- go (EVar x)           = [x]
    -- go (EApp f e)         = go f ++ go e
    -- go (ELam (x,_) e)     = filter (/= x) (go e)
    -- go (ECoerc _ _ e)     = go e
    -- go (ENeg e)           = go e
    -- go (EBin _ e1 e2)     = go e1 ++ go e2
    -- go (EIte p e1 e2)     = exprSymbols p ++ go e1 ++ go e2
    -- go (ECst e _)         = go e
    -- go (PAnd ps)          = concatMap go ps
    -- go (POr ps)           = concatMap go ps
    -- go (PNot p)           = go p
    -- go (PIff p1 p2)       = go p1 ++ go p2
    -- go (PImp p1 p2)       = go p1 ++ go p2
    -- go (PAtom _ e1 e2)    = exprSymbols e1 ++ exprSymbols e2
    -- go (PKVar _ (Su su))  = syms (M.elems su)
    -- go (PAll xts p)       = (fst <$> xts) ++ go p
    -- go _                  = []


exprSymbols :: Expr -> [Symbol]
exprSymbols :: ExprV Symbol -> [Symbol]
exprSymbols = HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> [Symbol])
-> (ExprV Symbol -> HashSet Symbol) -> ExprV Symbol -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV Symbol -> HashSet Symbol
exprSymbolsSet

instance Expression (Symbol, SortedReft) where
  expr :: (Symbol, SortedReft) -> ExprV Symbol
expr (Symbol
x, RR Sort
_ (Reft (Symbol
v, ExprV Symbol
r))) = ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
subst1 (ExprV Symbol -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
expr ExprV Symbol
r) (Symbol
v, Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
x)