{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE ViewPatterns               #-}

{-# OPTIONS_GHC -Wno-orphans            #-}

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

module Language.Fixpoint.Types.Refinements (

  -- * Representing Terms
    SymConst (..)
  , Constant (..)
  , Bop (..)
  , Brel (..)
  , Expr (..), Pred
  , GradInfo (..)
  , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot
  , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv
  , pattern EEq
  , KVar (..)
  , Subst (..)
  , KVSub (..)
  , Reft (..)
  , SortedReft (..)

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

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

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

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

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

  -- * Transforming
  , mapPredReft
  , onEverySubexpr
  , pprintReft

  , debruijnIndex

  -- * Gradual Type Manipulation
  , pGAnds, pGAnd
  , HasGradual (..)
  , srcGradInfo

  ) where

import           Prelude hiding ((<>))
import           Data.Bifunctor (second)
import qualified Data.Store as S
import           Data.Generics             (Data, gmapT, mkT, extT)
import           Data.Typeable             (Typeable)
import           Data.Hashable
import           Data.HashMap.Strict         (HashMap)
import qualified Data.HashMap.Strict       as HashMap
import           Data.HashSet              (HashSet)
import qualified Data.HashSet              as HashSet
import           GHC.Generics              (Generic)
import           Data.List                 (foldl', partition)
import qualified Data.Set                  as Set
import           Data.String
import           Data.Text                 (Text)
import qualified Data.Text                 as T
import qualified Data.HashMap.Strict       as M
import           Control.DeepSeq
import           Data.Maybe                (isJust)
import           Language.Fixpoint.Types.Names
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Types.Sorts
import           Language.Fixpoint.Misc
import           Text.PrettyPrint.HughesPJ.Compat
import qualified Data.Binary as B

-- import           Text.Printf               (printf)


instance NFData KVar
instance NFData Subst
instance NFData GradInfo
instance NFData Constant
instance NFData SymConst
instance NFData Brel
instance NFData Bop
instance NFData Expr
instance NFData Reft
instance NFData SortedReft

-- instance (Hashable k, Eq k, S.Store k, S.Store v) => S.Store (M.HashMap k v) where
  -- put = B.put . M.toList
  -- get = M.fromList <$> B.get

instance S.Store KVar
instance S.Store Subst
instance S.Store GradInfo
instance S.Store Constant
instance S.Store SymConst
instance S.Store Brel
instance S.Store Bop
instance S.Store Expr
instance S.Store Reft
instance S.Store SortedReft

instance B.Binary SymConst
instance B.Binary Constant
instance B.Binary Bop
instance B.Binary GradInfo
instance B.Binary Brel
instance B.Binary KVar
instance (Hashable a, Eq a, B.Binary a) => B.Binary (HashSet a) where
  put :: HashSet a -> Put
put = forall t. Binary t => t -> Put
B.put forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> [a]
HashSet.toList
  get :: Get (HashSet a)
get = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HashSet.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall t. Binary t => t -> Put
B.put forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList
  get :: Get (HashMap k v)
get = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Binary t => Get t
B.get

instance B.Binary Subst
instance B.Binary Expr
instance B.Binary Reft


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

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

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

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

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

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


instance HasGradual Reft where
  isGradual :: Reft -> Bool
isGradual (Reft (Symbol
_,Expr
r)) = forall a. HasGradual a => a -> Bool
isGradual Expr
r
  gVars :: Reft -> [KVar]
gVars (Reft (Symbol
_,Expr
r))     = forall a. HasGradual a => a -> [KVar]
gVars Expr
r
  ungrad :: Reft -> Reft
ungrad (Reft (Symbol
x,Expr
r))    = (Symbol, Expr) -> Reft
Reft(Symbol
x, forall a. HasGradual a => a -> a
ungrad Expr
r)

instance HasGradual SortedReft where
  isGradual :: SortedReft -> Bool
isGradual = forall a. HasGradual a => a -> Bool
isGradual forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
  gVars :: SortedReft -> [KVar]
gVars     = forall a. HasGradual a => a -> [KVar]
gVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
  ungrad :: SortedReft -> SortedReft
ungrad SortedReft
r  = SortedReft
r {sr_reft :: Reft
sr_reft = forall a. HasGradual a => a -> a
ungrad (SortedReft -> Reft
sr_reft SortedReft
r)}

refaConjuncts :: Expr -> [Expr]
refaConjuncts :: Expr -> [Expr]
refaConjuncts Expr
p = [Expr
p' | Expr
p' <- Expr -> [Expr]
conjuncts Expr
p, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isTautoPred Expr
p']



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

newtype KVar = KV { KVar -> Symbol
kv :: Symbol }
               deriving (KVar -> KVar -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KVar -> KVar -> Bool
$c/= :: KVar -> KVar -> Bool
== :: KVar -> KVar -> Bool
$c== :: KVar -> KVar -> Bool
Eq, Eq 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
min :: KVar -> KVar -> KVar
$cmin :: KVar -> KVar -> KVar
max :: KVar -> KVar -> KVar
$cmax :: KVar -> KVar -> KVar
>= :: KVar -> KVar -> Bool
$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
compare :: KVar -> KVar -> Ordering
$ccompare :: KVar -> KVar -> Ordering
Ord, Typeable KVar
KVar -> DataType
KVar -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVar -> m KVar
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> KVar -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KVar -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r
gmapT :: (forall b. Data b => b -> b) -> KVar -> KVar
$cgmapT :: (forall b. Data b => b -> b) -> KVar -> KVar
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVar)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVar)
dataTypeOf :: KVar -> DataType
$cdataTypeOf :: KVar -> DataType
toConstr :: KVar -> Constr
$ctoConstr :: KVar -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVar
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVar
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar
Data, Typeable, 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
$cto :: forall x. Rep KVar x -> KVar
$cfrom :: forall x. KVar -> Rep KVar x
Generic, String -> KVar
forall a. (String -> a) -> IsString a
fromString :: String -> KVar
$cfromString :: String -> KVar
IsString)

intKvar :: Integer -> KVar
intKvar :: Integer -> KVar
intKvar = Symbol -> KVar
KV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"k_"

instance Show KVar where
  show :: KVar -> String
show (KV Symbol
x) = String
"$" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Symbol
x

instance Hashable KVar
instance Hashable Brel
instance Hashable Bop
instance Hashable SymConst
instance Hashable Constant
instance Hashable GradInfo
instance Hashable Subst
instance Hashable Expr
instance Hashable Reft

--------------------------------------------------------------------------------
-- | Substitutions -------------------------------------------------------------
--------------------------------------------------------------------------------
newtype Subst = Su (M.HashMap Symbol Expr)
                deriving (Subst -> Subst -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c== :: Subst -> Subst -> Bool
Eq, Typeable Subst
Subst -> DataType
Subst -> Constr
(forall b. Data b => b -> b) -> Subst -> Subst
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
forall u. (forall d. Data d => d -> u) -> Subst -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Subst -> m Subst
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Subst -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Subst -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r
gmapT :: (forall b. Data b => b -> b) -> Subst -> Subst
$cgmapT :: (forall b. Data b => b -> b) -> Subst -> Subst
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Subst)
dataTypeOf :: Subst -> DataType
$cdataTypeOf :: Subst -> DataType
toConstr :: Subst -> Constr
$ctoConstr :: Subst -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Subst
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
Data, Eq Subst
Subst -> Subst -> Bool
Subst -> Subst -> Ordering
Subst -> Subst -> Subst
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Subst -> Subst -> Subst
$cmin :: Subst -> Subst -> Subst
max :: Subst -> Subst -> Subst
$cmax :: Subst -> Subst -> Subst
>= :: Subst -> Subst -> Bool
$c>= :: Subst -> Subst -> Bool
> :: Subst -> Subst -> Bool
$c> :: Subst -> Subst -> Bool
<= :: Subst -> Subst -> Bool
$c<= :: Subst -> Subst -> Bool
< :: Subst -> Subst -> Bool
$c< :: Subst -> Subst -> Bool
compare :: Subst -> Subst -> Ordering
$ccompare :: Subst -> Subst -> Ordering
Ord, Typeable, forall x. Rep Subst x -> Subst
forall x. Subst -> Rep Subst x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Subst x -> Subst
$cfrom :: forall x. Subst -> Rep Subst x
Generic)

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

instance Fixpoint Subst where
  toFix :: Subst -> Doc
toFix (Su HashMap Symbol Expr
m) = case forall a b. Ord a => HashMap a b -> [(a, b)]
hashMapToAscList HashMap Symbol Expr
m of
                   []  -> Doc
empty
                   [(Symbol, Expr)]
xys -> [Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
x,Expr
y) -> Doc -> Doc
brackets forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<-> String -> Doc
text String
":=" Doc -> Doc -> Doc
<-> forall a. Fixpoint a => a -> Doc
toFix Expr
y) [(Symbol, Expr)]
xys

