{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE PatternGuards              #-}
{-# LANGUAGE PatternSynonyms            #-}

-- | 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
  , pAnd, pOr, pIte
  , (&.&), (|.|)
  , 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
  , eApps
  , eAppC
  , splitEApp
  , splitPAnd
  , reftConjuncts

  -- * Transforming
  , mapPredReft
  , pprintReft

  , debruijnIndex

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

  ) where

import           Prelude hiding ((<>))
import qualified Data.Binary as B
import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           Data.Hashable
import           GHC.Generics              (Generic)
import           Data.List                 (foldl', partition)
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           Text.Printf               (printf)


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

instance (Eq a, Hashable a, B.Binary a) => B.Binary (TCEmb a) 
instance B.Binary SrcSpan
instance B.Binary KVar
instance B.Binary Subst
instance B.Binary GradInfo
instance B.Binary Constant
instance B.Binary SymConst
instance B.Binary Brel
instance B.Binary Bop
instance B.Binary Expr
instance B.Binary Reft
instance B.Binary SortedReft

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 [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
ps then [Expr]
ks else (([Expr] -> Expr
pAnd [Expr]
ps) Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
ks)
    ([Expr]
ks, [Expr]
ps)                 = (Expr -> Bool) -> [Expr] -> ([Expr], [Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\Expr
p -> Expr -> Bool
isKvar Expr
p Bool -> Bool -> Bool
|| Expr -> Bool
forall a. HasGradual a => a -> Bool
isGradual Expr
p) ([Expr] -> ([Expr], [Expr])) -> [Expr] -> ([Expr], [Expr])
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
refaConjuncts Expr
ra

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)  = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr -> Bool
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)       = (Expr -> [KVar]) -> [Expr] -> [KVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [KVar]
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 (Expr -> Expr
forall a. HasGradual a => a -> a
ungrad (Expr -> Expr) -> [Expr] -> [Expr]
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)) = Expr -> Bool
forall a. HasGradual a => a -> Bool
isGradual Expr
r
  gVars :: Reft -> [KVar]
gVars (Reft (Symbol
_,Expr
r))     = Expr -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars Expr
r
  ungrad :: Reft -> Reft
ungrad (Reft (Symbol
x,Expr
r))    = (Symbol, Expr) -> Reft
Reft(Symbol
x, Expr -> Expr
forall a. HasGradual a => a -> a
ungrad Expr
r)

instance HasGradual SortedReft where
  isGradual :: SortedReft -> Bool
isGradual = Reft -> Bool
forall a. HasGradual a => a -> Bool
isGradual (Reft -> Bool) -> (SortedReft -> Reft) -> SortedReft -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
  gVars :: SortedReft -> [KVar]
gVars     = Reft -> [KVar]
forall a. HasGradual a => a -> [KVar]
gVars (Reft -> [KVar]) -> (SortedReft -> Reft) -> SortedReft -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft
  ungrad :: SortedReft -> SortedReft
ungrad SortedReft
r  = SortedReft
r {sr_reft :: Reft
sr_reft = Reft -> 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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isTautoPred Expr
p']

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

newtype KVar = KV { KVar -> Symbol
kv :: Symbol }
               deriving (KVar -> KVar -> Bool
(KVar -> KVar -> Bool) -> (KVar -> KVar -> Bool) -> Eq KVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KVar -> KVar -> Bool
$c/= :: KVar -> KVar -> Bool
== :: KVar -> KVar -> Bool
$c== :: KVar -> KVar -> Bool
Eq, Eq KVar
Eq KVar
-> (KVar -> KVar -> Ordering)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> Bool)
-> (KVar -> KVar -> KVar)
-> (KVar -> KVar -> KVar)
-> Ord KVar
KVar -> KVar -> Bool
KVar -> KVar -> Ordering
KVar -> KVar -> KVar
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
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
$cp1Ord :: Eq KVar
Ord, Typeable KVar
DataType
Constr
Typeable KVar
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> KVar -> c KVar)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KVar)
-> (KVar -> Constr)
-> (KVar -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KVar))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVar))
-> ((forall b. Data b => b -> b) -> KVar -> KVar)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVar -> r)
-> (forall u. (forall d. Data d => d -> u) -> KVar -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KVar -> m KVar)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KVar -> m KVar)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KVar -> m KVar)
-> Data KVar
KVar -> DataType
KVar -> Constr
(forall b. Data b => b -> b) -> KVar -> KVar
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVar -> c KVar
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cKV :: Constr
$tKVar :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> KVar -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVar -> u
gmapQ :: (forall d. Data d => d -> u) -> KVar -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KVar -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable KVar
Data, Typeable, (forall x. KVar -> Rep KVar x)
-> (forall x. Rep KVar x -> KVar) -> Generic KVar
forall x. Rep KVar x -> KVar
forall x. KVar -> Rep KVar x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep KVar x -> KVar
$cfrom :: forall x. KVar -> Rep KVar x
Generic, String -> KVar
(String -> KVar) -> IsString KVar
forall a. (String -> a) -> IsString a
fromString :: String -> KVar
$cfromString :: String -> KVar
IsString)

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

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

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

