{-# 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
  ) 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 = 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 (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 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 forall a b. (a -> b) -> a -> b
$ 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'                     = forall a. Subable a => Subst -> a -> a
subst Subst
θ2 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, Expr) -> Bool
notTrivial
  where
    notTrivial :: (Symbol, Expr) -> Bool
notTrivial (Symbol
x, EVar Symbol
y) = Symbol
x 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) = 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) = forall a. Subable a => a -> [Symbol]
syms forall a b. (a -> b) -> a -> b
$ 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)   = forall a. Subable a => a -> [Symbol]
syms a
x forall a. [a] -> [a] -> [a]
++ forall a. Subable a => a -> [Symbol]
syms b
y
  subst :: Subst -> (a, b) -> (a, b)
subst Subst
su (a
x,b
y) = (forall a. Subable a => Subst -> a -> a
subst Subst
su a
x, 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) = (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f a
x, 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) = (forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f a
x, forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f b
y)

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

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


instance Subable a => Subable (M.HashMap k a) where
  syms :: HashMap k a -> [Symbol]
syms   = forall a. Subable a => a -> [Symbol]
syms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [v]
M.elems
  subst :: Subst -> HashMap k a -> HashMap k a
subst  = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => Subst -> a -> a
subst
  substf :: (Symbol -> Expr) -> HashMap k a -> HashMap k a
substf = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => (Symbol -> Expr) -> a -> a
substf
  substa :: (Symbol -> Symbol) -> HashMap k a -> HashMap k a
substa = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, Expr) -> a
subst1Except [Symbol]
xs a
z su :: (Symbol, Expr)
su@(Symbol
x, Expr
_)
  | Symbol
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs = a
z
  | Bool