instance PPrint Subst where
  pprintTidy :: Tidy -> Subst -> Doc
pprintTidy Tidy
_ = 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KVSub -> KVSub -> Bool
$c/= :: KVSub -> KVSub -> Bool
== :: KVSub -> KVSub -> Bool
$c== :: KVSub -> KVSub -> Bool
Eq, Typeable KVSub
KVSub -> DataType
KVSub -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> KVSub -> m KVSub
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> KVSub -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KVSub -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r
gmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub
$cgmapT :: (forall b. Data b => b -> b) -> KVSub -> KVSub
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVSub)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c KVSub)
dataTypeOf :: KVSub -> DataType
$cdataTypeOf :: KVSub -> DataType
toConstr :: KVSub -> Constr
$ctoConstr :: KVSub -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVSub
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c KVSub
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub
Data, Typeable, 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
$cto :: forall x. Rep KVSub x -> KVSub
$cfrom :: forall x. KVSub -> Rep KVSub x
Generic, Int -> KVSub -> ShowS
[KVSub] -> ShowS
KVSub -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KVSub] -> ShowS
$cshowList :: [KVSub] -> ShowS
show :: KVSub -> String
$cshow :: KVSub -> String
showsPrec :: Int -> KVSub -> ShowS
$cshowsPrec :: Int -> KVSub -> ShowS
Show)

instance PPrint KVSub where
  pprintTidy :: Tidy -> KVSub -> Doc
pprintTidy Tidy
k KVSub
ksu = 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymConst -> SymConst -> Bool
$c/= :: SymConst -> SymConst -> Bool
== :: SymConst -> SymConst -> Bool
$c== :: SymConst -> SymConst -> Bool
Eq, Eq 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
min :: SymConst -> SymConst -> SymConst
$cmin :: SymConst -> SymConst -> SymConst
max :: SymConst -> SymConst -> SymConst
$cmax :: SymConst -> SymConst -> SymConst
>= :: SymConst -> SymConst -> Bool
$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
compare :: SymConst -> SymConst -> Ordering
$ccompare :: SymConst -> SymConst -> Ordering
Ord, Int -> SymConst -> ShowS
[SymConst] -> ShowS
SymConst -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymConst] -> ShowS
$cshowList :: [SymConst] -> ShowS
show :: SymConst -> String
$cshow :: SymConst -> String
showsPrec :: Int -> SymConst -> ShowS
$cshowsPrec :: Int -> SymConst -> ShowS
Show, Typeable SymConst
SymConst -> DataType
SymConst -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SymConst -> m SymConst
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SymConst -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymConst -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SymConst -> r
gmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst
$cgmapT :: (forall b. Data b => b -> b) -> SymConst -> SymConst
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymConst)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SymConst)
dataTypeOf :: SymConst -> DataType
$cdataTypeOf :: SymConst -> DataType
toConstr :: SymConst -> Constr
$ctoConstr :: SymConst -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymConst
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SymConst
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst
Data, Typeable, 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
$cto :: forall x. Rep SymConst x -> SymConst
$cfrom :: forall x. SymConst -> Rep SymConst x
Generic)

data Constant = I !Integer
              | R !Double
              | L !Text !Sort
              deriving (Constant -> Constant -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constant -> Constant -> Bool
$c/= :: Constant -> Constant -> Bool
== :: Constant -> Constant -> Bool
$c== :: Constant -> Constant -> Bool
Eq, Eq 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
min :: Constant -> Constant -> Constant
$cmin :: Constant -> Constant -> Constant
max :: Constant -> Constant -> Constant
$cmax :: Constant -> Constant -> Constant
>= :: Constant -> Constant -> Bool
$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
compare :: Constant -> Constant -> Ordering
$ccompare :: Constant -> Constant -> Ordering
Ord, Int -> Constant -> ShowS
[Constant] -> ShowS
Constant -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constant] -> ShowS
$cshowList :: [Constant] -> ShowS
show :: Constant -> String
$cshow :: Constant -> String
showsPrec :: Int -> Constant -> ShowS
$cshowsPrec :: Int -> Constant -> ShowS
Show, Typeable Constant
Constant -> DataType
Constant -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constant -> m Constant
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Constant -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Constant -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constant -> r
gmapT :: (forall b. Data b => b -> b) -> Constant -> Constant
$cgmapT :: (forall b. Data b => b -> b) -> Constant -> Constant
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constant)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constant)
dataTypeOf :: Constant -> DataType
$cdataTypeOf :: Constant -> DataType
toConstr :: Constant -> Constr
$ctoConstr :: Constant -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constant
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constant
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant
Data, Typeable, 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
$cto :: forall x. Rep Constant x -> Constant
$cfrom :: forall x. Constant -> Rep Constant x
Generic)

data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une
            deriving (Brel -> Brel -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Brel -> Brel -> Bool
$c/= :: Brel -> Brel -> Bool
== :: Brel -> Brel -> Bool
$c== :: Brel -> Brel -> Bool
Eq, Eq 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
min :: Brel -> Brel -> Brel
$cmin :: Brel -> Brel -> Brel
max :: Brel -> Brel -> Brel
$cmax :: Brel -> Brel -> Brel
>= :: Brel -> Brel -> Bool
$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
compare :: Brel -> Brel -> Ordering
$ccompare :: Brel -> Brel -> Ordering
Ord, Int -> Brel -> ShowS
[Brel] -> ShowS
Brel -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Brel] -> ShowS
$cshowList :: [Brel] -> ShowS
show :: Brel -> String
$cshow :: Brel -> String
showsPrec :: Int -> Brel -> ShowS
$cshowsPrec :: Int -> Brel -> ShowS
Show, Typeable Brel
Brel -> DataType
Brel -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Brel -> m Brel
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Brel -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Brel -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r
gmapT :: (forall b. Data b => b -> b) -> Brel -> Brel
$cgmapT :: (forall b. Data b => b -> b) -> Brel -> Brel
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Brel)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Brel)
dataTypeOf :: Brel -> DataType
$cdataTypeOf :: Brel -> DataType
toConstr :: Brel -> Constr
$ctoConstr :: Brel -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Brel
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Brel
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel
Data, Typeable, 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
$cto :: forall x. Rep Brel x -> Brel
$cfrom :: forall x. Brel -> Rep Brel x
Generic)

