{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Syntax.Operators
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- Unary and binary operators along with information like precedence,
-- fixity, and concrete syntax.
--
-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

module Disco.Syntax.Operators
       ( -- * Operators
         UOp(..), BOp(..), TyOp(..)

         -- * Operator info
       , UFixity(..), BFixity(..), OpFixity(..), OpInfo(..)

         -- * Operator tables and lookup
       , opTable, uopMap, bopMap
       , uPrec, bPrec, assoc, funPrec

       ) where

import           Data.Data                        (Data)
import           GHC.Generics                     (Generic)
import           Unbound.Generics.LocallyNameless

import           Data.Map                         (Map, (!))
import qualified Data.Map                         as M

------------------------------------------------------------
-- Operators
------------------------------------------------------------

-- | Unary operators.
data UOp = Neg   -- ^ Arithmetic negation (@-@)
         | Not   -- ^ Logical negation (@not@)
         | Fact  -- ^ Factorial (@!@)
  deriving (Int -> UOp -> ShowS
[UOp] -> ShowS
UOp -> String
(Int -> UOp -> ShowS)
-> (UOp -> String) -> ([UOp] -> ShowS) -> Show UOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UOp] -> ShowS
$cshowList :: [UOp] -> ShowS
show :: UOp -> String
$cshow :: UOp -> String
showsPrec :: Int -> UOp -> ShowS
$cshowsPrec :: Int -> UOp -> ShowS
Show, ReadPrec [UOp]
ReadPrec UOp
Int -> ReadS UOp
ReadS [UOp]
(Int -> ReadS UOp)
-> ReadS [UOp] -> ReadPrec UOp -> ReadPrec [UOp] -> Read UOp
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [UOp]
$creadListPrec :: ReadPrec [UOp]
readPrec :: ReadPrec UOp
$creadPrec :: ReadPrec UOp
readList :: ReadS [UOp]
$creadList :: ReadS [UOp]
readsPrec :: Int -> ReadS UOp
$creadsPrec :: Int -> ReadS UOp
Read, UOp -> UOp -> Bool
(UOp -> UOp -> Bool) -> (UOp -> UOp -> Bool) -> Eq UOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UOp -> UOp -> Bool
$c/= :: UOp -> UOp -> Bool
== :: UOp -> UOp -> Bool
$c== :: UOp -> UOp -> Bool
Eq, Eq UOp
Eq UOp
-> (UOp -> UOp -> Ordering)
-> (UOp -> UOp -> Bool)
-> (UOp -> UOp -> Bool)
-> (UOp -> UOp -> Bool)
-> (UOp -> UOp -> Bool)
-> (UOp -> UOp -> UOp)
-> (UOp -> UOp -> UOp)
-> Ord UOp
UOp -> UOp -> Bool
UOp -> UOp -> Ordering
UOp -> UOp -> UOp
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 :: UOp -> UOp -> UOp
$cmin :: UOp -> UOp -> UOp
max :: UOp -> UOp -> UOp
$cmax :: UOp -> UOp -> UOp
>= :: UOp -> UOp -> Bool
$c>= :: UOp -> UOp -> Bool
> :: UOp -> UOp -> Bool
$c> :: UOp -> UOp -> Bool
<= :: UOp -> UOp -> Bool
$c<= :: UOp -> UOp -> Bool
< :: UOp -> UOp -> Bool
$c< :: UOp -> UOp -> Bool
compare :: UOp -> UOp -> Ordering
$ccompare :: UOp -> UOp -> Ordering
$cp1Ord :: Eq UOp
Ord, (forall x. UOp -> Rep UOp x)
-> (forall x. Rep UOp x -> UOp) -> Generic UOp
forall x. Rep UOp x -> UOp
forall x. UOp -> Rep UOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UOp x -> UOp
$cfrom :: forall x. UOp -> Rep UOp x
Generic, Typeable UOp
DataType
Constr
Typeable UOp
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> UOp -> c UOp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c UOp)
-> (UOp -> Constr)
-> (UOp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c UOp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UOp))
-> ((forall b. Data b => b -> b) -> UOp -> UOp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r)
-> (forall u. (forall d. Data d => d -> u) -> UOp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> UOp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> UOp -> m UOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UOp -> m UOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UOp -> m UOp)
-> Data UOp
UOp -> DataType
UOp -> Constr
(forall b. Data b => b -> b) -> UOp -> UOp
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UOp -> c UOp
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UOp
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) -> UOp -> u
forall u. (forall d. Data d => d -> u) -> UOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UOp -> m UOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UOp -> m UOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UOp -> c UOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UOp)
$cFact :: Constr
$cNot :: Constr
$cNeg :: Constr
$tUOp :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> UOp -> m UOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UOp -> m UOp
gmapMp :: (forall d. Data d => d -> m d) -> UOp -> m UOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UOp -> m UOp
gmapM :: (forall d. Data d => d -> m d) -> UOp -> m UOp
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UOp -> m UOp
gmapQi :: Int -> (forall d. Data d => d -> u) -> UOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UOp -> u
gmapQ :: (forall d. Data d => d -> u) -> UOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UOp -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UOp -> r
gmapT :: (forall b. Data b => b -> b) -> UOp -> UOp
$cgmapT :: (forall b. Data b => b -> b) -> UOp -> UOp
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UOp)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c UOp)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UOp)
dataTypeOf :: UOp -> DataType
$cdataTypeOf :: UOp -> DataType
toConstr :: UOp -> Constr
$ctoConstr :: UOp -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UOp
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UOp -> c UOp
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UOp -> c UOp
$cp1Data :: Typeable UOp
Data, Show UOp
Show UOp
-> (AlphaCtx -> UOp -> UOp -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> UOp -> f UOp)
-> (AlphaCtx -> NamePatFind -> UOp -> UOp)
-> (AlphaCtx -> NthPatFind -> UOp -> UOp)
-> (UOp -> DisjointSet AnyName)
-> (UOp -> All)
-> (UOp -> Bool)
-> (UOp -> NthPatFind)
-> (UOp -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> UOp -> UOp)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> UOp -> (UOp -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> UOp -> m (UOp, Perm AnyName))
-> (AlphaCtx -> UOp -> UOp -> Ordering)
-> Alpha UOp
AlphaCtx -> NthPatFind -> UOp -> UOp
AlphaCtx -> NamePatFind -> UOp -> UOp
AlphaCtx -> Perm AnyName -> UOp -> UOp
AlphaCtx -> UOp -> UOp -> Bool
AlphaCtx -> UOp -> UOp -> Ordering
UOp -> Bool
UOp -> All
UOp -> DisjointSet AnyName
UOp -> NthPatFind
UOp -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UOp -> f UOp
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UOp -> m (UOp, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UOp -> (UOp -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> UOp -> UOp -> Ordering
$cacompare' :: AlphaCtx -> UOp -> UOp -> Ordering
freshen' :: AlphaCtx -> UOp -> m (UOp, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UOp -> m (UOp, Perm AnyName)
lfreshen' :: AlphaCtx -> UOp -> (UOp -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> UOp -> (UOp -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> UOp -> UOp
$cswaps' :: AlphaCtx -> Perm AnyName -> UOp -> UOp
namePatFind :: UOp -> NamePatFind
$cnamePatFind :: UOp -> NamePatFind
nthPatFind :: UOp -> NthPatFind
$cnthPatFind :: UOp -> NthPatFind
isEmbed :: UOp -> Bool
$cisEmbed :: UOp -> Bool
isTerm :: UOp -> All
$cisTerm :: UOp -> All
isPat :: UOp -> DisjointSet AnyName
$cisPat :: UOp -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> UOp -> UOp
$copen :: AlphaCtx -> NthPatFind -> UOp -> UOp
close :: AlphaCtx -> NamePatFind -> UOp -> UOp
$cclose :: AlphaCtx -> NamePatFind -> UOp -> UOp
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> UOp -> f UOp
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> UOp -> f UOp
aeq' :: AlphaCtx -> UOp -> UOp -> Bool
$caeq' :: AlphaCtx -> UOp -> UOp -> Bool
$cp1Alpha :: Show UOp
Alpha, Subst t)

-- | Binary operators.
data BOp = Add      -- ^ Addition (@+@)
         | Sub      -- ^ Subtraction (@-@)
         | SSub     -- ^ Saturating Subtraction (@.-@ / @∸@)
         | Mul      -- ^ Multiplication (@*@)
         | Div      -- ^ Division (@/@)
         | Exp      -- ^ Exponentiation (@^@)
         | IDiv     -- ^ Integer division (@//@)
         | Eq       -- ^ Equality test (@==@)
         | Neq      -- ^ Not-equal (@/=@)
         | Lt       -- ^ Less than (@<@)
         | Gt       -- ^ Greater than (@>@)
         | Leq      -- ^ Less than or equal (@<=@)
         | Geq      -- ^ Greater than or equal (@>=@)
         | Min      -- ^ Minimum (@min@)
         | Max      -- ^ Maximum (@max@)
         | And      -- ^ Logical and (@&&@ / @and@)
         | Or       -- ^ Logical or (@||@ / @or@)
         | Impl     -- ^ Logical implies (@->@ / @implies@)
         | Iff      -- ^ Logical biconditional (@<->@ / @iff@)
         | Mod      -- ^ Modulo (@mod@)
         | Divides  -- ^ Divisibility test (@|@)
         | Choose   -- ^ Binomial and multinomial coefficients (@choose@)
         | Cons     -- ^ List cons (@::@)
         | CartProd -- ^ Cartesian product of sets (@**@ / @⨯@)
         | Union    -- ^ Union of two sets (@union@ / @∪@)
         | Inter    -- ^ Intersection of two sets (@intersect@ / @∩@)
         | Diff     -- ^ Difference between two sets (@\@)
         | Elem     -- ^ Element test (@∈@)
         | Subset   -- ^ Subset test (@⊆@)
         | ShouldEq -- ^ Equality assertion (@=!=@)
  deriving (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, ReadPrec [BOp]
ReadPrec BOp
Int -> ReadS BOp
ReadS [BOp]
(Int -> ReadS BOp)
-> ReadS [BOp] -> ReadPrec BOp -> ReadPrec [BOp] -> Read BOp
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [BOp]
$creadListPrec :: ReadPrec [BOp]
readPrec :: ReadPrec BOp
$creadPrec :: ReadPrec BOp
readList :: ReadS [BOp]
$creadList :: ReadS [BOp]
readsPrec :: Int -> ReadS BOp
$creadsPrec :: Int -> ReadS BOp
Read, 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, (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, 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)
$cShouldEq :: Constr
$cSubset :: Constr
$cElem :: Constr
$cDiff :: Constr
$cInter :: Constr
$cUnion :: Constr
$cCartProd :: Constr
$cCons :: Constr
$cChoose :: Constr
$cDivides :: Constr
$cMod :: Constr
$cIff :: Constr
$cImpl :: Constr
$cOr :: Constr
$cAnd :: Constr
$cMax :: Constr
$cMin :: Constr
$cGeq :: Constr
$cLeq :: Constr
$cGt :: Constr
$cLt :: Constr
$cNeq :: Constr
$cEq :: Constr
$cIDiv :: Constr
$cExp :: Constr
$cDiv :: Constr
$cMul :: Constr
$cSSub :: Constr
$cSub :: Constr
$cAdd :: 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, Show BOp
Show BOp
-> (AlphaCtx -> BOp -> BOp -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> BOp -> f BOp)
-> (AlphaCtx -> NamePatFind -> BOp -> BOp)
-> (AlphaCtx -> NthPatFind -> BOp -> BOp)
-> (BOp -> DisjointSet AnyName)
-> (BOp -> All)
-> (BOp -> Bool)
-> (BOp -> NthPatFind)
-> (BOp -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> BOp -> BOp)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> BOp -> (BOp -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> BOp -> m (BOp, Perm AnyName))
-> (AlphaCtx -> BOp -> BOp -> Ordering)
-> Alpha BOp
AlphaCtx -> NthPatFind -> BOp -> BOp
AlphaCtx -> NamePatFind -> BOp -> BOp
AlphaCtx -> Perm AnyName -> BOp -> BOp
AlphaCtx -> BOp -> BOp -> Bool
AlphaCtx -> BOp -> BOp -> Ordering
BOp -> Bool
BOp -> All
BOp -> DisjointSet AnyName
BOp -> NthPatFind
BOp -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BOp -> f BOp
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BOp -> m (BOp, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BOp -> (BOp -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> BOp -> BOp -> Ordering
$cacompare' :: AlphaCtx -> BOp -> BOp -> Ordering
freshen' :: AlphaCtx -> BOp -> m (BOp, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BOp -> m (BOp, Perm AnyName)
lfreshen' :: AlphaCtx -> BOp -> (BOp -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BOp -> (BOp -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> BOp -> BOp
$cswaps' :: AlphaCtx -> Perm AnyName -> BOp -> BOp
namePatFind :: BOp -> NamePatFind
$cnamePatFind :: BOp -> NamePatFind
nthPatFind :: BOp -> NthPatFind
$cnthPatFind :: BOp -> NthPatFind
isEmbed :: BOp -> Bool
$cisEmbed :: BOp -> Bool
isTerm :: BOp -> All
$cisTerm :: BOp -> All
isPat :: BOp -> DisjointSet AnyName
$cisPat :: BOp -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> BOp -> BOp
$copen :: AlphaCtx -> NthPatFind -> BOp -> BOp
close :: AlphaCtx -> NamePatFind -> BOp -> BOp
$cclose :: AlphaCtx -> NamePatFind -> BOp -> BOp
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> BOp -> f BOp
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BOp -> f BOp
aeq' :: AlphaCtx -> BOp -> BOp -> Bool
$caeq' :: AlphaCtx -> BOp -> BOp -> Bool
$cp1Alpha :: Show BOp
Alpha, Subst t)

-- | Type operators.
data TyOp = Enumerate -- ^ List all values of a type
          | Count     -- ^ Count how many values there are of a type
  deriving (Int -> TyOp -> ShowS
[TyOp] -> ShowS
TyOp -> String
(Int -> TyOp -> ShowS)
-> (TyOp -> String) -> ([TyOp] -> ShowS) -> Show TyOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyOp] -> ShowS
$cshowList :: [TyOp] -> ShowS
show :: TyOp -> String
$cshow :: TyOp -> String
showsPrec :: Int -> TyOp -> ShowS
$cshowsPrec :: Int -> TyOp -> ShowS
Show, TyOp -> TyOp -> Bool
(TyOp -> TyOp -> Bool) -> (TyOp -> TyOp -> Bool) -> Eq TyOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TyOp -> TyOp -> Bool
$c/= :: TyOp -> TyOp -> Bool
== :: TyOp -> TyOp -> Bool
$c== :: TyOp -> TyOp -> Bool
Eq, Eq TyOp
Eq TyOp
-> (TyOp -> TyOp -> Ordering)
-> (TyOp -> TyOp -> Bool)
-> (TyOp -> TyOp -> Bool)
-> (TyOp -> TyOp -> Bool)
-> (TyOp -> TyOp -> Bool)
-> (TyOp -> TyOp -> TyOp)
-> (TyOp -> TyOp -> TyOp)
-> Ord TyOp
TyOp -> TyOp -> Bool
TyOp -> TyOp -> Ordering
TyOp -> TyOp -> TyOp
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 :: TyOp -> TyOp -> TyOp
$cmin :: TyOp -> TyOp -> TyOp
max :: TyOp -> TyOp -> TyOp
$cmax :: TyOp -> TyOp -> TyOp
>= :: TyOp -> TyOp -> Bool
$c>= :: TyOp -> TyOp -> Bool
> :: TyOp -> TyOp -> Bool
$c> :: TyOp -> TyOp -> Bool
<= :: TyOp -> TyOp -> Bool
$c<= :: TyOp -> TyOp -> Bool
< :: TyOp -> TyOp -> Bool
$c< :: TyOp -> TyOp -> Bool
compare :: TyOp -> TyOp -> Ordering
$ccompare :: TyOp -> TyOp -> Ordering
$cp1Ord :: Eq TyOp
Ord, (forall x. TyOp -> Rep TyOp x)
-> (forall x. Rep TyOp x -> TyOp) -> Generic TyOp
forall x. Rep TyOp x -> TyOp
forall x. TyOp -> Rep TyOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TyOp x -> TyOp
$cfrom :: forall x. TyOp -> Rep TyOp x
Generic, Typeable TyOp
DataType
Constr
Typeable TyOp
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TyOp -> c TyOp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TyOp)
-> (TyOp -> Constr)
-> (TyOp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TyOp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyOp))
-> ((forall b. Data b => b -> b) -> TyOp -> TyOp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r)
-> (forall u. (forall d. Data d => d -> u) -> TyOp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TyOp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TyOp -> m TyOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TyOp -> m TyOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TyOp -> m TyOp)
-> Data TyOp
TyOp -> DataType
TyOp -> Constr
(forall b. Data b => b -> b) -> TyOp -> TyOp
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyOp -> c TyOp
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyOp
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) -> TyOp -> u
forall u. (forall d. Data d => d -> u) -> TyOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyOp -> m TyOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyOp -> m TyOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyOp -> c TyOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyOp)
$cCount :: Constr
$cEnumerate :: Constr
$tTyOp :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TyOp -> m TyOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyOp -> m TyOp
gmapMp :: (forall d. Data d => d -> m d) -> TyOp -> m TyOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TyOp -> m TyOp
gmapM :: (forall d. Data d => d -> m d) -> TyOp -> m TyOp
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TyOp -> m TyOp
gmapQi :: Int -> (forall d. Data d => d -> u) -> TyOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyOp -> u
gmapQ :: (forall d. Data d => d -> u) -> TyOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TyOp -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyOp -> r
gmapT :: (forall b. Data b => b -> b) -> TyOp -> TyOp
$cgmapT :: (forall b. Data b => b -> b) -> TyOp -> TyOp
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyOp)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TyOp)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TyOp)
dataTypeOf :: TyOp -> DataType
$cdataTypeOf :: TyOp -> DataType
toConstr :: TyOp -> Constr
$ctoConstr :: TyOp -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TyOp
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyOp -> c TyOp
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TyOp -> c TyOp
$cp1Data :: Typeable TyOp
Data, Show TyOp
Show TyOp
-> (AlphaCtx -> TyOp -> TyOp -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> TyOp -> f TyOp)
-> (AlphaCtx -> NamePatFind -> TyOp -> TyOp)
-> (AlphaCtx -> NthPatFind -> TyOp -> TyOp)
-> (TyOp -> DisjointSet AnyName)
-> (TyOp -> All)
-> (TyOp -> Bool)
-> (TyOp -> NthPatFind)
-> (TyOp -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> TyOp -> TyOp)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> TyOp -> (TyOp -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> TyOp -> m (TyOp, Perm AnyName))
-> (AlphaCtx -> TyOp -> TyOp -> Ordering)
-> Alpha TyOp
AlphaCtx -> NthPatFind -> TyOp -> TyOp
AlphaCtx -> NamePatFind -> TyOp -> TyOp
AlphaCtx -> Perm AnyName -> TyOp -> TyOp
AlphaCtx -> TyOp -> TyOp -> Bool
AlphaCtx -> TyOp -> TyOp -> Ordering
TyOp -> Bool
TyOp -> All
TyOp -> DisjointSet AnyName
TyOp -> NthPatFind
TyOp -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> TyOp -> f TyOp
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> TyOp -> m (TyOp, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> TyOp -> (TyOp -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> TyOp -> TyOp -> Ordering
$cacompare' :: AlphaCtx -> TyOp -> TyOp -> Ordering
freshen' :: AlphaCtx -> TyOp -> m (TyOp, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> TyOp -> m (TyOp, Perm AnyName)
lfreshen' :: AlphaCtx -> TyOp -> (TyOp -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> TyOp -> (TyOp -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> TyOp -> TyOp
$cswaps' :: AlphaCtx -> Perm AnyName -> TyOp -> TyOp
namePatFind :: TyOp -> NamePatFind
$cnamePatFind :: TyOp -> NamePatFind
nthPatFind :: TyOp -> NthPatFind
$cnthPatFind :: TyOp -> NthPatFind
isEmbed :: TyOp -> Bool
$cisEmbed :: TyOp -> Bool
isTerm :: TyOp -> All
$cisTerm :: TyOp -> All
isPat :: TyOp -> DisjointSet AnyName
$cisPat :: TyOp -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> TyOp -> TyOp
$copen :: AlphaCtx -> NthPatFind -> TyOp -> TyOp
close :: AlphaCtx -> NamePatFind -> TyOp -> TyOp
$cclose :: AlphaCtx -> NamePatFind -> TyOp -> TyOp
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> TyOp -> f TyOp
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> TyOp -> f TyOp
aeq' :: AlphaCtx -> TyOp -> TyOp -> Bool
$caeq' :: AlphaCtx -> TyOp -> TyOp -> Bool
$cp1Alpha :: Show TyOp
Alpha, Subst t)

------------------------------------------------------------
-- Operator info
------------------------------------------------------------

-- | Fixities of unary operators (either pre- or postfix).
data UFixity
  = Pre     -- ^ Unary prefix.
  | Post    -- ^ Unary postfix.
  deriving (UFixity -> UFixity -> Bool
(UFixity -> UFixity -> Bool)
-> (UFixity -> UFixity -> Bool) -> Eq UFixity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UFixity -> UFixity -> Bool
$c/= :: UFixity -> UFixity -> Bool
== :: UFixity -> UFixity -> Bool
$c== :: UFixity -> UFixity -> Bool
Eq, Eq UFixity
Eq UFixity
-> (UFixity -> UFixity -> Ordering)
-> (UFixity -> UFixity -> Bool)
-> (UFixity -> UFixity -> Bool)
-> (UFixity -> UFixity -> Bool)
-> (UFixity -> UFixity -> Bool)
-> (UFixity -> UFixity -> UFixity)
-> (UFixity -> UFixity -> UFixity)
-> Ord UFixity
UFixity -> UFixity -> Bool
UFixity -> UFixity -> Ordering
UFixity -> UFixity -> UFixity
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 :: UFixity -> UFixity -> UFixity
$cmin :: UFixity -> UFixity -> UFixity
max :: UFixity -> UFixity -> UFixity
$cmax :: UFixity -> UFixity -> UFixity
>= :: UFixity -> UFixity -> Bool
$c>= :: UFixity -> UFixity -> Bool
> :: UFixity -> UFixity -> Bool
$c> :: UFixity -> UFixity -> Bool
<= :: UFixity -> UFixity -> Bool
$c<= :: UFixity -> UFixity -> Bool
< :: UFixity -> UFixity -> Bool
$c< :: UFixity -> UFixity -> Bool
compare :: UFixity -> UFixity -> Ordering
$ccompare :: UFixity -> UFixity -> Ordering
$cp1Ord :: Eq UFixity
Ord, Int -> UFixity
UFixity -> Int
UFixity -> [UFixity]
UFixity -> UFixity
UFixity -> UFixity -> [UFixity]
UFixity -> UFixity -> UFixity -> [UFixity]
(UFixity -> UFixity)
-> (UFixity -> UFixity)
-> (Int -> UFixity)
-> (UFixity -> Int)
-> (UFixity -> [UFixity])
-> (UFixity -> UFixity -> [UFixity])
-> (UFixity -> UFixity -> [UFixity])
-> (UFixity -> UFixity -> UFixity -> [UFixity])
-> Enum UFixity
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: UFixity -> UFixity -> UFixity -> [UFixity]
$cenumFromThenTo :: UFixity -> UFixity -> UFixity -> [UFixity]
enumFromTo :: UFixity -> UFixity -> [UFixity]
$cenumFromTo :: UFixity -> UFixity -> [UFixity]
enumFromThen :: UFixity -> UFixity -> [UFixity]
$cenumFromThen :: UFixity -> UFixity -> [UFixity]
enumFrom :: UFixity -> [UFixity]
$cenumFrom :: UFixity -> [UFixity]
fromEnum :: UFixity -> Int
$cfromEnum :: UFixity -> Int
toEnum :: Int -> UFixity
$ctoEnum :: Int -> UFixity
pred :: UFixity -> UFixity
$cpred :: UFixity -> UFixity
succ :: UFixity -> UFixity
$csucc :: UFixity -> UFixity
Enum, UFixity
UFixity -> UFixity -> Bounded UFixity
forall a. a -> a -> Bounded a
maxBound :: UFixity
$cmaxBound :: UFixity
minBound :: UFixity
$cminBound :: UFixity
Bounded, Int -> UFixity -> ShowS
[UFixity] -> ShowS
UFixity -> String
(Int -> UFixity -> ShowS)
-> (UFixity -> String) -> ([UFixity] -> ShowS) -> Show UFixity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UFixity] -> ShowS
$cshowList :: [UFixity] -> ShowS
show :: UFixity -> String
$cshow :: UFixity -> String
showsPrec :: Int -> UFixity -> ShowS
$cshowsPrec :: Int -> UFixity -> ShowS
Show, (forall x. UFixity -> Rep UFixity x)
-> (forall x. Rep UFixity x -> UFixity) -> Generic UFixity
forall x. Rep UFixity x -> UFixity
forall x. UFixity -> Rep UFixity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UFixity x -> UFixity
$cfrom :: forall x. UFixity -> Rep UFixity x
Generic)

