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

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

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

-- |
-- 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.
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
  = -- | Arithmetic negation (@-@)
    Neg
  | -- | Logical negation (@not@)
    Not
  | -- | Factorial (@!@)
    Fact
  deriving (Int -> UOp -> ShowS
[UOp] -> ShowS
UOp -> String
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]
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
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
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
Ord, 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
UOp -> DataType
UOp -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> UOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UOp -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UOp -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UOp -> m (UOp, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> UOp -> m (UOp, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
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
  | -- | Minimum (@min@)
    Min
  | -- | Maximum (@max@)
    Max
  | -- | 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
  | -- | Equality assertion (@=!=@)
    ShouldEq
  | -- | Less than assertion (@!<@)
    ShouldLt
  deriving (Int -> BOp -> ShowS
[BOp] -> ShowS
BOp -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BOp] -> ShowS
$cshowList :: [BOp] -> ShowS
show :: BOp -> String
$cshow :: BOp -> String
showsPrec :: Int -> BOp -> ShowS
$cshowsPrec :: Int -> BOp -> ShowS
Show, ReadPrec [BOp]
ReadPrec BOp
Int -> ReadS BOp
ReadS [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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BOp -> BOp -> Bool
$c/= :: BOp -> BOp -> Bool
== :: BOp -> BOp -> Bool
$c== :: BOp -> BOp -> Bool
Eq, Eq BOp
BOp -> BOp -> Bool
BOp -> BOp -> Ordering
BOp -> BOp -> BOp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BOp -> BOp -> BOp
$cmin :: BOp -> BOp -> BOp
max :: BOp -> BOp -> BOp
$cmax :: BOp -> BOp -> BOp
>= :: BOp -> BOp -> Bool
$c>= :: BOp -> BOp -> Bool
> :: BOp -> BOp -> Bool
$c> :: BOp -> BOp -> Bool
<= :: BOp -> BOp -> Bool
$c<= :: BOp -> BOp -> Bool
< :: BOp -> BOp -> Bool
$c< :: BOp -> BOp -> Bool
compare :: BOp -> BOp -> Ordering
$ccompare :: BOp -> BOp -> Ordering
Ord, 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
BOp -> DataType
BOp -> Constr
(forall b. Data b => b -> b) -> BOp -> BOp
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u
forall u. (forall d. Data d => d -> u) -> BOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BOp -> c BOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BOp -> m BOp
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BOp -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> BOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BOp -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOp -> r
gmapT :: (forall b. Data b => b -> b) -> BOp -> BOp
$cgmapT :: (forall b. Data b => b -> b) -> BOp -> BOp
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOp)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BOp)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BOp)
dataTypeOf :: BOp -> DataType
$cdataTypeOf :: BOp -> DataType
toConstr :: BOp -> Constr
$ctoConstr :: BOp -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BOp
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BOp -> c BOp
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BOp -> c BOp
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BOp -> m (BOp, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> BOp -> m (BOp, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
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
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
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
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
Ord, 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
TyOp -> DataType
TyOp -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> TyOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TyOp -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> TyOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TyOp -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> TyOp -> m (TyOp, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> TyOp -> m (TyOp, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
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
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
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
Ord, Int -> UFixity
UFixity -> Int
UFixity -> [UFixity]
UFixity -> UFixity
UFixity -> UFixity -> [UFixity]
UFixity -> UFixity -> UFixity -> [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
forall a. a -> a -> Bounded a
maxBound :: UFixity
$cmaxBound :: UFixity
minBound :: UFixity
$cminBound :: UFixity
Bounded, Int -> UFixity -> ShowS
[UFixity] -> ShowS
UFixity -> String
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. 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
  = -- | Left-associative infix.
    InL
  | -- | Right-associative infix.
    InR
  | -- | Infix.
    In
  deriving (BFixity -> BFixity -> Bool
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
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
Ord, Int -> BFixity
BFixity -> Int
BFixity -> [BFixity]
BFixity -> BFixity
BFixity -> BFixity -> [BFixity]
BFixity -> BFixity -> BFixity -> [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
forall a. a -> a -> Bounded a
maxBound :: BFixity
$cmaxBound :: BFixity
minBound :: BFixity
$cminBound :: BFixity
Bounded, Int -> BFixity -> ShowS
[BFixity] -> ShowS
BFixity -> String
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. 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
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
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. 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
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
ShouldLt [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 = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> [OpInfo] -> [OpInfo]
assignPrecs (forall a. [a] -> [a]
reverse [Int
2 .. forall (t :: * -> *) a. Foldable t => t a -> Int
length [[OpInfo]]
table forall a. Num a => a -> a -> a
+ Int
1]) [[OpInfo]]
table
  assignPrec :: Int -> OpInfo -> OpInfo
assignPrec Int
p OpInfo
op = OpInfo
op {opPrec :: Int
opPrec = Int
p}
  assignPrecs :: Int -> [OpInfo] -> [OpInfo]
assignPrecs Int
p = 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 =
  forall k a. Ord k => [(k, a)] -> Map k a
M.fromList 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 =
  forall k a. Ord k => [(k, a)] -> Map k a
M.fromList 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map UOp OpInfo
uopMap 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map BOp OpInfo
bopMap 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 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
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"BOp " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BOp
op 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [[OpInfo]]
opTable forall a. Num a => a -> a -> a
+ Int
1