data Bop  = Plus | Minus | Times | Div | Mod | RTimes | RDiv
            deriving (Bop -> Bop -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bop -> Bop -> Bool
$c/= :: Bop -> Bop -> Bool
== :: Bop -> Bop -> Bool
$c== :: Bop -> Bop -> Bool
Eq, Eq 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
min :: Bop -> Bop -> Bop
$cmin :: Bop -> Bop -> Bop
max :: Bop -> Bop -> Bop
$cmax :: Bop -> Bop -> Bop
>= :: Bop -> Bop -> Bool
$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
compare :: Bop -> Bop -> Ordering
$ccompare :: Bop -> Bop -> Ordering
Ord, Int -> Bop -> ShowS
[Bop] -> ShowS
Bop -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Bop] -> ShowS
$cshowList :: [Bop] -> ShowS
show :: Bop -> String
$cshow :: Bop -> String
showsPrec :: Int -> Bop -> ShowS
$cshowsPrec :: Int -> Bop -> ShowS
Show, Typeable Bop
Bop -> DataType
Bop -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Bop -> m Bop
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Bop -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Bop -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r
gmapT :: (forall b. Data b => b -> b) -> Bop -> Bop
$cgmapT :: (forall b. Data b => b -> b) -> Bop -> Bop
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bop)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Bop)
dataTypeOf :: Bop -> DataType
$cdataTypeOf :: Bop -> DataType
toConstr :: Bop -> Constr
$ctoConstr :: Bop -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bop
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Bop
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop
Data, Typeable, 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
$cto :: forall x. Rep Bop x -> Bop
$cfrom :: forall x. Bop -> Rep Bop x
Generic)
            -- NOTE: For "Mod" 2nd expr should be a constant or a var *)

data Expr = ESym !SymConst
          | ECon !Constant
          | EVar !Symbol
          | EApp !Expr !Expr
          | ENeg !Expr
          | EBin !Bop !Expr !Expr
          | EIte !Expr !Expr !Expr
          | ECst !Expr !Sort
          | ELam !(Symbol, Sort)   !Expr
          | ETApp !Expr !Sort
          | ETAbs !Expr !Symbol
          | PAnd   ![Expr]
          | POr    ![Expr]
          | PNot   !Expr
          | PImp   !Expr !Expr
          | PIff   !Expr !Expr
          | PAtom  !Brel  !Expr !Expr
          | PKVar  !KVar !Subst
          | PAll   ![(Symbol, Sort)] !Expr
          | PExist ![(Symbol, Sort)] !Expr
          | PGrad  !KVar !Subst !GradInfo !Expr
          | ECoerc !Sort !Sort !Expr
          deriving (Expr -> Expr -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq, Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, Eq Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
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
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
Ord, Typeable Expr
Expr -> DataType
Expr -> Constr
(forall b. Data b => b -> b) -> Expr -> Expr
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) -> Expr -> u
forall u. (forall d. Data d => d -> u) -> Expr -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Expr)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Expr -> m Expr
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Expr -> r
gmapT :: (forall b. Data b => b -> b) -> Expr -> Expr
$cgmapT :: (forall b. Data b => b -> b) -> Expr -> Expr
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Expr)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Expr)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Expr)
dataTypeOf :: Expr -> DataType
$cdataTypeOf :: Expr -> DataType
toConstr :: Expr -> Constr
$ctoConstr :: Expr -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Expr
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
Data, Typeable, forall x. Rep Expr x -> Expr
forall x. Expr -> Rep Expr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Expr x -> Expr
$cfrom :: forall x. Expr -> Rep Expr x
Generic)

onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr
onEverySubexpr = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Data a => (forall b. Data b => b -> b) -> a -> a
gmapT (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT a -> a
go forall a b.
(Typeable a, Typeable b) =>
(a -> a) -> (b -> b) -> a -> a
`extT` forall a b. (a -> b) -> [a] -> [b]
map a -> a
go)

type Pred = Expr