-- | Fixity/associativity of infix binary operators (either left,
--   right, or non-associative).
data BFixity
  = InL   -- ^ Left-associative infix.
  | InR   -- ^ Right-associative infix.
  | In    -- ^ Infix.
  deriving (BFixity -> BFixity -> Bool
(BFixity -> BFixity -> Bool)
-> (BFixity -> BFixity -> Bool) -> Eq BFixity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BFixity -> BFixity -> Bool
$c/= :: BFixity -> BFixity -> Bool
== :: BFixity -> BFixity -> Bool
$c== :: BFixity -> BFixity -> Bool
Eq, Eq BFixity
Eq BFixity
-> (BFixity -> BFixity -> Ordering)
-> (BFixity -> BFixity -> Bool)
-> (BFixity -> BFixity -> Bool)
-> (BFixity -> BFixity -> Bool)
-> (BFixity -> BFixity -> Bool)
-> (BFixity -> BFixity -> BFixity)
-> (BFixity -> BFixity -> BFixity)
-> Ord BFixity
BFixity -> BFixity -> Bool
BFixity -> BFixity -> Ordering
BFixity -> BFixity -> BFixity
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 :: BFixity -> BFixity -> BFixity
$cmin :: BFixity -> BFixity -> BFixity
max :: BFixity -> BFixity -> BFixity
$cmax :: BFixity -> BFixity -> BFixity
>= :: BFixity -> BFixity -> Bool
$c>= :: BFixity -> BFixity -> Bool
> :: BFixity -> BFixity -> Bool
$c> :: BFixity -> BFixity -> Bool
<= :: BFixity -> BFixity -> Bool
$c<= :: BFixity -> BFixity -> Bool
< :: BFixity -> BFixity -> Bool
$c< :: BFixity -> BFixity -> Bool
compare :: BFixity -> BFixity -> Ordering
$ccompare :: BFixity -> BFixity -> Ordering
$cp1Ord :: Eq BFixity
Ord, Int -> BFixity
BFixity -> Int
BFixity -> [BFixity]
BFixity -> BFixity
BFixity -> BFixity -> [BFixity]
BFixity -> BFixity -> BFixity -> [BFixity]
(BFixity -> BFixity)
-> (BFixity -> BFixity)
-> (Int -> BFixity)
-> (BFixity -> Int)
-> (BFixity -> [BFixity])
-> (BFixity -> BFixity -> [BFixity])
-> (BFixity -> BFixity -> [BFixity])
-> (BFixity -> BFixity -> BFixity -> [BFixity])
-> Enum BFixity
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: BFixity -> BFixity -> BFixity -> [BFixity]
$cenumFromThenTo :: BFixity -> BFixity -> BFixity -> [BFixity]
enumFromTo :: BFixity -> BFixity -> [BFixity]
$cenumFromTo :: BFixity -> BFixity -> [BFixity]
enumFromThen :: BFixity -> BFixity -> [BFixity]
$cenumFromThen :: BFixity -> BFixity -> [BFixity]
enumFrom :: BFixity -> [BFixity]
$cenumFrom :: BFixity -> [BFixity]
fromEnum :: BFixity -> Int
$cfromEnum :: BFixity -> Int
toEnum :: Int -> BFixity
$ctoEnum :: Int -> BFixity
pred :: BFixity -> BFixity
$cpred :: BFixity -> BFixity
succ :: BFixity -> BFixity
$csucc :: BFixity -> BFixity
Enum, BFixity
BFixity -> BFixity -> Bounded BFixity
forall a. a -> a -> Bounded a
maxBound :: BFixity
$cmaxBound :: BFixity
minBound :: BFixity
$cminBound :: BFixity
Bounded, Int -> BFixity -> ShowS
[BFixity] -> ShowS
BFixity -> String
(Int -> BFixity -> ShowS)
-> (BFixity -> String) -> ([BFixity] -> ShowS) -> Show BFixity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BFixity] -> ShowS
$cshowList :: [BFixity] -> ShowS
show :: BFixity -> String
$cshow :: BFixity -> String
showsPrec :: Int -> BFixity -> ShowS
$cshowsPrec :: Int -> BFixity -> ShowS
Show, (forall x. BFixity -> Rep BFixity x)
-> (forall x. Rep BFixity x -> BFixity) -> Generic BFixity
forall x. Rep BFixity x -> BFixity
forall x. BFixity -> Rep BFixity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BFixity x -> BFixity
$cfrom :: forall x. BFixity -> Rep BFixity x
Generic)