otherwise   = 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 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 forall a b. (a -> b) -> a -> b
$ forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 (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 (forall a. a -> Maybe a
Just 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 = forall a. a -> Maybe a -> a
fromMaybe (Symbol -> Expr
EVar Symbol
x) (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 = forall a. (?callStack::CallStack) => String -> a
errorstar (forall r. PrintfType r => String -> r
printf String
"Cannot substitute symbol %s with expression %s" (forall a. Fixpoint a => a -> String
showFix Symbol
b) (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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf (\Symbol
y -> if Symbol
y 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                 = forall a. Subable a => (Symbol -> Expr) -> a -> a
substf (Symbol -> Expr
EVar 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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
s) (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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
e)
  substf Symbol -> Expr
f (ENeg Expr
e)        = Expr -> Expr
ENeg (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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
e1) (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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
p) (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
e1) (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 (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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f) [Expr]
ps
  substf Symbol -> Expr
f (POr  [Expr]
ps)       = [Expr] -> Expr
POr  forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f) [Expr]
ps
  substf Symbol -> Expr
f (PNot Expr
p)        = Expr -> Expr
PNot forall a b. (a -> b) -> a -> b
$ 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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
p1) (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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
p1) (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 (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
e1) (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f Expr
e2)
  substf Symbol -> Expr
f (PKVar KVar
k (Su HashMap Symbol Expr
su)) = KVar -> Subst -> Expr
PKVar KVar
k (HashMap Symbol Expr -> Subst
Su forall a b. (a -> b) -> a -> b
$ forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f) HashMap Symbol Expr
su)
  substf Symbol -> Expr
_  (PAll [(Symbol, Sort)]
_ 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 (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 (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
f) (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 (forall a. Subable a => Subst -> a -> a
subst (Subst -> Symbol -> Subst
removeSubst Subst
su (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 (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
e)
  subst Subst
su (ENeg Expr
e)        = Expr -> Expr
ENeg (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 (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
e1) (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 (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p) (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
e1) (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
e2)
  subst Subst
su (ECst Expr
e Sort
so)     = Expr -> Sort -> Expr
ECst (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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => Subst -> a -> a
subst Subst
su) [Expr]
ps
  subst Subst
su (POr  [Expr]
ps)       = [Expr] -> Expr
POr  forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => Subst -> a -> a
subst Subst
su) [Expr]
ps
  subst Subst
su (PNot Expr
p)        = Expr -> Expr
PNot forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p
  subst Subst
su (PImp Expr
p1 Expr
p2)    = Expr -> Expr -> Expr
PImp (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p1) (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p2)
  subst Subst
su (PIff Expr
p1 Expr
p2)    = Expr -> Expr -> Expr
PIff (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p1) (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 (forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
e1) (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 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 (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 forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p --(substExcept su (fst <$> bs)) p
          | Bool
otherwise      = 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 forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p --(substExcept su (fst <$> bs)) p
          | Bool
otherwise      = forall a. (?callStack::CallStack) => String -> a
errorstar (String
"subst: EXISTS (without disjoint binds)" forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ 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 = forall a. HashSet a -> Bool
S.null forall a b. (a -> b) -> a -> b
$ HashSet Symbol
suSyms forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.intersection` HashSet Symbol
bsSyms
  where
    suSyms :: HashSet Symbol
suSyms = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a. Subable a => a -> [Symbol]
syms (forall k v. HashMap k v -> [v]
M.elems HashMap Symbol Expr
su) forall a. [a] -> [a] -> [a]
++ forall a. Subable a => a -> [Symbol]
syms (forall k v. HashMap k v -> [k]
M.keys HashMap Symbol Expr
su)
    bsSyms :: HashSet Symbol
bsSyms = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a. Subable a => a -> [Symbol]
syms forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst 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 = 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 = 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 forall a. Eq a => a -> a -> Bool
== Symbol
v'          = (Symbol, Expr) -> Reft
Reft (Symbol
v , Expr
ra  forall a. Monoid a => a -> a -> a
`mappend` Expr
ra')
  | Symbol
v forall a. Eq a => a -> a -> Bool
== Symbol
dummySymbol = (Symbol, Expr) -> Reft
Reft (Symbol
v', Expr
ra' forall a. Monoid a => a -> a -> a
`mappend` (Expr
ra 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  forall a. Monoid a => a -> a -> a
`mappend` (Expr
ra' 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 (forall a. Monoid a => a -> a -> a
mappend (SortedReft -> Sort
sr_sort SortedReft
t1) (SortedReft -> Sort
sr_sort SortedReft
t2)) (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 forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  mappend :: SortedReft -> SortedReft -> SortedReft
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance Subable Reft where
  syms :: Reft -> [Symbol]
syms (Reft (Symbol
v, Expr
ras))      = Symbol
v forall a. a -> [a] -> [a]
: 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, 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, 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, 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, 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               = forall a. Subable a => a -> [Symbol]
syms 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 ()
_  = 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  = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isTautoPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
conjuncts 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   = forall a. a -> a
id
  ofReft :: Reft -> Reft
ofReft   = 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, 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 (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  = forall r. Reftable r => r -> Bool
isTauto forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Reftable r => r -> Reft
toReft
  ppTy :: SortedReft -> Doc -> Doc
ppTy     = forall r. Reftable r => r -> Doc -> Doc
ppTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Reftable r => r -> Reft
toReft
  toReft :: SortedReft -> Reft
toReft   = SortedReft -> Reft
sr_reft
  ofReft :: Reft -> SortedReft
ofReft   = 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
    | 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
    forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
v Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
so Doc -> Doc -> Doc
<+> String -> Doc
text String
"|" Doc -> Doc -> 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
    forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix Symbol
v Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
so Doc -> Doc -> Doc
<+> String -> Doc
text String
"|" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix (Expr -> [Expr]
conjuncts Expr
ra)
  simplify :: SortedReft -> SortedReft
simplify (RR Sort
so (Reft (Symbol
v, Expr
ra))) = Sort -> Reft -> SortedReft
RR (forall a. Fixpoint a => a -> a
simplify Sort
so) ((Symbol, Expr) -> Reft
Reft (forall a. Fixpoint a => a -> a
simplify Symbol
v, forall a. Fixpoint a => a -> a
simplify Expr
ra))

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

instance Show SortedReft where
  show :: SortedReft -> String
show  = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Fixpoint a => a -> Doc
toFix 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 = forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> HashSet Symbol
exprSymbolsSet

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