pattern PTrue :: Expr
pattern $bPTrue :: Expr
$mPTrue :: forall {r}. Expr -> ((# #) -> r) -> ((# #) -> r) -> r
PTrue = PAnd []

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

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

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

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

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

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

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

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

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

substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr
substSortInExpr :: (Symbol -> Sort) -> Expr -> Expr
substSortInExpr Symbol -> Sort
f = (Expr -> Expr) -> Expr -> Expr
onEverySubexpr Expr -> Expr
go
  where
    go :: Expr -> Expr
go = \case
      ELam (Symbol
x, Sort
t) Expr
e -> (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, (Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t) Expr
e
      PAll [(Symbol, Sort)]
xts Expr
e -> [(Symbol, Sort)] -> Expr -> Expr
PAll (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) Expr
e
      PExist [(Symbol, Sort)]
xts Expr
e -> [(Symbol, Sort)] -> Expr -> Expr
PExist (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts) Expr
e
      ECst Expr
e Sort
t -> Expr -> Sort -> Expr
ECst Expr
e ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t)
      ECoerc Sort
t0 Sort
t1 Expr
e -> Sort -> Sort -> Expr -> Expr
ECoerc ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t0) ((Symbol -> Sort) -> Sort -> Sort
substSort Symbol -> Sort
f Sort
t1) Expr
e
      Expr
e -> Expr
e

exprKVars :: Expr -> HashMap KVar [Subst]
exprKVars :: Expr -> HashMap KVar [Subst]
exprKVars = Expr -> HashMap KVar [Subst]
go
  where
    gos :: [Expr] -> HashMap KVar [Subst]
gos [Expr]
es                = forall k v. (Eq k, Hashable k) => [HashMap k v] -> HashMap k v
HashMap.unions (Expr -> HashMap KVar [Subst]
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go :: Expr -> HashMap KVar [Subst]
go (EVar Symbol
_)           = forall k v. HashMap k v
HashMap.empty
    go (EApp Expr
f Expr
e)         = [Expr] -> HashMap KVar [Subst]
gos [Expr
f, Expr
e]
    go (ELam (Symbol, Sort)
_ Expr
e)     = Expr -> HashMap KVar [Subst]
go Expr
e
    go (ECoerc Sort
_ Sort
_ Expr
e)     = Expr -> HashMap KVar [Subst]
go Expr
e
    go (ENeg Expr
e)           = Expr -> HashMap KVar [Subst]
go Expr
e
    go (EBin Bop
_ Expr
e1 Expr
e2)     = [Expr] -> HashMap KVar [Subst]
gos [Expr
e1, Expr
e2]
    go (EIte Expr
p Expr
e1 Expr
e2)     = [Expr] -> HashMap KVar [Subst]
gos [Expr
p, Expr
e1, Expr
e2]
    go (ECst Expr
e Sort
_)         = Expr -> HashMap KVar [Subst]
go Expr
e
    go (PAnd [Expr]
ps)          = [Expr] -> HashMap KVar [Subst]
gos [Expr]
ps
    go (POr [Expr]
ps)           = [Expr] -> HashMap KVar [Subst]
gos [Expr]
ps
    go (PNot Expr
p)           = Expr -> HashMap KVar [Subst]
go Expr
p
    go (PIff Expr
p1 Expr
p2)       = [Expr] -> HashMap KVar [Subst]
gos [Expr
p1, Expr
p2]
    go (PImp Expr
p1 Expr
p2)       = [Expr] -> HashMap KVar [Subst]
gos [Expr
p1, Expr
p2]
    go (PAtom Brel
_ Expr
e1 Expr
e2)    = [Expr] -> HashMap KVar [Subst]
gos [Expr
e1, Expr
e2]
    go (PKVar KVar
k substs :: Subst
substs@(Su HashMap Symbol Expr
su))  =
      forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HashMap.insertWith forall a. [a] -> [a] -> [a]
(++) KVar
k [Subst
substs] forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [HashMap k v] -> HashMap k v
HashMap.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Expr -> HashMap KVar [Subst]
exprKVars (forall k v. HashMap k v -> [v]
M.elems HashMap Symbol Expr
su)
    go (PAll [(Symbol, Sort)]
_xts Expr
p)       = Expr -> HashMap KVar [Subst]
go Expr
p
    go (PExist [(Symbol, Sort)]
_xts Expr
p)     = Expr -> HashMap KVar [Subst]
go Expr
p
    go Expr
_                  = 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GradInfo -> GradInfo -> Bool
$c/= :: GradInfo -> GradInfo -> Bool
== :: GradInfo -> GradInfo -> Bool
$c== :: GradInfo -> GradInfo -> Bool
Eq, Eq 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
min :: GradInfo -> GradInfo -> GradInfo
$cmin :: GradInfo -> GradInfo -> GradInfo
max :: GradInfo -> GradInfo -> GradInfo
$cmax :: GradInfo -> GradInfo -> GradInfo
>= :: GradInfo -> GradInfo -> Bool
$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
compare :: GradInfo -> GradInfo -> Ordering
$ccompare :: GradInfo -> GradInfo -> Ordering
Ord, Int -> GradInfo -> ShowS
[GradInfo] -> ShowS
GradInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GradInfo] -> ShowS
$cshowList :: [GradInfo] -> ShowS
show :: GradInfo -> String
$cshow :: GradInfo -> String
showsPrec :: Int -> GradInfo -> ShowS
$cshowsPrec :: Int -> GradInfo -> ShowS
Show, Typeable GradInfo
GradInfo -> DataType
GradInfo -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> GradInfo -> m GradInfo
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> GradInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GradInfo -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> GradInfo -> r
gmapT :: (forall b. Data b => b -> b) -> GradInfo -> GradInfo
$cgmapT :: (forall b. Data b => b -> b) -> GradInfo -> GradInfo
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GradInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c GradInfo)
dataTypeOf :: GradInfo -> DataType
$cdataTypeOf :: GradInfo -> DataType
toConstr :: GradInfo -> Constr
$ctoConstr :: GradInfo -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GradInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c GradInfo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo
Data, Typeable, 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
$cto :: forall x. Rep GradInfo x -> GradInfo
$cfrom :: forall x. GradInfo -> Rep GradInfo x
Generic)

srcGradInfo :: SourcePos -> GradInfo
srcGradInfo :: SourcePos -> GradInfo
srcGradInfo SourcePos
src = SrcSpan -> Maybe SrcSpan -> GradInfo
GradInfo (SourcePos -> SourcePos -> SrcSpan
SS SourcePos
src SourcePos
src) forall a. Maybe a
Nothing

mkEApp :: LocSymbol -> [Expr] -> Expr
mkEApp :: LocSymbol -> [Expr] -> Expr
mkEApp = Expr -> [Expr] -> Expr
eApps forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Expr
EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val

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

splitEApp :: Expr -> (Expr, [Expr])
splitEApp :: Expr -> (Expr, [Expr])
splitEApp = [Expr] -> Expr -> (Expr, [Expr])
go []
  where
    go :: [Expr] -> Expr -> (Expr, [Expr])
go [Expr]
acc (EApp Expr
f Expr
e) = [Expr] -> Expr -> (Expr, [Expr])
go (Expr
eforall a. a -> [a] -> [a]
:[Expr]
acc) Expr
f
    go [Expr]
acc Expr
e          = (Expr
e, [Expr]
acc)

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

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

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

eAppC :: Sort -> Expr -> Expr -> Expr
eAppC :: Sort -> Expr -> Expr -> Expr
eAppC Sort
s Expr
e1 Expr
e2 = Expr -> Sort -> Expr
eCst (Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2) Sort
s

-- | Eliminates redundant casts
eCst :: Expr -> Sort -> Expr
eCst :: Expr -> Sort -> Expr
eCst Expr
e Sort
t = Expr -> Sort -> Expr
ECst (Expr -> Expr
dropECst Expr
e) Sort
t

--------------------------------------------------------------------------------
debruijnIndex :: Expr -> Int
debruijnIndex :: Expr -> Int
debruijnIndex = forall {a}. Num a => Expr -> a
go
  where
    go :: Expr -> a
go (ELam (Symbol, Sort)
_ Expr
e)      = a
1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e
    go (ECst Expr
e Sort
_)      = Expr -> a
go Expr
e
    go (EApp Expr
e1 Expr
e2)    = Expr -> a
go Expr
e1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (ESym SymConst
_)        = a
1
    go (ECon Constant
_)        = a
1
    go (EVar Symbol
_)        = a
1
    go (ENeg Expr
e)        = Expr -> a
go Expr
e
    go (EBin Bop
_ Expr
e1 Expr
e2)  = Expr -> a
go Expr
e1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (EIte Expr
e Expr
e1 Expr
e2)  = Expr -> a
go Expr
e forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (ETAbs Expr
e Symbol
_)     = Expr -> a
go Expr
e
    go (ETApp Expr
e Sort
_)     = Expr -> a
go Expr
e
    go (PAnd [Expr]
es)       = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\a
n Expr
e -> a
n forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e) a
0 [Expr]
es
    go (POr [Expr]
es)        = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\a
n Expr
e -> a
n forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e) a
0 [Expr]
es
    go (PNot Expr
e)        = Expr -> a
go Expr
e
    go (PImp Expr
e1 Expr
e2)    = Expr -> a
go Expr
e1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (PIff Expr
e1 Expr
e2)    = Expr -> a
go Expr
e1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (PAtom Brel
_ Expr
e1 Expr
e2) = Expr -> a
go Expr
e1 forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (PAll [(Symbol, Sort)]
_ Expr
e)      = Expr -> a
go Expr
e
    go (PExist [(Symbol, Sort)]
_ Expr
e)    = Expr -> a
go Expr
e
    go (PKVar KVar
_ Subst
_)     = a
1
    go (PGrad KVar
_ Subst
_ GradInfo
_ Expr
e) = Expr -> a
go Expr
e
    go (ECoerc Sort
_ Sort
_ Expr
e)  = Expr -> a
go Expr
e

