{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}

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

-- |
-- Module      :  Disco.Syntax.Operators
-- Copyright   :  disco team and contributors
-- Maintainer  :  [email protected]
--
-- Unary and binary operators along with information like precedence,
-- fixity, and concrete syntax.
module Disco.Syntax.Operators (
  -- * Operators
  UOp (..),
  BOp (..),
  TyOp (..),

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

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

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

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

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

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

-- | Binary operators.
data BOp
  = -- | Addition (@+@)
    Add
  | -- | Subtraction (@-@)
    Sub
  | -- | Saturating Subtraction (@.-@ / @∸@)
    SSub
  | -- | Multiplication (@*@)
    Mul
  | -- | Division (@/@)
    Div
  | -- | Exponentiation (@^@)
    Exp
  | -- | Integer division (@//@)
    IDiv
  | -- | Equality test (@==@)
    Eq
  | -- | Not-equal (@/=@)
    Neq
  | -- | Less than (@<@)
    Lt
  | -- | Greater than (@>@)
    Gt
  | -- | Less than or equal (@<=@)
    Leq
  | -- | Greater than or equal (@>=@)
    Geq
  | -- | Logical and (@&&@ / @and@)
    And
  | -- | Logical or (@||@ / @or@)
    Or
  | -- | Logical implies (@->@ / @implies@)
    Impl
  | -- | Logical biconditional (@<->@ / @iff@)
    Iff
  | -- | Modulo (@mod@)
    Mod
  | -- | Divisibility test (@|@)
    Divides
  | -- | Binomial and multinomial coefficients (@choose@)
    Choose
  | -- | List cons (@::@)
    Cons
  | -- | Cartesian product of sets (@**@ / @⨯@)
    CartProd
  | -- | Union of two sets (@union@ / @∪@)
    Union
  | -- | Intersection of two sets (@intersect@ / @∩@)
    Inter
  | -- | Difference between two sets (@\@)
    Diff
  | -- | Element test (@∈@)
    Elem
  | -- | Subset test (@⊆@)
    Subset
  | -- | Make a binary boolean operator into a testable proposition
    Should BOp
  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
$cshowsPrec :: Int -> BOp -> ShowS
showsPrec :: Int -> BOp -> ShowS
$cshow :: BOp -> String
show :: BOp -> String
$cshowList :: [BOp] -> ShowS
showList :: [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
$creadsPrec :: Int -> ReadS BOp
readsPrec :: Int -> ReadS BOp
$creadList :: ReadS [BOp]
readList :: ReadS [BOp]
$creadPrec :: ReadPrec BOp
readPrec :: ReadPrec BOp
$creadListPrec :: ReadPrec [BOp]
readListPrec :: ReadPrec [BOp]
Read, BOp -> BOp -> Bool
(BOp -> BOp -> Bool) -> (BOp -> BOp -> Bool) -> Eq BOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BOp -> BOp -> Bool
== :: BOp -> BOp -> Bool
$c/= :: BOp -> BOp -> Bool
/= :: BOp -> BOp -> Bool
Eq, Eq BOp
Eq BOp =>
(BOp -> BOp -> Ordering)
-> (BOp -> BOp -> Bool)
-> (BOp -> BOp -> Bool)
-> (BOp -> BOp -> Bool)
-> (BOp -> BOp -> Bool)
-> (BOp -> BOp -> BOp)
-> (BOp -> BOp -> BOp)
-> Ord BOp
BOp -> BOp -> Bool
BOp -> BOp -> Ordering
BOp -> BOp -> BOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BOp -> BOp -> Ordering
compare :: BOp -> BOp -> Ordering
$c< :: BOp -> BOp -> Bool
< :: BOp -> BOp -> Bool
$c<= :: BOp -> BOp -> Bool
<= :: BOp -> BOp -> Bool
$c> :: BOp -> BOp -> Bool
> :: BOp -> BOp -> Bool
$c>= :: BOp -> BOp -> Bool
>= :: BOp -> BOp -> Bool
$cmax :: BOp -> BOp -> BOp
max :: BOp -> BOp -> BOp
$cmin :: BOp -> BOp -> BOp
min :: BOp -> BOp -> BOp
Ord, (forall x. BOp -> Rep BOp x)
-> (forall x. Rep BOp x -> BOp) -> Generic BOp
forall x. Rep BOp x -> BOp
forall x. BOp -> Rep BOp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BOp -> Rep BOp x
from :: forall x. BOp -> Rep BOp x
$cto :: forall x. Rep BOp x -> BOp
to :: forall x. Rep BOp x -> BOp
Generic, Typeable BOp
Typeable BOp =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BOp -> c BOp)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BOp)
-> (BOp -> Constr)
-> (BOp -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BOp))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp))
-> ((forall b. Data b => b -> b) -> BOp -> BOp)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r)
-> (forall u. (forall d. Data d => d -> u) -> BOp -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BOp -> m BOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BOp -> m BOp)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BOp -> m BOp)
-> Data BOp
BOp -> Constr
BOp -> DataType
(forall b. Data b => b -> b) -> BOp -> BOp
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u
forall u. (forall d. Data d => d -> u) -> BOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BOp -> c BOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BOp -> c BOp
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BOp -> c BOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BOp
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BOp
$ctoConstr :: BOp -> Constr
toConstr :: BOp -> Constr
$cdataTypeOf :: BOp -> DataType
dataTypeOf :: BOp -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BOp)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp)
$cgmapT :: (forall b. Data b => b -> b) -> BOp -> BOp
gmapT :: (forall b. Data b => b -> b) -> BOp -> BOp
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BOp -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BOp -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
Data, 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 -> Perm AnyName -> BOp -> BOp
AlphaCtx -> NamePatFind -> BOp -> BOp
AlphaCtx -> NthPatFind -> BOp -> BOp
AlphaCtx -> BOp -> BOp -> Bool
AlphaCtx -> BOp -> BOp -> Ordering
BOp -> Bool
BOp -> All
BOp -> NamePatFind
BOp -> NthPatFind
BOp -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> BOp -> BOp -> Bool
aeq' :: AlphaCtx -> BOp -> BOp -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BOp -> f BOp
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> BOp -> f BOp
$cclose :: AlphaCtx -> NamePatFind -> BOp -> BOp
close :: AlphaCtx -> NamePatFind -> BOp -> BOp
$copen :: AlphaCtx -> NthPatFind -> BOp -> BOp
open :: AlphaCtx -> NthPatFind -> BOp -> BOp
$cisPat :: BOp -> DisjointSet AnyName
isPat :: BOp -> DisjointSet AnyName
$cisTerm :: BOp -> All
isTerm :: BOp -> All
$cisEmbed :: BOp -> Bool
isEmbed :: BOp -> Bool
$cnthPatFind :: BOp -> NthPatFind
nthPatFind :: BOp -> NthPatFind
$cnamePatFind :: BOp -> NamePatFind
namePatFind :: BOp -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> BOp -> BOp
swaps' :: AlphaCtx -> Perm AnyName -> BOp -> BOp
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BOp -> (BOp -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> BOp -> (BOp -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BOp -> m (BOp, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BOp -> m (BOp, Perm AnyName)
$cacompare' :: AlphaCtx -> BOp -> BOp -> Ordering
acompare' :: AlphaCtx -> BOp -> BOp -> Ordering
Alpha, Subst t)

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

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

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

-- | Fixity/associativity of infix binary operators (either left,
--   right, or non-associative).
data BFixity
  = -- | Left-associative infix.
    InL
  | -- | Right-associative infix.
    InR
  | -- | Infix.
    In
  deriving (BFixity -> BFixity -> Bool
(BFixity -> BFixity -> Bool)
-> (BFixity -> BFixity -> Bool) -> Eq BFixity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BFixity -> BFixity -> Bool
== :: BFixity -> BFixity -> Bool
$c/= :: BFixity -> BFixity -> Bool
/= :: 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
$ccompare :: BFixity -> BFixity -> Ordering
compare :: BFixity -> BFixity -> Ordering
$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
>= :: BFixity -> BFixity -> Bool
$cmax :: BFixity -> BFixity -> BFixity
max :: BFixity -> BFixity -> BFixity
$cmin :: BFixity -> BFixity -> BFixity
min :: BFixity -> BFixity -> 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
$csucc :: BFixity -> BFixity
succ :: BFixity -> BFixity
$cpred :: BFixity -> BFixity
pred :: BFixity -> BFixity
$ctoEnum :: Int -> BFixity
toEnum :: Int -> BFixity
$cfromEnum :: BFixity -> Int
fromEnum :: BFixity -> Int
$cenumFrom :: BFixity -> [BFixity]
enumFrom :: BFixity -> [BFixity]
$cenumFromThen :: BFixity -> BFixity -> [BFixity]
enumFromThen :: BFixity -> BFixity -> [BFixity]
$cenumFromTo :: BFixity -> BFixity -> [BFixity]
enumFromTo :: BFixity -> BFixity -> [BFixity]
$cenumFromThenTo :: BFixity -> BFixity -> BFixity -> [BFixity]
enumFromThenTo :: BFixity -> BFixity -> BFixity -> [BFixity]
Enum, BFixity
BFixity -> BFixity -> Bounded BFixity
forall a. a -> a -> Bounded a
$cminBound :: BFixity
minBound :: BFixity
$cmaxBound :: BFixity
maxBound :: 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
$cshowsPrec :: Int -> BFixity -> ShowS
showsPrec :: Int -> BFixity -> ShowS
$cshow :: BFixity -> String
show :: BFixity -> String
$cshowList :: [BFixity] -> ShowS
showList :: [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
$cfrom :: forall x. BFixity -> Rep BFixity x
from :: forall x. BFixity -> Rep BFixity x
$cto :: forall x. Rep BFixity x -> BFixity
to :: forall x. Rep BFixity x -> BFixity
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
$c== :: OpFixity -> OpFixity -> Bool
== :: OpFixity -> OpFixity -> Bool
$c/= :: OpFixity -> OpFixity -> Bool
/= :: 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
$cshowsPrec :: Int -> OpFixity -> ShowS
showsPrec :: Int -> OpFixity -> ShowS
$cshow :: OpFixity -> String
show :: OpFixity -> String
$cshowList :: [OpFixity] -> ShowS
showList :: [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
$cfrom :: forall x. OpFixity -> Rep OpFixity x
from :: forall x. OpFixity -> Rep OpFixity x
$cto :: forall x. Rep OpFixity x -> OpFixity
to :: forall x. Rep OpFixity x -> OpFixity
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
$cshowsPrec :: Int -> OpInfo -> ShowS
showsPrec :: Int -> OpInfo -> ShowS
$cshow :: OpInfo -> String
show :: OpInfo -> String
$cshowList :: [OpInfo] -> ShowS
showList :: [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
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
Neq [String
"/=", 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
"≤", String
"=<"]
      , BFixity -> BOp -> [String] -> OpInfo
bopInfo BFixity
InR BOp
Geq [String
">=", 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[OpInfo]]
table Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1]) [[OpInfo]]
table
  assignPrec :: Int -> OpInfo -> OpInfo
assignPrec Int
p OpInfo
op = OpInfo
op {opPrec = p}
  assignPrecs :: Int -> [OpInfo] -> [OpInfo]
assignPrecs Int
p = (OpInfo -> OpInfo) -> [OpInfo] -> [OpInfo]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> OpInfo -> OpInfo
assignPrec 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]

opNames :: [String]
opNames :: [String]
opNames = [String
syn | OpInfo OpFixity
_ [String]
syns Int
_ <- [[OpInfo]] -> [OpInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[OpInfo]]
opTable, String
syn <- (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isAlpha) [String]
syns]

-- | 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 (Should BOp
op) = BOp -> Int
bPrec BOp
op
bPrec 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 OpFixity
_ [String]
_ Int
p) -> Int
p
  Maybe OpInfo
_ -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
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!"

-- | Look up the \"fixity\" (/i.e./ associativity) of a binary operator.
assoc :: BOp -> BFixity
assoc :: BOp -> BFixity
assoc (Should BOp
op) = BOp -> BFixity
assoc BOp
op
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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[OpInfo]]
opTable Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1