{-# LANGUAGE CPP #-}

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

{-# LANGUAGE FlexibleInstances #-}
module Language.Fixpoint.Types.Substitutions (
    mkSubst
  , isEmptySubst
  , substExcept
  , substfExcept
  , subst1Except
  , targetSubstSyms
  , filterSubst
  ) where

import           Data.Maybe
import qualified Data.HashMap.Strict       as M
import qualified Data.HashSet              as S
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

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 -> Expr -> Bool) -> Subst -> Subst
filterSubst Symbol -> Expr -> Bool
f (Su HashMap Symbol Expr
m) = HashMap Symbol Expr -> Subst
Su ((Symbol -> Expr -> Bool)
-> HashMap Symbol Expr -> HashMap Symbol Expr
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey Symbol -> Expr -> Bool
f HashMap Symbol Expr
m)

emptySubst :: Subst
emptySubst :: Subst
emptySubst = HashMap Symbol Expr -> Subst
Su HashMap Symbol Expr
forall k v. HashMap k v
M.empty

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

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

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

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


  
instance Subable () where
  syms :: () -> [Symbol]
syms ()
_      = []
  subst :: Subst -> () -> ()
subst Subst
_ ()  = ()
  substf :: (Symbol -> Expr) -> () -> ()
substf Symbol -> Expr
_ () = ()
  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 -> Expr) -> (a, b) -> (a, b)
substf Symbol -> Expr
f (a
x,b
y) = ((Symbol -> Expr) -> a -> a
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f a
x, (Symbol -> Expr) -> b -> b
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
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 (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 -> Expr) -> [a] -> [a]
substf = (a -> a) -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> [a] -> [a])
-> ((Symbol -> Expr) -> a -> a) -> (Symbol -> Expr) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr) -> a -> a
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> [a] -> [a]
substa = (a -> a) -> [a] -> [a]
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 (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 -> Expr) -> Maybe a -> Maybe a
substf = (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> ((Symbol -> Expr) -> a -> a)
-> (Symbol -> Expr)
-> Maybe a
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr) -> a -> a
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> Maybe a -> Maybe a
substa = (a -> a) -> Maybe a -> Maybe a
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 -> Expr) -> 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 -> Expr) -> a -> a)
-> (Symbol -> Expr)
-> HashMap k a
-> HashMap k a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Expr) -> a -> a
forall a. Subable a => (Symbol -> Expr) -> 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 :: [Symbol] -> a -> (Symbol, Expr) -> a
subst1Except [Symbol]
xs a
z su :: (Symbol, Expr)
su@(Symbol
x, Expr
_)
  | Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs = a
z
  | Bool
otherwise   = a -> (Symbol, Expr) -> a
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 a
z (Symbol, Expr)
su

substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
substfExcept Symbol -> Expr
f [Symbol]
xs Symbol
y = if Symbol
y Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs then Symbol -> Expr
EVar Symbol
y else Symbol -> Expr
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 Expr
xes) [Symbol]
xs = HashMap Symbol Expr -> Subst
Su (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> Expr -> Bool)
-> HashMap Symbol Expr -> HashMap Symbol Expr
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (Bool -> Expr -> Bool
forall a b. a -> b -> a
const (Bool -> Expr -> Bool)
-> (Symbol -> Bool) -> Symbol -> Expr -> 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs)) HashMap Symbol Expr
xes

instance Subable Symbol where
  substa :: (Symbol -> Symbol) -> Symbol -> Symbol
substa Symbol -> Symbol
f                 = Symbol -> Symbol
f
  substf :: (Symbol -> Expr) -> Symbol -> Symbol
substf Symbol -> Expr
f Symbol
x               = Maybe Expr -> Symbol -> Symbol
subSymbol (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Symbol -> Expr
f Symbol
x)) Symbol
x
  subst :: Subst -> Symbol -> Symbol
subst Subst
su Symbol
x               = Maybe Expr -> Symbol -> Symbol
subSymbol (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Subst -> Symbol -> Expr
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 -> Expr
appSubst (Su HashMap Symbol Expr
s) Symbol
x = Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (Symbol -> Expr
EVar Symbol
x) (Symbol -> HashMap Symbol Expr -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
x HashMap Symbol Expr
s)

subSymbol :: Maybe Expr -> Symbol -> Symbol
subSymbol :: Maybe Expr -> Symbol -> Symbol
subSymbol (Just (EVar Symbol
y)) Symbol
_ = Symbol
y
subSymbol Maybe Expr
Nothing         Symbol
x = Symbol
x
subSymbol Maybe Expr
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 Expr -> String
forall a. Fixpoint a => a -> String
showFix Maybe Expr
a))

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

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


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

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