-- | Parsed refinement of @Symbol@ as @Expr@
--   e.g. in '{v: _ | e }' v is the @Symbol@ and e the @Expr@
newtype Reft = Reft (Symbol, Expr)
               deriving (Reft -> Reft -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Reft -> Reft -> Bool
$c/= :: Reft -> Reft -> Bool
== :: Reft -> Reft -> Bool
$c== :: Reft -> Reft -> Bool
Eq, Eq Reft
Reft -> Reft -> Bool
Reft -> Reft -> Ordering
Reft -> Reft -> Reft
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Reft -> Reft -> Reft
$cmin :: Reft -> Reft -> Reft
max :: Reft -> Reft -> Reft
$cmax :: Reft -> Reft -> Reft
>= :: Reft -> Reft -> Bool
$c>= :: Reft -> Reft -> Bool
> :: Reft -> Reft -> Bool
$c> :: Reft -> Reft -> Bool
<= :: Reft -> Reft -> Bool
$c<= :: Reft -> Reft -> Bool
< :: Reft -> Reft -> Bool
$c< :: Reft -> Reft -> Bool
compare :: Reft -> Reft -> Ordering
$ccompare :: Reft -> Reft -> Ordering
Ord, Typeable Reft
Reft -> DataType
Reft -> Constr
(forall b. Data b => b -> b) -> Reft -> Reft
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
forall u. (forall d. Data d => d -> u) -> Reft -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Reft -> m Reft
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Reft -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Reft -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r
gmapT :: (forall b. Data b => b -> b) -> Reft -> Reft
$cgmapT :: (forall b. Data b => b -> b) -> Reft -> Reft
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Reft)
dataTypeOf :: Reft -> DataType
$cdataTypeOf :: Reft -> DataType
toConstr :: Reft -> Constr
$ctoConstr :: Reft -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Reft
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
Data, Typeable, forall x. Rep Reft x -> Reft
forall x. Reft -> Rep Reft x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Reft x -> Reft
$cfrom :: forall x. Reft -> Rep Reft x
Generic)

data SortedReft = RR { SortedReft -> Sort
sr_sort :: !Sort, SortedReft -> Reft
sr_reft :: !Reft }
                  deriving (SortedReft -> SortedReft -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortedReft -> SortedReft -> Bool
$c/= :: SortedReft -> SortedReft -> Bool
== :: SortedReft -> SortedReft -> Bool
$c== :: SortedReft -> SortedReft -> Bool
Eq, Eq 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
min :: SortedReft -> SortedReft -> SortedReft
$cmin :: SortedReft -> SortedReft -> SortedReft
max :: SortedReft -> SortedReft -> SortedReft
$cmax :: SortedReft -> SortedReft -> SortedReft
>= :: SortedReft -> SortedReft -> Bool
$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
compare :: SortedReft -> SortedReft -> Ordering
$ccompare :: SortedReft -> SortedReft -> Ordering
Ord, Typeable SortedReft
SortedReft -> DataType
SortedReft -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SortedReft -> m SortedReft
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SortedReft -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SortedReft -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SortedReft -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SortedReft -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SortedReft -> r
gmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft
$cgmapT :: (forall b. Data b => b -> b) -> SortedReft -> SortedReft
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SortedReft)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortedReft)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SortedReft)
dataTypeOf :: SortedReft -> DataType
$cdataTypeOf :: SortedReft -> DataType
toConstr :: SortedReft -> Constr
$ctoConstr :: SortedReft -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortedReft
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SortedReft
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft
Data, Typeable, 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
$cto :: forall x. Rep SortedReft x -> SortedReft
$cfrom :: forall x. SortedReft -> Rep SortedReft x
Generic)

instance Hashable SortedReft

sortedReftSymbols :: SortedReft -> HashSet Symbol
sortedReftSymbols :: SortedReft -> HashSet Symbol
sortedReftSymbols SortedReft
sr =
  forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union
    (Sort -> HashSet Symbol
sortSymbols forall a b. (a -> b) -> a -> b
$ SortedReft -> Sort
sr_sort SortedReft
sr)
    (Expr -> HashSet Symbol
exprSymbolsSet forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
sr)

elit :: Located Symbol -> Sort -> Expr
elit :: LocSymbol -> Sort -> Expr
elit LocSymbol
l Sort
s = Constant -> Expr
ECon forall a b. (a -> b) -> a -> b
$ Text -> Sort -> Constant
L (Symbol -> Text
symbolText forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSymbol
l) Sort
s

instance Fixpoint Constant where
  toFix :: Constant -> Doc
toFix (I Integer
i)   = forall a. Fixpoint a => a -> Doc
toFix Integer
i
  toFix (R Double
i)   = forall a. Fixpoint a => a -> Doc
toFix Double
i
  toFix (L Text
s Sort
t) = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"lit" Doc -> Doc -> Doc
<+> String -> Doc
text String
"\"" Doc -> Doc -> Doc
<-> forall a. Fixpoint a => a -> Doc
toFix Text
s Doc -> Doc -> Doc
<-> String -> Doc
text String
"\"" Doc -> Doc -> 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 forall a b. (a -> b) -> a -> b
$ 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 (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
<-> forall a. Fixpoint a => a -> Doc
toFix Symbol
k

instance Fixpoint Brel where
  toFix :: Brel -> Doc
toFix Brel
Eq  = String -> Doc
text String
"="
  toFix Brel
Ne  = String -> Doc
text String
"!="
  toFix Brel
Ueq = String -> Doc
text String
"~~"
  toFix Brel
Une = String -> Doc
text String
"!~"
  toFix Brel
Gt  = String -> Doc
text String
">"
  toFix Brel
Ge  = String -> Doc
text String
">="
  toFix Brel
Lt  = String -> Doc
text String
"<"
  toFix Brel
Le  = String -> Doc
text String
"<="

instance Fixpoint Bop where
  toFix :: Bop -> Doc
toFix Bop
Plus   = String -> Doc
text String
"+"
  toFix Bop
Minus  = String -> Doc
text String
"-"
  toFix Bop
RTimes = String -> Doc
text String
"*."
  toFix Bop
Times  = String -> Doc
text String
"*"
  toFix Bop
Div    = String -> Doc
text String
"/"
  toFix Bop
RDiv   = String -> Doc
text String
"/."
  toFix Bop
Mod    = String -> Doc
text String
"mod"

instance Fixpoint Expr where
  toFix :: Expr -> Doc
toFix (ESym SymConst
c)       = forall a. Fixpoint a => a -> Doc
toFix SymConst
c
  toFix (ECon Constant
c)       = forall a. Fixpoint a => a -> Doc
toFix Constant
c
  toFix (EVar Symbol
s)       = forall a. Fixpoint a => a -> Doc
toFix Symbol
s
  toFix e :: Expr
e@(EApp Expr
_ Expr
_)   = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
" " forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr
fforall a. a -> [a] -> [a]
:[Expr]
es) where (Expr
f, [Expr]
es) = Expr -> (Expr, [Expr])
splitEApp Expr
e
  toFix (ENeg Expr
e)       = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"-"  Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Expr
e)
  toFix (EBin Bop
o Expr
e1 Expr
e2) = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [forall a. Fixpoint a => a -> Doc
toFix Expr
e1  Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Bop
o, Int -> Doc -> Doc
nest Int
2 (forall a. Fixpoint a => a -> Doc
toFix Expr
e2)]
  toFix (EIte Expr
p Expr
e1 Expr
e2) = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [String -> Doc
text String
"if" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
p Doc -> Doc -> Doc
<+> String -> Doc
text String
"then", Int -> Doc -> Doc
nest Int
2 (forall a. Fixpoint a => a -> Doc
toFix Expr
e1), String -> Doc
text String
"else", Int -> Doc -> Doc
nest Int
2 (forall a. Fixpoint a => a -> Doc
toFix Expr
e2)]
  -- toFix (ECst e _so)   = toFix e
  toFix (ECst Expr
e Sort
so)    = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix Expr
e   Doc -> Doc -> Doc
<+> String -> Doc
text String
" : " Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
so
  -- toFix (EBot)         = text "_|_"
  -- toFix PTop           = text "???"
  toFix Expr
