{-# 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            #-}

-- | This module has the types for representing terms in the refinement logic.

module Language.Fixpoint.Types.Refinements (

  -- * Representing Terms
    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 (..)

  -- * Constructing Terms
  , eVar, elit
  , eProp
  , conj, pAnd, pOr, pIte, pAndNoDedup
  , (&.&), (|.|)
  , pExist
  , mkEApp
  , mkProp
  , intKvar
  , vv_

  -- * Generalizing Embedding with Typeclasses
  , Expression (..)
  , Predicate (..)
  , Subable (..)
  , Reftable (..)

  -- * Constructors
  , reft                    -- "smart
  , trueSortedReft          -- trivial reft
  , trueReft, falseReft     -- trivial reft
  , exprReft                -- singleton: v == e
  , notExprReft             -- singleton: v /= e
  , uexprReft               -- singleton: v ~~ e
  , symbolReft              -- singleton: v == x
  , usymbolReft             -- singleton: v ~~ x
  , propReft                -- singleton: v <=> p
  , predReft                -- any pred : p
  , reftPred
  , reftBind

  -- * Predicates
  , isFunctionSortedReft, functionSort
  , isNonTrivial
  , isContraPred
  , isTautoPred
  , isSingletonExpr
  , isSingletonReft
  , isFalse

  -- * Destructing
  , flattenRefas
  , conjuncts, concConjuncts
  , dropECst
  , eApps
  , eAppC
  , eCst
  , exprKVars
  , exprSymbolsSet
  , splitEApp
  , splitEAppThroughECst
  , splitPAnd
  , reftConjuncts
  , sortedReftSymbols
  , substSortInExpr

  -- * Transforming
  , mapPredReft
  , onEverySubexpr
  , pprintReft

  , debruijnIndex

  -- * Gradual Type Manipulation
  , 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

-- import           Text.Printf               (printf)


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 (Hashable k, Eq k, S.Store k, S.Store v) => S.Store (M.HashMap k v) where
  -- put = B.put . M.toList
  -- get = M.fromList <$> B.get

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  -- see [NOTE:pAnd-SLOW]
    ([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']



--------------------------------------------------------------------------------
-- | Kvars ---------------------------------------------------------------------
--------------------------------------------------------------------------------

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

--------------------------------------------------------------------------------
-- | Substitutions -------------------------------------------------------------
--------------------------------------------------------------------------------
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)

--------------------------------------------------------------------------------
-- | Expressions ---------------------------------------------------------------
--------------------------------------------------------------------------------

-- | Uninterpreted constants that are embedded as  "constant symbol : Str"

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)
            -- NOTE: For "Mod" 2nd expr should be a constant or a var *)

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

-- | Like 'Data.Generics.everywhere' but only traverses the nodes
-- of type @a@ or @[a]@.
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

-- | Eliminates redundant casts
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

-- | Parsed refinement of @Symbol@ as @Expr@
--   e.g. in '{v: _ | e }' v is the @Symbol@ and e the @Expr@
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

--------------------------------------------------------------------------------
-- | String Constants ----------------------------------------------------------
--------------------------------------------------------------------------------

-- | Replace all symbol-representations-of-string-literals with string-literal
--   Used to transform parsed output from fixpoint back into fq.

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

-- _decodeSymConst :: Symbol -> Maybe SymConst
-- _decodeSymConst = fmap (SL . symbolText) . unLitSymbol

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 e _so)   = toFix e
  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 (EBot)         = text "_|_"
  -- toFix PTop           = text "???"
  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 -- text "??" -- <+> toFix k <+> toFix su
  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
    -- XXX: Do not simplify PImp until PLE can handle it
    -- https://github.com/ucsd-progsys/liquid-fixpoint/issues/475
    -- go (PImp p q) =
    --   let sq = go q
    --    in if sq == PTrue then PTrue
    --       else if sq == PFalse then go (PNot p)
    --       else PImp (go p) sq
    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
                           -- Note: Performance of some tests is very sensitive to this code. See #480
      | 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

-- | Wrap the enclosed 'Doc' in parentheses only if the condition holds.
parensIf :: Bool -> Doc -> Doc
parensIf :: Bool -> Doc -> Doc
parensIf Bool
True  = Doc -> Doc
parens
parensIf Bool
False = Doc -> Doc
forall a. a -> a
id

-- NOTE: The following Expr and Pred printers use pprintPrec to print
-- expressions with minimal parenthesization. The precedence rules are somewhat
-- fragile, and it would be nice to have them directly tied to the parser, but
-- the general idea is (from lowest to highest precedence):
--
-- 1 - if-then-else
-- 2 - => and <=>
-- 3 - && and ||
-- 4 - ==, !=, <, <=, >, >=
-- 5 - mod
-- 6 - + and -
-- 7 - * and /
-- 8 - function application
--
-- Each printer `p` checks whether the precedence of the context is greater than
-- its own precedence. If so, the printer wraps itself in parentheses. Then it
-- sets the contextual precedence for recursive printer invocations to
-- (prec p + 1).

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 _ (EBot)          = text "_|_"
  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

  -- RJ: DO NOT DELETE!
  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
<+> {- const (text "...") -} Tidy -> Sort -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Sort
so
  -- pprintPrec z k (ECst e _)      = pprintPrec z k e
  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

------------------------------------------------------------------------
-- | Generalizing Symbol, Expression, Predicate into Classes -----------
------------------------------------------------------------------------

-- | Values that can be viewed as Constants

-- | Values that can be viewed as Expressions

class Expression a where
  expr   :: a -> Expr

-- | Values that can be viewed as Predicates

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

-- | The symbol may be an encoding of a SymConst.

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' is a fast version of 'pAnd' needed for the ebind tests
conj :: [Pred] -> Pred
conj :: [Pred] -> Pred
conj []  = Pred
PFalse
conj [Pred
p] = Pred
p
conj [Pred]
ps  = [Pred] -> Pred
PAnd [Pred]
ps

-- | [NOTE: pAnd-SLOW] 'pAnd' and 'pOr' are super slow as they go inside the predicates;
--   so they SHOULD NOT be used inside the solver loop. Instead, use 'conj' which ensures
--   some basic things but is faster.

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 -- EApp (EVar propConName)

--------------------------------------------------------------------------------
-- | Predicates ----------------------------------------------------------------
--------------------------------------------------------------------------------

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)

---------------------------------------------------------------
-- | Refinements ----------------------------------------------
---------------------------------------------------------------

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

------------------------------------------------------------
-- | Gradual Type Manipulation  ----------------------------
------------------------------------------------------------
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]

------------------------------------------------------------
-- | Generally Useful Refinements --------------------------
------------------------------------------------------------

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]


-------------------------------------------------------------------------
-- | TODO: This doesn't seem to merit a TC ------------------------------
-------------------------------------------------------------------------

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 Predicates for Valid Refinements -----------------------------
-------------------------------------------------------------------------

class Subable a where
  syms   :: a -> [Symbol]                   -- ^ free symbols of a
  substa :: (Symbol -> Symbol) -> a -> a
  -- substa f  = substf (EVar . f)

  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]          -- ^ parameters for Reft, vv + others

instance Fixpoint Doc where
  toFix :: Doc -> Doc
toFix = Doc -> Doc
forall a. a -> a
id