--------------------------------------------------------------------------------
-- | Substitutions -------------------------------------------------------------
--------------------------------------------------------------------------------
newtype Subst = Su (M.HashMap Symbol Expr)
                deriving (Subst -> Subst -> Bool
(Subst -> Subst -> Bool) -> (Subst -> Subst -> Bool) -> Eq Subst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c== :: Subst -> Subst -> Bool
Eq, Typeable Subst
DataType
Constr
Typeable Subst
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Subst -> c Subst)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Subst)
-> (Subst -> Constr)
-> (Subst -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Subst))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Subst))
-> ((forall b. Data b => b -> b) -> Subst -> Subst)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Subst -> r)
-> (forall u. (forall d. Data d => d -> u) -> Subst -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Subst -> m Subst)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Subst -> m Subst)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Subst -> m Subst)
-> Data Subst
Subst -> DataType
Subst -> Constr
(forall b. Data b => b -> b) -> Subst -> Subst
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Subst -> c Subst
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cSu :: Constr
$tSubst :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Subst -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Subst -> u
gmapQ :: (forall d. Data d => d -> u) -> Subst -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Subst -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Subst
Data, Typeable, (forall x. Subst -> Rep Subst x)
-> (forall x. Rep Subst x -> Subst) -> Generic Subst
forall x. Rep Subst x -> Subst
forall x. Subst -> Rep Subst x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Subst x -> Subst
$cfrom :: forall x. Subst -> Rep Subst x
Generic)

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

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

instance PPrint Subst where
  pprintTidy :: Tidy -> Subst -> Doc
pprintTidy Tidy
_ = Subst -> Doc
forall a. Fixpoint a => a -> Doc
toFix

data KVSub = KVS
  { KVSub -> Symbol
ksuVV    :: Symbol
  , KVSub -> Sort
ksuSort  :: Sort
  , KVSub -> KVar
ksuKVar  :: KVar
  , KVSub -> Subst
ksuSubst :: Subst
  } deriving (KVSub -> KVSub -> Bool
(KVSub -> KVSub -> Bool) -> (KVSub -> KVSub -> Bool) -> Eq KVSub
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KVSub -> KVSub -> Bool
$c/= :: KVSub -> KVSub -> Bool
== :: KVSub -> KVSub -> Bool
$c== :: KVSub -> KVSub -> Bool
Eq, Typeable KVSub
DataType
Constr
Typeable KVSub
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> KVSub -> c KVSub)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c KVSub)
-> (KVSub -> Constr)
-> (KVSub -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c KVSub))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c KVSub))
-> ((forall b. Data b => b -> b) -> KVSub -> KVSub)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> KVSub -> r)
-> (forall u. (forall d. Data d => d -> u) -> KVSub -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> KVSub -> m KVSub)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KVSub -> m KVSub)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> KVSub -> m KVSub)
-> Data KVSub
KVSub -> DataType
KVSub -> Constr
(forall b. Data b => b -> b) -> KVSub -> KVSub
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> KVSub -> c KVSub
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cKVS :: Constr
$tKVSub :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> KVSub -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> KVSub -> u
gmapQ :: (forall d. Data d => d -> u) -> KVSub -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> KVSub -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable KVSub
Data, Typeable, (forall x. KVSub -> Rep KVSub x)
-> (forall x. Rep KVSub x -> KVSub) -> Generic KVSub
forall x. Rep KVSub x -> KVSub
forall x. KVSub -> Rep KVSub x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep KVSub x -> KVSub
$cfrom :: forall x. KVSub -> Rep KVSub x
Generic, Int -> KVSub -> ShowS
[KVSub] -> ShowS
KVSub -> String
(Int -> KVSub -> ShowS)
-> (KVSub -> String) -> ([KVSub] -> ShowS) -> Show KVSub
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
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 = Tidy -> (Symbol, KVar, Subst) -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (KVSub -> Symbol
ksuVV KVSub
ksu, KVSub -> KVar
ksuKVar KVSub
ksu, KVSub -> Subst
ksuSubst KVSub
ksu)

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

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