-- | Operators together with their fixity.
data OpFixity =
    UOpF UFixity UOp
  | BOpF BFixity BOp
  deriving (OpFixity -> OpFixity -> Bool
(OpFixity -> OpFixity -> Bool)
-> (OpFixity -> OpFixity -> Bool) -> Eq OpFixity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OpFixity -> OpFixity -> Bool
$c/= :: OpFixity -> OpFixity -> Bool
== :: OpFixity -> OpFixity -> Bool
$c== :: OpFixity -> OpFixity -> Bool
Eq, Int -> OpFixity -> ShowS
[OpFixity] -> ShowS
OpFixity -> String
(Int -> OpFixity -> ShowS)
-> (OpFixity -> String) -> ([OpFixity] -> ShowS) -> Show OpFixity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpFixity] -> ShowS
$cshowList :: [OpFixity] -> ShowS
show :: OpFixity -> String
$cshow :: OpFixity -> String
showsPrec :: Int -> OpFixity -> ShowS
$cshowsPrec :: Int -> OpFixity -> ShowS
Show, (forall x. OpFixity -> Rep OpFixity x)
-> (forall x. Rep OpFixity x -> OpFixity) -> Generic OpFixity
forall x. Rep OpFixity x -> OpFixity
forall x. OpFixity -> Rep OpFixity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep OpFixity x -> OpFixity
$cfrom :: forall x. OpFixity -> Rep OpFixity x
Generic)