disjoint :: Subst -> [(Symbol, Sort)] -> Bool
disjoint :: Subst -> [(Symbol, Sort)] -> Bool
disjoint (Su HashMap Symbol Expr
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, Hashable 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
$ [Expr] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (HashMap Symbol Expr -> [Expr]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol Expr
su) [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (HashMap Symbol Expr -> [Symbol]
forall k v. HashMap k v -> [k]
M.keys HashMap Symbol Expr
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

instance Semigroup Expr where
  Expr
p <> :: Expr -> Expr -> Expr
<> Expr
q = [Expr] -> Expr
pAnd [Expr
p, Expr
q]

instance Monoid Expr where
  mempty :: Expr
mempty  = Expr
PTrue
  mappend :: Expr -> Expr -> Expr
mappend = Expr -> Expr -> Expr
forall a. Semigroup a => a -> a -> a
(<>)
  mconcat :: [Expr] -> Expr
mconcat = [Expr] -> Expr
pAnd

instance Semigroup Reft where
  <> :: Reft -> Reft -> Reft
(<>) = Reft -> Reft -> Reft
meetReft

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

meetReft :: Reft -> Reft -> Reft
meetReft :: Reft -> Reft -> Reft
meetReft (Reft (Symbol
v, Expr
ra)) (Reft (Symbol
v', Expr
ra'))
  | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
v'          = (Symbol, Expr) -> Reft
Reft (Symbol
v , Expr
ra  Expr -> Expr -> Expr
forall a. Monoid a => a -> a -> a
`mappend` Expr
ra')
  | Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dummySymbol = (Symbol, Expr) -> Reft
Reft (Symbol
v', Expr
ra' Expr -> Expr -> Expr
forall a. Monoid a => a -> a -> a
`mappend` (Expr
ra Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1`  (Symbol
v , Symbol -> Expr
EVar Symbol
v')))
  | Bool
otherwise        = (Symbol, Expr) -> Reft
Reft (Symbol
v , Expr
ra  Expr -> Expr -> Expr
forall a. Monoid a => a -> a -> a
`mappend` (Expr
ra' Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Symbol
v', Symbol -> Expr
EVar Symbol
v )))

instance Semigroup SortedReft where
  SortedReft
t1 <> :: SortedReft -> SortedReft -> SortedReft
<> SortedReft
t2 = Sort -> Reft -> SortedReft
RR (Sort -> Sort -> Sort
forall a. Monoid a => a -> a -> a
mappend (SortedReft -> Sort
sr_sort SortedReft
t1) (SortedReft -> Sort
sr_sort SortedReft
t2)) (Reft -> Reft -> Reft
forall a. Monoid a => a -> a -> a
mappend (SortedReft -> Reft
sr_reft SortedReft
t1) (SortedReft -> Reft
sr_reft SortedReft
t2))

instance Monoid SortedReft where
  mempty :: SortedReft
mempty  = Sort -> Reft -> SortedReft
RR Sort
forall a. Monoid a => a
mempty Reft
forall a. Monoid a => a
mempty
  mappend :: SortedReft -> SortedReft -> SortedReft
mappend = SortedReft -> SortedReft -> SortedReft
forall a. Semigroup a => a -> a -> a
(<>)

instance Subable Reft where
  syms :: Reft -> [Symbol]
syms (Reft (Symbol
v, Expr
ras))      = Symbol
v Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
ras
  substa :: (Symbol -> Symbol) -> Reft -> Reft
substa Symbol -> Symbol
f (Reft (Symbol
v, Expr
ras))  = (Symbol, Expr) -> Reft
Reft (Symbol -> Symbol
f Symbol
v, (Symbol -> Symbol) -> Expr -> Expr
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f Expr
ras)
  subst :: Subst -> Reft -> Reft
subst Subst
su (Reft (Symbol
v, Expr
ras))  = (Symbol, Expr) -> Reft
Reft (Symbol
v, Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst (Subst -> [Symbol] -> Subst
substExcept Subst
su [Symbol
v]) Expr
ras)
  substf :: (Symbol -> Expr) -> Reft -> Reft
substf Symbol -> Expr
f (Reft (Symbol
v, Expr
ras))  = (Symbol, Expr) -> Reft
Reft (Symbol
v, (Symbol -> Expr) -> Expr -> Expr
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf ((Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
substfExcept Symbol -> Expr
f [Symbol
v]) Expr
ras)
  subst1 :: Reft -> (Symbol, Expr) -> Reft
subst1 (Reft (Symbol
v, Expr
ras)) (Symbol, Expr)
su = (Symbol, Expr) -> Reft
Reft (Symbol
v, [Symbol] -> Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => [Symbol] -> a -> (Symbol, Expr) -> a
subst1Except [Symbol
v] Expr
ras (Symbol, Expr)
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 -> Expr) -> SortedReft -> SortedReft
substf Symbol -> Expr
f (RR Sort
so Reft
r) = Sort -> Reft -> SortedReft
RR Sort
so (Reft -> SortedReft) -> Reft -> SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Expr) -> Reft -> Reft
forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
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

instance Reftable () where
  isTauto :: () -> Bool
isTauto ()
_ = Bool
True
  ppTy :: () -> Doc -> Doc
ppTy ()
_  Doc
d = Doc
d
  top :: () -> ()
top  ()
_    = ()
  bot :: () -> ()
bot  ()
_    = ()
  meet :: () -> () -> ()
meet ()
_ ()
_  = ()
  toReft :: () -> Reft
toReft ()
_  = Reft
forall a. Monoid a => a
mempty
  ofReft :: Reft -> ()
ofReft Reft
_  = ()
forall a. Monoid a => a
mempty
  params :: () -> [Symbol]
params ()
_  = []

instance Reftable Reft where
  isTauto :: Reft -> Bool
isTauto  = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isTautoPred ([Expr] -> Bool) -> (Reft -> [Expr]) -> Reft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts (Expr -> [Expr]) -> (Reft -> Expr) -> Reft -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Expr
reftPred
  ppTy :: Reft -> Doc -> Doc
ppTy     = Reft -> Doc -> Doc
pprReft
  toReft :: Reft -> Reft
toReft   = Reft -> Reft
forall a. a -> a
id
  ofReft :: Reft -> Reft
ofReft   = Reft -> Reft
forall a. a -> a
id
  params :: Reft -> [Symbol]
params Reft
_ = []
  bot :: Reft -> Reft
bot    Reft
_        = Reft
falseReft
  top :: Reft -> Reft
top (Reft(Symbol
v,Expr
_)) = (Symbol, Expr) -> Reft
Reft (Symbol
v, Expr
forall a. Monoid a => a
mempty)

pprReft :: Reft -> Doc -> Doc
pprReft :: Reft -> Doc -> Doc
pprReft (Reft (Symbol
v, Expr
p)) Doc
d
  | Expr -> Bool
isTautoPred Expr
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
<+> [Expr] -> Doc
ppRas [Expr
p])

instance Reftable SortedReft where
  isTauto :: SortedReft -> Bool
isTauto  = Reft -> Bool
forall r. Reftable r => r -> Bool
isTauto (Reft -> Bool) -> (SortedReft -> Reft) -> SortedReft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
forall r. Reftable r => r -> Reft
toReft
  ppTy :: SortedReft -> Doc -> Doc
ppTy     = Reft -> Doc -> Doc
forall r. Reftable r => r -> Doc -> Doc
ppTy (Reft -> Doc -> Doc)
-> (SortedReft -> Reft) -> SortedReft -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
forall r. Reftable r => r -> Reft
toReft
  toReft :: SortedReft -> Reft
toReft   = SortedReft -> Reft
sr_reft
  ofReft :: Reft -> SortedReft
ofReft   = String -> Reft -> SortedReft
forall a. (?callStack::CallStack) => String -> a
errorstar String
"No instance of ofReft for SortedReft"
  params :: SortedReft -> [Symbol]
params SortedReft
_ = []
  bot :: SortedReft -> SortedReft
bot SortedReft
s    = SortedReft
s { sr_reft :: Reft
sr_reft = Reft
falseReft }
  top :: SortedReft -> SortedReft
top SortedReft
s    = SortedReft
s { sr_reft :: Reft
sr_reft = Reft
trueReft }

-- RJ: this depends on `isTauto` hence, here.
instance PPrint Reft where
  pprintTidy :: Tidy -> Reft -> Doc
pprintTidy Tidy
k Reft
r
    | Reft -> Bool
forall r. Reftable r => r -> Bool
isTauto Reft
r        = String -> Doc
text String
"true"
    | Bool
otherwise        = Tidy -> Reft -> Doc
pprintReft Tidy
k Reft
r

instance PPrint SortedReft where
  pprintTidy :: Tidy -> SortedReft -> Doc
pprintTidy Tidy
k (RR Sort
so (Reft (Symbol
v, Expr
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 -> Expr -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
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, Expr
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
<+> [Expr] -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Expr -> [Expr]
conjuncts Expr
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
_, Expr
p))
  | Expr -> Bool
isTautoPred Expr
p
  = String -> Doc
text String
"true"
  | Bool
otherwise
  = [Expr] -> Doc
ppRas [Expr
p]

ppRas :: [Expr] -> Doc
ppRas :: [Expr] -> Doc
ppRas = [Doc] -> Doc
cat ([Doc] -> Doc) -> ([Expr] -> [Doc]) -> [Expr] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> ([Expr] -> [Doc]) -> [Expr] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([Expr] -> [Doc]) -> ([Expr] -> [Expr]) -> [Expr] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
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 :: Expr -> [Symbol]
exprSymbols = HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet Symbol -> [Symbol])
-> (Expr -> HashSet Symbol) -> Expr -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> HashSet Symbol
go 
  where
    gos :: [Expr] -> HashSet Symbol
gos [Expr]
es                = [HashSet Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions (Expr -> HashSet Symbol
go (Expr -> HashSet Symbol) -> [Expr] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go :: Expr -> HashSet Symbol
go (EVar Symbol
x)           = Symbol -> HashSet Symbol
forall a. Hashable a => a -> HashSet a
S.singleton Symbol
x
    go (EApp Expr
f Expr
e)         = [Expr] -> HashSet Symbol
gos [Expr
f, Expr
e] 
    go (ELam (Symbol
x,Sort
_) Expr
e)     = Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.delete Symbol
x (Expr -> HashSet Symbol
go Expr
e) 
    go (ECoerc Sort
_ Sort
_ Expr
e)     = Expr -> HashSet Symbol
go Expr
e
    go (ENeg Expr
e)           = Expr -> HashSet Symbol
go Expr
e
    go (EBin Bop
_ Expr
e1 Expr
e2)     = [Expr] -> HashSet Symbol
gos [Expr
e1, Expr
e2] 
    go (EIte Expr
p Expr
e1 Expr
e2)     = [Expr] -> HashSet Symbol
gos [Expr
p, Expr
e1, Expr
e2] 
    go (ECst Expr
e Sort
_)         = Expr -> HashSet Symbol
go Expr
e
    go (PAnd [Expr]
ps)          = [Expr] -> HashSet Symbol
gos [Expr]
ps
    go (POr [Expr]
ps)           = [Expr] -> HashSet Symbol
gos [Expr]
ps
    go (PNot Expr
p)           = Expr -> HashSet Symbol
go Expr
p
    go (PIff Expr
p1 Expr
p2)       = [Expr] -> HashSet Symbol
gos [Expr
p1, Expr
p2] 
    go (PImp Expr
p1 Expr
p2)       = [Expr] -> HashSet Symbol
gos [Expr
p1, Expr
p2]
    go (PAtom Brel
_ Expr
e1 Expr
e2)    = [Expr] -> HashSet Symbol
gos [Expr
e1, Expr
e2] 
    go (PKVar KVar
_ (Su HashMap Symbol Expr
su))  = [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
$ [Expr] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ([Expr] -> [Symbol]) -> [Expr] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ HashMap Symbol Expr -> [Expr]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol Expr
su
    go (PAll [(Symbol, Sort)]
xts Expr
p)       = Expr -> HashSet Symbol
go Expr
p HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((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)]
xts) 
    go (PExist [(Symbol, Sort)]
xts Expr
p)     = Expr -> HashSet Symbol
go Expr
p HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((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)]
xts) 
    go Expr
_                  = HashSet Symbol
forall a. HashSet a
S.empty 

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