data SymConst = SL !Text
              deriving (SymConst -> SymConst -> Bool
(SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool) -> Eq SymConst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymConst -> SymConst -> Bool
$c/= :: SymConst -> SymConst -> Bool
== :: SymConst -> SymConst -> Bool
$c== :: SymConst -> SymConst -> Bool
Eq, Eq SymConst
Eq SymConst
-> (SymConst -> SymConst -> Ordering)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> Bool)
-> (SymConst -> SymConst -> SymConst)
-> (SymConst -> SymConst -> SymConst)
-> Ord SymConst
SymConst -> SymConst -> Bool
SymConst -> SymConst -> Ordering
SymConst -> SymConst -> SymConst
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
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
$cp1Ord :: Eq SymConst
Ord, Int -> SymConst -> ShowS
[SymConst] -> ShowS
SymConst -> String
(Int -> SymConst -> ShowS)
-> (SymConst -> String) -> ([SymConst] -> ShowS) -> Show SymConst
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymConst] -> ShowS
$cshowList :: [SymConst] -> ShowS
show :: SymConst -> String
$cshow :: SymConst -> String
showsPrec :: Int -> SymConst -> ShowS
$cshowsPrec :: Int -> SymConst -> ShowS
Show, Typeable SymConst
DataType
Constr
Typeable SymConst
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SymConst -> c SymConst)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SymConst)
-> (SymConst -> Constr)
-> (SymConst -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SymConst))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymConst))
-> ((forall b. Data b => b -> b) -> SymConst -> SymConst)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SymConst -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SymConst -> r)
-> (forall u. (forall d. Data d => d -> u) -> SymConst -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SymConst -> m SymConst)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymConst -> m SymConst)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SymConst -> m SymConst)
-> Data SymConst
SymConst -> DataType
SymConst -> Constr
(forall b. Data b => b -> b) -> SymConst -> SymConst
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SymConst -> c SymConst
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cSL :: Constr
$tSymConst :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> SymConst -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SymConst -> u
gmapQ :: (forall d. Data d => d -> u) -> SymConst -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SymConst -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable SymConst
Data, Typeable, (forall x. SymConst -> Rep SymConst x)
-> (forall x. Rep SymConst x -> SymConst) -> Generic SymConst
forall x. Rep SymConst x -> SymConst
forall x. SymConst -> Rep SymConst x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$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
(Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool) -> Eq Constant
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
Eq Constant
-> (Constant -> Constant -> Ordering)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Bool)
-> (Constant -> Constant -> Constant)
-> (Constant -> Constant -> Constant)
-> Ord Constant
Constant -> Constant -> Bool
Constant -> Constant -> Ordering
Constant -> Constant -> Constant
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
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
$cp1Ord :: Eq Constant
Ord, Int -> Constant -> ShowS
[Constant] -> ShowS
Constant -> String
(Int -> Constant -> ShowS)
-> (Constant -> String) -> ([Constant] -> ShowS) -> Show Constant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constant] -> ShowS
$cshowList :: [Constant] -> ShowS
show :: Constant -> String
$cshow :: Constant -> String
showsPrec :: Int -> Constant -> ShowS
$cshowsPrec :: Int -> Constant -> ShowS
Show, Typeable Constant
DataType
Constr
Typeable Constant
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Constant -> c Constant)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Constant)
-> (Constant -> Constr)
-> (Constant -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Constant))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constant))
-> ((forall b. Data b => b -> b) -> Constant -> Constant)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Constant -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Constant -> r)
-> (forall u. (forall d. Data d => d -> u) -> Constant -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Constant -> m Constant)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constant -> m Constant)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constant -> m Constant)
-> Data Constant
Constant -> DataType
Constant -> Constr
(forall b. Data b => b -> b) -> Constant -> Constant
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constant -> c Constant
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cL :: Constr
$cR :: Constr
$cI :: Constr
$tConstant :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Constant -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constant -> u
gmapQ :: (forall d. Data d => d -> u) -> Constant -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Constant -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Constant
Data, Typeable, (forall x. Constant -> Rep Constant x)
-> (forall x. Rep Constant x -> Constant) -> Generic Constant
forall x. Rep Constant x -> Constant
forall x. Constant -> Rep Constant x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$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
(Brel -> Brel -> Bool) -> (Brel -> Brel -> Bool) -> Eq Brel
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
Eq Brel
-> (Brel -> Brel -> Ordering)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Bool)
-> (Brel -> Brel -> Brel)
-> (Brel -> Brel -> Brel)
-> Ord Brel
Brel -> Brel -> Bool
Brel -> Brel -> Ordering
Brel -> Brel -> Brel
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
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
$cp1Ord :: Eq Brel
Ord, Int -> Brel -> ShowS
[Brel] -> ShowS
Brel -> String
(Int -> Brel -> ShowS)
-> (Brel -> String) -> ([Brel] -> ShowS) -> Show Brel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Brel] -> ShowS
$cshowList :: [Brel] -> ShowS
show :: Brel -> String
$cshow :: Brel -> String
showsPrec :: Int -> Brel -> ShowS
$cshowsPrec :: Int -> Brel -> ShowS
Show, Typeable Brel
DataType
Constr
Typeable Brel
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Brel -> c Brel)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Brel)
-> (Brel -> Constr)
-> (Brel -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Brel))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Brel))
-> ((forall b. Data b => b -> b) -> Brel -> Brel)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Brel -> r)
-> (forall u. (forall d. Data d => d -> u) -> Brel -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Brel -> m Brel)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Brel -> m Brel)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Brel -> m Brel)
-> Data Brel
Brel -> DataType
Brel -> Constr
(forall b. Data b => b -> b) -> Brel -> Brel
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Brel -> c Brel
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cUne :: Constr
$cUeq :: Constr
$cLe :: Constr
$cLt :: Constr
$cGe :: Constr
$cGt :: Constr
$cNe :: Constr
$cEq :: Constr
$tBrel :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Brel -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Brel -> u
gmapQ :: (forall d. Data d => d -> u) -> Brel -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Brel -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Brel
Data, Typeable, (forall x. Brel -> Rep Brel x)
-> (forall x. Rep Brel x -> Brel) -> Generic Brel
forall x. Rep Brel x -> Brel
forall x. Brel -> Rep Brel x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$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
(Bop -> Bop -> Bool) -> (Bop -> Bop -> Bool) -> Eq Bop
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
Eq Bop
-> (Bop -> Bop -> Ordering)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bool)
-> (Bop -> Bop -> Bop)
-> (Bop -> Bop -> Bop)
-> Ord Bop
Bop -> Bop -> Bool
Bop -> Bop -> Ordering
Bop -> Bop -> Bop
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
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
$cp1Ord :: Eq Bop
Ord, Int -> Bop -> ShowS
[Bop] -> ShowS
Bop -> String
(Int -> Bop -> ShowS)
-> (Bop -> String) -> ([Bop] -> ShowS) -> Show Bop
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Bop] -> ShowS
$cshowList :: [Bop] -> ShowS
show :: Bop -> String
$cshow :: Bop -> String
showsPrec :: Int -> Bop -> ShowS
$cshowsPrec :: Int -> Bop -> ShowS
Show, Typeable Bop
DataType
Constr
Typeable Bop
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Bop -> c Bop)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Bop)
-> (Bop -> Constr)
-> (Bop -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Bop))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Bop))
-> ((forall b. Data b => b -> b) -> Bop -> Bop)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Bop -> r)
-> (forall u. (forall d. Data d => d -> u) -> Bop -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Bop -> m Bop)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bop -> m Bop)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Bop -> m Bop)
-> Data Bop
Bop -> DataType
Bop -> Constr
(forall b. Data b => b -> b) -> Bop -> Bop
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Bop -> c Bop
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cRDiv :: Constr
$cRTimes :: Constr
$cMod :: Constr
$cDiv :: Constr
$cTimes :: Constr
$cMinus :: Constr
$cPlus :: Constr
$tBop :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Bop -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Bop -> u
gmapQ :: (forall d. Data d => d -> u) -> Bop -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Bop -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Bop
Data, Typeable, (forall x. Bop -> Rep Bop x)
-> (forall x. Rep Bop x -> Bop) -> Generic Bop
forall x. Rep Bop x -> Bop
forall x. Bop -> Rep Bop x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$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
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
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
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
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, Typeable Expr
DataType
Constr
Typeable Expr
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Expr -> c Expr)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Expr)
-> (Expr -> Constr)
-> (Expr -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Expr -> Expr)
-> (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 u. (forall d. Data d => d -> u) -> Expr -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Expr -> m Expr)
-> Data Expr
Expr -> DataType
Expr -> Constr
(forall b. Data b => b -> b) -> Expr -> Expr
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Expr -> c Expr
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cECoerc :: Constr
$cPGrad :: Constr
$cPExist :: Constr
$cPAll :: Constr
$cPKVar :: Constr
$cPAtom :: Constr
$cPIff :: Constr
$cPImp :: Constr
$cPNot :: Constr
$cPOr :: Constr
$cPAnd :: Constr
$cETAbs :: Constr
$cETApp :: Constr
$cELam :: Constr
$cECst :: Constr
$cEIte :: Constr
$cEBin :: Constr
$cENeg :: Constr
$cEApp :: Constr
$cEVar :: Constr
$cECon :: Constr
$cESym :: Constr
$tExpr :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Expr -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Expr -> u
gmapQ :: (forall d. Data d => d -> u) -> Expr -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Expr -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Expr
Data, Typeable, (forall x. Expr -> Rep Expr x)
-> (forall x. Rep Expr x -> Expr) -> Generic Expr
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)