PTrue          = String -> Doc
text String
"true"
  toFix Expr
PFalse         = String -> Doc
text String
"false"
  toFix (PNot Expr
p)       = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"~" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (forall a. Fixpoint a => a -> Doc
toFix Expr
p)
  toFix (PImp Expr
p1 Expr
p2)   = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix Expr
p1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"=>" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
p2
  toFix (PIff Expr
p1 Expr
p2)   = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall a. Fixpoint a => a -> Doc
toFix Expr
p1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"<=>" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
p2
  toFix (PAnd [Expr]
ps)      = String -> Doc
text String
"&&" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix [Expr]
ps
  toFix (POr  [Expr]
ps)      = String -> Doc
text String
"||" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix [Expr]
ps
  toFix (PAtom Brel
r Expr
e1 Expr
e2)  = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ forall a. Fixpoint a => a -> Doc
toFix Expr
e1 Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Brel
r, Int -> Doc -> Doc
nest Int
2 (forall a. Fixpoint a => a -> Doc
toFix Expr
e2)]
  toFix (PKVar KVar
k Subst
su)     = forall a. Fixpoint a => a -> Doc
toFix KVar
k Doc -> Doc -> Doc
<-> forall a. Fixpoint a => a -> Doc
toFix Subst
su
  toFix (PAll [(Symbol, Sort)]
xts Expr
p)     = Doc
"forall" Doc -> Doc -> Doc
<+> (forall a. Fixpoint a => a -> Doc
toFix [(Symbol, Sort)]
xts
                                        Doc -> Doc -> Doc
$+$ (Doc
"." Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
p))
  toFix (PExist [(Symbol, Sort)]
xts Expr
p)   = Doc
"exists" Doc -> Doc -> Doc
<+> (forall a. Fixpoint a => a -> Doc
toFix [(Symbol, Sort)]
xts
                                        Doc -> Doc -> Doc
$+$ (Doc
"." Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
p))
  toFix (ETApp Expr
e Sort
s)      = String -> Doc
text String
"tapp" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
s
  toFix (ETAbs Expr
e Symbol
s)      = String -> Doc
text String
"tabs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
s
  toFix (PGrad KVar
k Subst
_ GradInfo
_ Expr
e)  = forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text String
"&&" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix KVar
k -- text "??" -- <+> toFix k <+> toFix su
  toFix (ECoerc Sort
a Sort
t Expr
e)   = Doc -> Doc
parens (String -> Doc
text String
"coerce" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
a Doc -> Doc -> Doc
<+> String -> Doc
text String
"~" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"in" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
e)
  toFix (ELam (Symbol
x,Sort
s) Expr
e)   = String -> Doc
text String
"lam" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
s Doc -> Doc -> Doc
<+> Doc
"." Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
e

  simplify :: Expr -> Expr
simplify = ([Expr] -> [Expr]) -> Expr -> Expr
simplifyExpr forall {a}. Ord a => [a] -> [a]
dedup
    where
      dedup :: [a] -> [a]
dedup = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList

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

    go (PGrad KVar
k Subst
su GradInfo
i Expr
e)
      | Expr -> Bool
isContraPred Expr
e      = Expr
PFalse
      | Bool
otherwise           = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i (Expr -> Expr
go Expr
e)

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

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

    go Expr
p
      | Expr -> Bool
isContraPred Expr
p     = Expr
PFalse
      | Expr -> Bool
isTautoPred  Expr
p     = Expr
PTrue
      | Bool
otherwise          = Expr
p

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

    eqC :: Expr -> Bool
eqC (PAtom Brel
Eq (ECon Constant
x) (ECon Constant
y))
               = Constant
x forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqC (PAtom Brel
Ueq (ECon Constant
x) (ECon Constant
y))
               = Constant
x forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqC (PAtom Brel
Ne Expr
x Expr
y)
               = Expr
x forall a. Eq a => a -> a -> Bool
== Expr
y
    eqC (PAtom Brel
Une Expr
x Expr
y)
               = Expr
x forall a. Eq a => a -> a -> Bool
== Expr
y
    eqC Expr
_      = Bool
False

isTautoPred   :: Expr -> Bool
isTautoPred :: Expr -> Bool
isTautoPred Expr
z  = Expr
z forall a. Eq a => a -> a -> Bool
== Expr
PTop Bool -> Bool -> Bool
|| Expr
z forall a. Eq a => a -> a -> Bool
== Expr
PTrue Bool -> Bool -> Bool
|| Expr -> Bool
eqT Expr
z
  where
    eqT :: Expr -> Bool
eqT (PAnd [])
               = Bool
True
    eqT (PAtom Brel
Le Expr
x Expr
y)
               = Expr
x forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Ge Expr
x Expr
y)
               = Expr
x forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Eq Expr
x Expr
y)
               = Expr
x forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Ueq Expr
x Expr
y)
               = Expr
x forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Ne (ECon Constant
x) (ECon Constant
y))
               = Constant
x forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqT (PAtom Brel
Une (ECon Constant
x) (ECon Constant
y))
               = Constant
x forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqT Expr
_      = Bool
False

isEq  :: Brel -> Bool
isEq :: Brel -> Bool
isEq Brel
r          = Brel
r forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
r forall a. Eq a => a -> a -> Bool
== Brel
Ueq

instance PPrint Constant where
  pprintTidy :: Tidy -> Constant -> Doc
pprintTidy Tidy
_ = 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  = forall a. Fixpoint a => a -> Doc
toFix Brel
r

instance PPrint Bop where
  pprintTidy :: Tidy -> Bop -> Doc
pprintTidy Tidy
_  = 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
<-> 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 forall a b. (a -> b) -> a -> b
$ String -> Doc
text 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 = forall a. a -> a
id

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

opPrec :: Bop -> Int
opPrec :: Bop -> Int
opPrec Bop
Mod    = Int
5
opPrec Bop
Plus   = Int
6
opPrec Bop
Minus  = Int
6
opPrec Bop
Times  = Int
7
opPrec Bop
RTimes = Int
7
opPrec Bop
Div    = Int
7
opPrec Bop
RDiv   = Int
7

instance PPrint Expr where
  pprintPrec :: Int -> Tidy -> Expr -> Doc
pprintPrec Int
_ Tidy
k (ESym SymConst
c)        = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k SymConst
c
  pprintPrec Int
_ Tidy
k (ECon Constant
c)        = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Constant
c
  pprintPrec Int
_ Tidy
k (EVar Symbol
s)        = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
s
  -- pprintPrec _ (EBot)          = text "_|_"
  pprintPrec Int
