{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Fixpoint.Types.Refinements (
SymConst (..)
, Constant (..)
, Bop (..)
, Brel (..)
, Expr (..), Pred
, GradInfo (..)
, pattern PTrue, pattern PTop, pattern PFalse, pattern EBot
, pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv
, pattern EEq
, KVar (..)
, Subst (..)
, KVSub (..)
, Reft (..)
, SortedReft (..)
, eVar, elit
, eProp
, conj, pAnd, pOr, pIte, pAndNoDedup
, (&.&), (|.|)
, pExist
, mkEApp
, mkProp
, intKvar
, vv_
, Expression (..)
, Predicate (..)
, Subable (..)
, Reftable (..)
, reft
, trueSortedReft
, trueReft, falseReft
, exprReft
, notExprReft
, uexprReft
, symbolReft
, usymbolReft
, propReft
, predReft
, reftPred
, reftBind
, isFunctionSortedReft, functionSort
, isNonTrivial
, isContraPred
, isTautoPred
, isSingletonExpr
, isSingletonReft
, isFalse
, flattenRefas
, conjuncts, concConjuncts
, dropECst
, eApps
, eAppC
, eCst
, exprKVars
, exprSymbolsSet
, splitEApp
, splitEAppThroughECst
, splitPAnd
, reftConjuncts
, sortedReftSymbols
, substSortInExpr
, mapPredReft
, onEverySubexpr
, pprintReft
, debruijnIndex
, pGAnds, pGAnd
, HasGradual (..)
, srcGradInfo
) where
import Prelude hiding ((<>))
import Data.Bifunctor (second)
import qualified Data.Store as S
import Data.Generics (Data, gmapT, mkT, extT)
import Data.Typeable (Typeable)
import Data.Hashable
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import GHC.Generics (Generic)
import Data.List (foldl', partition)
import qualified Data.Set as Set
import Data.String
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.HashMap.Strict as M
import Control.DeepSeq
import Data.Maybe (isJust)
import Language.Fixpoint.Types.Names
import Language.Fixpoint.Types.PrettyPrint
import Language.Fixpoint.Types.Spans
import Language.Fixpoint.Types.Sorts
import Language.Fixpoint.Misc
import Text.PrettyPrint.HughesPJ.Compat
import qualified Data.Binary as B
instance NFData KVar
instance NFData Subst
instance NFData GradInfo
instance NFData Constant
instance NFData SymConst
instance NFData Brel
instance NFData Bop
instance NFData Expr
instance NFData Reft
instance NFData SortedReft
instance S.Store KVar
instance S.Store Subst
instance S.Store GradInfo
instance S.Store Constant
instance S.Store SymConst
instance S.Store Brel
instance S.Store Bop
instance S.Store Expr
instance S.Store Reft
instance S.Store SortedReft
instance B.Binary SymConst
instance B.Binary Constant
instance B.Binary Bop
instance B.Binary GradInfo
instance B.Binary Brel
instance B.Binary KVar
instance (Hashable a, Eq a, B.Binary a) => B.Binary (HashSet a) where
put :: HashSet a -> Put
put = [a] -> Put
forall t. Binary t => t -> Put
B.put ([a] -> Put) -> (HashSet a -> [a]) -> HashSet a -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet a -> [a]
forall a. HashSet a -> [a]
HashSet.toList
get :: Get (HashSet a)
get = [a] -> HashSet a
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList ([a] -> HashSet a) -> Get [a] -> Get (HashSet a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get [a]
forall t. Binary t => Get t
B.get
instance (Hashable k, Eq k, B.Binary k, B.Binary v) => B.Binary (M.HashMap k v) where
put :: HashMap k v -> Put
put = [(k, v)] -> Put
forall t. Binary t => t -> Put
B.put ([(k, v)] -> Put)
-> (HashMap k v -> [(k, v)]) -> HashMap k v -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap k v -> [(k, v)]
forall k v. HashMap k v -> [(k, v)]
M.toList
get :: Get (HashMap k v)
get = [(k, v)] -> HashMap k v
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(k, v)] -> HashMap k v) -> Get [(k, v)] -> Get (HashMap k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get [(k, v)]
forall t. Binary t => Get t
B.get
instance B.Binary Subst
instance B.Binary Expr
instance B.Binary Reft
reftConjuncts :: Reft -> [Reft]
reftConjuncts :: Reft -> [Reft]
reftConjuncts (Reft (Symbol
v, Pred
ra)) = [(Symbol, Pred) -> Reft
Reft (Symbol
v, Pred
ra') | Pred
ra' <- [Pred]
ras']
where
ras' :: [Pred]
ras' = if [Pred] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred]
ps then [Pred]
ks else [Pred] -> Pred
conj [Pred]
ps Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ks
([Pred]
ps, [Pred]
ks) = (Pred -> Bool) -> [Pred] -> ([Pred], [Pred])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Pred -> Bool
isConc (Pred -> [Pred]
refaConjuncts Pred
ra)
isConc :: Expr -> Bool
isConc :: Pred -> Bool
isConc Pred
p = Bool -> Bool
not (Pred -> Bool
isKvar Pred
p Bool -> Bool -> Bool
|| Pred -> Bool
forall a. HasGradual a => a -> Bool
isGradual Pred
p)
concConjuncts :: Expr -> [Expr]
concConjuncts :: Pred -> [Pred]
concConjuncts Pred
e = (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter Pred -> Bool
isConc (Pred -> [Pred]
refaConjuncts Pred
e)
isKvar :: Expr -> Bool
isKvar :: Pred -> Bool
isKvar (PKVar KVar
_ Subst
_) = Bool
True
isKvar Pred
_ = Bool
False
class HasGradual a where
isGradual :: a -> Bool
gVars :: a -> [KVar]
gVars a
_ = []
ungrad :: a -> a
ungrad a
x = a
x
instance HasGradual Expr where
isGradual :: Pred -> Bool
isGradual PGrad{} = Bool
True
isGradual (PAnd [Pred]
xs) = (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Pred -> Bool
forall a. HasGradual a => a -> Bool
isGradual [Pred]
xs
isGradual Pred
_ = Bool
False
gVars :: Pred -> [KVar]
gVars (PGrad KVar
k Subst
_ GradInfo
_ Pred
_) = [KVar
k]
gVars (PAnd [Pred]
xs) = (Pred -> [KVar]) -> [Pred] -> [KVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars [Pred]
xs
gVars Pred
_ = []
ungrad :: Pred -> Pred
ungrad PGrad{} = Pred
PTrue
ungrad (PAnd [Pred]
xs) = [Pred] -> Pred
PAnd (Pred -> Pred
forall a. HasGradual a => a -> a
ungrad (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
xs )
ungrad Pred
e = Pred
e
instance HasGradual Reft where
isGradual :: Reft -> Bool
isGradual (Reft (Symbol
_,Pred
r)) = Pred -> Bool
forall a. HasGradual a => a -> Bool
isGradual Pred
r
gVars :: Reft -> [KVar]
gVars (Reft (Symbol
_,Pred
r)) = Pred -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars Pred
r
ungrad :: Reft -> Reft
ungrad (Reft (Symbol
x,Pred
r)) = (Symbol, Pred) -> Reft
Reft(Symbol
x, Pred -> Pred
forall a. HasGradual a => a -> a
ungrad Pred
r)
instance HasGradual SortedReft where
isGradual :: SortedReft -> Bool
isGradual = Reft -> Bool
forall a. HasGradual a => a -> Bool
isGradual (Reft -> Bool) -> (SortedReft -> Reft) -> SortedReft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
gVars :: SortedReft -> [KVar]
gVars = Reft -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars (Reft -> [KVar]) -> (SortedReft -> Reft) -> SortedReft -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
ungrad :: SortedReft -> SortedReft
ungrad SortedReft
r = SortedReft
r {sr_reft = ungrad (sr_reft r)}
refaConjuncts :: Expr -> [Expr]
refaConjuncts :: Pred -> [Pred]
refaConjuncts Pred
p = [Pred
p' | Pred
p' <- Pred -> [Pred]
conjuncts Pred
p, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Pred -> Bool
isTautoPred Pred
p']
newtype KVar = KV { KVar -> Symbol
kv :: Symbol }
deriving (KVar -> KVar -> Bool
(KVar -> KVar -> Bool) -> (KVar -> KVar -> Bool) -> Eq KVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KVar -> KVar -> Bool
== :: KVar -> KVar -> Bool
$c/= :: KVar -> KVar -> Bool
/= :: KVar -> KVar -> Bool
Eq, Eq KVar
Eq KVar =>
(KVar -> KVar -> Ordering)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> KVar)
-> (KVar -> KVar -> KVar)
-> Ord KVar
KVar -> KVar -> Bool
KVar -> KVar -> Ordering
KVar -> KVar -> KVar
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: KVar -> KVar -> Ordering
compare :: KVar -> KVar -> Ordering
$c< :: KVar -> KVar -> Bool
< :: KVar -> KVar -> Bool
$c<= :: KVar -> KVar -> Bool
<= :: KVar -> KVar -> Bool
$c> :: KVar -> KVar -> Bool
> :: KVar -> KVar -> Bool
$c>= :: KVar -> KVar -> Bool
>= :: KVar -> KVar -> Bool
$cmax :: KVar -> KVar -> KVar
max :: KVar -> KVar -> KVar
$cmin :: KVar -> KVar -> KVar
min :: KVar -> KVar -> KVar
Ord, Typeable KVar
Typeable KVar =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVar)
-> (KVar -> Constr)
-> (KVar -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVar))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar))
-> ((forall b. Data b => b -> b) -> KVar -> KVar)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r)
-> (forall u. (forall d. Data d => d -> u) -> KVar -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar)
-> Data KVar
KVar -> Constr
KVar -> DataType
(forall b. Data b => b -> b) -> KVar -> KVar
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u
forall u. (forall d. Data d => d -> u) -> KVar -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVar
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVar)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVar
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVar
$ctoConstr :: KVar -> Constr
toConstr :: KVar -> Constr
$cdataTypeOf :: KVar -> DataType
dataTypeOf :: KVar -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVar)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVar)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar)
$cgmapT :: (forall b. Data b => b -> b) -> KVar -> KVar
gmapT :: (forall b. Data b => b -> b) -> KVar -> KVar
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KVar -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> KVar -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
Data, Typeable, (forall x. KVar -> Rep KVar x)
-> (forall x. Rep KVar x -> KVar) -> Generic KVar
forall x. Rep KVar x -> KVar
forall x. KVar -> Rep KVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. KVar -> Rep KVar x
from :: forall x. KVar -> Rep KVar x
$cto :: forall x. Rep KVar x -> KVar
to :: forall x. Rep KVar x -> KVar
Generic, String -> KVar
(String -> KVar) -> IsString KVar
forall a. (String -> a) -> IsString a
$cfromString :: String -> KVar
fromString :: String -> KVar
IsString)
intKvar :: Integer -> KVar
intKvar :: Integer -> KVar
intKvar = Symbol -> KVar
KV (Symbol -> KVar) -> (Integer -> Symbol) -> Integer -> KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Integer -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"k_"
instance Show KVar where
show :: KVar -> String
show (KV Symbol
x) = String
"$" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
x
instance Hashable KVar
instance Hashable Brel
instance Hashable Bop
instance Hashable SymConst
instance Hashable Constant
instance Hashable GradInfo
instance Hashable Subst
instance Hashable Expr
instance Hashable Reft
newtype Subst = Su (M.HashMap Symbol Expr)
deriving (Subst -> Subst -> Bool
(Subst -> Subst -> Bool) -> (Subst -> Subst -> Bool) -> Eq Subst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
/= :: Subst -> Subst -> Bool
Eq, Typeable Subst
Typeable Subst =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst)
-> (Subst -> Constr)
-> (Subst -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst))
-> ((forall b. Data b => b -> b) -> Subst -> Subst)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r)
-> (forall u. (forall d. Data d => d -> u) -> Subst -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst)
-> Data Subst
Subst -> Constr
Subst -> DataType
(forall b. Data b => b -> b) -> Subst -> Subst
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
forall u. (forall d. Data d => d -> u) -> Subst -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst
$ctoConstr :: Subst -> Constr
toConstr :: Subst -> Constr
$cdataTypeOf :: Subst -> DataType
dataTypeOf :: Subst -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst)
$cgmapT :: (forall b. Data b => b -> b) -> Subst -> Subst
gmapT :: (forall b. Data b => b -> b) -> Subst -> Subst
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Subst -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Subst -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
Data, Eq Subst
Eq Subst =>
(Subst -> Subst -> Ordering)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Subst)
-> (Subst -> Subst -> Subst)
-> Ord Subst
Subst -> Subst -> Bool
Subst -> Subst -> Ordering
Subst -> Subst -> Subst
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Subst -> Subst -> Ordering
compare :: Subst -> Subst -> Ordering
$c< :: Subst -> Subst -> Bool
< :: Subst -> Subst -> Bool
$c<= :: Subst -> Subst -> Bool
<= :: Subst -> Subst -> Bool
$c> :: Subst -> Subst -> Bool
> :: Subst -> Subst -> Bool
$c>= :: Subst -> Subst -> Bool
>= :: Subst -> Subst -> Bool
$cmax :: Subst -> Subst -> Subst
max :: Subst -> Subst -> Subst
$cmin :: Subst -> Subst -> Subst
min :: Subst -> Subst -> Subst
Ord, Typeable, (forall x. Subst -> Rep Subst x)
-> (forall x. Rep Subst x -> Subst) -> Generic Subst
forall x. Rep Subst x -> Subst
forall x. Subst -> Rep Subst x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Subst -> Rep Subst x
from :: forall x. Subst -> Rep Subst x
$cto :: forall x. Rep Subst x -> Subst
to :: forall x. Rep Subst x -> Subst
Generic)
instance Show Subst where
show :: Subst -> String
show = Subst -> String
forall a. Fixpoint a => a -> String
showFix
instance Fixpoint Subst where
toFix :: Subst -> Doc
toFix (Su HashMap Symbol Pred
m) = case HashMap Symbol Pred -> [(Symbol, Pred)]
forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList HashMap Symbol Pred
m of
[] -> Doc
empty
[(Symbol, Pred)]
xys -> [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Symbol, Pred) -> Doc) -> [(Symbol, Pred)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
x,Pred
y) -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<-> String -> Doc
text String
":=" Doc -> Doc -> Doc
<-> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
y) [(Symbol, Pred)]
xys
instance PPrint Subst where
pprintTidy :: Tidy -> Subst -> Doc
pprintTidy Tidy
_ = Subst -> Doc
forall a. Fixpoint a => a -> Doc
toFix
data KVSub = KVS
{ KVSub -> Symbol
ksuVV :: Symbol
, KVSub -> Sort
ksuSort :: Sort
, KVSub -> KVar
ksuKVar :: KVar
, KVSub -> Subst
ksuSubst :: Subst
} deriving (KVSub -> KVSub -> Bool
(KVSub -> KVSub -> Bool) -> (KVSub -> KVSub -> Bool) -> Eq KVSub
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KVSub -> KVSub -> Bool
== :: KVSub -> KVSub -> Bool
$c/= :: KVSub -> KVSub -> Bool
/= :: KVSub -> KVSub -> Bool
Eq, Typeable KVSub
Typeable KVSub =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVSub)
-> (KVSub -> Constr)
-> (KVSub -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVSub))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub))
-> ((forall b. Data b => b -> b) -> KVSub -> KVSub)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r)
-> (forall u. (forall d. Data d => d -> u) -> KVSub -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub)
-> Data KVSub
KVSub -> Constr
KVSub -> DataType
(forall b. Data b => b -> b) -> KVSub -> KVSub
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u
forall u. (forall d. Data d => d -> u) -> KVSub -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVSub
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVSub)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVSub
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVSub
$ctoConstr :: KVSub -> Constr
toConstr :: KVSub -> Constr
$cdataTypeOf :: KVSub -> DataType
dataTypeOf :: KVSub -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVSub)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVSub)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub)
$cgmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub
gmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KVSub -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> KVSub -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
Data, Typeable, (forall x. KVSub -> Rep KVSub x)
-> (forall x. Rep KVSub x -> KVSub) -> Generic KVSub
forall x. Rep KVSub x -> KVSub
forall x. KVSub -> Rep KVSub x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. KVSub -> Rep KVSub x
from :: forall x. KVSub -> Rep KVSub x
$cto :: forall x. Rep KVSub x -> KVSub
to :: forall x. Rep KVSub x -> KVSub
Generic, Int -> KVSub -> ShowS
[KVSub] -> ShowS
KVSub -> String
(Int -> KVSub -> ShowS)
-> (KVSub -> String) -> ([KVSub] -> ShowS) -> Show KVSub
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KVSub -> ShowS
showsPrec :: Int -> KVSub -> ShowS
$cshow :: KVSub -> String
show :: KVSub -> String
$cshowList :: [KVSub] -> ShowS
showList :: [KVSub] -> ShowS
Show)
instance PPrint KVSub where
pprintTidy :: Tidy -> KVSub -> Doc
pprintTidy Tidy
k KVSub
ksu = Tidy -> (Symbol, KVar, Subst) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (KVSub -> Symbol
ksuVV KVSub
ksu, KVSub -> KVar
ksuKVar KVSub
ksu, KVSub -> Subst
ksuSubst KVSub
ksu)
newtype SymConst = SL Text
deriving (SymConst -> SymConst -> Bool
(SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool) -> Eq SymConst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SymConst -> SymConst -> Bool
== :: SymConst -> SymConst -> Bool
$c/= :: SymConst -> SymConst -> Bool
/= :: SymConst -> SymConst -> Bool
Eq, Eq SymConst
Eq SymConst =>
(SymConst -> SymConst -> Ordering)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> SymConst)
-> (SymConst -> SymConst -> SymConst)
-> Ord SymConst
SymConst -> SymConst -> Bool
SymConst -> SymConst -> Ordering
SymConst -> SymConst -> SymConst
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SymConst -> SymConst -> Ordering
compare :: SymConst -> SymConst -> Ordering
$c< :: SymConst -> SymConst -> Bool
< :: SymConst -> SymConst -> Bool
$c<= :: SymConst -> SymConst -> Bool
<= :: SymConst -> SymConst -> Bool
$c> :: SymConst -> SymConst -> Bool
> :: SymConst -> SymConst -> Bool
$c>= :: SymConst -> SymConst -> Bool
>= :: SymConst -> SymConst -> Bool
$cmax :: SymConst -> SymConst -> SymConst
max :: SymConst -> SymConst -> SymConst
$cmin :: SymConst -> SymConst -> SymConst
min :: SymConst -> SymConst -> SymConst
Ord, Int -> SymConst -> ShowS
[SymConst] -> ShowS
SymConst -> String
(Int -> SymConst -> ShowS)
-> (SymConst -> String) -> ([SymConst] -> ShowS) -> Show SymConst
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SymConst -> ShowS
showsPrec :: Int -> SymConst -> ShowS
$cshow :: SymConst -> String
show :: SymConst -> String
$cshowList :: [SymConst] -> ShowS
showList :: [SymConst] -> ShowS
Show, Typeable SymConst
Typeable SymConst =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymConst)
-> (SymConst -> Constr)
-> (SymConst -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymConst))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst))
-> ((forall b. Data b => b -> b) -> SymConst -> SymConst)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymConst -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst)
-> Data SymConst
SymConst -> Constr
SymConst -> DataType
(forall b. Data b => b -> b) -> SymConst -> SymConst
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u
forall u. (forall d. Data d => d -> u) -> SymConst -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymConst
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymConst)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymConst
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymConst
$ctoConstr :: SymConst -> Constr
toConstr :: SymConst -> Constr
$cdataTypeOf :: SymConst -> DataType
dataTypeOf :: SymConst -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymConst)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymConst)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst)
$cgmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst
gmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymConst -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SymConst -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
Data, Typeable, (forall x. SymConst -> Rep SymConst x)
-> (forall x. Rep SymConst x -> SymConst) -> Generic SymConst
forall x. Rep SymConst x -> SymConst
forall x. SymConst -> Rep SymConst x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SymConst -> Rep SymConst x
from :: forall x. SymConst -> Rep SymConst x
$cto :: forall x. Rep SymConst x -> SymConst
to :: forall x. Rep SymConst x -> SymConst
Generic)
data Constant = I !Integer
| R !Double
| L !Text !Sort
deriving (Constant -> Constant -> Bool
(Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool) -> Eq Constant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Constant -> Constant -> Bool
== :: Constant -> Constant -> Bool
$c/= :: Constant -> Constant -> Bool
/= :: Constant -> Constant -> Bool
Eq, Eq Constant
Eq Constant =>
(Constant -> Constant -> Ordering)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Constant)
-> (Constant -> Constant -> Constant)
-> Ord Constant
Constant -> Constant -> Bool
Constant -> Constant -> Ordering
Constant -> Constant -> Constant
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Constant -> Constant -> Ordering
compare :: Constant -> Constant -> Ordering
$c< :: Constant -> Constant -> Bool
< :: Constant -> Constant -> Bool
$c<= :: Constant -> Constant -> Bool
<= :: Constant -> Constant -> Bool
$c> :: Constant -> Constant -> Bool
> :: Constant -> Constant -> Bool
$c>= :: Constant -> Constant -> Bool
>= :: Constant -> Constant -> Bool
$cmax :: Constant -> Constant -> Constant
max :: Constant -> Constant -> Constant
$cmin :: Constant -> Constant -> Constant
min :: Constant -> Constant -> Constant
Ord, Int -> Constant -> ShowS
[Constant] -> ShowS
Constant -> String
(Int -> Constant -> ShowS)
-> (Constant -> String) -> ([Constant] -> ShowS) -> Show Constant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constant -> ShowS
showsPrec :: Int -> Constant -> ShowS
$cshow :: Constant -> String
show :: Constant -> String
$cshowList :: [Constant] -> ShowS
showList :: [Constant] -> ShowS
Show, Typeable Constant
Typeable Constant =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constant)
-> (Constant -> Constr)
-> (Constant -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constant))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant))
-> ((forall b. Data b => b -> b) -> Constant -> Constant)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r)
-> (forall u. (forall d. Data d => d -> u) -> Constant -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant)
-> Data Constant
Constant -> Constr
Constant -> DataType
(forall b. Data b => b -> b) -> Constant -> Constant
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u
forall u. (forall d. Data d => d -> u) -> Constant -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constant
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constant)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constant
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constant
$ctoConstr :: Constant -> Constr
toConstr :: Constant -> Constr
$cdataTypeOf :: Constant -> DataType
dataTypeOf :: Constant -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constant)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constant)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant)
$cgmapT :: (forall b. Data b => b -> b) -> Constant -> Constant
gmapT :: (forall b. Data b => b -> b) -> Constant -> Constant
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Constant -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Constant -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
Data, Typeable, (forall x. Constant -> Rep Constant x)
-> (forall x. Rep Constant x -> Constant) -> Generic Constant
forall x. Rep Constant x -> Constant
forall x. Constant -> Rep Constant x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Constant -> Rep Constant x
from :: forall x. Constant -> Rep Constant x
$cto :: forall x. Rep Constant x -> Constant
to :: forall x. Rep Constant x -> Constant
Generic)
data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une
deriving (Brel -> Brel -> Bool
(Brel -> Brel -> Bool) -> (Brel -> Brel -> Bool) -> Eq Brel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Brel -> Brel -> Bool
== :: Brel -> Brel -> Bool
$c/= :: Brel -> Brel -> Bool
/= :: Brel -> Brel -> Bool
Eq, Eq Brel
Eq Brel =>
(Brel -> Brel -> Ordering)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Brel)
-> (Brel -> Brel -> Brel)
-> Ord Brel
Brel -> Brel -> Bool
Brel -> Brel -> Ordering
Brel -> Brel -> Brel
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Brel -> Brel -> Ordering
compare :: Brel -> Brel -> Ordering
$c< :: Brel -> Brel -> Bool
< :: Brel -> Brel -> Bool
$c<= :: Brel -> Brel -> Bool
<= :: Brel -> Brel -> Bool
$c> :: Brel -> Brel -> Bool
> :: Brel -> Brel -> Bool
$c>= :: Brel -> Brel -> Bool
>= :: Brel -> Brel -> Bool
$cmax :: Brel -> Brel -> Brel
max :: Brel -> Brel -> Brel
$cmin :: Brel -> Brel -> Brel
min :: Brel -> Brel -> Brel
Ord, Int -> Brel -> ShowS
[Brel] -> ShowS
Brel -> String
(Int -> Brel -> ShowS)
-> (Brel -> String) -> ([Brel] -> ShowS) -> Show Brel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Brel -> ShowS
showsPrec :: Int -> Brel -> ShowS
$cshow :: Brel -> String
show :: Brel -> String
$cshowList :: [Brel] -> ShowS
showList :: [Brel] -> ShowS
Show, Typeable Brel
Typeable Brel =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Brel)
-> (Brel -> Constr)
-> (Brel -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Brel))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel))
-> ((forall b. Data b => b -> b) -> Brel -> Brel)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r)
-> (forall u. (forall d. Data d => d -> u) -> Brel -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel)
-> Data Brel
Brel -> Constr
Brel -> DataType
(forall b. Data b => b -> b) -> Brel -> Brel
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u
forall u. (forall d. Data d => d -> u) -> Brel -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Brel
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Brel)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Brel
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Brel
$ctoConstr :: Brel -> Constr
toConstr :: Brel -> Constr
$cdataTypeOf :: Brel -> DataType
dataTypeOf :: Brel -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Brel)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Brel)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel)
$cgmapT :: (forall b. Data b => b -> b) -> Brel -> Brel
gmapT :: (forall b. Data b => b -> b) -> Brel -> Brel
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Brel -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Brel -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
Data, Typeable, (forall x. Brel -> Rep Brel x)
-> (forall x. Rep Brel x -> Brel) -> Generic Brel
forall x. Rep Brel x -> Brel
forall x. Brel -> Rep Brel x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Brel -> Rep Brel x
from :: forall x. Brel -> Rep Brel x
$cto :: forall x. Rep Brel x -> Brel
to :: forall x. Rep Brel x -> Brel
Generic)
data Bop = Plus | Minus | Times | Div | Mod | RTimes | RDiv
deriving (Bop -> Bop -> Bool
(Bop -> Bop -> Bool) -> (Bop -> Bop -> Bool) -> Eq Bop
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bop -> Bop -> Bool
== :: Bop -> Bop -> Bool
$c/= :: Bop -> Bop -> Bool
/= :: Bop -> Bop -> Bool
Eq, Eq Bop
Eq Bop =>
(Bop -> Bop -> Ordering)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bop)
-> (Bop -> Bop -> Bop)
-> Ord Bop
Bop -> Bop -> Bool
Bop -> Bop -> Ordering
Bop -> Bop -> Bop
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Bop -> Bop -> Ordering
compare :: Bop -> Bop -> Ordering
$c< :: Bop -> Bop -> Bool
< :: Bop -> Bop -> Bool
$c<= :: Bop -> Bop -> Bool
<= :: Bop -> Bop -> Bool
$c> :: Bop -> Bop -> Bool
> :: Bop -> Bop -> Bool
$c>= :: Bop -> Bop -> Bool
>= :: Bop -> Bop -> Bool
$cmax :: Bop -> Bop -> Bop
max :: Bop -> Bop -> Bop
$cmin :: Bop -> Bop -> Bop
min :: Bop -> Bop -> Bop
Ord, Int -> Bop -> ShowS
[Bop] -> ShowS
Bop -> String
(Int -> Bop -> ShowS)
-> (Bop -> String) -> ([Bop] -> ShowS) -> Show Bop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bop -> ShowS
showsPrec :: Int -> Bop -> ShowS
$cshow :: Bop -> String
show :: Bop -> String
$cshowList :: [Bop] -> ShowS
showList :: [Bop] -> ShowS
Show, Typeable Bop
Typeable Bop =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bop)
-> (Bop -> Constr)
-> (Bop -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bop))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop))
-> ((forall b. Data b => b -> b) -> Bop -> Bop)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bop -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop)
-> Data Bop
Bop -> Constr
Bop -> DataType
(forall b. Data b => b -> b) -> Bop -> Bop
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u
forall u. (forall d. Data d => d -> u) -> Bop -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bop
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bop)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bop
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bop
$ctoConstr :: Bop -> Constr
toConstr :: Bop -> Constr
$cdataTypeOf :: Bop -> DataType
dataTypeOf :: Bop -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bop)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bop)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop)
$cgmapT :: (forall b. Data b => b -> b) -> Bop -> Bop
gmapT :: (forall b. Data b => b -> b) -> Bop -> Bop
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Bop -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Bop -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
Data, Typeable, (forall x. Bop -> Rep Bop x)
-> (forall x. Rep Bop x -> Bop) -> Generic Bop
forall x. Rep Bop x -> Bop
forall x. Bop -> Rep Bop x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Bop -> Rep Bop x
from :: forall x. Bop -> Rep Bop x
$cto :: forall x. Rep Bop x -> Bop
to :: forall x. Rep Bop x -> Bop
Generic)
data Expr = ESym !SymConst
| ECon !Constant
| EVar !Symbol
| EApp !Expr !Expr
| ENeg !Expr
| EBin !Bop !Expr !Expr
| EIte !Expr !Expr !Expr
| ECst !Expr !Sort
| ELam !(Symbol, Sort) !Expr
| ETApp !Expr !Sort
| ETAbs !Expr !Symbol
| PAnd ![Expr]
| POr ![Expr]
| PNot !Expr
| PImp !Expr !Expr
| PIff !Expr !Expr
| PAtom !Brel !Expr !Expr
| PKVar !KVar !Subst
| PAll ![(Symbol, Sort)] !Expr
| PExist ![(Symbol, Sort)] !Expr
| PGrad !KVar !Subst !GradInfo !Expr
| ECoerc !Sort !Sort !Expr
deriving (Pred -> Pred -> Bool
(Pred -> Pred -> Bool) -> (Pred -> Pred -> Bool) -> Eq Pred
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pred -> Pred -> Bool
== :: Pred -> Pred -> Bool
$c/= :: Pred -> Pred -> Bool
/= :: Pred -> Pred -> Bool
Eq, Int -> Pred -> ShowS
[Pred] -> ShowS
Pred -> String
(Int -> Pred -> ShowS)
-> (Pred -> String) -> ([Pred] -> ShowS) -> Show Pred
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Pred -> ShowS
showsPrec :: Int -> Pred -> ShowS
$cshow :: Pred -> String
show :: Pred -> String
$cshowList :: [Pred] -> ShowS
showList :: [Pred] -> ShowS
Show, Eq Pred
Eq Pred =>
(Pred -> Pred -> Ordering)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Bool)
-> (Pred -> Pred -> Pred)
-> (Pred -> Pred -> Pred)
-> Ord Pred
Pred -> Pred -> Bool
Pred -> Pred -> Ordering
Pred -> Pred -> Pred
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Pred -> Pred -> Ordering
compare :: Pred -> Pred -> Ordering
$c< :: Pred -> Pred -> Bool
< :: Pred -> Pred -> Bool
$c<= :: Pred -> Pred -> Bool
<= :: Pred -> Pred -> Bool
$c> :: Pred -> Pred -> Bool
> :: Pred -> Pred -> Bool
$c>= :: Pred -> Pred -> Bool
>= :: Pred -> Pred -> Bool
$cmax :: Pred -> Pred -> Pred
max :: Pred -> Pred -> Pred
$cmin :: Pred -> Pred -> Pred
min :: Pred -> Pred -> Pred
Ord, Typeable Pred
Typeable Pred =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred)
-> (Pred -> Constr)
-> (Pred -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred))
-> ((forall b. Data b => b -> b) -> Pred -> Pred)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r)
-> (forall u. (forall d. Data d => d -> u) -> Pred -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred)
-> Data Pred
Pred -> Constr
Pred -> DataType
(forall b. Data b => b -> b) -> Pred -> Pred
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
forall u. (forall d. Data d => d -> u) -> Pred -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Pred -> c Pred
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Pred
$ctoConstr :: Pred -> Constr
toConstr :: Pred -> Constr
$cdataTypeOf :: Pred -> DataType
dataTypeOf :: Pred -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Pred)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Pred)
$cgmapT :: (forall b. Data b => b -> b) -> Pred -> Pred
gmapT :: (forall b. Data b => b -> b) -> Pred -> Pred
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pred -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Pred -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Pred -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Pred -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Pred -> m Pred
Data, Typeable, (forall x. Pred -> Rep Pred x)
-> (forall x. Rep Pred x -> Pred) -> Generic Pred
forall x. Rep Pred x -> Pred
forall x. Pred -> Rep Pred x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Pred -> Rep Pred x
from :: forall x. Pred -> Rep Pred x
$cto :: forall x. Rep Pred x -> Pred
to :: forall x. Rep Pred x -> Pred
Generic)
onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
onEverySubexpr :: (Pred -> Pred) -> Pred -> Pred
onEverySubexpr = (Pred -> Pred) -> Pred -> Pred
forall a. Data a => (a -> a) -> a -> a
everywhereOnA
everywhereOnA :: forall a. Data a => (a -> a) -> a -> a
everywhereOnA :: forall a. Data a => (a -> a) -> a -> a
everywhereOnA a -> a
f = a -> a
go
where
go :: a -> a
go :: a -> a
go = a -> a
f (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b. Data b => b -> b) -> a -> a
forall a. Data a => (forall b. Data b => b -> b) -> a -> a
gmapT ((a -> a) -> b -> b
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT a -> a
go (b -> b) -> ([a] -> [a]) -> b -> b
forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
go)
type Pred = Expr
pattern PTrue :: Expr
pattern $mPTrue :: forall {r}. Pred -> ((# #) -> r) -> ((# #) -> r) -> r
$bPTrue :: Pred
PTrue = PAnd []
pattern PTop :: Expr
pattern $mPTop :: forall {r}. Pred -> ((# #) -> r) -> ((# #) -> r) -> r
$bPTop :: Pred
PTop = PAnd []
pattern PFalse :: Expr
pattern $mPFalse :: forall {r}. Pred -> ((# #) -> r) -> ((# #) -> r) -> r
$bPFalse :: Pred
PFalse = POr []
pattern EBot :: Expr
pattern $mEBot :: forall {r}. Pred -> ((# #) -> r) -> ((# #) -> r) -> r
$bEBot :: Pred
EBot = POr []
pattern EEq :: Expr -> Expr -> Expr
pattern $mEEq :: forall {r}. Pred -> (Pred -> Pred -> r) -> ((# #) -> r) -> r
$bEEq :: Pred -> Pred -> Pred
EEq e1 e2 = PAtom Eq e1 e2
pattern ETimes :: Expr -> Expr -> Expr
pattern $mETimes :: forall {r}. Pred -> (Pred -> Pred -> r) -> ((# #) -> r) -> r
$bETimes :: Pred -> Pred -> Pred
ETimes e1 e2 = EBin Times e1 e2
pattern ERTimes :: Expr -> Expr -> Expr
pattern $mERTimes :: forall {r}. Pred -> (Pred -> Pred -> r) -> ((# #) -> r) -> r
$bERTimes :: Pred -> Pred -> Pred
ERTimes e1 e2 = EBin RTimes e1 e2
pattern EDiv :: Expr -> Expr -> Expr
pattern $mEDiv :: forall {r}. Pred -> (Pred -> Pred -> r) -> ((# #) -> r) -> r
$bEDiv :: Pred -> Pred -> Pred
EDiv e1 e2 = EBin Div e1 e2
pattern ERDiv :: Expr -> Expr -> Expr
pattern $mERDiv :: forall {r}. Pred -> (Pred -> Pred -> r) -> ((# #) -> r) -> r
$bERDiv :: Pred -> Pred -> Pred
ERDiv e1 e2 = EBin RDiv e1 e2
exprSymbolsSet :: Expr -> HashSet Symbol
exprSymbolsSet :: Pred -> HashSet Symbol
exprSymbolsSet = Pred -> HashSet Symbol
go
where
gos :: [Pred] -> HashSet Symbol
gos [Pred]
es = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
HashSet.unions (Pred -> HashSet Symbol
go (Pred -> HashSet Symbol) -> [Pred] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
es)
go :: Pred -> HashSet Symbol
go (EVar Symbol
x) = Symbol -> HashSet Symbol
forall a. Hashable a => a -> HashSet a
HashSet.singleton Symbol
x
go (EApp Pred
f Pred
e) = [Pred] -> HashSet Symbol
gos [Pred
f, Pred
e]
go (ELam (Symbol
x,Sort
_) Pred
e) = Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.delete Symbol
x (Pred -> HashSet Symbol
go Pred
e)
go (ECoerc Sort
_ Sort
_ Pred
e) = Pred -> HashSet Symbol
go Pred
e
go (ENeg Pred
e) = Pred -> HashSet Symbol
go Pred
e
go (EBin Bop
_ Pred
e1 Pred
e2) = [Pred] -> HashSet Symbol
gos [Pred
e1, Pred
e2]
go (EIte Pred
p Pred
e1 Pred
e2) = [Pred] -> HashSet Symbol
gos [Pred
p, Pred
e1, Pred
e2]
go (ECst Pred
e Sort
_) = Pred -> HashSet Symbol
go Pred
e
go (PAnd [Pred]
ps) = [Pred] -> HashSet Symbol
gos [Pred]
ps
go (POr [Pred]
ps) = [Pred] -> HashSet Symbol
gos [Pred]
ps
go (PNot Pred
p) = Pred -> HashSet Symbol
go Pred
p
go (PIff Pred
p1 Pred
p2) = [Pred] -> HashSet Symbol
gos [Pred
p1, Pred
p2]
go (PImp Pred
p1 Pred
p2) = [Pred] -> HashSet Symbol
gos [Pred
p1, Pred
p2]
go (PAtom Brel
_ Pred
e1 Pred
e2) = [Pred] -> HashSet Symbol
gos [Pred
e1, Pred
e2]
go (PKVar KVar
_ (Su HashMap Symbol Pred
su)) = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
HashSet.unions ([HashSet Symbol] -> HashSet Symbol)
-> [HashSet Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ (Pred -> HashSet Symbol) -> [Pred] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> HashSet Symbol
exprSymbolsSet (HashMap Symbol Pred -> [Pred]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol Pred
su)
go (PAll [(Symbol, Sort)]
xts Pred
p) = Pred -> HashSet Symbol
go Pred
p HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.difference` [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.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 Pred
p) = Pred -> HashSet Symbol
go Pred
p HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`HashSet.difference` [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.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 Pred
_ = HashSet Symbol
forall a. HashSet a
HashSet.empty
substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr
substSortInExpr :: (Symbol -> Sort) -> Pred -> Pred
substSortInExpr Symbol -> Sort
f = (Pred -> Pred) -> Pred -> Pred
onEverySubexpr Pred -> Pred
go
where
go :: Pred -> Pred
go = \case
ELam (Symbol
x, Sort
t) Pred
e -> (Symbol, Sort) -> Pred -> Pred
ELam (Symbol
x, (Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t) Pred
e
PAll [(Symbol, Sort)]
xts Pred
e -> [(Symbol, Sort)] -> Pred -> Pred
PAll ((Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f) ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) Pred
e
PExist [(Symbol, Sort)]
xts Pred
e -> [(Symbol, Sort)] -> Pred -> Pred
PExist ((Sort -> Sort) -> (Symbol, Sort) -> (Symbol, Sort)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f) ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) Pred
e
ECst Pred
e Sort
t -> Pred -> Sort -> Pred
ECst Pred
e ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t)
ECoerc Sort
t0 Sort
t1 Pred
e -> Sort -> Sort -> Pred -> Pred
ECoerc ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t0) ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t1) Pred
e
Pred
e -> Pred
e
exprKVars :: Expr -> HashMap KVar [Subst]
exprKVars :: Pred -> HashMap KVar [Subst]
exprKVars = Pred -> HashMap KVar [Subst]
go
where
gos :: [Pred] -> HashMap KVar [Subst]
gos [Pred]
es = [HashMap KVar [Subst]] -> HashMap KVar [Subst]
forall k v. Eq k => [HashMap k v] -> HashMap k v
HashMap.unions (Pred -> HashMap KVar [Subst]
go (Pred -> HashMap KVar [Subst]) -> [Pred] -> [HashMap KVar [Subst]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
es)
go :: Pred -> HashMap KVar [Subst]
go (EVar Symbol
_) = HashMap KVar [Subst]
forall k v. HashMap k v
HashMap.empty
go (EApp Pred
f Pred
e) = [Pred] -> HashMap KVar [Subst]
gos [Pred
f, Pred
e]
go (ELam (Symbol, Sort)
_ Pred
e) = Pred -> HashMap KVar [Subst]
go Pred
e
go (ECoerc Sort
_ Sort
_ Pred
e) = Pred -> HashMap KVar [Subst]
go Pred
e
go (ENeg Pred
e) = Pred -> HashMap KVar [Subst]
go Pred
e
go (EBin Bop
_ Pred
e1 Pred
e2) = [Pred] -> HashMap KVar [Subst]
gos [Pred
e1, Pred
e2]
go (EIte Pred
p Pred
e1 Pred
e2) = [Pred] -> HashMap KVar [Subst]
gos [Pred
p, Pred
e1, Pred
e2]
go (ECst Pred
e Sort
_) = Pred -> HashMap KVar [Subst]
go Pred
e
go (PAnd [Pred]
ps) = [Pred] -> HashMap KVar [Subst]
gos [Pred]
ps
go (POr [Pred]
ps) = [Pred] -> HashMap KVar [Subst]
gos [Pred]
ps
go (PNot Pred
p) = Pred -> HashMap KVar [Subst]
go Pred
p
go (PIff Pred
p1 Pred
p2) = [Pred] -> HashMap KVar [Subst]
gos [Pred
p1, Pred
p2]
go (PImp Pred
p1 Pred
p2) = [Pred] -> HashMap KVar [Subst]
gos [Pred
p1, Pred
p2]
go (PAtom Brel
_ Pred
e1 Pred
e2) = [Pred] -> HashMap KVar [Subst]
gos [Pred
e1, Pred
e2]
go (PKVar KVar
k substs :: Subst
substs@(Su HashMap Symbol Pred
su)) =
([Subst] -> [Subst] -> [Subst])
-> KVar -> [Subst] -> HashMap KVar [Subst] -> HashMap KVar [Subst]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HashMap.insertWith [Subst] -> [Subst] -> [Subst]
forall a. [a] -> [a] -> [a]
(++) KVar
k [Subst
substs] (HashMap KVar [Subst] -> HashMap KVar [Subst])
-> HashMap KVar [Subst] -> HashMap KVar [Subst]
forall a b. (a -> b) -> a -> b
$ [HashMap KVar [Subst]] -> HashMap KVar [Subst]
forall k v. Eq k => [HashMap k v] -> HashMap k v
HashMap.unions ([HashMap KVar [Subst]] -> HashMap KVar [Subst])
-> [HashMap KVar [Subst]] -> HashMap KVar [Subst]
forall a b. (a -> b) -> a -> b
$ (Pred -> HashMap KVar [Subst]) -> [Pred] -> [HashMap KVar [Subst]]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> HashMap KVar [Subst]
exprKVars (HashMap Symbol Pred -> [Pred]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol Pred
su)
go (PAll [(Symbol, Sort)]
_xts Pred
p) = Pred -> HashMap KVar [Subst]
go Pred
p
go (PExist [(Symbol, Sort)]
_xts Pred
p) = Pred -> HashMap KVar [Subst]
go Pred
p
go Pred
_ = HashMap KVar [Subst]
forall k v. HashMap k v
HashMap.empty
data GradInfo = GradInfo {GradInfo -> SrcSpan
gsrc :: SrcSpan, GradInfo -> Maybe SrcSpan
gused :: Maybe SrcSpan}
deriving (GradInfo -> GradInfo -> Bool
(GradInfo -> GradInfo -> Bool)
-> (GradInfo -> GradInfo -> Bool) -> Eq GradInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GradInfo -> GradInfo -> Bool
== :: GradInfo -> GradInfo -> Bool
$c/= :: GradInfo -> GradInfo -> Bool
/= :: GradInfo -> GradInfo -> Bool
Eq, Eq GradInfo
Eq GradInfo =>
(GradInfo -> GradInfo -> Ordering)
-> (GradInfo -> GradInfo -> Bool)
-> (GradInfo -> GradInfo -> Bool)
-> (GradInfo -> GradInfo -> Bool)
-> (GradInfo -> GradInfo -> Bool)
-> (GradInfo -> GradInfo -> GradInfo)
-> (GradInfo -> GradInfo -> GradInfo)
-> Ord GradInfo
GradInfo -> GradInfo -> Bool
GradInfo -> GradInfo -> Ordering
GradInfo -> GradInfo -> GradInfo
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GradInfo -> GradInfo -> Ordering
compare :: GradInfo -> GradInfo -> Ordering
$c< :: GradInfo -> GradInfo -> Bool
< :: GradInfo -> GradInfo -> Bool
$c<= :: GradInfo -> GradInfo -> Bool
<= :: GradInfo -> GradInfo -> Bool
$c> :: GradInfo -> GradInfo -> Bool
> :: GradInfo -> GradInfo -> Bool
$c>= :: GradInfo -> GradInfo -> Bool
>= :: GradInfo -> GradInfo -> Bool
$cmax :: GradInfo -> GradInfo -> GradInfo
max :: GradInfo -> GradInfo -> GradInfo
$cmin :: GradInfo -> GradInfo -> GradInfo
min :: GradInfo -> GradInfo -> GradInfo
Ord, Int -> GradInfo -> ShowS
[GradInfo] -> ShowS
GradInfo -> String
(Int -> GradInfo -> ShowS)
-> (GradInfo -> String) -> ([GradInfo] -> ShowS) -> Show GradInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GradInfo -> ShowS
showsPrec :: Int -> GradInfo -> ShowS
$cshow :: GradInfo -> String
show :: GradInfo -> String
$cshowList :: [GradInfo] -> ShowS
showList :: [GradInfo] -> ShowS
Show, Typeable GradInfo
Typeable GradInfo =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GradInfo)
-> (GradInfo -> Constr)
-> (GradInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GradInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo))
-> ((forall b. Data b => b -> b) -> GradInfo -> GradInfo)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> GradInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo)
-> Data GradInfo
GradInfo -> Constr
GradInfo -> DataType
(forall b. Data b => b -> b) -> GradInfo -> GradInfo
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u
forall u. (forall d. Data d => d -> u) -> GradInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GradInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GradInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GradInfo
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GradInfo
$ctoConstr :: GradInfo -> Constr
toConstr :: GradInfo -> Constr
$cdataTypeOf :: GradInfo -> DataType
dataTypeOf :: GradInfo -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GradInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GradInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo)
$cgmapT :: (forall b. Data b => b -> b) -> GradInfo -> GradInfo
gmapT :: (forall b. Data b => b -> b) -> GradInfo -> GradInfo
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GradInfo -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> GradInfo -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
Data, Typeable, (forall x. GradInfo -> Rep GradInfo x)
-> (forall x. Rep GradInfo x -> GradInfo) -> Generic GradInfo
forall x. Rep GradInfo x -> GradInfo
forall x. GradInfo -> Rep GradInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. GradInfo -> Rep GradInfo x
from :: forall x. GradInfo -> Rep GradInfo x
$cto :: forall x. Rep GradInfo x -> GradInfo
to :: forall x. Rep GradInfo x -> GradInfo
Generic)
srcGradInfo :: SourcePos -> GradInfo
srcGradInfo :: SourcePos -> GradInfo
srcGradInfo SourcePos
src = SrcSpan -> Maybe SrcSpan -> GradInfo
GradInfo (SourcePos -> SourcePos -> SrcSpan
SS SourcePos
src SourcePos
src) Maybe SrcSpan
forall a. Maybe a
Nothing
mkEApp :: LocSymbol -> [Expr] -> Expr
mkEApp :: LocSymbol -> [Pred] -> Pred
mkEApp = Pred -> [Pred] -> Pred
eApps (Pred -> [Pred] -> Pred)
-> (LocSymbol -> Pred) -> LocSymbol -> [Pred] -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Pred
EVar (Symbol -> Pred) -> (LocSymbol -> Symbol) -> LocSymbol -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> Symbol
forall a. Located a -> a
val
eApps :: Expr -> [Expr] -> Expr
eApps :: Pred -> [Pred] -> Pred
eApps Pred
f [Pred]
es = (Pred -> Pred -> Pred) -> Pred -> [Pred] -> Pred
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Pred -> Pred -> Pred
EApp Pred
f [Pred]
es
splitEApp :: Expr -> (Expr, [Expr])
splitEApp :: Pred -> (Pred, [Pred])
splitEApp = [Pred] -> Pred -> (Pred, [Pred])
go []
where
go :: [Pred] -> Pred -> (Pred, [Pred])
go [Pred]
acc (EApp Pred
f Pred
e) = [Pred] -> Pred -> (Pred, [Pred])
go (Pred
ePred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
acc) Pred
f
go [Pred]
acc Pred
e = (Pred
e, [Pred]
acc)
splitEAppThroughECst :: Expr -> (Expr, [Expr])
splitEAppThroughECst :: Pred -> (Pred, [Pred])
splitEAppThroughECst = [Pred] -> Pred -> (Pred, [Pred])
go []
where
go :: [Pred] -> Pred -> (Pred, [Pred])
go [Pred]
acc (Pred -> Pred
dropECst -> (EApp Pred
f Pred
e)) = [Pred] -> Pred -> (Pred, [Pred])
go (Pred
ePred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
acc) Pred
f
go [Pred]
acc Pred
e = (Pred
e, [Pred]
acc)
dropECst :: Expr -> Expr
dropECst :: Pred -> Pred
dropECst Pred
e = case Pred
e of
ECst Pred
e' Sort
_ -> Pred -> Pred
dropECst Pred
e'
Pred
_ -> Pred
e
splitPAnd :: Expr -> [Expr]
splitPAnd :: Pred -> [Pred]
splitPAnd (PAnd [Pred]
es) = (Pred -> [Pred]) -> [Pred] -> [Pred]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [Pred]
splitPAnd [Pred]
es
splitPAnd Pred
e = [Pred
e]
eAppC :: Sort -> Expr -> Expr -> Expr
eAppC :: Sort -> Pred -> Pred -> Pred
eAppC Sort
s Pred
e1 Pred
e2 = Pred -> Sort -> Pred
eCst (Pred -> Pred -> Pred
EApp Pred
e1 Pred
e2) Sort
s
eCst :: Expr -> Sort -> Expr
eCst :: Pred -> Sort -> Pred
eCst Pred
e Sort
t = Pred -> Sort -> Pred
ECst (Pred -> Pred
dropECst Pred
e) Sort
t
debruijnIndex :: Expr -> Int
debruijnIndex :: Pred -> Int
debruijnIndex = Pred -> Int
forall {a}. Num a => Pred -> a
go
where
go :: Pred -> a
go (ELam (Symbol, Sort)
_ Pred
e) = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e
go (ECst Pred
e Sort
_) = Pred -> a
go Pred
e
go (EApp Pred
e1 Pred
e2) = Pred -> a
go Pred
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e2
go (ESym SymConst
_) = a
1
go (ECon Constant
_) = a
1
go (EVar Symbol
_) = a
1
go (ENeg Pred
e) = Pred -> a
go Pred
e
go (EBin Bop
_ Pred
e1 Pred
e2) = Pred -> a
go Pred
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e2
go (EIte Pred
e Pred
e1 Pred
e2) = Pred -> a
go Pred
e a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e2
go (ETAbs Pred
e Symbol
_) = Pred -> a
go Pred
e
go (ETApp Pred
e Sort
_) = Pred -> a
go Pred
e
go (PAnd [Pred]
es) = (a -> Pred -> a) -> a -> [Pred] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\a
n Pred
e -> a
n a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e) a
0 [Pred]
es
go (POr [Pred]
es) = (a -> Pred -> a) -> a -> [Pred] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\a
n Pred
e -> a
n a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e) a
0 [Pred]
es
go (PNot Pred
e) = Pred -> a
go Pred
e
go (PImp Pred
e1 Pred
e2) = Pred -> a
go Pred
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e2
go (PIff Pred
e1 Pred
e2) = Pred -> a
go Pred
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e2
go (PAtom Brel
_ Pred
e1 Pred
e2) = Pred -> a
go Pred
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Pred -> a
go Pred
e2
go (PAll [(Symbol, Sort)]
_ Pred
e) = Pred -> a
go Pred
e
go (PExist [(Symbol, Sort)]
_ Pred
e) = Pred -> a
go Pred
e
go (PKVar KVar
_ Subst
_) = a
1
go (PGrad KVar
_ Subst
_ GradInfo
_ Pred
e) = Pred -> a
go Pred
e
go (ECoerc Sort
_ Sort
_ Pred
e) = Pred -> a
go Pred
e
newtype Reft = Reft (Symbol, Expr)
deriving (Reft -> Reft -> Bool
(Reft -> Reft -> Bool) -> (Reft -> Reft -> Bool) -> Eq Reft
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Reft -> Reft -> Bool
== :: Reft -> Reft -> Bool
$c/= :: Reft -> Reft -> Bool
/= :: Reft -> Reft -> Bool
Eq, Eq Reft
Eq Reft =>
(Reft -> Reft -> Ordering)
-> (Reft -> Reft -> Bool)
-> (Reft -> Reft -> Bool)
-> (Reft -> Reft -> Bool)
-> (Reft -> Reft -> Bool)
-> (Reft -> Reft -> Reft)
-> (Reft -> Reft -> Reft)
-> Ord Reft
Reft -> Reft -> Bool
Reft -> Reft -> Ordering
Reft -> Reft -> Reft
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Reft -> Reft -> Ordering
compare :: Reft -> Reft -> Ordering
$c< :: Reft -> Reft -> Bool
< :: Reft -> Reft -> Bool
$c<= :: Reft -> Reft -> Bool
<= :: Reft -> Reft -> Bool
$c> :: Reft -> Reft -> Bool
> :: Reft -> Reft -> Bool
$c>= :: Reft -> Reft -> Bool
>= :: Reft -> Reft -> Bool
$cmax :: Reft -> Reft -> Reft
max :: Reft -> Reft -> Reft
$cmin :: Reft -> Reft -> Reft
min :: Reft -> Reft -> Reft
Ord, Typeable Reft
Typeable Reft =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft)
-> (Reft -> Constr)
-> (Reft -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft))
-> ((forall b. Data b => b -> b) -> Reft -> Reft)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r)
-> (forall u. (forall d. Data d => d -> u) -> Reft -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft)
-> Data Reft
Reft -> Constr
Reft -> DataType
(forall b. Data b => b -> b) -> Reft -> Reft
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
forall u. (forall d. Data d => d -> u) -> Reft -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft
$ctoConstr :: Reft -> Constr
toConstr :: Reft -> Constr
$cdataTypeOf :: Reft -> DataType
dataTypeOf :: Reft -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft)
$cgmapT :: (forall b. Data b => b -> b) -> Reft -> Reft
gmapT :: (forall b. Data b => b -> b) -> Reft -> Reft
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Reft -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Reft -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
Data, Typeable, (forall x. Reft -> Rep Reft x)
-> (forall x. Rep Reft x -> Reft) -> Generic Reft
forall x. Rep Reft x -> Reft
forall x. Reft -> Rep Reft x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Reft -> Rep Reft x
from :: forall x. Reft -> Rep Reft x
$cto :: forall x. Rep Reft x -> Reft
to :: forall x. Rep Reft x -> Reft
Generic)
data SortedReft = RR { SortedReft -> Sort
sr_sort :: !Sort, SortedReft -> Reft
sr_reft :: !Reft }
deriving (SortedReft -> SortedReft -> Bool
(SortedReft -> SortedReft -> Bool)
-> (SortedReft -> SortedReft -> Bool) -> Eq SortedReft
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SortedReft -> SortedReft -> Bool
== :: SortedReft -> SortedReft -> Bool
$c/= :: SortedReft -> SortedReft -> Bool
/= :: SortedReft -> SortedReft -> Bool
Eq, Eq SortedReft
Eq SortedReft =>
(SortedReft -> SortedReft -> Ordering)
-> (SortedReft -> SortedReft -> Bool)
-> (SortedReft -> SortedReft -> Bool)
-> (SortedReft -> SortedReft -> Bool)
-> (SortedReft -> SortedReft -> Bool)
-> (SortedReft -> SortedReft -> SortedReft)
-> (SortedReft -> SortedReft -> SortedReft)
-> Ord SortedReft
SortedReft -> SortedReft -> Bool
SortedReft -> SortedReft -> Ordering
SortedReft -> SortedReft -> SortedReft
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SortedReft -> SortedReft -> Ordering
compare :: SortedReft -> SortedReft -> Ordering
$c< :: SortedReft -> SortedReft -> Bool
< :: SortedReft -> SortedReft -> Bool
$c<= :: SortedReft -> SortedReft -> Bool
<= :: SortedReft -> SortedReft -> Bool
$c> :: SortedReft -> SortedReft -> Bool
> :: SortedReft -> SortedReft -> Bool
$c>= :: SortedReft -> SortedReft -> Bool
>= :: SortedReft -> SortedReft -> Bool
$cmax :: SortedReft -> SortedReft -> SortedReft
max :: SortedReft -> SortedReft -> SortedReft
$cmin :: SortedReft -> SortedReft -> SortedReft
min :: SortedReft -> SortedReft -> SortedReft
Ord, Typeable SortedReft
Typeable SortedReft =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortedReft)
-> (SortedReft -> Constr)
-> (SortedReft -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortedReft))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SortedReft))
-> ((forall b. Data b => b -> b) -> SortedReft -> SortedReft)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r)
-> (forall u. (forall d. Data d => d -> u) -> SortedReft -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> SortedReft -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft)
-> Data SortedReft
SortedReft -> Constr
SortedReft -> DataType
(forall b. Data b => b -> b) -> SortedReft -> SortedReft
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SortedReft -> u
forall u. (forall d. Data d => d -> u) -> SortedReft -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortedReft
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortedReft)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortedReft
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortedReft
$ctoConstr :: SortedReft -> Constr
toConstr :: SortedReft -> Constr
$cdataTypeOf :: SortedReft -> DataType
dataTypeOf :: SortedReft -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortedReft)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortedReft)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft)
$cgmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft
gmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SortedReft -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SortedReft -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SortedReft -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SortedReft -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
Data, Typeable, (forall x. SortedReft -> Rep SortedReft x)
-> (forall x. Rep SortedReft x -> SortedReft) -> Generic SortedReft
forall x. Rep SortedReft x -> SortedReft
forall x. SortedReft -> Rep SortedReft x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SortedReft -> Rep SortedReft x
from :: forall x. SortedReft -> Rep SortedReft x
$cto :: forall x. Rep SortedReft x -> SortedReft
to :: forall x. Rep SortedReft x -> SortedReft
Generic)
instance Hashable SortedReft
sortedReftSymbols :: SortedReft -> HashSet Symbol
sortedReftSymbols :: SortedReft -> HashSet Symbol
sortedReftSymbols SortedReft
sr =
HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HashSet.union
(Sort -> HashSet Symbol
sortSymbols (Sort -> HashSet Symbol) -> Sort -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> Sort
sr_sort SortedReft
sr)
(Pred -> HashSet Symbol
exprSymbolsSet (Pred -> HashSet Symbol) -> Pred -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Reft -> Pred
reftPred (Reft -> Pred) -> Reft -> Pred
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr)
elit :: Located Symbol -> Sort -> Expr
elit :: LocSymbol -> Sort -> Pred
elit LocSymbol
l Sort
s = Constant -> Pred
ECon (Constant -> Pred) -> Constant -> Pred
forall a b. (a -> b) -> a -> b
$ Text -> Sort -> Constant
L (Symbol -> Text
symbolText (Symbol -> Text) -> Symbol -> Text
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
l) Sort
s
instance Fixpoint Constant where
toFix :: Constant -> Doc
toFix (I Integer
i) = Integer -> Doc
forall a. Fixpoint a => a -> Doc
toFix Integer
i
toFix (R Double
i) = Double -> Doc
forall a. Fixpoint a => a -> Doc
toFix Double
i
toFix (L Text
s Sort
t) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"lit" Doc -> Doc -> Doc
<+> String -> Doc
text String
"\"" Doc -> Doc -> Doc
<-> Text -> Doc
forall a. Fixpoint a => a -> Doc
toFix Text
s Doc -> Doc -> Doc
<-> String -> Doc
text String
"\"" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
t
instance Symbolic SymConst where
symbol :: SymConst -> Symbol
symbol = SymConst -> Symbol
encodeSymConst
encodeSymConst :: SymConst -> Symbol
encodeSymConst :: SymConst -> Symbol
encodeSymConst (SL Text
s) = Symbol -> Symbol
litSymbol (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Text
s
instance Fixpoint SymConst where
toFix :: SymConst -> Doc
toFix (SL Text
t) = String -> Doc
text (Text -> String
forall a. Show a => a -> String
show Text
t)
instance Fixpoint KVar where
toFix :: KVar -> Doc
toFix (KV Symbol
k) = String -> Doc
text String
"$" Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
k
instance Fixpoint Brel where
toFix :: Brel -> Doc
toFix Brel
Eq = String -> Doc
text String
"="
toFix Brel
Ne = String -> Doc
text String
"!="
toFix Brel
Ueq = String -> Doc
text String
"~~"
toFix Brel
Une = String -> Doc
text String
"!~"
toFix Brel
Gt = String -> Doc
text String
">"
toFix Brel
Ge = String -> Doc
text String
">="
toFix Brel
Lt = String -> Doc
text String
"<"
toFix Brel
Le = String -> Doc
text String
"<="
instance Fixpoint Bop where
toFix :: Bop -> Doc
toFix Bop
Plus = String -> Doc
text String
"+"
toFix Bop
Minus = String -> Doc
text String
"-"
toFix Bop
RTimes = String -> Doc
text String
"*."
toFix Bop
Times = String -> Doc
text String
"*"
toFix Bop
Div = String -> Doc
text String
"/"
toFix Bop
RDiv = String -> Doc
text String
"/."
toFix Bop
Mod = String -> Doc
text String
"mod"
instance Fixpoint Expr where
toFix :: Pred -> Doc
toFix (ESym SymConst
c) = SymConst -> Doc
forall a. Fixpoint a => a -> Doc
toFix SymConst
c
toFix (ECon Constant
c) = Constant -> Doc
forall a. Fixpoint a => a -> Doc
toFix Constant
c
toFix (EVar Symbol
s) = Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
s
toFix e :: Pred
e@(EApp Pred
_ Pred
_) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
" " ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Pred -> Doc) -> [Pred] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred
fPred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
es) where (Pred
f, [Pred]
es) = Pred -> (Pred, [Pred])
splitEApp Pred
e
toFix (ENeg Pred
e) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"-" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e)
toFix (EBin Bop
o Pred
e1 Pred
e2) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e1 Doc -> Doc -> Doc
<+> Bop -> Doc
forall a. Fixpoint a => a -> Doc
toFix Bop
o, Int -> Doc -> Doc
nest Int
2 (Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e2)]
toFix (EIte Pred
p Pred
e1 Pred
e2) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [String -> Doc
text String
"if" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p Doc -> Doc -> Doc
<+> String -> Doc
text String
"then", Int -> Doc -> Doc
nest Int
2 (Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e1), String -> Doc
text String
"else", Int -> Doc -> Doc
nest Int
2 (Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e2)]
toFix (ECst Pred
e Sort
so) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e Doc -> Doc -> Doc
<+> String -> Doc
text String
" : " Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
so
toFix Pred
PTrue = String -> Doc
text String
"true"
toFix Pred
PFalse = String -> Doc
text String
"false"
toFix (PNot Pred
p) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"~" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p)
toFix (PImp Pred
p1 Pred
p2) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"=>" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p2
toFix (PIff Pred
p1 Pred
p2) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"<=>" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p2
toFix (PAnd [Pred]
ps) = String -> Doc
text String
"&&" Doc -> Doc -> Doc
<+> [Pred] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [Pred]
ps
toFix (POr [Pred]
ps) = String -> Doc
text String
"||" Doc -> Doc -> Doc
<+> [Pred] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [Pred]
ps
toFix (PAtom Brel
r Pred
e1 Pred
e2) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e1 Doc -> Doc -> Doc
<+> Brel -> Doc
forall a. Fixpoint a => a -> Doc
toFix Brel
r, Int -> Doc -> Doc
nest Int
2 (Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e2)]
toFix (PKVar KVar
k Subst
su) = KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix KVar
k Doc -> Doc -> Doc
<-> Subst -> Doc
forall a. Fixpoint a => a -> Doc
toFix Subst
su
toFix (PAll [(Symbol, Sort)]
xts Pred
p) = Doc
"forall" Doc -> Doc -> Doc
<+> ([(Symbol, Sort)] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [(Symbol, Sort)]
xts
Doc -> Doc -> Doc
$+$ (Doc
"." Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p))
toFix (PExist [(Symbol, Sort)]
xts Pred
p) = Doc
"exists" Doc -> Doc -> Doc
<+> ([(Symbol, Sort)] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [(Symbol, Sort)]
xts
Doc -> Doc -> Doc
$+$ (Doc
"." Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p))
toFix (ETApp Pred
e Sort
s) = String -> Doc
text String
"tapp" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s
toFix (ETAbs Pred
e Symbol
s) = String -> Doc
text String
"tabs" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
s
toFix (PGrad KVar
k Subst
_ GradInfo
_ Pred
e) = Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e Doc -> Doc -> Doc
<+> String -> Doc
text String
"&&" Doc -> Doc -> Doc
<+> KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix KVar
k
toFix (ECoerc Sort
a Sort
t Pred
e) = Doc -> Doc
parens (String -> Doc
text String
"coerce" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
a Doc -> Doc -> Doc
<+> String -> Doc
text String
"~" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"in" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e)
toFix (ELam (Symbol
x,Sort
s) Pred
e) = String -> Doc
text String
"lam" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e
simplify :: Pred -> Pred
simplify = ([Pred] -> [Pred]) -> Pred -> Pred
simplifyExpr [Pred] -> [Pred]
forall {a}. Ord a => [a] -> [a]
dedup
where
dedup :: [a] -> [a]
dedup = Set a -> [a]
forall a. Set a -> [a]
Set.toList (Set a -> [a]) -> ([a] -> Set a) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList
simplifyExpr :: ([Expr] -> [Expr]) -> Expr -> Expr
simplifyExpr :: ([Pred] -> [Pred]) -> Pred -> Pred
simplifyExpr [Pred] -> [Pred]
dedup = Pred -> Pred
go
where
go :: Pred -> Pred
go (POr []) = Pred
PFalse
go (POr [Pred
p]) = Pred -> Pred
go Pred
p
go (PNot Pred
p) =
let sp :: Pred
sp = Pred -> Pred
go Pred
p
in case Pred
sp of
PNot Pred
e -> Pred
e
Pred
_ -> Pred -> Pred
PNot Pred
sp
go (PIff Pred
p Pred
q) =
let sp :: Pred
sp = Pred -> Pred
go Pred
p
sq :: Pred
sq = Pred -> Pred
go Pred
q
in if Pred
sp Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
sq then Pred
PTrue
else if Pred
sp Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
PTrue then Pred
sq
else if Pred
sq Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
PTrue then Pred
sp
else if Pred
sp Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
PFalse then Pred -> Pred
PNot Pred
sq
else if Pred
sq Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
PFalse then Pred -> Pred
PNot Pred
sp
else Pred -> Pred -> Pred
PIff Pred
sp Pred
sq
go (PGrad KVar
k Subst
su GradInfo
i Pred
e)
| Pred -> Bool
isContraPred Pred
e = Pred
PFalse
| Bool
otherwise = KVar -> Subst -> GradInfo -> Pred -> Pred
PGrad KVar
k Subst
su GradInfo
i (Pred -> Pred
go Pred
e)
go (PAnd [Pred]
ps)
| (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Pred -> Bool
isContraPred [Pred]
ps = Pred
PFalse
| Bool
otherwise = [Pred] -> Pred
simplPAnd ([Pred] -> Pred) -> ([Pred] -> [Pred]) -> [Pred] -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> [Pred]
dedup ([Pred] -> [Pred]) -> ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> [Pred]
flattenRefas ([Pred] -> [Pred]) -> ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pred -> Bool) -> Pred -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Bool
isTautoPred) ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
go [Pred]
ps
where
simplPAnd :: [Pred] -> Pred
simplPAnd [] = Pred
PTrue
simplPAnd [Pred
p] = Pred
p
simplPAnd [Pred]
xs = [Pred] -> Pred
PAnd [Pred]
xs
go (POr [Pred]
ps)
| (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Pred -> Bool
isTautoPred [Pred]
ps = Pred
PTrue
| Bool
otherwise = [Pred] -> Pred
POr ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Pred -> Bool) -> [Pred] -> [Pred]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pred -> Bool) -> Pred -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pred -> Bool
isContraPred) ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall a b. (a -> b) -> a -> b
$ (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
go [Pred]
ps
go Pred
p
| Pred -> Bool
isContraPred Pred
p = Pred
PFalse
| Pred -> Bool
isTautoPred Pred
p = Pred
PTrue
| Bool
otherwise = Pred
p
isContraPred :: Expr -> Bool
isContraPred :: Pred -> Bool
isContraPred Pred
z = Pred -> Bool
eqC Pred
z Bool -> Bool -> Bool
|| (Pred
z Pred -> [Pred] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pred]
contras)
where
contras :: [Pred]
contras = [Pred
PFalse]
eqC :: Pred -> Bool
eqC (PAtom Brel
Eq (ECon Constant
x) (ECon Constant
y))
= Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
eqC (PAtom Brel
Ueq (ECon Constant
x) (ECon Constant
y))
= Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
eqC (PAtom Brel
Ne Pred
x Pred
y)
= Pred
x Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
y
eqC (PAtom Brel
Une Pred
x Pred
y)
= Pred
x Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
y
eqC Pred
_ = Bool
False
isTautoPred :: Expr -> Bool
isTautoPred :: Pred -> Bool
isTautoPred Pred
z = Pred
z Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
PTop Bool -> Bool -> Bool
|| Pred
z Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
PTrue Bool -> Bool -> Bool
|| Pred -> Bool
eqT Pred
z
where
eqT :: Pred -> Bool
eqT (PAnd [])
= Bool
True
eqT (PAtom Brel
Le Pred
x Pred
y)
= Pred
x Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
y
eqT (PAtom Brel
Ge Pred
x Pred
y)
= Pred
x Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
y
eqT (PAtom Brel
Eq Pred
x Pred
y)
= Pred
x Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
y
eqT (PAtom Brel
Ueq Pred
x Pred
y)
= Pred
x Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Pred
y
eqT (PAtom Brel
Ne (ECon Constant
x) (ECon Constant
y))
= Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
eqT (PAtom Brel
Une (ECon Constant
x) (ECon Constant
y))
= Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
eqT Pred
_ = Bool
False
isEq :: Brel -> Bool
isEq :: Brel -> Bool
isEq Brel
r = Brel
r Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
r Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ueq
instance PPrint Constant where
pprintTidy :: Tidy -> Constant -> Doc
pprintTidy Tidy
_ = Constant -> Doc
forall a. Fixpoint a => a -> Doc
toFix
instance PPrint Brel where
pprintTidy :: Tidy -> Brel -> Doc
pprintTidy Tidy
_ Brel
Eq = Doc
"=="
pprintTidy Tidy
_ Brel
Ne = Doc
"/="
pprintTidy Tidy
_ Brel
r = Brel -> Doc
forall a. Fixpoint a => a -> Doc
toFix Brel
r
instance PPrint Bop where
pprintTidy :: Tidy -> Bop -> Doc
pprintTidy Tidy
_ = Bop -> Doc
forall a. Fixpoint a => a -> Doc
toFix
instance PPrint KVar where
pprintTidy :: Tidy -> KVar -> Doc
pprintTidy Tidy
_ (KV Symbol
x) = String -> Doc
text String
"$" Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
x
instance PPrint SymConst where
pprintTidy :: Tidy -> SymConst -> Doc
pprintTidy Tidy
_ (SL Text
x) = Doc -> Doc
doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
x
parensIf :: Bool -> Doc -> Doc
parensIf :: Bool -> Doc -> Doc
parensIf Bool
True = Doc -> Doc
parens
parensIf Bool
False = Doc -> Doc
forall a. a -> a
id
opPrec :: Bop -> Int
opPrec :: Bop -> Int
opPrec Bop
Mod = Int
5
opPrec Bop
Plus = Int
6
opPrec Bop
Minus = Int
6
opPrec Bop
Times = Int
7
opPrec Bop
RTimes = Int
7
opPrec Bop
Div = Int
7
opPrec Bop
RDiv = Int
7
instance PPrint Expr where
pprintPrec :: Int -> Tidy -> Pred -> Doc
pprintPrec Int
_ Tidy
k (ESym SymConst
c) = Tidy -> SymConst -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k SymConst
c
pprintPrec Int
_ Tidy
k (ECon Constant
c) = Tidy -> Constant -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Constant
c
pprintPrec Int
_ Tidy
k (EVar Symbol
s) = Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s
pprintPrec Int
z Tidy
k (ENeg Pred
e) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
zn) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc
"-" Doc -> Doc -> Doc
<-> Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
zn Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Pred
e
where zn :: a
zn = a
2
pprintPrec Int
z Tidy
k (EApp Pred
f Pred
es) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
za) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
forall {a}. Num a => a
za Tidy
k Pred
f Doc -> Doc -> Doc
<+> Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
zaInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
es
where za :: a
za = a
8
pprintPrec Int
z Tidy
k (EBin Bop
o Pred
e1 Pred
e2) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
zo) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
zoInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
e1 Doc -> Doc -> Doc
<+>
Tidy -> Bop -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Bop
o Doc -> Doc -> Doc
<+>
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
zoInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
e2
where zo :: Int
zo = Bop -> Int
opPrec Bop
o
pprintPrec Int
z Tidy
k (EIte Pred
p Pred
e1 Pred
e2) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
zi) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc
"if" Doc -> Doc -> Doc
<+> Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
p Doc -> Doc -> Doc
<+>
Doc
"then" Doc -> Doc -> Doc
<+> Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
e1 Doc -> Doc -> Doc
<+>
Doc
"else" Doc -> Doc -> Doc
<+> Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
e2
where zi :: a
zi = a
1
pprintPrec Int
_ Tidy
k (ECst Pred
e Sort
so) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Pred -> Doc
forall a. PPrint a => a -> Doc
pprint Pred
e Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Tidy -> Sort -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Sort
so
pprintPrec Int
_ Tidy
_ Pred
PTrue = Doc
trueD
pprintPrec Int
_ Tidy
_ Pred
PFalse = Doc
falseD
pprintPrec Int
z Tidy
k (PNot Pred
p) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
zn) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Doc
"not" Doc -> Doc -> Doc
<+> Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
znInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
p
where zn :: a
zn = a
8
pprintPrec Int
z Tidy
k (PImp Pred
p1 Pred
p2) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
zi) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
p1 Doc -> Doc -> Doc
<+>
Doc
"=>" Doc -> Doc -> Doc
<+>
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
p2
where zi :: a
zi = a
2
pprintPrec Int
z Tidy
k (PIff Pred
p1 Pred
p2) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
zi) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
p1 Doc -> Doc -> Doc
<+>
Doc
"<=>" Doc -> Doc -> Doc
<+>
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
p2
where zi :: a
zi = a
2
pprintPrec Int
z Tidy
k (PAnd [Pred]
ps) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
za) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Doc -> Doc -> [Pred] -> Doc
forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin (Int
forall {a}. Num a => a
za Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Doc
trueD Doc
andD [Pred]
ps
where za :: a
za = a
3
pprintPrec Int
z Tidy
k (POr [Pred]
ps) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
zo) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Doc -> Doc -> [Pred] -> Doc
forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin (Int
forall {a}. Num a => a
zo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Doc
falseD Doc
orD [Pred]
ps
where zo :: a
zo = a
3
pprintPrec Int
z Tidy
k (PAtom Brel
r Pred
e1 Pred
e2) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
za) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
zaInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
e1 Doc -> Doc -> Doc
<+>
Tidy -> Brel -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Brel
r Doc -> Doc -> Doc
<+>
Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall {a}. Num a => a
zaInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Pred
e2
where za :: a
za = a
4
pprintPrec Int
_ Tidy
k (PAll [(Symbol, Sort)]
xts Pred
p) = Tidy -> Doc -> [(Symbol, Sort)] -> Pred -> Doc
pprintQuant Tidy
k Doc
"forall" [(Symbol, Sort)]
xts Pred
p
pprintPrec Int
_ Tidy
k (PExist [(Symbol, Sort)]
xts Pred
p) = Tidy -> Doc -> [(Symbol, Sort)] -> Pred -> Doc
pprintQuant Tidy
k Doc
"exists" [(Symbol, Sort)]
xts Pred
p
pprintPrec Int
_ Tidy
k (ELam (Symbol
x,Sort
t) Pred
e) = Doc
"lam" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> Tidy -> Pred -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Pred
e
pprintPrec Int
_ Tidy
k (ECoerc Sort
a Sort
t Pred
e) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"coerce" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
a Doc -> Doc -> Doc
<+> Doc
"~" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"in" Doc -> Doc -> Doc
<+> Tidy -> Pred -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Pred
e
pprintPrec Int
_ Tidy
_ p :: Pred
p@PKVar{} = Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
p
pprintPrec Int
_ Tidy
_ (ETApp Pred
e Sort
s) = Doc
"ETApp" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s
pprintPrec Int
_ Tidy
_ (ETAbs Pred
e Symbol
s) = Doc
"ETAbs" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. Fixpoint a => a -> Doc
toFix Pred
e Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
s
pprintPrec Int
z Tidy
k (PGrad KVar
x Subst
_ GradInfo
_ Pred
e) = Int -> Tidy -> Pred -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k Pred
e Doc -> Doc -> Doc
<+> Doc
"&&" Doc -> Doc -> Doc
<+> KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix KVar
x
pprintQuant :: Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc
pprintQuant :: Tidy -> Doc -> [(Symbol, Sort)] -> Pred -> Doc
pprintQuant Tidy
k Doc
d [(Symbol, Sort)]
xts Pred
p = (Doc
d Doc -> Doc -> Doc
<+> [(Symbol, Sort)] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [(Symbol, Sort)]
xts)
Doc -> Doc -> Doc
$+$
(Doc
" ." Doc -> Doc -> Doc
<+> Tidy -> Pred -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Pred
p)
trueD, falseD, andD, orD :: Doc
trueD :: Doc
trueD = Doc
"true"
falseD :: Doc
falseD = Doc
"false"
andD :: Doc
andD = Doc
"&&"
orD :: Doc
orD = Doc
"||"
pprintBin :: (PPrint a) => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin :: forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin Int
_ Tidy
_ Doc
b Doc
_ [] = Doc
b
pprintBin Int
z Tidy
k Doc
_ Doc
o [a]
xs = Doc -> [Doc] -> Doc
vIntersperse Doc
o ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Tidy -> a -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs
vIntersperse :: Doc -> [Doc] -> Doc
vIntersperse :: Doc -> [Doc] -> Doc
vIntersperse Doc
_ [] = Doc
empty
vIntersperse Doc
_ [Doc
d] = Doc
d
vIntersperse Doc
s (Doc
d:[Doc]
ds) = [Doc] -> Doc
vcat (Doc
d Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Doc
s Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> [Doc] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
ds))
pprintReft :: Tidy -> Reft -> Doc
pprintReft :: Tidy -> Reft -> Doc
pprintReft Tidy
k (Reft (Symbol
_,Pred
ra)) = Int -> Tidy -> Doc -> Doc -> [Pred] -> Doc
forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin Int
z Tidy
k Doc
trueD Doc
andD [Pred]
flat
where
flat :: [Pred]
flat = [Pred] -> [Pred]
flattenRefas [Pred
ra]
z :: Int
z = if [Pred] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pred]
flat Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 then Int
3 else Int
0
class Expression a where
expr :: a -> Expr
class Predicate a where
prop :: a -> Expr
instance Expression SortedReft where
expr :: SortedReft -> Pred
expr (RR Sort
_ Reft
r) = Reft -> Pred
forall a. Expression a => a -> Pred
expr Reft
r
instance Expression Reft where
expr :: Reft -> Pred
expr (Reft(Symbol
_, Pred
e)) = Pred
e
instance Expression Expr where
expr :: Pred -> Pred
expr = Pred -> Pred
forall a. a -> a
id
instance Expression Symbol where
expr :: Symbol -> Pred
expr Symbol
s = Symbol -> Pred
forall a. Symbolic a => a -> Pred
eVar Symbol
s
instance Expression Text where
expr :: Text -> Pred
expr = SymConst -> Pred
ESym (SymConst -> Pred) -> (Text -> SymConst) -> Text -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SymConst
SL
instance Expression Integer where
expr :: Integer -> Pred
expr = Constant -> Pred
ECon (Constant -> Pred) -> (Integer -> Constant) -> Integer -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Constant
I
instance Expression Int where
expr :: Int -> Pred
expr = Integer -> Pred
forall a. Expression a => a -> Pred
expr (Integer -> Pred) -> (Int -> Integer) -> Int -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
instance Predicate Symbol where
prop :: Symbol -> Pred
prop = Symbol -> Pred
forall a. Symbolic a => a -> Pred
eProp
instance Predicate Expr where
prop :: Pred -> Pred
prop = Pred -> Pred
forall a. a -> a
id
instance Predicate Bool where
prop :: Bool -> Pred
prop Bool
True = Pred
PTrue
prop Bool
False = Pred
PFalse
instance Expression a => Expression (Located a) where
expr :: Located a -> Pred
expr = a -> Pred
forall a. Expression a => a -> Pred
expr (a -> Pred) -> (Located a -> a) -> Located a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val
eVar :: Symbolic a => a -> Expr
eVar :: forall a. Symbolic a => a -> Pred
eVar = Symbol -> Pred
EVar (Symbol -> Pred) -> (a -> Symbol) -> a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol
eProp :: Symbolic a => a -> Expr
eProp :: forall a. Symbolic a => a -> Pred
eProp = Pred -> Pred
mkProp (Pred -> Pred) -> (a -> Pred) -> a -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Pred
forall a. Symbolic a => a -> Pred
eVar
isSingletonExpr :: Symbol -> Expr -> Maybe Expr
isSingletonExpr :: Symbol -> Pred -> Maybe Pred
isSingletonExpr Symbol
v (PAtom Brel
r Pred
e1 Pred
e2)
| Pred
e1 Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Pred
EVar Symbol
v Bool -> Bool -> Bool
&& Brel -> Bool
isEq Brel
r = Pred -> Maybe Pred
forall a. a -> Maybe a
Just Pred
e2
| Pred
e2 Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Pred
EVar Symbol
v Bool -> Bool -> Bool
&& Brel -> Bool
isEq Brel
r = Pred -> Maybe Pred
forall a. a -> Maybe a
Just Pred
e1
isSingletonExpr Symbol
v (PIff Pred
e1 Pred
e2)
| Pred
e1 Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Pred
EVar Symbol
v = Pred -> Maybe Pred
forall a. a -> Maybe a
Just Pred
e2
| Pred
e2 Pred -> Pred -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Pred
EVar Symbol
v = Pred -> Maybe Pred
forall a. a -> Maybe a
Just Pred
e1
isSingletonExpr Symbol
_ Pred
_ = Maybe Pred
forall a. Maybe a
Nothing
conj :: [Pred] -> Pred
conj :: [Pred] -> Pred
conj [] = Pred
PFalse
conj [Pred
p] = Pred
p
conj [Pred]
ps = [Pred] -> Pred
PAnd [Pred]
ps
pAnd, pOr :: ListNE Pred -> Pred
pAnd :: [Pred] -> Pred
pAnd = Pred -> Pred
forall a. Fixpoint a => a -> a
simplify (Pred -> Pred) -> ([Pred] -> Pred) -> [Pred] -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> Pred
PAnd
pAndNoDedup :: ListNE Pred -> Pred
pAndNoDedup :: [Pred] -> Pred
pAndNoDedup = ([Pred] -> [Pred]) -> Pred -> Pred
simplifyExpr [Pred] -> [Pred]
forall a. a -> a
id (Pred -> Pred) -> ([Pred] -> Pred) -> [Pred] -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> Pred
PAnd
pOr :: [Pred] -> Pred
pOr = Pred -> Pred
forall a. Fixpoint a => a -> a
simplify (Pred -> Pred) -> ([Pred] -> Pred) -> [Pred] -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> Pred
POr
infixl 9 &.&
(&.&) :: Pred -> Pred -> Pred
&.& :: Pred -> Pred -> Pred
(&.&) Pred
p Pred
q = [Pred] -> Pred
pAnd [Pred
p, Pred
q]
infixl 9 |.|
(|.|) :: Pred -> Pred -> Pred
|.| :: Pred -> Pred -> Pred
(|.|) Pred
p Pred
q = [Pred] -> Pred
pOr [Pred
p, Pred
q]
pIte :: Pred -> Expr -> Expr -> Expr
pIte :: Pred -> Pred -> Pred -> Pred
pIte Pred
p1 Pred
p2 Pred
p3 = [Pred] -> Pred
pAnd [Pred
p1 Pred -> Pred -> Pred
`PImp` Pred
p2, Pred -> Pred
PNot Pred
p1 Pred -> Pred -> Pred
`PImp` Pred
p3]
pExist :: [(Symbol, Sort)] -> Pred -> Pred
pExist :: [(Symbol, Sort)] -> Pred -> Pred
pExist [] Pred
p = Pred
p
pExist [(Symbol, Sort)]
xts Pred
p = [(Symbol, Sort)] -> Pred -> Pred
PExist [(Symbol, Sort)]
xts Pred
p
mkProp :: Expr -> Pred
mkProp :: Pred -> Pred
mkProp = Pred -> Pred
forall a. a -> a
id
isSingletonReft :: Reft -> Maybe Expr
isSingletonReft :: Reft -> Maybe Pred
isSingletonReft (Reft (Symbol
v, Pred
ra)) = (Pred -> Maybe Pred) -> [Pred] -> Maybe Pred
forall a b. (a -> Maybe b) -> [a] -> Maybe b
firstMaybe (Symbol -> Pred -> Maybe Pred
isSingletonExpr Symbol
v) ([Pred] -> Maybe Pred) -> [Pred] -> Maybe Pred
forall a b. (a -> b) -> a -> b
$ Pred -> [Pred]
conjuncts Pred
ra
relReft :: (Expression a) => Brel -> a -> Reft
relReft :: forall a. Expression a => Brel -> a -> Reft
relReft Brel
r a
e = (Symbol, Pred) -> Reft
Reft (Symbol
vv_, Brel -> Pred -> Pred -> Pred
PAtom Brel
r (Symbol -> Pred
forall a. Symbolic a => a -> Pred
eVar Symbol
vv_) (a -> Pred
forall a. Expression a => a -> Pred
expr a
e))
exprReft, notExprReft, uexprReft :: (Expression a) => a -> Reft
exprReft :: forall a. Expression a => a -> Reft
exprReft = Brel -> a -> Reft
forall a. Expression a => Brel -> a -> Reft
relReft Brel
Eq
notExprReft :: forall a. Expression a => a -> Reft
notExprReft = Brel -> a -> Reft
forall a. Expression a => Brel -> a -> Reft
relReft Brel
Ne
uexprReft :: forall a. Expression a => a -> Reft
uexprReft = Brel -> a -> Reft
forall a. Expression a => Brel -> a -> Reft
relReft Brel
Ueq
propReft :: (Predicate a) => a -> Reft
propReft :: forall a. Predicate a => a -> Reft
propReft a
p = (Symbol, Pred) -> Reft
Reft (Symbol
vv_, Pred -> Pred -> Pred
PIff (Symbol -> Pred
forall a. Symbolic a => a -> Pred
eProp Symbol
vv_) (a -> Pred
forall a. Predicate a => a -> Pred
prop a
p))
predReft :: (Predicate a) => a -> Reft
predReft :: forall a. Predicate a => a -> Reft
predReft a
p = (Symbol, Pred) -> Reft
Reft (Symbol
vv_, a -> Pred
forall a. Predicate a => a -> Pred
prop a
p)
reft :: Symbol -> Expr -> Reft
reft :: Symbol -> Pred -> Reft
reft Symbol
v Pred
p = (Symbol, Pred) -> Reft
Reft (Symbol
v, Pred
p)
mapPredReft :: (Expr -> Expr) -> Reft -> Reft
mapPredReft :: (Pred -> Pred) -> Reft -> Reft
mapPredReft Pred -> Pred
f (Reft (Symbol
v, Pred
p)) = (Symbol, Pred) -> Reft
Reft (Symbol
v, Pred -> Pred
f Pred
p)
isFunctionSortedReft :: SortedReft -> Bool
isFunctionSortedReft :: SortedReft -> Bool
isFunctionSortedReft = Maybe ([Int], [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ([Int], [Sort], Sort) -> Bool)
-> (SortedReft -> Maybe ([Int], [Sort], Sort))
-> SortedReft
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe ([Int], [Sort], Sort)
functionSort (Sort -> Maybe ([Int], [Sort], Sort))
-> (SortedReft -> Sort)
-> SortedReft
-> Maybe ([Int], [Sort], Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Sort
sr_sort
isNonTrivial :: Reftable r => r -> Bool
isNonTrivial :: forall r. Reftable r => r -> Bool
isNonTrivial = Bool -> Bool
not (Bool -> Bool) -> (r -> Bool) -> r -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> Bool
forall r. Reftable r => r -> Bool
isTauto
reftPred :: Reft -> Expr
reftPred :: Reft -> Pred
reftPred (Reft (Symbol
_, Pred
p)) = Pred
p
reftBind :: Reft -> Symbol
reftBind :: Reft -> Symbol
reftBind (Reft (Symbol
x, Pred
_)) = Symbol
x
pGAnds :: [Expr] -> Expr
pGAnds :: [Pred] -> Pred
pGAnds = (Pred -> Pred -> Pred) -> Pred -> [Pred] -> Pred
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Pred -> Pred -> Pred
pGAnd Pred
PTrue
pGAnd :: Expr -> Expr -> Expr
pGAnd :: Pred -> Pred -> Pred
pGAnd (PGrad KVar
k Subst
su GradInfo
i Pred
p) Pred
q = KVar -> Subst -> GradInfo -> Pred -> Pred
PGrad KVar
k Subst
su GradInfo
i ([Pred] -> Pred
pAnd [Pred
p, Pred
q])
pGAnd Pred
p (PGrad KVar
k Subst
su GradInfo
i Pred
q) = KVar -> Subst -> GradInfo -> Pred -> Pred
PGrad KVar
k Subst
su GradInfo
i ([Pred] -> Pred
pAnd [Pred
p, Pred
q])
pGAnd Pred
p Pred
q = [Pred] -> Pred
pAnd [Pred
p,Pred
q]
symbolReft :: (Symbolic a) => a -> Reft
symbolReft :: forall a. Symbolic a => a -> Reft
symbolReft = Pred -> Reft
forall a. Expression a => a -> Reft
exprReft (Pred -> Reft) -> (a -> Pred) -> a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Pred
forall a. Symbolic a => a -> Pred
eVar
usymbolReft :: (Symbolic a) => a -> Reft
usymbolReft :: forall a. Symbolic a => a -> Reft
usymbolReft = Pred -> Reft
forall a. Expression a => a -> Reft
uexprReft (Pred -> Reft) -> (a -> Pred) -> a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Pred
forall a. Symbolic a => a -> Pred
eVar
vv_ :: Symbol
vv_ :: Symbol
vv_ = Maybe Integer -> Symbol
vv Maybe Integer
forall a. Maybe a
Nothing
trueSortedReft :: Sort -> SortedReft
trueSortedReft :: Sort -> SortedReft
trueSortedReft = (Sort -> Reft -> SortedReft
`RR` Reft
trueReft)
trueReft, falseReft :: Reft
trueReft :: Reft
trueReft = (Symbol, Pred) -> Reft
Reft (Symbol
vv_, Pred
PTrue)
falseReft :: Reft
falseReft = (Symbol, Pred) -> Reft
Reft (Symbol
vv_, Pred
PFalse)
flattenRefas :: [Expr] -> [Expr]
flattenRefas :: [Pred] -> [Pred]
flattenRefas = [Pred] -> [Pred] -> [Pred]
flatP []
where
flatP :: [Pred] -> [Pred] -> [Pred]
flatP [Pred]
acc (PAnd [Pred]
ps:[Pred]
xs) = [Pred] -> [Pred] -> [Pred]
flatP ([Pred] -> [Pred] -> [Pred]
flatP [Pred]
acc [Pred]
xs) [Pred]
ps
flatP [Pred]
acc (Pred
p:[Pred]
xs) = Pred
p Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred] -> [Pred] -> [Pred]
flatP [Pred]
acc [Pred]
xs
flatP [Pred]
acc [] = [Pred]
acc
conjuncts :: Expr -> [Expr]
conjuncts :: Pred -> [Pred]
conjuncts (PAnd [Pred]
ps) = (Pred -> [Pred]) -> [Pred] -> [Pred]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [Pred]
conjuncts [Pred]
ps
conjuncts Pred
p
| Pred -> Bool
isTautoPred Pred
p = []
| Bool
otherwise = [Pred
p]
class Falseable a where
isFalse :: a -> Bool
instance Falseable Expr where
isFalse :: Pred -> Bool
isFalse Pred
PFalse = Bool
True
isFalse Pred
_ = Bool
False
instance Falseable Reft where
isFalse :: Reft -> Bool
isFalse (Reft (Symbol
_, Pred
ra)) = Pred -> Bool
forall a. Falseable a => a -> Bool
isFalse Pred
ra
class Subable a where
syms :: a -> [Symbol]
substa :: (Symbol -> Symbol) -> a -> a
substf :: (Symbol -> Expr) -> a -> a
subst :: Subst -> a -> a
subst1 :: a -> (Symbol, Expr) -> a
subst1 a
y (Symbol
x, Pred
e) = Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst (HashMap Symbol Pred -> Subst
Su (HashMap Symbol Pred -> Subst) -> HashMap Symbol Pred -> Subst
forall a b. (a -> b) -> a -> b
$ [(Symbol, Pred)] -> HashMap Symbol Pred
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol
x,Pred
e)]) a
y
instance Subable a => Subable (Located a) where
syms :: Located a -> [Symbol]
syms (Loc SourcePos
_ SourcePos
_ a
x) = a -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms a
x
substa :: (Symbol -> Symbol) -> Located a -> Located a
substa Symbol -> Symbol
f (Loc SourcePos
l SourcePos
l' a
x) = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' ((Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f a
x)
substf :: (Symbol -> Pred) -> Located a -> Located a
substf Symbol -> Pred
f (Loc SourcePos
l SourcePos
l' a
x) = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' ((Symbol -> Pred) -> a -> a
forall a. Subable a => (Symbol -> Pred) -> a -> a
substf Symbol -> Pred
f a
x)
subst :: Subst -> Located a -> Located a
subst Subst
su (Loc SourcePos
l SourcePos
l' a
x) = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst Subst
su a
x)
class (Monoid r, Subable r) => Reftable r where
isTauto :: r -> Bool
ppTy :: r -> Doc -> Doc
top :: r -> r
top r
_ = r
forall a. Monoid a => a
mempty
bot :: r -> r
meet :: r -> r -> r
meet = r -> r -> r
forall a. Monoid a => a -> a -> a
mappend
toReft :: r -> Reft
ofReft :: Reft -> r
params :: r -> [Symbol]
instance Fixpoint Doc where
toFix :: Doc -> Doc
toFix = Doc -> Doc
forall a. a -> a
id