type Pred = Expr

pattern $bPTrue :: Expr
$mPTrue :: forall r. Expr -> (Void# -> r) -> (Void# -> r) -> r
PTrue         = PAnd []
pattern $bPTop :: Expr
$mPTop :: forall r. Expr -> (Void# -> r) -> (Void# -> r) -> r
PTop          = PAnd []
pattern $bPFalse :: Expr
$mPFalse :: forall r. Expr -> (Void# -> r) -> (Void# -> r) -> r
PFalse        = POr  []
pattern $bEBot :: Expr
$mEBot :: forall r. Expr -> (Void# -> r) -> (Void# -> r) -> r
EBot          = POr  []
pattern $bEEq :: Expr -> Expr -> Expr
$mEEq :: forall r. Expr -> (Expr -> Expr -> r) -> (Void# -> r) -> r
EEq e1 e2     = PAtom Eq    e1 e2
pattern $bETimes :: Expr -> Expr -> Expr
$mETimes :: forall r. Expr -> (Expr -> Expr -> r) -> (Void# -> r) -> r
ETimes e1 e2  = EBin Times  e1 e2
pattern $bERTimes :: Expr -> Expr -> Expr
$mERTimes :: forall r. Expr -> (Expr -> Expr -> r) -> (Void# -> r) -> r
ERTimes e1 e2 = EBin RTimes e1 e2
pattern $bEDiv :: Expr -> Expr -> Expr
$mEDiv :: forall r. Expr -> (Expr -> Expr -> r) -> (Void# -> r) -> r
EDiv e1 e2    = EBin Div    e1 e2
pattern $bERDiv :: Expr -> Expr -> Expr
$mERDiv :: forall r. Expr -> (Expr -> Expr -> r) -> (Void# -> r) -> r
ERDiv e1 e2   = EBin RDiv   e1 e2


data GradInfo = GradInfo {GradInfo -> SrcSpan
gsrc :: SrcSpan, GradInfo -> Maybe SrcSpan
gused :: Maybe SrcSpan}
          deriving (GradInfo -> GradInfo -> Bool
(GradInfo -> GradInfo -> Bool)
-> (GradInfo -> GradInfo -> Bool) -> Eq GradInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GradInfo -> GradInfo -> Bool
$c/= :: GradInfo -> GradInfo -> Bool
== :: GradInfo -> GradInfo -> Bool
$c== :: GradInfo -> GradInfo -> Bool
Eq, Int -> GradInfo -> ShowS
[GradInfo] -> ShowS
GradInfo -> String
(Int -> GradInfo -> ShowS)
-> (GradInfo -> String) -> ([GradInfo] -> ShowS) -> Show GradInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GradInfo] -> ShowS
$cshowList :: [GradInfo] -> ShowS
show :: GradInfo -> String
$cshow :: GradInfo -> String
showsPrec :: Int -> GradInfo -> ShowS
$cshowsPrec :: Int -> GradInfo -> ShowS
Show, Typeable GradInfo
DataType
Constr
Typeable GradInfo
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> GradInfo -> c GradInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c GradInfo)
-> (GradInfo -> Constr)
-> (GradInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c GradInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GradInfo))
-> ((forall b. Data b => b -> b) -> GradInfo -> GradInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> GradInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> GradInfo -> r)
-> (forall u. (forall d. Data d => d -> u) -> GradInfo -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> GradInfo -> m GradInfo)
-> Data GradInfo
GradInfo -> DataType
GradInfo -> Constr
(forall b. Data b => b -> b) -> GradInfo -> GradInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> GradInfo -> c GradInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cGradInfo :: Constr
$tGradInfo :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> GradInfo -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> GradInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> GradInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> GradInfo -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable GradInfo
Data, Typeable, (forall x. GradInfo -> Rep GradInfo x)
-> (forall x. Rep GradInfo x -> GradInfo) -> Generic GradInfo
forall x. Rep GradInfo x -> GradInfo
forall x. GradInfo -> Rep GradInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$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) Maybe SrcSpan
forall a. Maybe a
Nothing

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

eApps :: Expr -> [Expr] -> Expr
eApps :: Expr -> [Expr] -> Expr
eApps Expr
f [Expr]
es  = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
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
eExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
acc) Expr
f
    go [Expr]
acc Expr
e          = (Expr
e, [Expr]
acc)

splitPAnd :: Expr -> [Expr]
splitPAnd :: Expr -> [Expr]
splitPAnd (PAnd [Expr]
es) = (Expr -> [Expr]) -> [Expr] -> [Expr]
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

--------------------------------------------------------------------------------
debruijnIndex :: Expr -> Int
debruijnIndex :: Expr -> Int
debruijnIndex = Expr -> Int
forall a. Num a => Expr -> a
go
  where
    go :: Expr -> a
go (ELam (Symbol, Sort)
_ Expr
e)      = a
1 a -> a -> a
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 a -> a -> a
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 a -> a -> a
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 a -> a -> a
forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e1 a -> a -> a
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)       = (a -> Expr -> a) -> a -> [Expr] -> a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\a
n Expr
e -> a
n a -> a -> a
forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e) a
0 [Expr]
es
    go (POr [Expr]
es)        = (a -> Expr -> a) -> a -> [Expr] -> a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\a
n Expr
e -> a
n a -> a -> a
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 a -> a -> a
forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (PIff Expr
e1 Expr
e2)    = Expr -> a
go Expr
e1 a -> a -> a
forall a. Num a => a -> a -> a
+ Expr -> a
go Expr
e2
    go (PAtom Brel
_ Expr
e1 Expr
e2) = Expr -> a
go Expr
e1 a -> a -> a
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
(Reft -> Reft -> Bool) -> (Reft -> Reft -> Bool) -> Eq Reft
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, Typeable Reft
DataType
Constr
Typeable Reft
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Reft -> c Reft)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Reft)
-> (Reft -> Constr)
-> (Reft -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Reft))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Reft))
-> ((forall b. Data b => b -> b) -> Reft -> Reft)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Reft -> r)
-> (forall u. (forall d. Data d => d -> u) -> Reft -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Reft -> m Reft)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Reft -> m Reft)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Reft -> m Reft)
-> Data Reft
Reft -> DataType
Reft -> Constr
(forall b. Data b => b -> b) -> Reft -> Reft
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Reft -> c Reft
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cReft :: Constr
$tReft :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Reft -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Reft -> u
gmapQ :: (forall d. Data d => d -> u) -> Reft -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Reft -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Reft
Data, Typeable, (forall x. Reft -> Rep Reft x)
-> (forall x. Rep Reft x -> Reft) -> Generic Reft
forall x. Rep Reft x -> Reft
forall x. Reft -> Rep Reft x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$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
(SortedReft -> SortedReft -> Bool)
-> (SortedReft -> SortedReft -> Bool) -> Eq SortedReft
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, Typeable SortedReft
DataType
Constr
Typeable SortedReft
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SortedReft -> c SortedReft)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SortedReft)
-> (SortedReft -> Constr)
-> (SortedReft -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SortedReft))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SortedReft))
-> ((forall b. Data b => b -> b) -> SortedReft -> SortedReft)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SortedReft -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SortedReft -> r)
-> (forall u. (forall d. Data d => d -> u) -> SortedReft -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SortedReft -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SortedReft -> m SortedReft)
-> Data SortedReft
SortedReft -> DataType
SortedReft -> Constr
(forall b. Data b => b -> b) -> SortedReft -> SortedReft
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SortedReft -> c SortedReft
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cRR :: Constr
$tSortedReft :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> SortedReft -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SortedReft -> u
gmapQ :: (forall d. Data d => d -> u) -> SortedReft -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SortedReft -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable SortedReft
Data, Typeable, (forall x. SortedReft -> Rep SortedReft x)
-> (forall x. Rep SortedReft x -> SortedReft) -> Generic SortedReft
forall x. Rep SortedReft x -> SortedReft
forall x. SortedReft -> Rep SortedReft x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SortedReft x -> SortedReft
$cfrom :: forall x. SortedReft -> Rep SortedReft x
Generic)

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

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

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

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

