{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
module Disco.Syntax.Operators (
UOp (..),
BOp (..),
TyOp (..),
UFixity (..),
BFixity (..),
OpFixity (..),
OpInfo (..),
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
data UOp
=
Neg
|
Not
|
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)
data BOp
=
Add
|
Sub
|
SSub
|
Mul
|
Div
|
Exp
|
IDiv
|
Eq
|
Neq
|
Lt
|
Gt
|
Leq
|
Geq
|
Min
|
Max
|
And
|
Or
|
Impl
|
Iff
|
Mod
|
Divides
|
Choose
|
Cons
|
CartProd
|
Union
|
Inter
|
Diff
|
Elem
|
Subset
|
ShouldEq
|
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)
data TyOp
=
Enumerate
|
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)
data UFixity
=
Pre
|
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)
data BFixity
=
InL
|
InR
|
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)
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)
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)
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)
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)
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]
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]
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
!)
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
!)
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!"
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