-- | An @OpInfo@ record contains information about an operator, such
--   as the operator itself, its fixity, a list of concrete syntax
--   representations, and a numeric precedence level.
data OpInfo =
  OpInfo
  { OpInfo -> OpFixity
opFixity :: OpFixity
  , OpInfo -> [String]
opSyns   :: [String]
  , OpInfo -> Int
opPrec   :: Int
  }
  deriving Int -> OpInfo -> ShowS
[OpInfo] -> ShowS
OpInfo -> String
(Int -> OpInfo -> ShowS)
-> (OpInfo -> String) -> ([OpInfo] -> ShowS) -> Show OpInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OpInfo] -> ShowS
$cshowList :: [OpInfo] -> ShowS
show :: OpInfo -> String
$cshow :: OpInfo -> String
showsPrec :: Int -> OpInfo -> ShowS
$cshowsPrec :: Int -> OpInfo -> ShowS
Show

------------------------------------------------------------
-- Operator table
------------------------------------------------------------

-- | The @opTable@ lists all the operators in the language, in order
--   of precedence (highest precedence first).  Operators in the same
--   list have the same precedence.  This table is used by both the
--   parser and the pretty-printer.
opTable :: [[OpInfo]]
opTable :: [[OpInfo]]
opTable =
  [[OpInfo]] -> [[OpInfo]]