instance Symbolic SymConst where
  symbol :: SymConst -> Symbol
symbol = SymConst -> Symbol
encodeSymConst

encodeSymConst        :: SymConst -> Symbol
encodeSymConst :: SymConst -> Symbol
encodeSymConst (SL Text
s) = Symbol -> Symbol
litSymbol (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Text
s

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

instance Fixpoint SymConst where
  toFix :: SymConst -> Doc
toFix  = Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Symbol -> Doc) -> (SymConst -> Symbol) -> SymConst -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymConst -> Symbol
encodeSymConst

instance Fixpoint KVar where
  toFix :: KVar -> Doc
toFix (KV Symbol
k) = String -> Doc
text String
"$" Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
k

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

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

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

  simplify :: Expr -> Expr
simplify (PAnd [])     = Expr
PTrue
  simplify (POr  [])     = Expr
PFalse
  simplify (PAnd [Expr
p])    = Expr -> Expr
forall a. Fixpoint a => a -> a
simplify Expr
p
  simplify (POr  [Expr
p])    = Expr -> Expr
forall a. Fixpoint a => a -> a
simplify Expr
p

  simplify (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
forall a. Fixpoint a => a -> a
simplify Expr
e)

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

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

  simplify 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 Expr -> [Expr] -> Bool
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 Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqC (PAtom Brel
Ueq (ECon Constant
x) (ECon Constant
y))
               = Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqC (PAtom Brel
Ne Expr
x Expr
y)
               = Expr
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
y
    eqC (PAtom Brel
Une Expr
x Expr
y)
               = Expr
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
y
    eqC Expr