z Tidy
k (ENeg Expr
e)        = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
zn) forall a b. (a -> b) -> a -> b
$
                                   Doc
"-" Doc -> Doc -> Doc
<-> forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
zn forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Expr
e
    where zn :: a
zn = a
2
  pprintPrec Int
z Tidy
k (EApp Expr
f Expr
es)     = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
za) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec forall {a}. Num a => a
za Tidy
k Expr
f Doc -> Doc -> Doc
<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
zaforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
es
    where za :: a
za = a
8
  pprintPrec Int
z Tidy
k (EBin Bop
o Expr
e1 Expr
e2)  = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> Int
zo) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
zoforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e1 Doc -> Doc -> Doc
<+>
                                   forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Bop
o         Doc -> Doc -> Doc
<+>
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
zoforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e2
    where zo :: Int
zo = Bop -> Int
opPrec Bop
o
  pprintPrec Int
z Tidy
k (EIte Expr
p Expr
e1 Expr
e2)  = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
zi) forall a b. (a -> b) -> a -> b
$
                                   Doc
"if"   Doc -> Doc -> Doc
<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p  Doc -> Doc -> Doc
<+>
                                   Doc
"then" Doc -> Doc -> Doc
<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e1 Doc -> Doc -> Doc
<+>
                                   Doc
"else" Doc -> Doc -> Doc
<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e2
    where zi :: a
zi = a
1

  -- RJ: DO NOT DELETE!
  pprintPrec Int
_ Tidy
k (ECst Expr
e Sort
so)     = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> Doc
pprint Expr
e Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> {- const (text "...") -} forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Sort
so
  -- pprintPrec z k (ECst e _)      = pprintPrec z k e
  pprintPrec Int
_ Tidy
_ Expr
PTrue           = Doc
trueD
  pprintPrec Int
_ Tidy
_ Expr
PFalse          = Doc
falseD
  pprintPrec Int
z Tidy
k (PNot Expr
p)        = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
zn) forall a b. (a -> b) -> a -> b
$
                                   Doc
"not" Doc -> Doc -> Doc
<+> forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
znforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p
    where zn :: a
zn = a
8
  pprintPrec Int
z Tidy
k (PImp Expr
p1 Expr
p2)    = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
zi) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p1 Doc -> Doc -> Doc
<+>
                                   Doc
"=>"                     Doc -> Doc -> Doc
<+>
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p2
    where zi :: a
zi = a
2
  pprintPrec Int
z Tidy
k (PIff Expr
p1 Expr
p2)    = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
zi) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p1 Doc -> Doc -> Doc
<+>
                                   Doc
"<=>"                    Doc -> Doc -> Doc
<+>
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
ziforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p2
    where zi :: a
zi = a
2
  pprintPrec Int
