{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# 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 (..)
  , ExprV (..), Pred
  , Expr
  , GradInfo (..)
  , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot
  , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv
  , pattern EEq
  , KVar (..)
  , Subst
  , SubstV (..)
  , KVSub (..)
  , Reft
  , ReftV (..)
  , SortedReft (..)

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

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

  -- * 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
  , isTautoReft
  , isSingletonExpr
  , isSingletonReft
  , isFalse

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

  -- * 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)
#if MIN_VERSION_base(4,20,0)
import           Data.List                 (partition)
#else
import           Data.List                 (foldl', partition)
#endif
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           Data.Aeson

-- import           Text.Printf               (printf)


instance NFData KVar
instance NFData v => NFData (SubstV v)
instance NFData GradInfo
instance NFData Constant
instance NFData SymConst
instance NFData Brel
instance NFData Bop
instance NFData v => NFData (ExprV v)
instance NFData v => NFData (ReftV v)
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 v => B.Binary (SubstV v)
instance B.Binary v => B.Binary (ExprV v)
instance B.Binary v => B.Binary (ReftV v)


reftConjuncts :: Reft -> [Reft]
reftConjuncts :: Reft -> [Reft]
reftConjuncts (Reft (Symbol
v, ExprV Symbol
ra)) = [(Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, ExprV Symbol
ra') | ExprV Symbol
ra' <- [ExprV Symbol]
ras']
  where
    ras' :: [ExprV Symbol]
ras'                     = if [ExprV Symbol] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ExprV Symbol]
ps then [ExprV Symbol]
ks else [ExprV Symbol] -> ExprV Symbol
conj [ExprV Symbol]
ps ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
: [ExprV Symbol]
ks  -- see [NOTE:pAnd-SLOW]
    ([ExprV Symbol]
ps, [ExprV Symbol]
ks)                 = (ExprV Symbol -> Bool)
-> [ExprV Symbol] -> ([ExprV Symbol], [ExprV Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ExprV Symbol -> Bool
isConc (ExprV Symbol -> [ExprV Symbol]
refaConjuncts ExprV Symbol
ra)

isConc :: Expr -> Bool
isConc :: ExprV Symbol -> Bool
isConc ExprV Symbol
p = Bool -> Bool
not (ExprV Symbol -> Bool
isKvar ExprV Symbol
p Bool -> Bool -> Bool
|| ExprV Symbol -> Bool
forall a. HasGradual a => a -> Bool
isGradual ExprV Symbol
p)

concConjuncts :: Expr -> [Expr]
concConjuncts :: ExprV Symbol -> [ExprV Symbol]
concConjuncts ExprV Symbol
e = (ExprV Symbol -> Bool) -> [ExprV Symbol] -> [ExprV Symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter ExprV Symbol -> Bool
isConc (ExprV Symbol -> [ExprV Symbol]
refaConjuncts ExprV Symbol
e)

isKvar :: Expr -> Bool
isKvar :: ExprV Symbol -> Bool
isKvar (PKVar KVar
_ Subst
_) = Bool
True
isKvar ExprV Symbol
_           = 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 :: ExprV Symbol -> Bool
isGradual PGrad{} = Bool
True
  isGradual (PAnd [ExprV Symbol]
xs)  = (ExprV Symbol -> Bool) -> [ExprV Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ExprV Symbol -> Bool
forall a. HasGradual a => a -> Bool
isGradual [ExprV Symbol]
xs
  isGradual ExprV Symbol
_          = Bool
False

  gVars :: ExprV Symbol -> [KVar]
gVars (PGrad KVar
k Subst
_ GradInfo
_ ExprV Symbol
_) = [KVar
k]
  gVars (PAnd [ExprV Symbol]
xs)       = (ExprV Symbol -> [KVar]) -> [ExprV Symbol] -> [KVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV Symbol -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars [ExprV Symbol]
xs
  gVars ExprV Symbol
_               = []

  ungrad :: ExprV Symbol -> ExprV Symbol
ungrad PGrad{} = ExprV Symbol
forall v. ExprV v
PTrue
  ungrad (PAnd [ExprV Symbol]
xs)  = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd (ExprV Symbol -> ExprV Symbol
forall a. HasGradual a => a -> a
ungrad (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
xs )
  ungrad ExprV Symbol
e          = ExprV Symbol
e


instance HasGradual Reft where
  isGradual :: Reft -> Bool
isGradual (Reft (Symbol
_,ExprV Symbol
r)) = ExprV Symbol -> Bool
forall a. HasGradual a => a -> Bool
isGradual ExprV Symbol
r
  gVars :: Reft -> [KVar]
gVars (Reft (Symbol
_,ExprV Symbol
r))     = ExprV Symbol -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars ExprV Symbol
r
  ungrad :: Reft -> Reft
ungrad (Reft (Symbol
x,ExprV Symbol
r))    = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft(Symbol
x, ExprV Symbol -> ExprV Symbol
forall a. HasGradual a => a -> a
ungrad ExprV Symbol
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 :: ExprV Symbol -> [ExprV Symbol]
refaConjuncts ExprV Symbol
p = [ExprV Symbol
p' | ExprV Symbol
p' <- ExprV Symbol -> [ExprV Symbol]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts ExprV Symbol
p, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV Symbol
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, [KVar] -> Value
[KVar] -> Encoding
KVar -> Bool
KVar -> Value
KVar -> Encoding
(KVar -> Value)
-> (KVar -> Encoding)
-> ([KVar] -> Value)
-> ([KVar] -> Encoding)
-> (KVar -> Bool)
-> ToJSON KVar
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: KVar -> Value
toJSON :: KVar -> Value
$ctoEncoding :: KVar -> Encoding
toEncoding :: KVar -> Encoding
$ctoJSONList :: [KVar] -> Value
toJSONList :: [KVar] -> Value
$ctoEncodingList :: [KVar] -> Encoding
toEncodingList :: [KVar] -> Encoding
$comitField :: KVar -> Bool
omitField :: KVar -> Bool
ToJSON, Maybe KVar
Value -> Parser [KVar]
Value -> Parser KVar
(Value -> Parser KVar)
-> (Value -> Parser [KVar]) -> Maybe KVar -> FromJSON KVar
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser KVar
parseJSON :: Value -> Parser KVar
$cparseJSONList :: Value -> Parser [KVar]
parseJSONList :: Value -> Parser [KVar]
$comittedField :: Maybe KVar
omittedField :: Maybe KVar
FromJSON)

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 v => Hashable (SubstV v)
instance Hashable v => Hashable (ExprV v)
instance Hashable v => Hashable (ReftV v)

--------------------------------------------------------------------------------
-- | Substitutions -------------------------------------------------------------
--------------------------------------------------------------------------------
type Subst = SubstV Symbol
newtype SubstV v = Su (M.HashMap Symbol (ExprV v))
                deriving (SubstV v -> SubstV v -> Bool
(SubstV v -> SubstV v -> Bool)
-> (SubstV v -> SubstV v -> Bool) -> Eq (SubstV v)
forall v. Eq v => SubstV v -> SubstV v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => SubstV v -> SubstV v -> Bool
== :: SubstV v -> SubstV v -> Bool
$c/= :: forall v. Eq v => SubstV v -> SubstV v -> Bool
/= :: SubstV v -> SubstV v -> Bool
Eq, Typeable (SubstV v)
Typeable (SubstV v) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> SubstV v -> c (SubstV v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (SubstV v))
-> (SubstV v -> Constr)
-> (SubstV v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (SubstV v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (SubstV v)))
-> ((forall b. Data b => b -> b) -> SubstV v -> SubstV v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SubstV v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SubstV v -> r)
-> (forall u. (forall d. Data d => d -> u) -> SubstV v -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SubstV v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v))
-> Data (SubstV v)
SubstV v -> Constr
SubstV v -> DataType
(forall b. Data b => b -> b) -> SubstV v -> SubstV v
forall v. Data v => Typeable (SubstV v)
forall v. Data v => SubstV v -> Constr
forall v. Data v => SubstV v -> DataType
forall v.
Data v =>
(forall b. Data b => b -> b) -> SubstV v -> SubstV v
forall v u.
Data v =>
Int -> (forall d. Data d => d -> u) -> SubstV v -> u
forall v u.
Data v =>
(forall d. Data d => d -> u) -> SubstV v -> [u]
forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SubstV v)
forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SubstV v -> c (SubstV v)
forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SubstV v))
forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SubstV v))
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) -> SubstV v -> u
forall u. (forall d. Data d => d -> u) -> SubstV v -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SubstV v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SubstV v -> c (SubstV v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SubstV v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SubstV v))
$cgfoldl :: forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SubstV v -> c (SubstV v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SubstV v -> c (SubstV v)
$cgunfold :: forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SubstV v)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SubstV v)
$ctoConstr :: forall v. Data v => SubstV v -> Constr
toConstr :: SubstV v -> Constr
$cdataTypeOf :: forall v. Data v => SubstV v -> DataType
dataTypeOf :: SubstV v -> DataType
$cdataCast1 :: forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SubstV v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SubstV v))
$cdataCast2 :: forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SubstV v))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SubstV v))
$cgmapT :: forall v.
Data v =>
(forall b. Data b => b -> b) -> SubstV v -> SubstV v
gmapT :: (forall b. Data b => b -> b) -> SubstV v -> SubstV v
$cgmapQl :: forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
$cgmapQr :: forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SubstV v -> r
$cgmapQ :: forall v u.
Data v =>
(forall d. Data d => d -> u) -> SubstV v -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> SubstV v -> [u]
$cgmapQi :: forall v u.
Data v =>
Int -> (forall d. Data d => d -> u) -> SubstV v -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SubstV v -> u
$cgmapM :: forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
$cgmapMp :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
$cgmapMo :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SubstV v -> m (SubstV v)
Data, Eq (SubstV v)
Eq (SubstV v) =>
(SubstV v -> SubstV v -> Ordering)
-> (SubstV v -> SubstV v -> Bool)
-> (SubstV v -> SubstV v -> Bool)
-> (SubstV v -> SubstV v -> Bool)
-> (SubstV v -> SubstV v -> Bool)
-> (SubstV v -> SubstV v -> SubstV v)
-> (SubstV v -> SubstV v -> SubstV v)
-> Ord (SubstV v)
SubstV v -> SubstV v -> Bool
SubstV v -> SubstV v -> Ordering
SubstV v -> SubstV v -> SubstV v
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
forall v. Ord v => Eq (SubstV v)
forall v. Ord v => SubstV v -> SubstV v -> Bool
forall v. Ord v => SubstV v -> SubstV v -> Ordering
forall v. Ord v => SubstV v -> SubstV v -> SubstV v
$ccompare :: forall v. Ord v => SubstV v -> SubstV v -> Ordering
compare :: SubstV v -> SubstV v -> Ordering
$c< :: forall v. Ord v => SubstV v -> SubstV v -> Bool
< :: SubstV v -> SubstV v -> Bool
$c<= :: forall v. Ord v => SubstV v -> SubstV v -> Bool
<= :: SubstV v -> SubstV v -> Bool
$c> :: forall v. Ord v => SubstV v -> SubstV v -> Bool
> :: SubstV v -> SubstV v -> Bool
$c>= :: forall v. Ord v => SubstV v -> SubstV v -> Bool
>= :: SubstV v -> SubstV v -> Bool
$cmax :: forall v. Ord v => SubstV v -> SubstV v -> SubstV v
max :: SubstV v -> SubstV v -> SubstV v
$cmin :: forall v. Ord v => SubstV v -> SubstV v -> SubstV v
min :: SubstV v -> SubstV v -> SubstV v
Ord, Typeable, (forall x. SubstV v -> Rep (SubstV v) x)
-> (forall x. Rep (SubstV v) x -> SubstV v) -> Generic (SubstV v)
forall x. Rep (SubstV v) x -> SubstV v
forall x. SubstV v -> Rep (SubstV v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x. Rep (SubstV v) x -> SubstV v
forall v x. SubstV v -> Rep (SubstV v) x
$cfrom :: forall v x. SubstV v -> Rep (SubstV v) x
from :: forall x. SubstV v -> Rep (SubstV v) x
$cto :: forall v x. Rep (SubstV v) x -> SubstV v
to :: forall x. Rep (SubstV v) x -> SubstV v
Generic, (forall a b. (a -> b) -> SubstV a -> SubstV b)
-> (forall a b. a -> SubstV b -> SubstV a) -> Functor SubstV
forall a b. a -> SubstV b -> SubstV a
forall a b. (a -> b) -> SubstV a -> SubstV b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SubstV a -> SubstV b
fmap :: forall a b. (a -> b) -> SubstV a -> SubstV b
$c<$ :: forall a b. a -> SubstV b -> SubstV a
<$ :: forall a b. a -> SubstV b -> SubstV a
Functor, (forall m. Monoid m => SubstV m -> m)
-> (forall m a. Monoid m => (a -> m) -> SubstV a -> m)
-> (forall m a. Monoid m => (a -> m) -> SubstV a -> m)
-> (forall a b. (a -> b -> b) -> b -> SubstV a -> b)
-> (forall a b. (a -> b -> b) -> b -> SubstV a -> b)
-> (forall b a. (b -> a -> b) -> b -> SubstV a -> b)
-> (forall b a. (b -> a -> b) -> b -> SubstV a -> b)
-> (forall a. (a -> a -> a) -> SubstV a -> a)
-> (forall a. (a -> a -> a) -> SubstV a -> a)
-> (forall a. SubstV a -> [a])
-> (forall a. SubstV a -> Bool)
-> (forall a. SubstV a -> Int)
-> (forall a. Eq a => a -> SubstV a -> Bool)
-> (forall a. Ord a => SubstV a -> a)
-> (forall a. Ord a => SubstV a -> a)
-> (forall a. Num a => SubstV a -> a)
-> (forall a. Num a => SubstV a -> a)
-> Foldable SubstV
forall a. Eq a => a -> SubstV a -> Bool
forall a. Num a => SubstV a -> a
forall a. Ord a => SubstV a -> a
forall m. Monoid m => SubstV m -> m
forall a. SubstV a -> Bool
forall a. SubstV a -> Int
forall a. SubstV a -> [a]
forall a. (a -> a -> a) -> SubstV a -> a
forall m a. Monoid m => (a -> m) -> SubstV a -> m
forall b a. (b -> a -> b) -> b -> SubstV a -> b
forall a b. (a -> b -> b) -> b -> SubstV a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => SubstV m -> m
fold :: forall m. Monoid m => SubstV m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SubstV a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> SubstV a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SubstV a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> SubstV a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> SubstV a -> b
foldr :: forall a b. (a -> b -> b) -> b -> SubstV a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SubstV a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> SubstV a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SubstV a -> b
foldl :: forall b a. (b -> a -> b) -> b -> SubstV a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SubstV a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> SubstV a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> SubstV a -> a
foldr1 :: forall a. (a -> a -> a) -> SubstV a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SubstV a -> a
foldl1 :: forall a. (a -> a -> a) -> SubstV a -> a
$ctoList :: forall a. SubstV a -> [a]
toList :: forall a. SubstV a -> [a]
$cnull :: forall a. SubstV a -> Bool
null :: forall a. SubstV a -> Bool
$clength :: forall a. SubstV a -> Int
length :: forall a. SubstV a -> Int
$celem :: forall a. Eq a => a -> SubstV a -> Bool
elem :: forall a. Eq a => a -> SubstV a -> Bool
$cmaximum :: forall a. Ord a => SubstV a -> a
maximum :: forall a. Ord a => SubstV a -> a
$cminimum :: forall a. Ord a => SubstV a -> a
minimum :: forall a. Ord a => SubstV a -> a
$csum :: forall a. Num a => SubstV a -> a
sum :: forall a. Num a => SubstV a -> a
$cproduct :: forall a. Num a => SubstV a -> a
product :: forall a. Num a => SubstV a -> a
Foldable, Functor SubstV
Foldable SubstV
(Functor SubstV, Foldable SubstV) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> SubstV a -> f (SubstV b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SubstV (f a) -> f (SubstV a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SubstV a -> m (SubstV b))
-> (forall (m :: * -> *) a.
    Monad m =>
    SubstV (m a) -> m (SubstV a))
-> Traversable SubstV
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => SubstV (m a) -> m (SubstV a)
forall (f :: * -> *) a.
Applicative f =>
SubstV (f a) -> f (SubstV a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SubstV a -> m (SubstV b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SubstV a -> f (SubstV b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SubstV a -> f (SubstV b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SubstV a -> f (SubstV b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SubstV (f a) -> f (SubstV a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SubstV (f a) -> f (SubstV a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SubstV a -> m (SubstV b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SubstV a -> m (SubstV b)
$csequence :: forall (m :: * -> *) a. Monad m => SubstV (m a) -> m (SubstV a)
sequence :: forall (m :: * -> *) a. Monad m => SubstV (m a) -> m (SubstV a)
Traversable)

instance ToJSON Subst
instance FromJSON Subst

instance (Fixpoint v, Ord v, Show v) => Show (SubstV v) where
  show :: SubstV v -> String
show = SubstV v -> String
forall a. Fixpoint a => a -> String
showFix

instance (Ord v, Fixpoint v) => Fixpoint (SubstV v) where
  toFix :: SubstV v -> Doc
toFix (Su HashMap Symbol (ExprV v)
m) = case HashMap Symbol (ExprV v) -> [(Symbol, ExprV v)]
forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList HashMap Symbol (ExprV v)
m of
                   []  -> Doc
empty
                   [(Symbol, ExprV v)]
xys -> [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Symbol, ExprV v) -> Doc) -> [(Symbol, ExprV v)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
x,ExprV v
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
<-> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
y) [(Symbol, ExprV v)]
xys

instance (Ord v, Fixpoint v) => PPrint (SubstV v) where
  pprintTidy :: Tidy -> SubstV v -> Doc
pprintTidy Tidy
_ = SubstV v -> 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, [SymConst] -> Value
[SymConst] -> Encoding
SymConst -> Bool
SymConst -> Value
SymConst -> Encoding
(SymConst -> Value)
-> (SymConst -> Encoding)
-> ([SymConst] -> Value)
-> ([SymConst] -> Encoding)
-> (SymConst -> Bool)
-> ToJSON SymConst
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: SymConst -> Value
toJSON :: SymConst -> Value
$ctoEncoding :: SymConst -> Encoding
toEncoding :: SymConst -> Encoding
$ctoJSONList :: [SymConst] -> Value
toJSONList :: [SymConst] -> Value
$ctoEncodingList :: [SymConst] -> Encoding
toEncodingList :: [SymConst] -> Encoding
$comitField :: SymConst -> Bool
omitField :: SymConst -> Bool
ToJSON, Maybe SymConst
Value -> Parser [SymConst]
Value -> Parser SymConst
(Value -> Parser SymConst)
-> (Value -> Parser [SymConst])
-> Maybe SymConst
-> FromJSON SymConst
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser SymConst
parseJSON :: Value -> Parser SymConst
$cparseJSONList :: Value -> Parser [SymConst]
parseJSONList :: Value -> Parser [SymConst]
$comittedField :: Maybe SymConst
omittedField :: Maybe SymConst
FromJSON)

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

instance ToJSON Constant  where
instance ToJSON Brel      where
instance ToJSON Bop       where
instance ToJSON Expr      where

instance FromJSON Constant  where
instance FromJSON Brel      where
instance FromJSON Bop       where
instance FromJSON Expr      where


type Expr = ExprV Symbol

data ExprV v
          = ESym !SymConst
          | ECon !Constant
          | EVar !v
          | EApp !(ExprV v) !(ExprV v)
          | ENeg !(ExprV v)
          | EBin !Bop !(ExprV v) !(ExprV v)
          | EIte !(ExprV v) !(ExprV v) !(ExprV v)
          | ECst !(ExprV v) !Sort
          | ELam !(Symbol, Sort)   !(ExprV v)
          | ETApp !(ExprV v) !Sort
          | ETAbs !(ExprV v) !Symbol
          | PAnd   ![ExprV v]
          | POr    ![ExprV v]
          | PNot   !(ExprV v)
          | PImp   !(ExprV v) !(ExprV v)
          | PIff   !(ExprV v) !(ExprV v)
          | PAtom  !Brel  !(ExprV v) !(ExprV v)
          | PKVar  !KVar !(SubstV v)
          | PAll   ![(Symbol, Sort)] !(ExprV v)
          | PExist ![(Symbol, Sort)] !(ExprV v)
          | PGrad  !KVar !(SubstV v) !GradInfo !(ExprV v)
          | ECoerc !Sort !Sort !(ExprV v)
          deriving (ExprV v -> ExprV v -> Bool
(ExprV v -> ExprV v -> Bool)
-> (ExprV v -> ExprV v -> Bool) -> Eq (ExprV v)
forall v. Eq v => ExprV v -> ExprV v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => ExprV v -> ExprV v -> Bool
== :: ExprV v -> ExprV v -> Bool
$c/= :: forall v. Eq v => ExprV v -> ExprV v -> Bool
/= :: ExprV v -> ExprV v -> Bool
Eq, Int -> ExprV v -> ShowS
[ExprV v] -> ShowS
ExprV v -> String
(Int -> ExprV v -> ShowS)
-> (ExprV v -> String) -> ([ExprV v] -> ShowS) -> Show (ExprV v)
forall v. (Show v, Fixpoint v, Ord v) => Int -> ExprV v -> ShowS
forall v. (Show v, Fixpoint v, Ord v) => [ExprV v] -> ShowS
forall v. (Show v, Fixpoint v, Ord v) => ExprV v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. (Show v, Fixpoint v, Ord v) => Int -> ExprV v -> ShowS
showsPrec :: Int -> ExprV v -> ShowS
$cshow :: forall v. (Show v, Fixpoint v, Ord v) => ExprV v -> String
show :: ExprV v -> String
$cshowList :: forall v. (Show v, Fixpoint v, Ord v) => [ExprV v] -> ShowS
showList :: [ExprV v] -> ShowS
Show, Eq (ExprV v)
Eq (ExprV v) =>
(ExprV v -> ExprV v -> Ordering)
-> (ExprV v -> ExprV v -> Bool)
-> (ExprV v -> ExprV v -> Bool)
-> (ExprV v -> ExprV v -> Bool)
-> (ExprV v -> ExprV v -> Bool)
-> (ExprV v -> ExprV v -> ExprV v)
-> (ExprV v -> ExprV v -> ExprV v)
-> Ord (ExprV v)
ExprV v -> ExprV v -> Bool
ExprV v -> ExprV v -> Ordering
ExprV v -> ExprV v -> ExprV v
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
forall v. Ord v => Eq (ExprV v)
forall v. Ord v => ExprV v -> ExprV v -> Bool
forall v. Ord v => ExprV v -> ExprV v -> Ordering
forall v. Ord v => ExprV v -> ExprV v -> ExprV v
$ccompare :: forall v. Ord v => ExprV v -> ExprV v -> Ordering
compare :: ExprV v -> ExprV v -> Ordering
$c< :: forall v. Ord v => ExprV v -> ExprV v -> Bool
< :: ExprV v -> ExprV v -> Bool
$c<= :: forall v. Ord v => ExprV v -> ExprV v -> Bool
<= :: ExprV v -> ExprV v -> Bool
$c> :: forall v. Ord v => ExprV v -> ExprV v -> Bool
> :: ExprV v -> ExprV v -> Bool
$c>= :: forall v. Ord v => ExprV v -> ExprV v -> Bool
>= :: ExprV v -> ExprV v -> Bool
$cmax :: forall v. Ord v => ExprV v -> ExprV v -> ExprV v
max :: ExprV v -> ExprV v -> ExprV v
$cmin :: forall v. Ord v => ExprV v -> ExprV v -> ExprV v
min :: ExprV v -> ExprV v -> ExprV v
Ord, Typeable (ExprV v)
Typeable (ExprV v) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ExprV v -> c (ExprV v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (ExprV v))
-> (ExprV v -> Constr)
-> (ExprV v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (ExprV v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v)))
-> ((forall b. Data b => b -> b) -> ExprV v -> ExprV v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExprV v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExprV v -> r)
-> (forall u. (forall d. Data d => d -> u) -> ExprV v -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ExprV v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v))
-> Data (ExprV v)
ExprV v -> Constr
ExprV v -> DataType
(forall b. Data b => b -> b) -> ExprV v -> ExprV v
forall v. Data v => Typeable (ExprV v)
forall v. Data v => ExprV v -> Constr
forall v. Data v => ExprV v -> DataType
forall v.
Data v =>
(forall b. Data b => b -> b) -> ExprV v -> ExprV v
forall v u.
Data v =>
Int -> (forall d. Data d => d -> u) -> ExprV v -> u
forall v u.
Data v =>
(forall d. Data d => d -> u) -> ExprV v -> [u]
forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExprV v)
forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExprV v -> c (ExprV v)
forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ExprV v))
forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v))
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) -> ExprV v -> u
forall u. (forall d. Data d => d -> u) -> ExprV v -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExprV v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExprV v -> c (ExprV v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ExprV v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v))
$cgfoldl :: forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExprV v -> c (ExprV v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExprV v -> c (ExprV v)
$cgunfold :: forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExprV v)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExprV v)
$ctoConstr :: forall v. Data v => ExprV v -> Constr
toConstr :: ExprV v -> Constr
$cdataTypeOf :: forall v. Data v => ExprV v -> DataType
dataTypeOf :: ExprV v -> DataType
$cdataCast1 :: forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ExprV v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ExprV v))
$cdataCast2 :: forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ExprV v))
$cgmapT :: forall v.
Data v =>
(forall b. Data b => b -> b) -> ExprV v -> ExprV v
gmapT :: (forall b. Data b => b -> b) -> ExprV v -> ExprV v
$cgmapQl :: forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
$cgmapQr :: forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExprV v -> r
$cgmapQ :: forall v u.
Data v =>
(forall d. Data d => d -> u) -> ExprV v -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ExprV v -> [u]
$cgmapQi :: forall v u.
Data v =>
Int -> (forall d. Data d => d -> u) -> ExprV v -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ExprV v -> u
$cgmapM :: forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
$cgmapMp :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
$cgmapMo :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExprV v -> m (ExprV v)
Data, Typeable, (forall x. ExprV v -> Rep (ExprV v) x)
-> (forall x. Rep (ExprV v) x -> ExprV v) -> Generic (ExprV v)
forall x. Rep (ExprV v) x -> ExprV v
forall x. ExprV v -> Rep (ExprV v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x. Rep (ExprV v) x -> ExprV v
forall v x. ExprV v -> Rep (ExprV v) x
$cfrom :: forall v x. ExprV v -> Rep (ExprV v) x
from :: forall x. ExprV v -> Rep (ExprV v) x
$cto :: forall v x. Rep (ExprV v) x -> ExprV v
to :: forall x. Rep (ExprV v) x -> ExprV v
Generic, (forall a b. (a -> b) -> ExprV a -> ExprV b)
-> (forall a b. a -> ExprV b -> ExprV a) -> Functor ExprV
forall a b. a -> ExprV b -> ExprV a
forall a b. (a -> b) -> ExprV a -> ExprV b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ExprV a -> ExprV b
fmap :: forall a b. (a -> b) -> ExprV a -> ExprV b
$c<$ :: forall a b. a -> ExprV b -> ExprV a
<$ :: forall a b. a -> ExprV b -> ExprV a
Functor, (forall m. Monoid m => ExprV m -> m)
-> (forall m a. Monoid m => (a -> m) -> ExprV a -> m)
-> (forall m a. Monoid m => (a -> m) -> ExprV a -> m)
-> (forall a b. (a -> b -> b) -> b -> ExprV a -> b)
-> (forall a b. (a -> b -> b) -> b -> ExprV a -> b)
-> (forall b a. (b -> a -> b) -> b -> ExprV a -> b)
-> (forall b a. (b -> a -> b) -> b -> ExprV a -> b)
-> (forall a. (a -> a -> a) -> ExprV a -> a)
-> (forall a. (a -> a -> a) -> ExprV a -> a)
-> (forall a. ExprV a -> [a])
-> (forall a. ExprV a -> Bool)
-> (forall a. ExprV a -> Int)
-> (forall a. Eq a => a -> ExprV a -> Bool)
-> (forall a. Ord a => ExprV a -> a)
-> (forall a. Ord a => ExprV a -> a)
-> (forall a. Num a => ExprV a -> a)
-> (forall a. Num a => ExprV a -> a)
-> Foldable ExprV
forall a. Eq a => a -> ExprV a -> Bool
forall a. Num a => ExprV a -> a
forall a. Ord a => ExprV a -> a
forall m. Monoid m => ExprV m -> m
forall a. ExprV a -> Bool
forall a. ExprV a -> Int
forall a. ExprV a -> [a]
forall a. (a -> a -> a) -> ExprV a -> a
forall m a. Monoid m => (a -> m) -> ExprV a -> m
forall b a. (b -> a -> b) -> b -> ExprV a -> b
forall a b. (a -> b -> b) -> b -> ExprV a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => ExprV m -> m
fold :: forall m. Monoid m => ExprV m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ExprV a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ExprV a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ExprV a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> ExprV a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> ExprV a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ExprV a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ExprV a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ExprV a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ExprV a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ExprV a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ExprV a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> ExprV a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> ExprV a -> a
foldr1 :: forall a. (a -> a -> a) -> ExprV a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ExprV a -> a
foldl1 :: forall a. (a -> a -> a) -> ExprV a -> a
$ctoList :: forall a. ExprV a -> [a]
toList :: forall a. ExprV a -> [a]
$cnull :: forall a. ExprV a -> Bool
null :: forall a. ExprV a -> Bool
$clength :: forall a. ExprV a -> Int
length :: forall a. ExprV a -> Int
$celem :: forall a. Eq a => a -> ExprV a -> Bool
elem :: forall a. Eq a => a -> ExprV a -> Bool
$cmaximum :: forall a. Ord a => ExprV a -> a
maximum :: forall a. Ord a => ExprV a -> a
$cminimum :: forall a. Ord a => ExprV a -> a
minimum :: forall a. Ord a => ExprV a -> a
$csum :: forall a. Num a => ExprV a -> a
sum :: forall a. Num a => ExprV a -> a
$cproduct :: forall a. Num a => ExprV a -> a
product :: forall a. Num a => ExprV a -> a
Foldable, Functor ExprV
Foldable ExprV
(Functor ExprV, Foldable ExprV) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> ExprV a -> f (ExprV b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    ExprV (f a) -> f (ExprV a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ExprV a -> m (ExprV b))
-> (forall (m :: * -> *) a. Monad m => ExprV (m a) -> m (ExprV a))
-> Traversable ExprV
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => ExprV (m a) -> m (ExprV a)
forall (f :: * -> *) a. Applicative f => ExprV (f a) -> f (ExprV a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ExprV a -> m (ExprV b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ExprV a -> f (ExprV b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ExprV a -> f (ExprV b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ExprV a -> f (ExprV b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => ExprV (f a) -> f (ExprV a)
sequenceA :: forall (f :: * -> *) a. Applicative f => ExprV (f a) -> f (ExprV a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ExprV a -> m (ExprV b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ExprV a -> m (ExprV b)
$csequence :: forall (m :: * -> *) a. Monad m => ExprV (m a) -> m (ExprV a)
sequence :: forall (m :: * -> *) a. Monad m => ExprV (m a) -> m (ExprV a)
Traversable)

onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
onEverySubexpr :: (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
onEverySubexpr = (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
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 :: ExprV v
pattern $mPTrue :: forall {r} {v}. ExprV v -> ((# #) -> r) -> ((# #) -> r) -> r
$bPTrue :: forall v. ExprV v
PTrue = PAnd []

pattern PTop :: ExprV v
pattern $mPTop :: forall {r} {v}. ExprV v -> ((# #) -> r) -> ((# #) -> r) -> r
$bPTop :: forall v. ExprV v
PTop = PAnd []

pattern PFalse :: ExprV v
pattern $mPFalse :: forall {r} {v}. ExprV v -> ((# #) -> r) -> ((# #) -> r) -> r
$bPFalse :: forall v. ExprV v
PFalse = POr  []

pattern EBot :: ExprV v
pattern $mEBot :: forall {r} {v}. ExprV v -> ((# #) -> r) -> ((# #) -> r) -> r
$bEBot :: forall v. ExprV v
EBot = POr  []

pattern EEq :: ExprV v -> ExprV v -> ExprV v
pattern $mEEq :: forall {r} {v}.
ExprV v -> (ExprV v -> ExprV v -> r) -> ((# #) -> r) -> r
$bEEq :: forall v. ExprV v -> ExprV v -> ExprV v
EEq e1 e2 = PAtom Eq    e1 e2

pattern ETimes :: ExprV v -> ExprV v -> ExprV v
pattern $mETimes :: forall {r} {v}.
ExprV v -> (ExprV v -> ExprV v -> r) -> ((# #) -> r) -> r
$bETimes :: forall v. ExprV v -> ExprV v -> ExprV v
ETimes e1 e2 = EBin Times  e1 e2

pattern ERTimes :: ExprV v -> ExprV v -> ExprV v
pattern $mERTimes :: forall {r} {v}.
ExprV v -> (ExprV v -> ExprV v -> r) -> ((# #) -> r) -> r
$bERTimes :: forall v. ExprV v -> ExprV v -> ExprV v
ERTimes e1 e2 = EBin RTimes e1 e2

pattern EDiv :: ExprV v -> ExprV v -> ExprV v
pattern $mEDiv :: forall {r} {v}.
ExprV v -> (ExprV v -> ExprV v -> r) -> ((# #) -> r) -> r
$bEDiv :: forall v. ExprV v -> ExprV v -> ExprV v
EDiv e1 e2 = EBin Div    e1 e2

pattern ERDiv :: ExprV v -> ExprV v -> ExprV v
pattern $mERDiv :: forall {r} {v}.
ExprV v -> (ExprV v -> ExprV v -> r) -> ((# #) -> r) -> r
$bERDiv :: forall v. ExprV v -> ExprV v -> ExprV v
ERDiv e1 e2 = EBin RDiv   e1 e2

exprSymbolsSet :: Expr -> HashSet Symbol
exprSymbolsSet :: ExprV Symbol -> HashSet Symbol
exprSymbolsSet = ExprV Symbol -> HashSet Symbol
go
  where
    gos :: [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol]
es                = [HashSet Symbol] -> HashSet Symbol
forall a. Eq a => [HashSet a] -> HashSet a
HashSet.unions (ExprV Symbol -> HashSet Symbol
go (ExprV Symbol -> HashSet Symbol)
-> [ExprV Symbol] -> [HashSet Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es)
    go :: ExprV Symbol -> HashSet Symbol
go (EVar Symbol
x)           = Symbol -> HashSet Symbol
forall a. Hashable a => a -> HashSet a
HashSet.singleton Symbol
x
    go (EApp ExprV Symbol
f ExprV Symbol
e)         = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol
f, ExprV Symbol
e]
    go (ELam (Symbol
x,Sort
_) ExprV Symbol
e)     = Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.delete Symbol
x (ExprV Symbol -> HashSet Symbol
go ExprV Symbol
e)
    go (ECoerc Sort
_ Sort
_ ExprV Symbol
e)     = ExprV Symbol -> HashSet Symbol
go ExprV Symbol
e
    go (ENeg ExprV Symbol
e)           = ExprV Symbol -> HashSet Symbol
go ExprV Symbol
e
    go (EBin Bop
_ ExprV Symbol
e1 ExprV Symbol
e2)     = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol
e1, ExprV Symbol
e2]
    go (EIte ExprV Symbol
p ExprV Symbol
e1 ExprV Symbol
e2)     = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol
p, ExprV Symbol
e1, ExprV Symbol
e2]
    go (ECst ExprV Symbol
e Sort
_)         = ExprV Symbol -> HashSet Symbol
go ExprV Symbol
e
    go (PAnd [ExprV Symbol]
ps)          = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol]
ps
    go (POr [ExprV Symbol]
ps)           = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol]
ps
    go (PNot ExprV Symbol
p)           = ExprV Symbol -> HashSet Symbol
go ExprV Symbol
p
    go (PIff ExprV Symbol
p1 ExprV Symbol
p2)       = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol
p1, ExprV Symbol
p2]
    go (PImp ExprV Symbol
p1 ExprV Symbol
p2)       = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol
p1, ExprV Symbol
p2]
    go (PAtom Brel
_ ExprV Symbol
e1 ExprV Symbol
e2)    = [ExprV Symbol] -> HashSet Symbol
gos [ExprV Symbol
e1, ExprV Symbol
e2]
    go (PKVar KVar
_ (Su HashMap Symbol (ExprV Symbol)
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
$ (ExprV Symbol -> HashSet Symbol)
-> [ExprV Symbol] -> [HashSet Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ExprV Symbol -> HashSet Symbol
exprSymbolsSet (HashMap Symbol (ExprV Symbol) -> [ExprV Symbol]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol (ExprV Symbol)
su)
    go (PAll [(Symbol, Sort)]
xts ExprV Symbol
p)       = ExprV Symbol -> HashSet Symbol
go ExprV Symbol
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 ExprV Symbol
p)     = ExprV Symbol -> HashSet Symbol
go ExprV Symbol
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 ExprV Symbol
_                  = HashSet Symbol
forall a. HashSet a
HashSet.empty

substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr
substSortInExpr :: (Symbol -> Sort) -> ExprV Symbol -> ExprV Symbol
substSortInExpr Symbol -> Sort
f = (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
onEverySubexpr ExprV Symbol -> ExprV Symbol
go
  where
    go :: ExprV Symbol -> ExprV Symbol
go = \case
      ELam (Symbol
x, Sort
t) ExprV Symbol
e -> (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, (Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t) ExprV Symbol
e
      PAll [(Symbol, Sort)]
xts ExprV Symbol
e -> [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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) ExprV Symbol
e
      PExist [(Symbol, Sort)]
xts ExprV Symbol
e -> [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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) ExprV Symbol
e
      ECst ExprV Symbol
e Sort
t -> ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst ExprV Symbol
e ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t)
      ECoerc Sort
t0 Sort
t1 ExprV Symbol
e -> Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t0) ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t1) ExprV Symbol
e
      ExprV Symbol
e -> ExprV Symbol
e


sortSubstInExpr :: SortSubst -> Expr -> Expr
sortSubstInExpr :: SortSubst -> ExprV Symbol -> ExprV Symbol
sortSubstInExpr SortSubst
f = (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
onEverySubexpr ExprV Symbol -> ExprV Symbol
go
  where
    go :: ExprV Symbol -> ExprV Symbol
go = \case
      ELam (Symbol
x, Sort
t) ExprV Symbol
e -> (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, SortSubst -> Sort -> Sort
sortSubst SortSubst
f Sort
t) ExprV Symbol
e
      PAll [(Symbol, Sort)]
xts ExprV Symbol
e -> [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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 (SortSubst -> Sort -> Sort
sortSubst SortSubst
f) ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) ExprV Symbol
e
      PExist [(Symbol, Sort)]
xts ExprV Symbol
e -> [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
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 (SortSubst -> Sort -> Sort
sortSubst SortSubst
f) ((Symbol, Sort) -> (Symbol, Sort))
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) ExprV Symbol
e
      ECst ExprV Symbol
e Sort
t -> ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst ExprV Symbol
e (SortSubst -> Sort -> Sort
sortSubst SortSubst
f Sort
t)
      ECoerc Sort
t0 Sort
t1 ExprV Symbol
e -> Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc (SortSubst -> Sort -> Sort
sortSubst SortSubst
f Sort
t0) (SortSubst -> Sort -> Sort
sortSubst SortSubst
f Sort
t1) ExprV Symbol
e
      ExprV Symbol
e -> ExprV Symbol
e

exprKVars :: Expr -> HashMap KVar [Subst]
exprKVars :: ExprV Symbol -> HashMap KVar [Subst]
exprKVars = ExprV Symbol -> HashMap KVar [Subst]
go
  where
    gos :: [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol]
es                = [HashMap KVar [Subst]] -> HashMap KVar [Subst]
forall k v. Eq k => [HashMap k v] -> HashMap k v
HashMap.unions (ExprV Symbol -> HashMap KVar [Subst]
go (ExprV Symbol -> HashMap KVar [Subst])
-> [ExprV Symbol] -> [HashMap KVar [Subst]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es)
    go :: ExprV Symbol -> HashMap KVar [Subst]
go (EVar Symbol
_)           = HashMap KVar [Subst]
forall k v. HashMap k v
HashMap.empty
    go (EApp ExprV Symbol
f ExprV Symbol
e)         = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol
f, ExprV Symbol
e]
    go (ELam (Symbol, Sort)
_ ExprV Symbol
e)     = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
e
    go (ECoerc Sort
_ Sort
_ ExprV Symbol
e)     = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
e
    go (ENeg ExprV Symbol
e)           = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
e
    go (EBin Bop
_ ExprV Symbol
e1 ExprV Symbol
e2)     = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol
e1, ExprV Symbol
e2]
    go (EIte ExprV Symbol
p ExprV Symbol
e1 ExprV Symbol
e2)     = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol
p, ExprV Symbol
e1, ExprV Symbol
e2]
    go (ECst ExprV Symbol
e Sort
_)         = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
e
    go (PAnd [ExprV Symbol]
ps)          = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol]
ps
    go (POr [ExprV Symbol]
ps)           = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol]
ps
    go (PNot ExprV Symbol
p)           = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
p
    go (PIff ExprV Symbol
p1 ExprV Symbol
p2)       = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol
p1, ExprV Symbol
p2]
    go (PImp ExprV Symbol
p1 ExprV Symbol
p2)       = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol
p1, ExprV Symbol
p2]
    go (PAtom Brel
_ ExprV Symbol
e1 ExprV Symbol
e2)    = [ExprV Symbol] -> HashMap KVar [Subst]
gos [ExprV Symbol
e1, ExprV Symbol
e2]
    go (PKVar KVar
k substs :: Subst
substs@(Su HashMap Symbol (ExprV Symbol)
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
$ (ExprV Symbol -> HashMap KVar [Subst])
-> [ExprV Symbol] -> [HashMap KVar [Subst]]
forall a b. (a -> b) -> [a] -> [b]
map ExprV Symbol -> HashMap KVar [Subst]
exprKVars (HashMap Symbol (ExprV Symbol) -> [ExprV Symbol]
forall k v. HashMap k v -> [v]
M.elems HashMap Symbol (ExprV Symbol)
su)
    go (PAll [(Symbol, Sort)]
_xts ExprV Symbol
p)       = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
p
    go (PExist [(Symbol, Sort)]
_xts ExprV Symbol
p)     = ExprV Symbol -> HashMap KVar [Subst]
go ExprV Symbol
p
    go ExprV Symbol
_                  = 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)

instance ToJSON   GradInfo
instance FromJSON GradInfo

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 -> [ExprV Symbol] -> ExprV Symbol
mkEApp = ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol)
-> (LocSymbol -> ExprV Symbol)
-> LocSymbol
-> [ExprV Symbol]
-> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol)
-> (LocSymbol -> Symbol) -> LocSymbol -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> Symbol
forall a. Located a -> a
val

eApps :: ExprV v -> [ExprV v] -> ExprV v
eApps :: forall v. ExprV v -> [ExprV v] -> ExprV v
eApps ExprV v
f [ExprV v]
es  = (ExprV v -> ExprV v -> ExprV v) -> ExprV v -> [ExprV v] -> ExprV v
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
EApp ExprV v
f [ExprV v]
es

splitEApp :: ExprV v -> (ExprV v, [ExprV v])
splitEApp :: forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp = [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
forall {v}. [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
go []
  where
    go :: [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
go [ExprV v]
acc (EApp ExprV v
f ExprV v
e) = [ExprV v] -> ExprV v -> (ExprV v, [ExprV v])
go (ExprV v
eExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
acc) ExprV v
f
    go [ExprV v]
acc ExprV v
e          = (ExprV v
e, [ExprV v]
acc)

splitEAppThroughECst :: Expr -> (Expr, [Expr])
splitEAppThroughECst :: ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
splitEAppThroughECst = [ExprV Symbol] -> ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
go []
  where
    go :: [ExprV Symbol] -> ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
go [ExprV Symbol]
acc (ExprV Symbol -> ExprV Symbol
dropECst -> (EApp ExprV Symbol
f ExprV Symbol
e)) = [ExprV Symbol] -> ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
go (ExprV Symbol
eExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
:[ExprV Symbol]
acc) ExprV Symbol
f
    go [ExprV Symbol]
acc ExprV Symbol
e                        = (ExprV Symbol
e, [ExprV Symbol]
acc)

dropECst :: Expr -> Expr
dropECst :: ExprV Symbol -> ExprV Symbol
dropECst ExprV Symbol
e = case ExprV Symbol
e of
  ECst ExprV Symbol
e' Sort
_ -> ExprV Symbol -> ExprV Symbol
dropECst ExprV Symbol
e'
  ExprV Symbol
_         -> ExprV Symbol
e

splitPAnd :: Expr -> [Expr]
splitPAnd :: ExprV Symbol -> [ExprV Symbol]
splitPAnd (PAnd [ExprV Symbol]
es) = (ExprV Symbol -> [ExprV Symbol])
-> [ExprV Symbol] -> [ExprV Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV Symbol -> [ExprV Symbol]
splitPAnd [ExprV Symbol]
es
splitPAnd ExprV Symbol
e         = [ExprV Symbol
e]

eAppC :: Sort -> Expr -> Expr -> Expr
eAppC :: Sort -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
eAppC Sort
s ExprV Symbol
e1 ExprV Symbol
e2 = ExprV Symbol -> Sort -> ExprV Symbol
eCst (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp ExprV Symbol
e1 ExprV Symbol
e2) Sort
s

-- | Eliminates redundant casts
eCst :: Expr -> Sort -> Expr
eCst :: ExprV Symbol -> Sort -> ExprV Symbol
eCst ExprV Symbol
e Sort
s = ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst (ExprV Symbol -> ExprV Symbol
dropECst ExprV Symbol
e) Sort
s

--------------------------------------------------------------------------------
debruijnIndex :: Expr -> Int
debruijnIndex :: ExprV Symbol -> Int
debruijnIndex = ExprV Symbol -> Int
forall {a} {v}. Num a => ExprV v -> a
go
  where
    go :: ExprV v -> a
go (ELam (Symbol, Sort)
_ ExprV v
e)      = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e
    go (ECst ExprV v
e Sort
_)      = ExprV v -> a
go ExprV v
e
    go (EApp ExprV v
e1 ExprV v
e2)    = ExprV v -> a
go ExprV v
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e2
    go (ESym SymConst
_)        = a
1
    go (ECon Constant
_)        = a
1
    go (EVar v
_)        = a
1
    go (ENeg ExprV v
e)        = ExprV v -> a
go ExprV v
e
    go (EBin Bop
_ ExprV v
e1 ExprV v
e2)  = ExprV v -> a
go ExprV v
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e2
    go (EIte ExprV v
e ExprV v
e1 ExprV v
e2)  = ExprV v -> a
go ExprV v
e a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e2
    go (ETAbs ExprV v
e Symbol
_)     = ExprV v -> a
go ExprV v
e
    go (ETApp ExprV v
e Sort
_)     = ExprV v -> a
go ExprV v
e
    go (PAnd [ExprV v]
es)       = (a -> ExprV v -> a) -> a -> [ExprV v] -> 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 ExprV v
e -> a
n a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e) a
0 [ExprV v]
es
    go (POr [ExprV v]
es)        = (a -> ExprV v -> a) -> a -> [ExprV v] -> 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 ExprV v
e -> a
n a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e) a
0 [ExprV v]
es
    go (PNot ExprV v
e)        = ExprV v -> a
go ExprV v
e
    go (PImp ExprV v
e1 ExprV v
e2)    = ExprV v -> a
go ExprV v
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e2
    go (PIff ExprV v
e1 ExprV v
e2)    = ExprV v -> a
go ExprV v
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e2
    go (PAtom Brel
_ ExprV v
e1 ExprV v
e2) = ExprV v -> a
go ExprV v
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ ExprV v -> a
go ExprV v
e2
    go (PAll [(Symbol, Sort)]
_ ExprV v
e)      = ExprV v -> a
go ExprV v
e
    go (PExist [(Symbol, Sort)]
_ ExprV v
e)    = ExprV v -> a
go ExprV v
e
    go (PKVar KVar
_ SubstV v
_)     = a
1
    go (PGrad KVar
_ SubstV v
_ GradInfo
_ ExprV v
e) = ExprV v -> a
go ExprV v
e
    go (ECoerc Sort
_ Sort
_ ExprV v
e)  = ExprV v -> a
go ExprV v
e

type Reft = ReftV Symbol

-- | Refinement of @v@ satisfying a predicate
--   e.g. in '{x: _ | e }' x is the @Symbol@ and e the @ExprV v@
newtype ReftV v = Reft (Symbol, ExprV v)
    deriving (ReftV v -> ReftV v -> Bool
(ReftV v -> ReftV v -> Bool)
-> (ReftV v -> ReftV v -> Bool) -> Eq (ReftV v)
forall v. Eq v => ReftV v -> ReftV v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => ReftV v -> ReftV v -> Bool
== :: ReftV v -> ReftV v -> Bool
$c/= :: forall v. Eq v => ReftV v -> ReftV v -> Bool
/= :: ReftV v -> ReftV v -> Bool
Eq, Eq (ReftV v)
Eq (ReftV v) =>
(ReftV v -> ReftV v -> Ordering)
-> (ReftV v -> ReftV v -> Bool)
-> (ReftV v -> ReftV v -> Bool)
-> (ReftV v -> ReftV v -> Bool)
-> (ReftV v -> ReftV v -> Bool)
-> (ReftV v -> ReftV v -> ReftV v)
-> (ReftV v -> ReftV v -> ReftV v)
-> Ord (ReftV v)
ReftV v -> ReftV v -> Bool
ReftV v -> ReftV v -> Ordering
ReftV v -> ReftV v -> ReftV v
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
forall v. Ord v => Eq (ReftV v)
forall v. Ord v => ReftV v -> ReftV v -> Bool
forall v. Ord v => ReftV v -> ReftV v -> Ordering
forall v. Ord v => ReftV v -> ReftV v -> ReftV v
$ccompare :: forall v. Ord v => ReftV v -> ReftV v -> Ordering
compare :: ReftV v -> ReftV v -> Ordering
$c< :: forall v. Ord v => ReftV v -> ReftV v -> Bool
< :: ReftV v -> ReftV v -> Bool
$c<= :: forall v. Ord v => ReftV v -> ReftV v -> Bool
<= :: ReftV v -> ReftV v -> Bool
$c> :: forall v. Ord v => ReftV v -> ReftV v -> Bool
> :: ReftV v -> ReftV v -> Bool
$c>= :: forall v. Ord v => ReftV v -> ReftV v -> Bool
>= :: ReftV v -> ReftV v -> Bool
$cmax :: forall v. Ord v => ReftV v -> ReftV v -> ReftV v
max :: ReftV v -> ReftV v -> ReftV v
$cmin :: forall v. Ord v => ReftV v -> ReftV v -> ReftV v
min :: ReftV v -> ReftV v -> ReftV v
Ord, Typeable (ReftV v)
Typeable (ReftV v) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ReftV v -> c (ReftV v))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (ReftV v))
-> (ReftV v -> Constr)
-> (ReftV v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (ReftV v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v)))
-> ((forall b. Data b => b -> b) -> ReftV v -> ReftV v)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ReftV v -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ReftV v -> r)
-> (forall u. (forall d. Data d => d -> u) -> ReftV v -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> ReftV v -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v))
-> Data (ReftV v)
ReftV v -> Constr
ReftV v -> DataType
(forall b. Data b => b -> b) -> ReftV v -> ReftV v
forall v. Data v => Typeable (ReftV v)
forall v. Data v => ReftV v -> Constr
forall v. Data v => ReftV v -> DataType
forall v.
Data v =>
(forall b. Data b => b -> b) -> ReftV v -> ReftV v
forall v u.
Data v =>
Int -> (forall d. Data d => d -> u) -> ReftV v -> u
forall v u.
Data v =>
(forall d. Data d => d -> u) -> ReftV v -> [u]
forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReftV v)
forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ReftV v -> c (ReftV v)
forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ReftV v))
forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v))
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) -> ReftV v -> u
forall u. (forall d. Data d => d -> u) -> ReftV v -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReftV v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ReftV v -> c (ReftV v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ReftV v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v))
$cgfoldl :: forall v (c :: * -> *).
Data v =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ReftV v -> c (ReftV v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ReftV v -> c (ReftV v)
$cgunfold :: forall v (c :: * -> *).
Data v =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReftV v)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReftV v)
$ctoConstr :: forall v. Data v => ReftV v -> Constr
toConstr :: ReftV v -> Constr
$cdataTypeOf :: forall v. Data v => ReftV v -> DataType
dataTypeOf :: ReftV v -> DataType
$cdataCast1 :: forall v (t :: * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ReftV v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ReftV v))
$cdataCast2 :: forall v (t :: * -> * -> *) (c :: * -> *).
(Data v, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ReftV v))
$cgmapT :: forall v.
Data v =>
(forall b. Data b => b -> b) -> ReftV v -> ReftV v
gmapT :: (forall b. Data b => b -> b) -> ReftV v -> ReftV v
$cgmapQl :: forall v r r'.
Data v =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
$cgmapQr :: forall v r r'.
Data v =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ReftV v -> r
$cgmapQ :: forall v u.
Data v =>
(forall d. Data d => d -> u) -> ReftV v -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ReftV v -> [u]
$cgmapQi :: forall v u.
Data v =>
Int -> (forall d. Data d => d -> u) -> ReftV v -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ReftV v -> u
$cgmapM :: forall v (m :: * -> *).
(Data v, Monad m) =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
$cgmapMp :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
$cgmapMo :: forall v (m :: * -> *).
(Data v, MonadPlus m) =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ReftV v -> m (ReftV v)
Data, Typeable, (forall x. ReftV v -> Rep (ReftV v) x)
-> (forall x. Rep (ReftV v) x -> ReftV v) -> Generic (ReftV v)
forall x. Rep (ReftV v) x -> ReftV v
forall x. ReftV v -> Rep (ReftV v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x. Rep (ReftV v) x -> ReftV v
forall v x. ReftV v -> Rep (ReftV v) x
$cfrom :: forall v x. ReftV v -> Rep (ReftV v) x
from :: forall x. ReftV v -> Rep (ReftV v) x
$cto :: forall v x. Rep (ReftV v) x -> ReftV v
to :: forall x. Rep (ReftV v) x -> ReftV v
Generic, (forall a b. (a -> b) -> ReftV a -> ReftV b)
-> (forall a b. a -> ReftV b -> ReftV a) -> Functor ReftV
forall a b. a -> ReftV b -> ReftV a
forall a b. (a -> b) -> ReftV a -> ReftV b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> ReftV a -> ReftV b
fmap :: forall a b. (a -> b) -> ReftV a -> ReftV b
$c<$ :: forall a b. a -> ReftV b -> ReftV a
<$ :: forall a b. a -> ReftV b -> ReftV a
Functor, (forall m. Monoid m => ReftV m -> m)
-> (forall m a. Monoid m => (a -> m) -> ReftV a -> m)
-> (forall m a. Monoid m => (a -> m) -> ReftV a -> m)
-> (forall a b. (a -> b -> b) -> b -> ReftV a -> b)
-> (forall a b. (a -> b -> b) -> b -> ReftV a -> b)
-> (forall b a. (b -> a -> b) -> b -> ReftV a -> b)
-> (forall b a. (b -> a -> b) -> b -> ReftV a -> b)
-> (forall a. (a -> a -> a) -> ReftV a -> a)
-> (forall a. (a -> a -> a) -> ReftV a -> a)
-> (forall a. ReftV a -> [a])
-> (forall a. ReftV a -> Bool)
-> (forall a. ReftV a -> Int)
-> (forall a. Eq a => a -> ReftV a -> Bool)
-> (forall a. Ord a => ReftV a -> a)
-> (forall a. Ord a => ReftV a -> a)
-> (forall a. Num a => ReftV a -> a)
-> (forall a. Num a => ReftV a -> a)
-> Foldable ReftV
forall a. Eq a => a -> ReftV a -> Bool
forall a. Num a => ReftV a -> a
forall a. Ord a => ReftV a -> a
forall m. Monoid m => ReftV m -> m
forall a. ReftV a -> Bool
forall a. ReftV a -> Int
forall a. ReftV a -> [a]
forall a. (a -> a -> a) -> ReftV a -> a
forall m a. Monoid m => (a -> m) -> ReftV a -> m
forall b a. (b -> a -> b) -> b -> ReftV a -> b
forall a b. (a -> b -> b) -> b -> ReftV a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => ReftV m -> m
fold :: forall m. Monoid m => ReftV m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ReftV a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ReftV a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ReftV a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> ReftV a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> ReftV a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ReftV a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ReftV a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ReftV a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ReftV a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ReftV a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ReftV a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> ReftV a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> ReftV a -> a
foldr1 :: forall a. (a -> a -> a) -> ReftV a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ReftV a -> a
foldl1 :: forall a. (a -> a -> a) -> ReftV a -> a
$ctoList :: forall a. ReftV a -> [a]
toList :: forall a. ReftV a -> [a]
$cnull :: forall a. ReftV a -> Bool
null :: forall a. ReftV a -> Bool
$clength :: forall a. ReftV a -> Int
length :: forall a. ReftV a -> Int
$celem :: forall a. Eq a => a -> ReftV a -> Bool
elem :: forall a. Eq a => a -> ReftV a -> Bool
$cmaximum :: forall a. Ord a => ReftV a -> a
maximum :: forall a. Ord a => ReftV a -> a
$cminimum :: forall a. Ord a => ReftV a -> a
minimum :: forall a. Ord a => ReftV a -> a
$csum :: forall a. Num a => ReftV a -> a
sum :: forall a. Num a => ReftV a -> a
$cproduct :: forall a. Num a => ReftV a -> a
product :: forall a. Num a => ReftV a -> a
Foldable, Functor ReftV
Foldable ReftV
(Functor ReftV, Foldable ReftV) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> ReftV a -> f (ReftV b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    ReftV (f a) -> f (ReftV a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ReftV a -> m (ReftV b))
-> (forall (m :: * -> *) a. Monad m => ReftV (m a) -> m (ReftV a))
-> Traversable ReftV
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => ReftV (m a) -> m (ReftV a)
forall (f :: * -> *) a. Applicative f => ReftV (f a) -> f (ReftV a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ReftV a -> m (ReftV b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ReftV a -> f (ReftV b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ReftV a -> f (ReftV b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ReftV a -> f (ReftV b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => ReftV (f a) -> f (ReftV a)
sequenceA :: forall (f :: * -> *) a. Applicative f => ReftV (f a) -> f (ReftV a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ReftV a -> m (ReftV b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ReftV a -> m (ReftV b)
$csequence :: forall (m :: * -> *) a. Monad m => ReftV (m a) -> m (ReftV a)
sequence :: forall (m :: * -> *) a. Monad m => ReftV (m a) -> m (ReftV a)
Traversable)

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)
    (ExprV Symbol -> HashSet Symbol
exprSymbolsSet (ExprV Symbol -> HashSet Symbol) -> ExprV Symbol -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Reft -> ExprV Symbol
forall v. ReftV v -> ExprV v
reftPred (Reft -> ExprV Symbol) -> Reft -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr)

elit :: Located Symbol -> Sort -> Expr
elit :: LocSymbol -> Sort -> ExprV Symbol
elit LocSymbol
l Sort
s = Constant -> ExprV Symbol
forall v. Constant -> ExprV v
ECon (Constant -> ExprV Symbol) -> Constant -> ExprV Symbol
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 (Ord v, Fixpoint v) => Fixpoint (ExprV v) where
  toFix :: ExprV v -> 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 v
s)       = v -> Doc
forall a. Fixpoint a => a -> Doc
toFix v
s
  toFix e :: ExprV v
e@(EApp ExprV v
_ ExprV v
_)   = 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
$ ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix (ExprV v -> Doc) -> [ExprV v] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExprV v
fExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
es) where (ExprV v
f, [ExprV v]
es) = ExprV v -> (ExprV v, [ExprV v])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV v
e
  toFix (ENeg ExprV v
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 (ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e)
  toFix (EBin Bop
o ExprV v
e1 ExprV v
e2) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e1  Doc -> Doc -> Doc
<+> Bop -> Doc
forall a. Fixpoint a => a -> Doc
toFix Bop
o, Int -> Doc -> Doc
nest Int
2 (ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e2)]
  toFix (EIte ExprV v
p ExprV v
e1 ExprV v
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
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p Doc -> Doc -> Doc
<+> String -> Doc
text String
"then", Int -> Doc -> Doc
nest Int
2 (ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e1), String -> Doc
text String
"else", Int -> Doc -> Doc
nest Int
2 (ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e2)]
  -- toFix (ECst e _so)   = toFix e
  toFix (ECst ExprV v
e Sort
so)    = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
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 ExprV v
PTrue          = String -> Doc
text String
"true"
  toFix ExprV v
PFalse         = String -> Doc
text String
"false"
  toFix (PNot ExprV v
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 (ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p)
  toFix (PImp ExprV v
p1 ExprV v
p2)   = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"=>" Doc -> Doc -> Doc
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p2
  toFix (PIff ExprV v
p1 ExprV v
p2)   = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"<=>" Doc -> Doc -> Doc
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p2
  toFix (PAnd [ExprV v]
ps)      = String -> Doc
text String
"&&" Doc -> Doc -> Doc
<+> [ExprV v] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [ExprV v]
ps
  toFix (POr  [ExprV v]
ps)      = String -> Doc
text String
"||" Doc -> Doc -> Doc
<+> [ExprV v] -> Doc
forall a. Fixpoint a => a -> Doc
toFix [ExprV v]
ps
  toFix (PAtom Brel
r ExprV v
e1 ExprV v
e2)  = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e1 Doc -> Doc -> Doc
<+> Brel -> Doc
forall a. Fixpoint a => a -> Doc
toFix Brel
r, Int -> Doc -> Doc
nest Int
2 (ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e2)]
  toFix (PKVar KVar
k SubstV v
su)     = KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix KVar
k Doc -> Doc -> Doc
<-> SubstV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix SubstV v
su
  toFix (PAll [(Symbol, Sort)]
xts ExprV v
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
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p))
  toFix (PExist [(Symbol, Sort)]
xts ExprV v
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
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p))
  toFix (ETApp ExprV v
e Sort
s)      = String -> Doc
text String
"tapp" Doc -> Doc -> Doc
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s
  toFix (ETAbs ExprV v
e Symbol
s)      = String -> Doc
text String
"tabs" Doc -> Doc -> Doc
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
s
  toFix (PGrad KVar
k SubstV v
_ GradInfo
_ ExprV v
e)  = ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
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 ExprV v
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
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e)
  toFix (ELam (Symbol
x,Sort
s) ExprV v
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
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e

  simplify :: ExprV v -> ExprV v
simplify = ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v
forall v. Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v
simplifyExpr [ExprV v] -> [ExprV v]
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 :: Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v
simplifyExpr :: forall v. Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v
simplifyExpr [ExprV v] -> [ExprV v]
dedup = ExprV v -> ExprV v
go
  where
    go :: ExprV v -> ExprV v
go (POr  [])     = ExprV v
forall v. ExprV v
PFalse
    go (POr  [ExprV v
p])    = ExprV v -> ExprV v
go ExprV v
p
    go (PNot ExprV v
p) =
      let sp :: ExprV v
sp = ExprV v -> ExprV v
go ExprV v
p
       in case ExprV v
sp of
            PNot ExprV v
e -> ExprV v
e
            ExprV v
_ -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v
PNot ExprV v
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 ExprV v
p ExprV v
q)    =
      let sp :: ExprV v
sp = ExprV v -> ExprV v
go ExprV v
p
          sq :: ExprV v
sq = ExprV v -> ExprV v
go ExprV v
q
       in if ExprV v
sp ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
sq then ExprV v
forall v. ExprV v
PTrue
          else if ExprV v
sp ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PTrue then ExprV v
sq
          else if ExprV v
sq ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PTrue then ExprV v
sp
          else if ExprV v
sp ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PFalse then ExprV v -> ExprV v
forall v. ExprV v -> ExprV v
PNot ExprV v
sq
          else if ExprV v
sq ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PFalse then ExprV v -> ExprV v
forall v. ExprV v -> ExprV v
PNot ExprV v
sp
          else ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PIff ExprV v
sp ExprV v
sq

    go (PGrad KVar
k SubstV v
su GradInfo
i ExprV v
e)
      | ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isContraPred ExprV v
e      = ExprV v
forall v. ExprV v
PFalse
      | Bool
otherwise           = KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV v
su GradInfo
i (ExprV v -> ExprV v
go ExprV v
e)

    go (PAnd [ExprV v]
ps)
      | (ExprV v -> Bool) -> [ExprV v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isContraPred [ExprV v]
ps = ExprV v
forall v. ExprV v
PFalse
                           -- Note: Performance of some tests is very sensitive to this code. See #480
      | Bool
otherwise           = [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
simplPAnd ([ExprV v] -> ExprV v)
-> ([ExprV v] -> [ExprV v]) -> [ExprV v] -> ExprV v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExprV v] -> [ExprV v]
dedup ([ExprV v] -> [ExprV v])
-> ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExprV v] -> [ExprV v]
forall v. [ExprV v] -> [ExprV v]
flattenRefas ([ExprV v] -> [ExprV v])
-> ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExprV v -> Bool) -> [ExprV v] -> [ExprV v]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (ExprV v -> Bool) -> ExprV v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred) ([ExprV v] -> ExprV v) -> [ExprV v] -> ExprV v
forall a b. (a -> b) -> a -> b
$ (ExprV v -> ExprV v) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> [a] -> [b]
map ExprV v -> ExprV v
go [ExprV v]
ps
      where
        simplPAnd :: [ExprV v] -> ExprV v
simplPAnd [] = ExprV v
forall v. ExprV v
PTrue
        simplPAnd [ExprV v
p] = ExprV v
p
        simplPAnd [ExprV v]
xs = [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
PAnd [ExprV v]
xs

    go (POr  [ExprV v]
ps)
      | (ExprV v -> Bool) -> [ExprV v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred [ExprV v]
ps = ExprV v
forall v. ExprV v
PTrue
      | Bool
otherwise          = [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
POr  ([ExprV v] -> ExprV v) -> [ExprV v] -> ExprV v
forall a b. (a -> b) -> a -> b
$ (ExprV v -> Bool) -> [ExprV v] -> [ExprV v]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (ExprV v -> Bool) -> ExprV v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isContraPred) ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ (ExprV v -> ExprV v) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> [a] -> [b]
map ExprV v -> ExprV v
go [ExprV v]
ps

    go ExprV v
p
      | ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isContraPred ExprV v
p     = ExprV v
forall v. ExprV v
PFalse
      | ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred  ExprV v
p     = ExprV v
forall v. ExprV v
PTrue
      | Bool
otherwise          = ExprV v
p

isContraPred   :: Eq v => ExprV v -> Bool
isContraPred :: forall v. Eq v => ExprV v -> Bool
isContraPred ExprV v
z = ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
eqC ExprV v
z Bool -> Bool -> Bool
|| (ExprV v
z ExprV v -> [ExprV v] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ExprV v]
forall {v}. [ExprV v]
contras)
  where
    contras :: [ExprV v]
contras    = [ExprV v
forall v. ExprV v
PFalse]

    eqC :: ExprV v -> 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 ExprV v
x ExprV v
y)
               = ExprV v
x ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
y
    eqC (PAtom Brel
Une ExprV v
x ExprV v
y)
               = ExprV v
x ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
y
    eqC ExprV v
_      = Bool
False

isTautoPred   :: Eq v => ExprV v -> Bool
isTautoPred :: forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV v
z  = ExprV v
z ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PTop Bool -> Bool -> Bool
|| ExprV v
z ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PTrue Bool -> Bool -> Bool
|| ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
eqT ExprV v
z
  where
    eqT :: ExprV v -> Bool
eqT (PAnd [])
               = Bool
True
    eqT (PAtom Brel
Le ExprV v
x ExprV v
y)
               = ExprV v
x ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
y
    eqT (PAtom Brel
Ge ExprV v
x ExprV v
y)
               = ExprV v
x ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
y
    eqT (PAtom Brel
Eq ExprV v
x ExprV v
y)
               = ExprV v
x ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
y
    eqT (PAtom Brel
Ueq ExprV v
x ExprV v
y)
               = ExprV v
x ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
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 ExprV v
_      = 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 (Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v) where
  pprintPrec :: Int -> Tidy -> ExprV v -> 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 v
s)        = Tidy -> v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k v
s
  -- pprintPrec _ (EBot)          = text "_|_"
  pprintPrec Int
z Tidy
k (ENeg ExprV v
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 -> ExprV v -> 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 ExprV v
e
    where zn :: a
zn = a
2
  pprintPrec Int
z Tidy
k (EApp ExprV v
f ExprV v
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 -> ExprV v -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
forall {a}. Num a => a
za Tidy
k ExprV v
f Doc -> Doc -> Doc
<+> Int -> Tidy -> ExprV v -> 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 ExprV v
es
    where za :: a
za = a
8
  pprintPrec Int
z Tidy
k (EBin Bop
o ExprV v
e1 ExprV v
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 -> ExprV v -> 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 ExprV v
e1 Doc -> Doc -> Doc
<+>
                                   Tidy -> Bop -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Bop
o         Doc -> Doc -> Doc
<+>
                                   Int -> Tidy -> ExprV v -> 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 ExprV v
e2
    where zo :: Int
zo = Bop -> Int
opPrec Bop
o
  pprintPrec Int
z Tidy
k (EIte ExprV v
p ExprV v
e1 ExprV v
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 -> ExprV v -> 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 ExprV v
p  Doc -> Doc -> Doc
<+>
                                   Doc
"then" Doc -> Doc -> Doc
<+> Int -> Tidy -> ExprV v -> 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 ExprV v
e1 Doc -> Doc -> Doc
<+>
                                   Doc
"else" Doc -> Doc -> Doc
<+> Int -> Tidy -> ExprV v -> 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 ExprV v
e2
    where zi :: a
zi = a
1

  -- RJ: DO NOT DELETE!
  pprintPrec Int
_ Tidy
k (ECst ExprV v
e Sort
so)     = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ExprV v -> Doc
forall a. PPrint a => a -> Doc
pprint ExprV v
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
_ ExprV v
PTrue           = Doc
trueD
  pprintPrec Int
_ Tidy
_ ExprV v
PFalse          = Doc
falseD
  pprintPrec Int
z Tidy
k (PNot ExprV v
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 -> ExprV v -> 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 ExprV v
p
    where zn :: a
zn = a
8
  pprintPrec Int
z Tidy
k (PImp ExprV v
p1 ExprV v
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 -> ExprV v -> 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 ExprV v
p1 Doc -> Doc -> Doc
<+>
                                   Doc
"=>"                     Doc -> Doc -> Doc
<+>
                                   Int -> Tidy -> ExprV v -> 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 ExprV v
p2
    where zi :: a
zi = a
2
  pprintPrec Int
z Tidy
k (PIff ExprV v
p1 ExprV v
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 -> ExprV v -> 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 ExprV v
p1 Doc -> Doc -> Doc
<+>
                                   Doc
"<=>"                    Doc -> Doc -> Doc
<+>
                                   Int -> Tidy -> ExprV v -> 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 ExprV v
p2
    where zi :: a
zi = a
2
  pprintPrec Int
z Tidy
k (PAnd [ExprV v]
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 -> [ExprV v] -> 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 [ExprV v]
ps
    where za :: a
za = a
3
  pprintPrec Int
z Tidy
k (POr  [ExprV v]
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 -> [ExprV v] -> 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 [ExprV v]
ps
    where zo :: a
zo = a
3
  pprintPrec Int
z Tidy
k (PAtom Brel
r ExprV v
e1 ExprV v
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 -> ExprV v -> 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 ExprV v
e1 Doc -> Doc -> Doc
<+>
                                   Tidy -> Brel -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Brel
r         Doc -> Doc -> Doc
<+>
                                   Int -> Tidy -> ExprV v -> 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 ExprV v
e2
    where za :: a
za = a
4
  pprintPrec Int
_ Tidy
k (PAll [(Symbol, Sort)]
xts ExprV v
p)    = Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
forall v.
(Ord v, Fixpoint v, PPrint v) =>
Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
pprintQuant Tidy
k Doc
"forall" [(Symbol, Sort)]
xts ExprV v
p
  pprintPrec Int
_ Tidy
k (PExist [(Symbol, Sort)]
xts ExprV v
p)  = Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
forall v.
(Ord v, Fixpoint v, PPrint v) =>
Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
pprintQuant Tidy
k Doc
"exists" [(Symbol, Sort)]
xts ExprV v
p
  pprintPrec Int
_ Tidy
k (ELam (Symbol
x,Sort
t) ExprV v
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 -> ExprV v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ExprV v
e
  pprintPrec Int
_ Tidy
k (ECoerc Sort
a Sort
t ExprV v
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 -> ExprV v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ExprV v
e
  pprintPrec Int
_ Tidy
_ p :: ExprV v
p@PKVar{}    = ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
p
  pprintPrec Int
_ Tidy
_ (ETApp ExprV v
e Sort
s)     = Doc
"ETApp" Doc -> Doc -> Doc
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s
  pprintPrec Int
_ Tidy
_ (ETAbs ExprV v
e Symbol
s)     = Doc
"ETAbs" Doc -> Doc -> Doc
<+> ExprV v -> Doc
forall a. Fixpoint a => a -> Doc
toFix ExprV v
e Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
s
  pprintPrec Int
z Tidy
k (PGrad KVar
x SubstV v
_ GradInfo
_ ExprV v
e) = Int -> Tidy -> ExprV v -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k ExprV v
e Doc -> Doc -> Doc
<+> Doc
"&&" Doc -> Doc -> Doc
<+> KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix KVar
x -- "??"

pprintQuant
  :: (Ord v, Fixpoint v, PPrint v)
  => Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
pprintQuant :: forall v.
(Ord v, Fixpoint v, PPrint v) =>
Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc
pprintQuant Tidy
k Doc
d [(Symbol, Sort)]
xts ExprV v
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 -> ExprV v -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ExprV v
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 :: (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc
pprintReft :: forall v. (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc
pprintReft Tidy
k (Reft (Symbol
_,ExprV v
ra)) = Int -> Tidy -> Doc -> Doc -> [ExprV v] -> Doc
forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin Int
z Tidy
k Doc
trueD Doc
andD [ExprV v]
flat
  where
    flat :: [ExprV v]
flat = [ExprV v] -> [ExprV v]
forall v. [ExprV v] -> [ExprV v]
flattenRefas [ExprV v
ra]
    z :: Int
z    = if [ExprV v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprV v]
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 -> ExprV Symbol
expr (RR Sort
_ Reft
r) = Reft -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
expr Reft
r

instance Expression Reft where
  expr :: Reft -> ExprV Symbol
expr (Reft(Symbol
_, ExprV Symbol
e)) = ExprV Symbol
e

instance Expression Expr where
  expr :: ExprV Symbol -> ExprV Symbol
expr = ExprV Symbol -> ExprV Symbol
forall a. a -> a
id

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

instance Expression Symbol where
  expr :: Symbol -> ExprV Symbol
expr Symbol
s = Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar Symbol
s

instance Expression Text where
  expr :: Text -> ExprV Symbol
expr = SymConst -> ExprV Symbol
forall v. SymConst -> ExprV v
ESym (SymConst -> ExprV Symbol)
-> (Text -> SymConst) -> Text -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> SymConst
SL

instance Expression Integer where
  expr :: Integer -> ExprV Symbol
expr = Constant -> ExprV Symbol
forall v. Constant -> ExprV v
ECon (Constant -> ExprV Symbol)
-> (Integer -> Constant) -> Integer -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Constant
I

instance Expression Int where
  expr :: Int -> ExprV Symbol
expr = Integer -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
expr (Integer -> ExprV Symbol)
-> (Int -> Integer) -> Int -> ExprV Symbol
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 -> ExprV Symbol
prop = Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eProp

instance Predicate Expr where
  prop :: ExprV Symbol -> ExprV Symbol
prop = ExprV Symbol -> ExprV Symbol
forall a. a -> a
id

instance Predicate Bool where
  prop :: Bool -> ExprV Symbol
prop Bool
True  = ExprV Symbol
forall v. ExprV v
PTrue
  prop Bool
False = ExprV Symbol
forall v. ExprV v
PFalse

instance Expression a => Expression (Located a) where
  expr :: Located a -> ExprV Symbol
expr   = a -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
expr (a -> ExprV Symbol)
-> (Located a -> a) -> Located a -> ExprV Symbol
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 -> ExprV Symbol
eVar = Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol) -> (a -> Symbol) -> a -> ExprV Symbol
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 -> ExprV Symbol
eProp = ExprV Symbol -> ExprV Symbol
mkProp (ExprV Symbol -> ExprV Symbol)
-> (a -> ExprV Symbol) -> a -> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar

isSingletonExpr :: Symbol -> Expr -> Maybe Expr
isSingletonExpr :: Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingletonExpr Symbol
v (PAtom Brel
r ExprV Symbol
e1 ExprV Symbol
e2)
  | ExprV Symbol
e1 ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v Bool -> Bool -> Bool
&& Brel -> Bool
isEq Brel
r = ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
e2
  | ExprV Symbol
e2 ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v Bool -> Bool -> Bool
&& Brel -> Bool
isEq Brel
r = ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
e1
isSingletonExpr Symbol
v (PIff ExprV Symbol
e1 ExprV Symbol
e2)
  | ExprV Symbol
e1 ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v           = ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
e2
  | ExprV Symbol
e2 ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v           = ExprV Symbol -> Maybe (ExprV Symbol)
forall a. a -> Maybe a
Just ExprV Symbol
e1
isSingletonExpr Symbol
_ ExprV Symbol
_        = Maybe (ExprV Symbol)
forall a. Maybe a
Nothing

-- | 'conj' is a fast version of 'pAnd' needed for the ebind tests
conj :: [Pred] -> Pred
conj :: [ExprV Symbol] -> ExprV Symbol
conj []  = ExprV Symbol
forall v. ExprV v
PFalse
conj [ExprV Symbol
p] = ExprV Symbol
p
conj [ExprV Symbol]
ps  = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd [ExprV Symbol]
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     :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd :: forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd          = ExprV v -> ExprV v
forall a. Fixpoint a => a -> a
simplify (ExprV v -> ExprV v)
-> (ListNE (ExprV v) -> ExprV v) -> ListNE (ExprV v) -> ExprV v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListNE (ExprV v) -> ExprV v
forall v. [ExprV v] -> ExprV v
PAnd

pAndNoDedup :: ListNE Pred -> Pred
pAndNoDedup :: [ExprV Symbol] -> ExprV Symbol
pAndNoDedup = ([ExprV Symbol] -> [ExprV Symbol]) -> ExprV Symbol -> ExprV Symbol
forall v. Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v
simplifyExpr [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> a
id (ExprV Symbol -> ExprV Symbol)
-> ([ExprV Symbol] -> ExprV Symbol)
-> [ExprV Symbol]
-> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd

pOr :: forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pOr           = ExprV v -> ExprV v
forall a. Fixpoint a => a -> a
simplify (ExprV v -> ExprV v)
-> (ListNE (ExprV v) -> ExprV v) -> ListNE (ExprV v) -> ExprV v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListNE (ExprV v) -> ExprV v
forall v. [ExprV v] -> ExprV v
POr

infixl 9 &.&
(&.&) :: Pred -> Pred -> Pred
&.& :: ExprV Symbol -> ExprV Symbol -> ExprV Symbol
(&.&) ExprV Symbol
p ExprV Symbol
q = [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV Symbol
p, ExprV Symbol
q]

infixl 9 |.|
(|.|) :: Pred -> Pred -> Pred
|.| :: ExprV Symbol -> ExprV Symbol -> ExprV Symbol
(|.|) ExprV Symbol
p ExprV Symbol
q = [ExprV Symbol] -> ExprV Symbol
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pOr [ExprV Symbol
p, ExprV Symbol
q]

pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v
pIte :: forall v.
(Fixpoint v, Ord v) =>
ExprV v -> ExprV v -> ExprV v -> ExprV v
pIte ExprV v
p1 ExprV v
p2 ExprV v
p3 = ListNE (ExprV v) -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV v
p1 ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
`PImp` ExprV v
p2, ExprV v -> ExprV v
forall v. ExprV v -> ExprV v
PNot ExprV v
p1 ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
`PImp` ExprV v
p3]

pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v
pExist :: forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
pExist []  ExprV v
p = ExprV v
p
pExist [(Symbol, Sort)]
xts ExprV v
p = [(Symbol, Sort)] -> ExprV v -> ExprV v
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xts ExprV v
p

mkProp :: Expr -> Pred
mkProp :: ExprV Symbol -> ExprV Symbol
mkProp = ExprV Symbol -> ExprV Symbol
forall a. a -> a
id

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

isSingletonReft :: Reft -> Maybe Expr
isSingletonReft :: Reft -> Maybe (ExprV Symbol)
isSingletonReft (Reft (Symbol
v, ExprV Symbol
ra)) = (ExprV Symbol -> Maybe (ExprV Symbol))
-> [ExprV Symbol] -> Maybe (ExprV Symbol)
forall a b. (a -> Maybe b) -> [a] -> Maybe b
firstMaybe (Symbol -> ExprV Symbol -> Maybe (ExprV Symbol)
isSingletonExpr Symbol
v) ([ExprV Symbol] -> Maybe (ExprV Symbol))
-> [ExprV Symbol] -> Maybe (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> [ExprV Symbol]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts ExprV Symbol
ra

relReft :: (Expression a) => Brel -> a -> Reft
relReft :: forall a. Expression a => Brel -> a -> Reft
relReft Brel
r a
e   = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
vv_, Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar Symbol
vv_)  (a -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
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, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
vv_, ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eProp Symbol
vv_) (a -> ExprV Symbol
forall a. Predicate a => a -> ExprV Symbol
prop a
p))

predReft      :: (Predicate a) => a -> Reft
predReft :: forall a. Predicate a => a -> Reft
predReft a
p    = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
vv_, a -> ExprV Symbol
forall a. Predicate a => a -> ExprV Symbol
prop a
p)

reft :: Symbol -> ExprV v -> ReftV v
reft :: forall v. Symbol -> ExprV v -> ReftV v
reft Symbol
v ExprV v
p = (Symbol, ExprV v) -> ReftV v
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, ExprV v
p)

mapPredReft :: (Expr -> Expr) -> Reft -> Reft
mapPredReft :: (ExprV Symbol -> ExprV Symbol) -> Reft -> Reft
mapPredReft ExprV Symbol -> ExprV Symbol
f (Reft (Symbol
v, ExprV Symbol
p)) = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
v, ExprV Symbol -> ExprV Symbol
f ExprV Symbol
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 :: SortedReft -> Bool
isNonTrivial :: SortedReft -> Bool
isNonTrivial = Bool -> Bool
not (Bool -> Bool) -> (SortedReft -> Bool) -> SortedReft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reft -> Bool
forall v. Eq v => ReftV v -> Bool
isTautoReft (Reft -> Bool) -> (SortedReft -> Reft) -> SortedReft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft

isTautoReft :: Eq v => ReftV v -> Bool
isTautoReft :: forall v. Eq v => ReftV v -> Bool
isTautoReft = (ExprV v -> Bool) -> [ExprV v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ([ExprV v] -> Bool) -> (ReftV v -> [ExprV v]) -> ReftV v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV v -> [ExprV v]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts (ExprV v -> [ExprV v])
-> (ReftV v -> ExprV v) -> ReftV v -> [ExprV v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReftV v -> ExprV v
forall v. ReftV v -> ExprV v
reftPred

reftPred :: ReftV v -> ExprV v
reftPred :: forall v. ReftV v -> ExprV v
reftPred (Reft (Symbol
_, ExprV v
p)) = ExprV v
p

reftBind :: ReftV v -> Symbol
reftBind :: forall v. ReftV v -> Symbol
reftBind (Reft (Symbol
x, ExprV v
_)) = Symbol
x

------------------------------------------------------------
-- | Gradual Type Manipulation  ----------------------------
------------------------------------------------------------
pGAnds :: (Fixpoint v, Ord v) => [ExprV v] -> ExprV v
pGAnds :: forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pGAnds = (ExprV v -> ExprV v -> ExprV v) -> ExprV v -> [ExprV v] -> ExprV v
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ExprV v -> ExprV v -> ExprV v
forall v. (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v
pGAnd ExprV v
forall v. ExprV v
PTrue

pGAnd :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v
pGAnd :: forall v. (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v
pGAnd (PGrad KVar
k SubstV v
su GradInfo
i ExprV v
p) ExprV v
q = KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV v
su GradInfo
i (ListNE (ExprV v) -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV v
p, ExprV v
q])
pGAnd ExprV v
p (PGrad KVar
k SubstV v
su GradInfo
i ExprV v
q) = KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV v
su GradInfo
i (ListNE (ExprV v) -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV v
p, ExprV v
q])
pGAnd ExprV v
p ExprV v
q              = ListNE (ExprV v) -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [ExprV v
p,ExprV v
q]

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

symbolReft    :: (Symbolic a) => a -> Reft
symbolReft :: forall a. Symbolic a => a -> Reft
symbolReft    = ExprV Symbol -> Reft
forall a. Expression a => a -> Reft
exprReft (ExprV Symbol -> Reft) -> (a -> ExprV Symbol) -> a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar

usymbolReft   :: (Symbolic a) => a -> Reft
usymbolReft :: forall a. Symbolic a => a -> Reft
usymbolReft   = ExprV Symbol -> Reft
forall a. Expression a => a -> Reft
uexprReft (ExprV Symbol -> Reft) -> (a -> ExprV Symbol) -> a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
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
forall v. ReftV v
trueReft)

trueReft, falseReft :: ReftV v
trueReft :: forall v. ReftV v
trueReft  = (Symbol, ExprV v) -> ReftV v
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
vv_, ExprV v
forall v. ExprV v
PTrue)
falseReft :: forall v. ReftV v
falseReft = (Symbol, ExprV v) -> ReftV v
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
vv_, ExprV v
forall v. ExprV v
PFalse)

flattenRefas :: [ExprV v] -> [ExprV v]
flattenRefas :: forall v. [ExprV v] -> [ExprV v]
flattenRefas        = [ExprV v] -> [ExprV v] -> [ExprV v]
forall {v}. [ExprV v] -> [ExprV v] -> [ExprV v]
flatP []
  where
    flatP :: [ExprV v] -> [ExprV v] -> [ExprV v]
flatP [ExprV v]
acc (PAnd [ExprV v]
ps:[ExprV v]
xs) = [ExprV v] -> [ExprV v] -> [ExprV v]
flatP ([ExprV v] -> [ExprV v] -> [ExprV v]
flatP [ExprV v]
acc [ExprV v]
xs) [ExprV v]
ps
    flatP [ExprV v]
acc (ExprV v
p:[ExprV v]
xs)       = ExprV v
p ExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
: [ExprV v] -> [ExprV v] -> [ExprV v]
flatP [ExprV v]
acc [ExprV v]
xs
    flatP [ExprV v]
acc []           = [ExprV v]
acc

conjuncts :: Eq v => ExprV v -> [ExprV v]
conjuncts :: forall v. Eq v => ExprV v -> [ExprV v]
conjuncts (PAnd [ExprV v]
ps) = (ExprV v -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV v -> [ExprV v]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts [ExprV v]
ps
conjuncts ExprV v
p
  | ExprV v -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV v
p   = []
  | Bool
otherwise       = [ExprV v
p]


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

class Falseable a where
  isFalse :: a -> Bool

instance Falseable Expr where
  isFalse :: ExprV Symbol -> Bool
isFalse ExprV Symbol
PFalse = Bool
True
  isFalse ExprV Symbol
_      = Bool
False

instance Falseable Reft where
  isFalse :: Reft -> Bool
isFalse (Reft (Symbol
_, ExprV Symbol
ra)) = ExprV Symbol -> Bool
forall a. Falseable a => a -> Bool
isFalse ExprV Symbol
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, ExprV Symbol
e) = Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst (HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$ [(Symbol, ExprV Symbol)] -> HashMap Symbol (ExprV Symbol)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol
x,ExprV Symbol
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 -> ExprV Symbol) -> Located a -> Located a
substf Symbol -> ExprV 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 -> ExprV Symbol) -> a -> a
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
substf Symbol -> ExprV Symbol
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)

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