_      = Bool
False

isTautoPred   :: Expr -> Bool
isTautoPred :: Expr -> Bool
isTautoPred Expr
z  = Expr
z Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
PTop Bool -> Bool -> Bool
|| Expr
z Expr -> Expr -> Bool
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 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Ge Expr
x Expr
y)
               = Expr
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Eq Expr
x Expr
y)
               = Expr
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Ueq Expr
x Expr
y)
               = Expr
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
y
    eqT (PAtom Brel
Ne (ECon Constant
x) (ECon Constant
y))
               = Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqT (PAtom Brel
Une (ECon Constant
x) (ECon Constant
y))
               = Constant
x Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
/= Constant
y
    eqT Expr
_      = Bool
False

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

instance PPrint Constant where
  pprintTidy :: Tidy -> Constant -> Doc
pprintTidy Tidy
_ = Constant -> Doc
forall a. Fixpoint a => a -> Doc
toFix

instance PPrint Brel where
  pprintTidy :: Tidy -> Brel -> Doc
pprintTidy Tidy
_ Brel
Eq = Doc
"=="
  pprintTidy Tidy
_ Brel
Ne = Doc
"/="
  pprintTidy Tidy
_ Brel
r  = Brel -> Doc
forall a. Fixpoint a => a -> Doc
toFix Brel
r

instance PPrint Bop where
  pprintTidy :: Tidy -> Bop -> Doc
pprintTidy Tidy
_  = Bop -> Doc
forall a. Fixpoint a => a -> Doc
toFix

instance PPrint Sort where
  pprintTidy :: Tidy -> Sort -> Doc
pprintTidy Tidy
_ = Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix

instance PPrint a => PPrint (TCEmb a) where 
  pprintTidy :: Tidy -> TCEmb a -> Doc
pprintTidy Tidy
k = Tidy -> [(a, (Sort, TCArgs))] -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k ([(a, (Sort, TCArgs))] -> Doc)
-> (TCEmb a -> [(a, (Sort, TCArgs))]) -> TCEmb a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb a -> [(a, (Sort, TCArgs))]
forall a. TCEmb a -> [(a, (Sort, TCArgs))]
tceToList 

instance PPrint KVar where
  pprintTidy :: Tidy -> KVar -> Doc
pprintTidy Tidy
_ (KV Symbol
x) = String -> Doc
text String
"$" Doc -> Doc -> Doc
<-> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
x

instance PPrint SymConst where
  pprintTidy :: Tidy -> SymConst -> Doc
pprintTidy Tidy
_ (SL Text
x) = Doc -> Doc
doubleQuotes (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
x

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

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

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

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

  -- RJ: DO NOT DELETE!
  --  pprintPrec _ k (ECst e so)     = parens $ pprint e <+> ":" <+> {- const (text "...") -} (pprintTidy k so)
  pprintPrec Int
z Tidy
k (ECst Expr
e Sort
_)      = Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k Expr
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall p. Num p => p
zn) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                                   Doc
"not" Doc -> Doc -> Doc
<+> Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
znInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p
    where zn :: p
zn = p
8
  pprintPrec Int
z Tidy
k (PImp Expr
p1 Expr
p2)    = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall p. Num p => p
zi) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                                   (Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p1) Doc -> Doc -> Doc
<+>
                                   Doc
"=>"                     Doc -> Doc -> Doc
<+>
                                   (Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p2)
    where zi :: p
zi = p
2
  pprintPrec Int
z Tidy
k (PIff Expr
p1 Expr
p2)    = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall p. Num p => p
zi) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                                   (Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p1) Doc -> Doc -> Doc
<+>
                                   Doc
"<=>"                    Doc -> Doc -> Doc
<+>
                                   (Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
ziInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
p2)
    where zi :: p
zi = p
2
  pprintPrec Int