assignPrecLevels
  [ [ UFixity -> UOp -> [String] -> OpInfo
uopInfo UFixity
Pre  UOp
Not     [String
"not", String
"¬"]
    ]
  , [ UFixity -> UOp -> [String] -> OpInfo
uopInfo UFixity
Post UOp
Fact    [String
"!"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Exp     [String
"^"]
    ]
  , [ UFixity -> UOp -> [String] -> OpInfo
uopInfo UFixity
Pre  UOp
Neg     [String
"-"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
In   BOp
Choose  [String
"choose"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
CartProd [String
"><", String
"⨯"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Union   [String
"union", String
"∪"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Inter   [String
"intersect", String
"∩"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Diff    [String
"\\"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Min     [String
"min"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Max     [String
"max"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Mul     [String
"*"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Div     [String
"/"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Mod     [String
"mod", String
"%"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
IDiv    [String
"//"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Add     [String
"+"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Sub     [String
"-"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
SSub    [String
".-", String
"∸"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Cons    [String
"::"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Eq      [String
"=="]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
ShouldEq [String
"=!="]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Neq     [String
"/=", String
"≠"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Lt      [String
"<"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Gt      [String
">"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Leq     [String
"<=", String
"≤"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Geq     [String
">=", String
"≥"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Divides [String
"divides"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Subset  [String
"subset", String
"⊆"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InL  BOp
Elem    [String
"elem", String
"∈"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
And     [String
"/\\", String
"and", String
"∧", String
"&&"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR  BOp
Or      [String
"\\/", String
"or", String
"∨", String
"||"]
    ]
  , [ BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR BOp
Impl     [String
"->", String
"==>", String
"→", String
"implies"]
    , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR BOp
Iff      [String
"<->", String
"<==>", String
"↔", String
"iff"]
    ]
  ]
  where
    uopInfo :: UFixity -> UOp -> [String] -> OpInfo
uopInfo UFixity
fx UOp
op [String]
syns = OpFixity -> [String] -> Int -> OpInfo
OpInfo (UFixity -> UOp -> OpFixity
UOpF UFixity
fx UOp
op) [String]
syns (-Int
1)
    bopInfo :: BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
fx BOp
op [String]
syns = OpFixity -> [String] -> Int -> OpInfo
OpInfo (BFixity -> BOp -> OpFixity
BOpF BFixity
fx BOp
op) [String]
syns (-Int
1)

    -- Start at precedence level 2 so we can give level 1 to ascription, and level 0
    -- to the ambient context + parentheses etc.
    assignPrecLevels :: [[OpInfo]] -> [[OpInfo]]
assignPrecLevels [[OpInfo]]
table = (Int -> [OpInfo] -> [OpInfo]) -> [Int] -> [[OpInfo]] -> [[OpInfo]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> [OpInfo] -> [OpInfo]
assignPrecs ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
2 .. [[OpInfo]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[OpInfo]]
tableInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1]) [[OpInfo]]
table
    assignPrecs :: Int -> [OpInfo] -> [OpInfo]
assignPrecs Int
p [OpInfo]
ops      = (OpInfo -> OpInfo) -> [OpInfo] -> [OpInfo]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> OpInfo -> OpInfo
assignPrec Int
p) [OpInfo]
ops
    assignPrec :: Int -> OpInfo -> OpInfo
assignPrec  Int
p OpInfo
op       = OpInfo
op { opPrec :: Int
opPrec = Int
p }

-- | A map from all unary operators to their associated 'OpInfo' records.
uopMap :: Map UOp OpInfo
uopMap :: Map UOp OpInfo
uopMap = [(UOp, OpInfo)] -> Map UOp OpInfo
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(UOp, OpInfo)] -> Map UOp OpInfo)
-> [(UOp, OpInfo)] -> Map UOp OpInfo
forall a b. (a -> b) -> a -> b
$
  [ (UOp
op, OpInfo
info) | [OpInfo]
opLevel <- [[OpInfo]]
opTable, info :: OpInfo
info@(OpInfo (UOpF UFixity
_ UOp
op) [String]
_ Int
_) <- [OpInfo]
opLevel ]

-- | A map from all binary operators to their associatied 'OpInfo' records.
bopMap :: Map BOp OpInfo
bopMap :: Map BOp OpInfo
bopMap = [(BOp, OpInfo)] -> Map BOp OpInfo
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(BOp, OpInfo)] -> Map BOp OpInfo)
-> [(BOp, OpInfo)] -> Map BOp OpInfo
forall a b. (a -> b) -> a -> b
$
  [ (BOp
op, OpInfo
info) | [OpInfo]
opLevel <- [[OpInfo]]
opTable, info :: OpInfo
info@(OpInfo (BOpF BFixity
_ BOp
op) [String]
_ Int
_) <- [OpInfo]
opLevel ]

-- | A convenient function for looking up the precedence of a unary operator.
uPrec :: UOp -> Int
uPrec :: UOp -> Int
uPrec = OpInfo -> Int
opPrec (OpInfo -> Int) -> (UOp -> OpInfo) -> UOp -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map UOp OpInfo
uopMap Map UOp OpInfo -> UOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
!)

-- | A convenient function for looking up the precedence of a binary operator.
bPrec :: BOp -> Int
bPrec :: BOp -> Int
bPrec = OpInfo -> Int
opPrec (OpInfo -> Int) -> (BOp -> OpInfo) -> BOp -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map BOp OpInfo
bopMap Map BOp OpInfo -> BOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
!)

-- | Look up the \"fixity\" (/i.e./ associativity) of a binary operator.
assoc :: BOp -> BFixity
assoc :: BOp -> BFixity
assoc BOp
op =
  case BOp -> Map BOp OpInfo -> Maybe OpInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup BOp
op Map BOp OpInfo
bopMap of
    Just (OpInfo (BOpF BFixity
fx BOp
_) [String]
_ Int
_) -> BFixity
fx
    Maybe OpInfo
_                             -> String -> BFixity
forall a. HasCallStack => String -> a
error (String -> BFixity) -> String -> BFixity
forall a b. (a -> b) -> a -> b
$ String
"BOp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BOp -> String
forall a. Show a => a -> String
show BOp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in bopMap!"

-- | The precedence level of function application (higher than any
--   other precedence level).
funPrec :: Int
funPrec :: Int
funPrec = [[OpInfo]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[OpInfo]]
opTableInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1