z Tidy
k (PAnd [Expr]
ps)       = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
za) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin (forall {a}. Num a => a
za forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Doc
trueD Doc
andD [Expr]
ps
    where za :: a
za = a
3
  pprintPrec Int
z Tidy
k (POr  [Expr]
ps)       = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
zo) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin (forall {a}. Num a => a
zo forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Doc
falseD Doc
orD [Expr]
ps
    where zo :: a
zo = a
3
  pprintPrec Int
z Tidy
k (PAtom Brel
r Expr
e1 Expr
e2) = Bool -> Doc -> Doc
parensIf (Int
z forall a. Ord a => a -> a -> Bool
> forall {a}. Num a => a
za) forall a b. (a -> b) -> a -> b
$
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
zaforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e1 Doc -> Doc -> Doc
<+>
                                   forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Brel
r         Doc -> Doc -> Doc
<+>
                                   forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (forall {a}. Num a => a
zaforall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e2
    where za :: a
za = a
4
  pprintPrec Int
_ Tidy
k (PAll [(Symbol, Sort)]
xts Expr
p)    = Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc
pprintQuant Tidy
k Doc
"forall" [(Symbol, Sort)]
xts Expr
p
  pprintPrec Int
_ Tidy
k (PExist [(Symbol, Sort)]
xts Expr
p)  = Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc
pprintQuant Tidy
k Doc
"exists" [(Symbol, Sort)]
xts Expr
p
  pprintPrec Int
_ Tidy
k (ELam (Symbol
x,Sort
t) Expr
e)  = Doc
"lam" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
e
  pprintPrec Int
_ Tidy
k (ECoerc Sort
a Sort
t Expr
e)  = Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ Doc
"coerce" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
a Doc -> Doc -> Doc
<+> Doc
"~" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"in" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
e
  pprintPrec Int
_ Tidy
_ p :: Expr
p@PKVar{}    = forall a. Fixpoint a => a -> Doc
toFix Expr
p
  pprintPrec Int
_ Tidy
_ (ETApp Expr
e Sort
s)     = Doc
"ETApp" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Sort
s
  pprintPrec Int
_ Tidy
_ (ETAbs Expr
e Symbol
s)     = Doc
"ETAbs" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix Symbol
s
  pprintPrec Int
z Tidy
k (PGrad KVar
x Subst
_ GradInfo
_ Expr
e) = forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k Expr
e Doc -> Doc -> Doc
<+> Doc
"&&" Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix KVar
x -- "??"

pprintQuant :: Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc
pprintQuant :: Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc
pprintQuant Tidy
k Doc
d [(Symbol, Sort)]
xts Expr
p = (Doc
d Doc -> Doc -> Doc
<+> forall a. Fixpoint a => a -> Doc
toFix [(Symbol, Sort)]
xts)
                        Doc -> Doc -> Doc
$+$
                        (Doc
"  ." Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
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 forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k 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 forall a. a -> [a] -> [a]
: ((Doc
s Doc -> Doc -> Doc
<+>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
ds))

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

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

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

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

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

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

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

instance Expression Int where
  expr :: Int -> Expr
expr = forall a. Expression a => a -> Expr
expr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance Predicate Symbol where
  prop :: Symbol -> Expr
prop = forall a. Symbolic a => a -> Expr
eProp

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

instance Predicate Bool where
  prop :: Bool -> Expr
prop Bool
True  = Expr
PTrue
  prop Bool
False = Expr
PFalse

instance Expression a => Expression (Located a) where
  expr :: Located a -> Expr
expr   = forall a. Expression a => a -> Expr
expr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val

eVar ::  Symbolic a => a -> Expr
eVar :: forall a. Symbolic a => a -> Expr
eVar = Symbol -> Expr
EVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol

eProp ::  Symbolic a => a -> Expr
eProp :: forall a. Symbolic a => a -> Expr
eProp = Expr -> Expr
mkProp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Expr
eVar

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

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

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

pAnd, pOr     :: ListNE Pred -> Pred
pAnd :: [Expr] -> Expr
pAnd          = forall a. Fixpoint a => a -> a
simplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
PAnd

pAndNoDedup :: ListNE Pred -> Pred
pAndNoDedup :: [Expr] -> Expr
pAndNoDedup = ([Expr] -> [Expr]) -> Expr -> Expr
simplifyExpr forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
PAnd

pOr :: [Expr] -> Expr
pOr           = forall a. Fixpoint a => a -> a
simplify forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
POr

infixl 9 &.&
(&.&) :: Pred -> Pred -> Pred
&.& :: Expr -> Expr -> Expr
(&.&) Expr
p Expr
q = [Expr] -> Expr
pAnd [Expr
p, Expr
q]

infixl 9 |.|
(|.|) :: Pred -> Pred -> Pred
|.| :: Expr -> Expr -> Expr
(|.|) Expr
p Expr
q = [Expr] -> Expr
pOr [Expr
p, Expr
q]

pIte :: Pred -> Expr -> Expr -> Expr
pIte :: Expr -> Expr -> Expr -> Expr
pIte Expr
p1 Expr
p2 Expr
p3 = [Expr] -> Expr
pAnd [Expr
p1 Expr -> Expr -> Expr
`PImp` Expr
p2, Expr -> Expr
PNot Expr
p1 Expr -> Expr -> Expr
`PImp` Expr
p3]

pExist :: [(Symbol, Sort)] -> Pred -> Pred
pExist :: [(Symbol, Sort)] -> Expr -> Expr
pExist []  Expr
p = Expr
p
pExist [(Symbol, Sort)]
xts Expr
p = [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xts Expr
p

mkProp :: Expr -> Pred
mkProp :: Expr -> Expr
mkProp = forall a. a -> a
id -- EApp (EVar propConName)

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

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

relReft :: (Expression a) => Brel -> a -> Reft
relReft :: forall a. Expression a => Brel -> a -> Reft
relReft Brel
r a
e   = (Symbol, Expr) -> Reft
Reft (Symbol
vv_, Brel -> Expr -> Expr -> Expr
PAtom Brel
r (forall a. Symbolic a => a -> Expr
eVar Symbol
vv_)  (forall a. Expression a => a -> Expr
expr a
e))

exprReft, notExprReft, uexprReft ::  (Expression a) => a -> Reft
exprReft :: forall a. Expression a => a -> Reft
exprReft      = forall a. Expression a => Brel -> a -> Reft
relReft Brel
Eq
notExprReft :: forall a. Expression a => a -> Reft
notExprReft   = forall a. Expression a => Brel -> a -> Reft
relReft Brel
Ne
uexprReft :: forall a. Expression a => a -> Reft
uexprReft     = 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, Expr) -> Reft
Reft (Symbol
vv_, Expr -> Expr -> Expr
PIff (forall a. Symbolic a => a -> Expr
eProp Symbol
vv_) (forall a. Predicate a => a -> Expr
prop a
p))

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

reft :: Symbol -> Expr -> Reft
reft :: Symbol -> Expr -> Reft
reft Symbol
v Expr
p = (Symbol, Expr) -> Reft
Reft (Symbol
v, Expr
p)

mapPredReft :: (Expr -> Expr) -> Reft -> Reft
mapPredReft :: (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
f (Reft (Symbol
v, Expr
p)) = (Symbol, Expr) -> Reft
Reft (Symbol
v, Expr -> Expr
f Expr
p)

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

isFunctionSortedReft :: SortedReft -> Bool
isFunctionSortedReft :: SortedReft -> Bool
isFunctionSortedReft = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe ([Int], [Sort], Sort)
functionSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Sort
sr_sort

isNonTrivial :: Reftable r => r -> Bool
isNonTrivial :: forall r. Reftable r => r -> Bool
isNonTrivial = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Reftable r => r -> Bool
isTauto

reftPred :: Reft -> Expr
reftPred :: Reft -> Expr
reftPred (Reft (Symbol
_, Expr
p)) = Expr
p

reftBind :: Reft -> Symbol
reftBind :: Reft -> Symbol
reftBind (Reft (Symbol
x, Expr
_)) = Symbol
x

------------------------------------------------------------
-- | Gradual Type Manipulation  ----------------------------
------------------------------------------------------------
pGAnds :: [Expr] -> Expr
pGAnds :: [Expr] -> Expr
pGAnds = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr -> Expr -> Expr
pGAnd Expr
PTrue

pGAnd :: Expr -> Expr -> Expr
pGAnd :: Expr -> Expr -> Expr
pGAnd (PGrad KVar
k Subst
su GradInfo
i Expr
p) Expr
q = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i ([Expr] -> Expr
pAnd [Expr
p, Expr
q])
pGAnd Expr
p (PGrad KVar
k Subst
su GradInfo
i Expr
q) = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i ([Expr] -> Expr
pAnd [Expr
p, Expr
q])
pGAnd Expr
p Expr
q              = [Expr] -> Expr
pAnd [Expr
p,Expr
q]

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

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

usymbolReft   :: (Symbolic a) => a -> Reft
usymbolReft :: forall a. Symbolic a => a -> Reft
usymbolReft   = forall a. Expression a => a -> Reft
uexprReft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Expr
eVar

vv_ :: Symbol
vv_ :: Symbol
vv_ = Maybe Integer -> Symbol
vv forall a. Maybe a
Nothing

trueSortedReft :: Sort -> SortedReft
trueSortedReft :: Sort -> SortedReft
trueSortedReft = (Sort -> Reft -> SortedReft
`RR` Reft
trueReft)

trueReft, falseReft :: Reft
trueReft :: Reft
trueReft  = (Symbol, Expr) -> Reft
Reft (Symbol
vv_, Expr
PTrue)
falseReft :: Reft
falseReft = (Symbol, Expr) -> Reft
Reft (Symbol
vv_, Expr
PFalse)

flattenRefas :: [Expr] -> [Expr]
flattenRefas :: [Expr] -> [Expr]
flattenRefas        = [Expr] -> [Expr] -> [Expr]
flatP []
  where
    flatP :: [Expr] -> [Expr] -> [Expr]
flatP [Expr]
acc (PAnd [Expr]
ps:[Expr]
xs) = [Expr] -> [Expr] -> [Expr]
flatP ([Expr] -> [Expr] -> [Expr]
flatP [Expr]
acc [Expr]
xs) [Expr]
ps
    flatP [Expr]
acc (Expr
p:[Expr]
xs)       = Expr
p forall a. a -> [a] -> [a]
: [Expr] -> [Expr] -> [Expr]
flatP [Expr]
acc [Expr]
xs
    flatP [Expr]
acc []           = [Expr]
acc

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


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

class Falseable a where
  isFalse :: a -> Bool

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

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

instance Subable a => Subable (Located a) where
  syms :: Located a -> [Symbol]
syms (Loc SourcePos
_ SourcePos
_ a
x)   = 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) = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f a
x)
  substf :: (Symbol -> Expr) -> Located a -> Located a
substf Symbol -> Expr
f (Loc SourcePos
l SourcePos
l' a
x) = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (forall a. Subable a => (Symbol -> Expr) -> a -> a
substf Symbol -> Expr
f a
x)
  subst :: Subst -> Located a -> Located a
subst Subst
su (Loc SourcePos
l SourcePos
l' a
x) = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (forall a. Subable a => Subst -> a -> a
subst Subst
su a
x)


class (Monoid r, Subable r) => Reftable r where
  isTauto :: r -> Bool
  ppTy    :: r -> Doc -> Doc

  top     :: r -> r
  top r
_   =  forall a. Monoid a => a
mempty

  bot     :: r -> r

  meet    :: r -> r -> r
  meet    = forall a. Monoid a => a -> a -> a
mappend

  toReft  :: r -> Reft
  ofReft  :: Reft -> r
  params  :: r -> [Symbol]          -- ^ parameters for Reft, vv + others

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