z Tidy
k (PAnd [Expr]
ps)       = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall p. Num p => p
za) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                                   Int -> Tidy -> Doc -> Doc -> [Expr] -> Doc
forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin (Int
forall p. Num p => p
za Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Doc
trueD Doc
andD [Expr]
ps
    where za :: p
za = p
3
  pprintPrec Int
z Tidy
k (POr  [Expr]
ps)       = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall p. Num p => p
zo) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                                   Int -> Tidy -> Doc -> Doc -> [Expr] -> Doc
forall a. PPrint a => Int -> Tidy -> Doc -> Doc -> [a] -> Doc
pprintBin (Int
forall p. Num p => p
zo Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Tidy
k Doc
falseD Doc
orD [Expr]
ps
    where zo :: p
zo = p
3
  pprintPrec Int
z Tidy
k (PAtom Brel
r Expr
e1 Expr
e2) = Bool -> Doc -> Doc
parensIf (Int
z Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall p. Num p => p
za) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
                                   Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
zaInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e1 Doc -> Doc -> Doc
<+>
                                   Tidy -> Brel -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Brel
r         Doc -> Doc -> Doc
<+>
                                   Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec (Int
forall p. Num p => p
zaInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Tidy
k Expr
e2
    where za :: p
za = p
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
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> Tidy -> Expr -> 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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"coerce" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
a Doc -> Doc -> Doc
<+> Doc
"~" Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"in" Doc -> Doc -> Doc
<+> Tidy -> Expr -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Expr
e
  pprintPrec Int
_ Tidy
_ p :: Expr
p@(PKVar {})    = Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
p
  pprintPrec Int
_ Tidy
_ (ETApp Expr
e Sort
s)     = Doc
"ETApp" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> Sort -> Doc
forall a. Fixpoint a => a -> Doc
toFix Sort
s
  pprintPrec Int
_ Tidy
_ (ETAbs Expr
e Symbol
s)     = Doc
"ETAbs" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix Expr
e Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. Fixpoint a => a -> Doc
toFix Symbol
s
  pprintPrec Int
z Tidy
k (PGrad KVar
x Subst
_ GradInfo
_ Expr
e) = Int -> Tidy -> Expr -> Doc
forall a. PPrint a => Int -> Tidy -> a -> Doc
pprintPrec Int
z Tidy
k Expr
e Doc -> Doc -> Doc
<+> Doc
"&&" Doc -> Doc -> Doc
<+> KVar -> Doc
forall a. Fixpoint a => a -> Doc
toFix KVar
x -- "??"

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

vIntersperse :: Doc -> [Doc] -> Doc
vIntersperse :: Doc -> [Doc] -> Doc
vIntersperse Doc
_ []     = Doc
empty
vIntersperse Doc
_ [Doc
d]    = Doc
d
vIntersperse Doc
s (Doc
d:[Doc]
ds) = [Doc] -> Doc
vcat (Doc
d Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ((Doc
s Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> [Doc] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Doc]
ds))

pprintReft :: Tidy -> Reft -> Doc
pprintReft :: Tidy -> Reft -> Doc
pprintReft Tidy
k (Reft (Symbol
_,Expr
ra)) = Int -> Tidy -> Doc -> Doc -> [Expr] -> Doc
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 [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
flat Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 then Int
3 else Int
0

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

-- | Values that can be viewed as Constants

-- | Values that can be viewed as Expressions

class Expression a where
  expr   :: a -> Expr

-- | Values that can be viewed as Predicates

class Predicate a where
  prop   :: a -> Expr

instance Expression SortedReft where
  expr :: SortedReft -> Expr
expr (RR Sort
_ Reft
r) = Reft -> Expr
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 = 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 = Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
s

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

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

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

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

instance Predicate Expr where
  prop :: Expr -> Expr
prop = Expr -> Expr
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   = a -> Expr
forall a. Expression a => a -> Expr
expr (a -> Expr) -> (Located a -> a) -> Located a -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val

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

eProp ::  Symbolic a => a -> Expr
eProp :: a -> Expr
eProp = Expr -> Expr
mkProp (Expr -> Expr) -> (a -> Expr) -> a -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Expr
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 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
EVar Symbol
v Bool -> Bool -> Bool
&& Brel -> Bool
isEq Brel
r = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e2
  | Expr
e2 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
EVar Symbol
v Bool -> Bool -> Bool
&& Brel -> Bool
isEq Brel
r = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e1
isSingletonExpr Symbol
v (PIff Expr
e1 Expr
e2) 
  | Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
EVar Symbol
v           = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e2
  | Expr
e2 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
EVar Symbol
v           = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e1
isSingletonExpr Symbol
_ Expr
_        = Maybe Expr
forall a. Maybe a
Nothing

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

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

(|.|) :: 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 = Expr -> Expr
forall a. a -> a
id -- EApp (EVar propConName)

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

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

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

exprReft, notExprReft, uexprReft ::  (Expression a) => a -> Reft
exprReft :: a -> Reft
exprReft      = Brel -> a -> Reft
forall a. Expression a => Brel -> a -> Reft
relReft Brel
Eq
notExprReft :: a -> Reft
notExprReft   = Brel -> a -> Reft
forall a. Expression a => Brel -> a -> Reft
relReft Brel
Ne
uexprReft :: a -> Reft
uexprReft     = Brel -> a -> Reft
forall a. Expression a => Brel -> a -> Reft
relReft Brel
Ueq

propReft      ::  (Predicate a) => a -> Reft
propReft :: a -> Reft
propReft a
p    = (Symbol, Expr) -> Reft
Reft (Symbol
vv_, Expr -> Expr -> Expr
PIff (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eProp Symbol
vv_) (a -> Expr
forall a. Predicate a => a -> Expr
prop a
p))

predReft      :: (Predicate a) => a -> Reft
predReft :: a -> Reft
predReft a
p    = (Symbol, Expr) -> Reft
Reft (Symbol
vv_, a -> Expr
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 = Maybe ([Int], [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ([Int], [Sort], Sort) -> Bool)
-> (SortedReft -> Maybe ([Int], [Sort], Sort))
-> SortedReft
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe ([Int], [Sort], Sort)
functionSort (Sort -> Maybe ([Int], [Sort], Sort))
-> (SortedReft -> Sort)
-> SortedReft
-> Maybe ([Int], [Sort], Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Sort
sr_sort

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

reftPred :: Reft -> Expr
reftPred :: Reft -> 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 = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
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 :: a -> Reft
symbolReft    = Expr -> Reft
forall a. Expression a => a -> Reft
exprReft (Expr -> Reft) -> (a -> Expr) -> a -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Expr
forall a. Symbolic a => a -> Expr
eVar

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

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

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

trueReft, falseReft :: Reft
trueReft :: Reft
trueReft  = (Symbol, 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] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
flatP
  where
    flatP :: Expr -> [Expr]
flatP (PAnd [Expr]
ps) = (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
flatP [Expr]
ps
    flatP Expr
p         = [Expr
p]

conjuncts :: Expr -> [Expr]
conjuncts :: Expr -> [Expr]
conjuncts (PAnd [Expr]
ps) = (Expr -> [Expr]) -> [Expr] -> [Expr]
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)) = Expr -> Bool
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) = Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst (HashMap Symbol Expr -> Subst
Su (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> HashMap Symbol Expr
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)   = a -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms a
x
  substa :: (Symbol -> Symbol) -> Located a -> Located a
substa Symbol -> Symbol
f (Loc SourcePos
l SourcePos
l' a
x) = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' ((Symbol -> Symbol) -> a -> a
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
f a
x)
  substf :: (Symbol -> Expr) -> Located a -> Located a
substf Symbol -> Expr
f (Loc SourcePos
l SourcePos
l' a
x) = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' ((Symbol -> Expr) -> a -> a
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) = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (Subst -> a -> a
forall a. Subable a => Subst -> a -> a
subst Subst
su a
x)


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

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

  bot     :: r -> r

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

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