{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
module Disco.AST.Core
(
RationalDisplay(..)
, Core(..)
, Op(..), opArity, substQC, substsQC
)
where
import Control.Lens.Plated
import Data.Data (Data)
import Data.Data.Lens (uniplate)
import qualified Data.Set as S
import GHC.Generics
import Prelude hiding ((<>))
import qualified Prelude as P
import Unbound.Generics.LocallyNameless hiding (LFresh, lunbind)
import Disco.Effects.LFresh
import Polysemy (Members, Sem)
import Polysemy.Reader
import Data.Ratio
import Disco.AST.Generic (Side, selectSide)
import Disco.Names (QName)
import Disco.Pretty
import Disco.Types
data RationalDisplay = Fraction | Decimal
deriving (RationalDisplay -> RationalDisplay -> Bool
(RationalDisplay -> RationalDisplay -> Bool)
-> (RationalDisplay -> RationalDisplay -> Bool)
-> Eq RationalDisplay
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RationalDisplay -> RationalDisplay -> Bool
$c/= :: RationalDisplay -> RationalDisplay -> Bool
== :: RationalDisplay -> RationalDisplay -> Bool
$c== :: RationalDisplay -> RationalDisplay -> Bool
Eq, Int -> RationalDisplay -> ShowS
[RationalDisplay] -> ShowS
RationalDisplay -> String
(Int -> RationalDisplay -> ShowS)
-> (RationalDisplay -> String)
-> ([RationalDisplay] -> ShowS)
-> Show RationalDisplay
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RationalDisplay] -> ShowS
$cshowList :: [RationalDisplay] -> ShowS
show :: RationalDisplay -> String
$cshow :: RationalDisplay -> String
showsPrec :: Int -> RationalDisplay -> ShowS
$cshowsPrec :: Int -> RationalDisplay -> ShowS
Show, (forall x. RationalDisplay -> Rep RationalDisplay x)
-> (forall x. Rep RationalDisplay x -> RationalDisplay)
-> Generic RationalDisplay
forall x. Rep RationalDisplay x -> RationalDisplay
forall x. RationalDisplay -> Rep RationalDisplay x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RationalDisplay x -> RationalDisplay
$cfrom :: forall x. RationalDisplay -> Rep RationalDisplay x
Generic, Typeable RationalDisplay
DataType
Constr
Typeable RationalDisplay
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RationalDisplay -> c RationalDisplay)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RationalDisplay)
-> (RationalDisplay -> Constr)
-> (RationalDisplay -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RationalDisplay))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RationalDisplay))
-> ((forall b. Data b => b -> b)
-> RationalDisplay -> RationalDisplay)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r)
-> (forall u.
(forall d. Data d => d -> u) -> RationalDisplay -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> RationalDisplay -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay)
-> Data RationalDisplay
RationalDisplay -> DataType
RationalDisplay -> Constr
(forall b. Data b => b -> b) -> RationalDisplay -> RationalDisplay
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RationalDisplay -> c RationalDisplay
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RationalDisplay
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) -> RationalDisplay -> u
forall u. (forall d. Data d => d -> u) -> RationalDisplay -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RationalDisplay
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RationalDisplay -> c RationalDisplay
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RationalDisplay)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RationalDisplay)
$cDecimal :: Constr
$cFraction :: Constr
$tRationalDisplay :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
gmapMp :: (forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
gmapM :: (forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> RationalDisplay -> m RationalDisplay
gmapQi :: Int -> (forall d. Data d => d -> u) -> RationalDisplay -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> RationalDisplay -> u
gmapQ :: (forall d. Data d => d -> u) -> RationalDisplay -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RationalDisplay -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RationalDisplay -> r
gmapT :: (forall b. Data b => b -> b) -> RationalDisplay -> RationalDisplay
$cgmapT :: (forall b. Data b => b -> b) -> RationalDisplay -> RationalDisplay
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RationalDisplay)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RationalDisplay)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RationalDisplay)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RationalDisplay)
dataTypeOf :: RationalDisplay -> DataType
$cdataTypeOf :: RationalDisplay -> DataType
toConstr :: RationalDisplay -> Constr
$ctoConstr :: RationalDisplay -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RationalDisplay
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RationalDisplay
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RationalDisplay -> c RationalDisplay
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RationalDisplay -> c RationalDisplay
$cp1Data :: Typeable RationalDisplay
Data, Eq RationalDisplay
Eq RationalDisplay
-> (RationalDisplay -> RationalDisplay -> Ordering)
-> (RationalDisplay -> RationalDisplay -> Bool)
-> (RationalDisplay -> RationalDisplay -> Bool)
-> (RationalDisplay -> RationalDisplay -> Bool)
-> (RationalDisplay -> RationalDisplay -> Bool)
-> (RationalDisplay -> RationalDisplay -> RationalDisplay)
-> (RationalDisplay -> RationalDisplay -> RationalDisplay)
-> Ord RationalDisplay
RationalDisplay -> RationalDisplay -> Bool
RationalDisplay -> RationalDisplay -> Ordering
RationalDisplay -> RationalDisplay -> RationalDisplay
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 :: RationalDisplay -> RationalDisplay -> RationalDisplay
$cmin :: RationalDisplay -> RationalDisplay -> RationalDisplay
max :: RationalDisplay -> RationalDisplay -> RationalDisplay
$cmax :: RationalDisplay -> RationalDisplay -> RationalDisplay
>= :: RationalDisplay -> RationalDisplay -> Bool
$c>= :: RationalDisplay -> RationalDisplay -> Bool
> :: RationalDisplay -> RationalDisplay -> Bool
$c> :: RationalDisplay -> RationalDisplay -> Bool
<= :: RationalDisplay -> RationalDisplay -> Bool
$c<= :: RationalDisplay -> RationalDisplay -> Bool
< :: RationalDisplay -> RationalDisplay -> Bool
$c< :: RationalDisplay -> RationalDisplay -> Bool
compare :: RationalDisplay -> RationalDisplay -> Ordering
$ccompare :: RationalDisplay -> RationalDisplay -> Ordering
$cp1Ord :: Eq RationalDisplay
Ord, Show RationalDisplay
Show RationalDisplay
-> (AlphaCtx -> RationalDisplay -> RationalDisplay -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> RationalDisplay -> f RationalDisplay)
-> (AlphaCtx -> NamePatFind -> RationalDisplay -> RationalDisplay)
-> (AlphaCtx -> NthPatFind -> RationalDisplay -> RationalDisplay)
-> (RationalDisplay -> DisjointSet AnyName)
-> (RationalDisplay -> All)
-> (RationalDisplay -> Bool)
-> (RationalDisplay -> NthPatFind)
-> (RationalDisplay -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> RationalDisplay -> RationalDisplay)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> RationalDisplay
-> (RationalDisplay -> Perm AnyName -> m b)
-> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> RationalDisplay -> m (RationalDisplay, Perm AnyName))
-> (AlphaCtx -> RationalDisplay -> RationalDisplay -> Ordering)
-> Alpha RationalDisplay
AlphaCtx -> NthPatFind -> RationalDisplay -> RationalDisplay
AlphaCtx -> NamePatFind -> RationalDisplay -> RationalDisplay
AlphaCtx -> Perm AnyName -> RationalDisplay -> RationalDisplay
AlphaCtx -> RationalDisplay -> RationalDisplay -> Bool
AlphaCtx -> RationalDisplay -> RationalDisplay -> Ordering
RationalDisplay -> Bool
RationalDisplay -> All
RationalDisplay -> DisjointSet AnyName
RationalDisplay -> NthPatFind
RationalDisplay -> 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) -> RationalDisplay -> f RationalDisplay
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> RationalDisplay -> m (RationalDisplay, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> RationalDisplay
-> (RationalDisplay -> Perm AnyName -> m b)
-> m b
acompare' :: AlphaCtx -> RationalDisplay -> RationalDisplay -> Ordering
$cacompare' :: AlphaCtx -> RationalDisplay -> RationalDisplay -> Ordering
freshen' :: AlphaCtx -> RationalDisplay -> m (RationalDisplay, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> RationalDisplay -> m (RationalDisplay, Perm AnyName)
lfreshen' :: AlphaCtx
-> RationalDisplay
-> (RationalDisplay -> Perm AnyName -> m b)
-> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> RationalDisplay
-> (RationalDisplay -> Perm AnyName -> m b)
-> m b
swaps' :: AlphaCtx -> Perm AnyName -> RationalDisplay -> RationalDisplay
$cswaps' :: AlphaCtx -> Perm AnyName -> RationalDisplay -> RationalDisplay
namePatFind :: RationalDisplay -> NamePatFind
$cnamePatFind :: RationalDisplay -> NamePatFind
nthPatFind :: RationalDisplay -> NthPatFind
$cnthPatFind :: RationalDisplay -> NthPatFind
isEmbed :: RationalDisplay -> Bool
$cisEmbed :: RationalDisplay -> Bool
isTerm :: RationalDisplay -> All
$cisTerm :: RationalDisplay -> All
isPat :: RationalDisplay -> DisjointSet AnyName
$cisPat :: RationalDisplay -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> RationalDisplay -> RationalDisplay
$copen :: AlphaCtx -> NthPatFind -> RationalDisplay -> RationalDisplay
close :: AlphaCtx -> NamePatFind -> RationalDisplay -> RationalDisplay
$cclose :: AlphaCtx -> NamePatFind -> RationalDisplay -> RationalDisplay
fvAny' :: AlphaCtx
-> (AnyName -> f AnyName) -> RationalDisplay -> f RationalDisplay
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> RationalDisplay -> f RationalDisplay
aeq' :: AlphaCtx -> RationalDisplay -> RationalDisplay -> Bool
$caeq' :: AlphaCtx -> RationalDisplay -> RationalDisplay -> Bool
$cp1Alpha :: Show RationalDisplay
Alpha)
instance Semigroup RationalDisplay where
RationalDisplay
Decimal <> :: RationalDisplay -> RationalDisplay -> RationalDisplay
<> RationalDisplay
_ = RationalDisplay
Decimal
RationalDisplay
_ <> RationalDisplay
Decimal = RationalDisplay
Decimal
RationalDisplay
_ <> RationalDisplay
_ = RationalDisplay
Fraction
instance Monoid RationalDisplay where
mempty :: RationalDisplay
mempty = RationalDisplay
Fraction
mappend :: RationalDisplay -> RationalDisplay -> RationalDisplay
mappend = RationalDisplay -> RationalDisplay -> RationalDisplay
forall a. Semigroup a => a -> a -> a
(P.<>)
data Core where
CVar :: QName Core -> Core
CNum :: RationalDisplay -> Rational -> Core
CConst :: Op -> Core
CInj :: Side -> Core -> Core
CCase :: Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core
CUnit :: Core
CPair :: Core -> Core -> Core
CProj :: Side -> Core -> Core
CAbs :: Bind [Name Core] Core -> Core
CApp :: Core -> Core -> Core
CTest :: [(String, Type, Name Core)] -> Core -> Core
CType :: Type -> Core
CDelay :: Bind [Name Core] [Core] -> Core
CForce :: Core -> Core
deriving (Int -> Core -> ShowS
[Core] -> ShowS
Core -> String
(Int -> Core -> ShowS)
-> (Core -> String) -> ([Core] -> ShowS) -> Show Core
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Core] -> ShowS
$cshowList :: [Core] -> ShowS
show :: Core -> String
$cshow :: Core -> String
showsPrec :: Int -> Core -> ShowS
$cshowsPrec :: Int -> Core -> ShowS
Show, (forall x. Core -> Rep Core x)
-> (forall x. Rep Core x -> Core) -> Generic Core
forall x. Rep Core x -> Core
forall x. Core -> Rep Core x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Core x -> Core
$cfrom :: forall x. Core -> Rep Core x
Generic, Typeable Core
DataType
Constr
Typeable Core
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core)
-> (Core -> Constr)
-> (Core -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Core))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Core))
-> ((forall b. Data b => b -> b) -> Core -> Core)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r)
-> (forall u. (forall d. Data d => d -> u) -> Core -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Core -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Core -> m Core)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m Core)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m Core)
-> Data Core
Core -> DataType
Core -> Constr
(forall b. Data b => b -> b) -> Core -> Core
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core
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) -> Core -> u
forall u. (forall d. Data d => d -> u) -> Core -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Core -> m Core
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m Core
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Core)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Core)
$cCForce :: Constr
$cCDelay :: Constr
$cCType :: Constr
$cCTest :: Constr
$cCApp :: Constr
$cCAbs :: Constr
$cCProj :: Constr
$cCPair :: Constr
$cCUnit :: Constr
$cCCase :: Constr
$cCInj :: Constr
$cCConst :: Constr
$cCNum :: Constr
$cCVar :: Constr
$tCore :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Core -> m Core
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m Core
gmapMp :: (forall d. Data d => d -> m d) -> Core -> m Core
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m Core
gmapM :: (forall d. Data d => d -> m d) -> Core -> m Core
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Core -> m Core
gmapQi :: Int -> (forall d. Data d => d -> u) -> Core -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Core -> u
gmapQ :: (forall d. Data d => d -> u) -> Core -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Core -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
gmapT :: (forall b. Data b => b -> b) -> Core -> Core
$cgmapT :: (forall b. Data b => b -> b) -> Core -> Core
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Core)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Core)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Core)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Core)
dataTypeOf :: Core -> DataType
$cdataTypeOf :: Core -> DataType
toConstr :: Core -> Constr
$ctoConstr :: Core -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core
$cp1Data :: Typeable Core
Data, Show Core
Show Core
-> (AlphaCtx -> Core -> Core -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Core -> f Core)
-> (AlphaCtx -> NamePatFind -> Core -> Core)
-> (AlphaCtx -> NthPatFind -> Core -> Core)
-> (Core -> DisjointSet AnyName)
-> (Core -> All)
-> (Core -> Bool)
-> (Core -> NthPatFind)
-> (Core -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Core -> Core)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Core -> (Core -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName))
-> (AlphaCtx -> Core -> Core -> Ordering)
-> Alpha Core
AlphaCtx -> NthPatFind -> Core -> Core
AlphaCtx -> NamePatFind -> Core -> Core
AlphaCtx -> Perm AnyName -> Core -> Core
AlphaCtx -> Core -> Core -> Bool
AlphaCtx -> Core -> Core -> Ordering
Core -> Bool
Core -> All
Core -> DisjointSet AnyName
Core -> NthPatFind
Core -> 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) -> Core -> f Core
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Core -> (Core -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Core -> Core -> Ordering
$cacompare' :: AlphaCtx -> Core -> Core -> Ordering
freshen' :: AlphaCtx -> Core -> m (Core, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName)
lfreshen' :: AlphaCtx -> Core -> (Core -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Core -> (Core -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Core -> Core
$cswaps' :: AlphaCtx -> Perm AnyName -> Core -> Core
namePatFind :: Core -> NamePatFind
$cnamePatFind :: Core -> NamePatFind
nthPatFind :: Core -> NthPatFind
$cnthPatFind :: Core -> NthPatFind
isEmbed :: Core -> Bool
$cisEmbed :: Core -> Bool
isTerm :: Core -> All
$cisTerm :: Core -> All
isPat :: Core -> DisjointSet AnyName
$cisPat :: Core -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Core -> Core
$copen :: AlphaCtx -> NthPatFind -> Core -> Core
close :: AlphaCtx -> NamePatFind -> Core -> Core
$cclose :: AlphaCtx -> NamePatFind -> Core -> Core
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Core -> f Core
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Core -> f Core
aeq' :: AlphaCtx -> Core -> Core -> Bool
$caeq' :: AlphaCtx -> Core -> Core -> Bool
$cp1Alpha :: Show Core
Alpha)
instance Plated Core where
plate :: (Core -> f Core) -> Core -> f Core
plate = (Core -> f Core) -> Core -> f Core
forall a. Data a => Traversal' a a
uniplate
data Op
=
OAdd
|
ONeg
|
OSqrt
|
OFloor
|
OCeil
|
OAbs
|
OMul
|
ODiv
|
OExp
|
OMod
|
ODivides
|
OMultinom
|
OFact
|
OEq
|
OLt
|
OEnum
|
OCount
|
OPower
|
OBagElem
|
OListElem
|
OEachBag
|
OEachSet
|
OFilterBag
|
OMerge
|
OBagUnions
|
OSummary
|
OEmptyGraph
|
OVertex
|
OOverlay
|
OConnect
|
OInsert
|
OLookup
|
OUntil
|
OSetToList
|
OBagToSet
|
OBagToList
|
OListToSet
|
OListToBag
|
OBagToCounts
|
OCountsToBag
|
OUnsafeCountsToBag
|
OMapToSet
|
OSetToMap
|
OIsPrime
|
OFactor
|
OFrac
|
OForall [Type]
|
OExists [Type]
|
OHolds
|
ONotProp
|
OShouldEq Type
|
OMatchErr
|
OCrash
|
OId
|
OLookupSeq
|
OExtendSeq
deriving (Int -> Op -> ShowS
[Op] -> ShowS
Op -> String
(Int -> Op -> ShowS)
-> (Op -> String) -> ([Op] -> ShowS) -> Show Op
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Op] -> ShowS
$cshowList :: [Op] -> ShowS
show :: Op -> String
$cshow :: Op -> String
showsPrec :: Int -> Op -> ShowS
$cshowsPrec :: Int -> Op -> ShowS
Show, (forall x. Op -> Rep Op x)
-> (forall x. Rep Op x -> Op) -> Generic Op
forall x. Rep Op x -> Op
forall x. Op -> Rep Op x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Op x -> Op
$cfrom :: forall x. Op -> Rep Op x
Generic, Typeable Op
DataType
Constr
Typeable Op
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op)
-> (Op -> Constr)
-> (Op -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op))
-> ((forall b. Data b => b -> b) -> Op -> Op)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r)
-> (forall u. (forall d. Data d => d -> u) -> Op -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Op -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Op -> m Op)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op)
-> Data Op
Op -> DataType
Op -> Constr
(forall b. Data b => b -> b) -> Op -> Op
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
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) -> Op -> u
forall u. (forall d. Data d => d -> u) -> Op -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Op -> m Op
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
$cOExtendSeq :: Constr
$cOLookupSeq :: Constr
$cOId :: Constr
$cOCrash :: Constr
$cOMatchErr :: Constr
$cOShouldEq :: Constr
$cONotProp :: Constr
$cOHolds :: Constr
$cOExists :: Constr
$cOForall :: Constr
$cOFrac :: Constr
$cOFactor :: Constr
$cOIsPrime :: Constr
$cOSetToMap :: Constr
$cOMapToSet :: Constr
$cOUnsafeCountsToBag :: Constr
$cOCountsToBag :: Constr
$cOBagToCounts :: Constr
$cOListToBag :: Constr
$cOListToSet :: Constr
$cOBagToList :: Constr
$cOBagToSet :: Constr
$cOSetToList :: Constr
$cOUntil :: Constr
$cOLookup :: Constr
$cOInsert :: Constr
$cOConnect :: Constr
$cOOverlay :: Constr
$cOVertex :: Constr
$cOEmptyGraph :: Constr
$cOSummary :: Constr
$cOBagUnions :: Constr
$cOMerge :: Constr
$cOFilterBag :: Constr
$cOEachSet :: Constr
$cOEachBag :: Constr
$cOListElem :: Constr
$cOBagElem :: Constr
$cOPower :: Constr
$cOCount :: Constr
$cOEnum :: Constr
$cOLt :: Constr
$cOEq :: Constr
$cOFact :: Constr
$cOMultinom :: Constr
$cODivides :: Constr
$cOMod :: Constr
$cOExp :: Constr
$cODiv :: Constr
$cOMul :: Constr
$cOAbs :: Constr
$cOCeil :: Constr
$cOFloor :: Constr
$cOSqrt :: Constr
$cONeg :: Constr
$cOAdd :: Constr
$tOp :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Op -> m Op
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapMp :: (forall d. Data d => d -> m d) -> Op -> m Op
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapM :: (forall d. Data d => d -> m d) -> Op -> m Op
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapQi :: Int -> (forall d. Data d => d -> u) -> Op -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
gmapQ :: (forall d. Data d => d -> u) -> Op -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
gmapT :: (forall b. Data b => b -> b) -> Op -> Op
$cgmapT :: (forall b. Data b => b -> b) -> Op -> Op
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Op)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
dataTypeOf :: Op -> DataType
$cdataTypeOf :: Op -> DataType
toConstr :: Op -> Constr
$ctoConstr :: Op -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
$cp1Data :: Typeable Op
Data, Show Op
Show Op
-> (AlphaCtx -> Op -> Op -> Bool)
-> (forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Op -> f Op)
-> (AlphaCtx -> NamePatFind -> Op -> Op)
-> (AlphaCtx -> NthPatFind -> Op -> Op)
-> (Op -> DisjointSet AnyName)
-> (Op -> All)
-> (Op -> Bool)
-> (Op -> NthPatFind)
-> (Op -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Op -> Op)
-> (forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Op -> (Op -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName))
-> (AlphaCtx -> Op -> Op -> Ordering)
-> Alpha Op
AlphaCtx -> NthPatFind -> Op -> Op
AlphaCtx -> NamePatFind -> Op -> Op
AlphaCtx -> Perm AnyName -> Op -> Op
AlphaCtx -> Op -> Op -> Bool
AlphaCtx -> Op -> Op -> Ordering
Op -> Bool
Op -> All
Op -> DisjointSet AnyName
Op -> NthPatFind
Op -> 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) -> Op -> f Op
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Op -> (Op -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Op -> Op -> Ordering
$cacompare' :: AlphaCtx -> Op -> Op -> Ordering
freshen' :: AlphaCtx -> Op -> m (Op, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName)
lfreshen' :: AlphaCtx -> Op -> (Op -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Op -> (Op -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Op -> Op
$cswaps' :: AlphaCtx -> Perm AnyName -> Op -> Op
namePatFind :: Op -> NamePatFind
$cnamePatFind :: Op -> NamePatFind
nthPatFind :: Op -> NthPatFind
$cnthPatFind :: Op -> NthPatFind
isEmbed :: Op -> Bool
$cisEmbed :: Op -> Bool
isTerm :: Op -> All
$cisTerm :: Op -> All
isPat :: Op -> DisjointSet AnyName
$cisPat :: Op -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Op -> Op
$copen :: AlphaCtx -> NthPatFind -> Op -> Op
close :: AlphaCtx -> NamePatFind -> Op -> Op
$cclose :: AlphaCtx -> NamePatFind -> Op -> Op
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Op -> f Op
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Op -> f Op
aeq' :: AlphaCtx -> Op -> Op -> Bool
$caeq' :: AlphaCtx -> Op -> Op -> Bool
$cp1Alpha :: Show Op
Alpha, Op -> Op -> Bool
(Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c== :: Op -> Op -> Bool
Eq, Eq Op
Eq Op
-> (Op -> Op -> Ordering)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Op)
-> (Op -> Op -> Op)
-> Ord Op
Op -> Op -> Bool
Op -> Op -> Ordering
Op -> Op -> Op
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 :: Op -> Op -> Op
$cmin :: Op -> Op -> Op
max :: Op -> Op -> Op
$cmax :: Op -> Op -> Op
>= :: Op -> Op -> Bool
$c>= :: Op -> Op -> Bool
> :: Op -> Op -> Bool
$c> :: Op -> Op -> Bool
<= :: Op -> Op -> Bool
$c<= :: Op -> Op -> Bool
< :: Op -> Op -> Bool
$c< :: Op -> Op -> Bool
compare :: Op -> Op -> Ordering
$ccompare :: Op -> Op -> Ordering
$cp1Ord :: Eq Op
Ord)
opArity :: Op -> Int
opArity :: Op -> Int
opArity Op
OEmptyGraph = Int
0
opArity Op
OMatchErr = Int
0
opArity Op
_ = Int
1
substQC :: QName Core -> Core -> Core -> Core
substQC :: QName Core -> Core -> Core -> Core
substQC QName Core
x Core
s = (Core -> Core) -> Core -> Core
forall a. Plated a => (a -> a) -> a -> a
transform ((Core -> Core) -> Core -> Core) -> (Core -> Core) -> Core -> Core
forall a b. (a -> b) -> a -> b
$ \case
CVar QName Core
y
| QName Core
x QName Core -> QName Core -> Bool
forall a. Eq a => a -> a -> Bool
== QName Core
y -> Core
s
| Bool
otherwise -> QName Core -> Core
CVar QName Core
y
Core
t -> Core
t
substsQC :: [(QName Core, Core)] -> Core -> Core
substsQC :: [(QName Core, Core)] -> Core -> Core
substsQC [(QName Core, Core)]
xs = (Core -> Core) -> Core -> Core
forall a. Plated a => (a -> a) -> a -> a
transform ((Core -> Core) -> Core -> Core) -> (Core -> Core) -> Core -> Core
forall a b. (a -> b) -> a -> b
$ \case
CVar QName Core
y -> case QName Core -> [(QName Core, Core)] -> Maybe Core
forall a b. Eq a => a -> [(a, b)] -> Maybe b
P.lookup QName Core
y [(QName Core, Core)]
xs of
Just Core
c -> Core
c
Maybe Core
_ -> QName Core -> Core
CVar QName Core
y
Core
t -> Core
t
instance Pretty Core where
pretty :: Core -> Sem r Doc
pretty = \case
CVar QName Core
qn -> QName Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty QName Core
qn
CNum RationalDisplay
_ Rational
r
| Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r))
| Bool
otherwise -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r)) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"/" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r))
CApp (CConst Op
op) (CPair Core
c1 Core
c2)
| Op -> Bool
isInfix Op
op -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c2)
CApp (CConst Op
op) Core
c
| Op -> Bool
isPrefix Op
op -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c
| Op -> Bool
isPostfix Op
op -> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op)
CConst Op
op -> Op -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Op
op
CInj Side
s Core
c -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Side -> Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Side -> a -> a -> a
selectSide Side
s Sem r Doc
"left" Sem r Doc
"right" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c)
CCase Core
c Bind (Name Core) Core
l Bind (Name Core) Core
r -> do
Bind (Name Core) Core
-> ((Name Core, Core) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind (Name Core) Core
l (((Name Core, Core) -> Sem r Doc) -> Sem r Doc)
-> ((Name Core, Core) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Name Core
x, Core
lc) -> do
Bind (Name Core) Core
-> ((Name Core, Core) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind (Name Core) Core
r (((Name Core, Core) -> Sem r Doc) -> Sem r Doc)
-> ((Name Core, Core) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \(Name Core
y, Core
rc) -> do
Sem r Doc
"case" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"of {"
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Int -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat
[ PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"left" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Name Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Core
x) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"->" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
lc
, PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"right" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Name Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Name Core
y) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"->" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
rc
])
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"}"
Core
CUnit -> Sem r Doc
"unit"
CPair Core
c1 Core
c2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c1 Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
", " Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c2)
CProj Side
s Core
c -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Side -> Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Side -> a -> a -> a
selectSide Side
s Sem r Doc
"fst" Sem r Doc
"snd" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c)
CAbs Bind [Name Core] Core
lam -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
Bind [Name Core] Core
-> (([Name Core], Core) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Core] Core
lam ((([Name Core], Core) -> Sem r Doc) -> Sem r Doc)
-> (([Name Core], Core) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Name Core]
xs, Core
body) -> Sem r Doc
"λ" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," ((Name Core -> Sem r Doc) -> [Name Core] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Name Core]
xs) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"." Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
body)
CApp Core
c1 Core
c2 -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
lt (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c1) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c2)
CTest [(String, Type, Name Core)]
xs Core
c -> Sem r Doc
"test" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> [(String, Type, Name Core)] -> Sem r Doc
forall (r :: EffectRow).
Members '[Reader PA, LFresh] r =>
[(String, Type, Name Core)] -> Sem r Doc
prettyTestVars [(String, Type, Name Core)]
xs Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c
CType Type
ty -> Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Type
ty
CDelay Bind [Name Core] [Core]
d -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
initPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ do
Bind [Name Core] [Core]
-> (([Name Core], [Core]) -> Sem r Doc) -> Sem r Doc
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Core] [Core]
d ((([Name Core], [Core]) -> Sem r Doc) -> Sem r Doc)
-> (([Name Core], [Core]) -> Sem r Doc) -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ \([Name Core]
xs, [Core]
bodies) ->
Sem r Doc
"delay" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," ((Name Core -> Sem r Doc) -> [Name Core] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Name Core]
xs) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"." Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ([Core] -> Core
toTuple [Core]
bodies)
CForce Core
c -> PA -> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
PA -> Sem r Doc -> Sem r Doc
withPA PA
funPA (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"force" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc -> Sem r Doc
forall (r :: EffectRow).
Member (Reader PA) r =>
Sem r Doc -> Sem r Doc
rt (Core -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty Core
c)
toTuple :: [Core] -> Core
toTuple :: [Core] -> Core
toTuple = (Core -> Core -> Core) -> Core -> [Core] -> Core
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Core -> Core -> Core
CPair Core
CUnit
prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r Doc
prettyTestVars :: [(String, Type, Name Core)] -> Sem r Doc
prettyTestVars = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
brackets (Sem r Doc -> Sem r Doc)
-> ([(String, Type, Name Core)] -> Sem r Doc)
-> [(String, Type, Name Core)]
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," ([Sem r Doc] -> Sem r Doc)
-> ([(String, Type, Name Core)] -> [Sem r Doc])
-> [(String, Type, Name Core)]
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Type, Name Core) -> Sem r Doc)
-> [(String, Type, Name Core)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type, Name Core) -> Sem r Doc
forall (r :: EffectRow) t t.
(Member (Reader PA) r, Member LFresh r, Pretty t, Pretty t) =>
(String, t, t) -> Sem r Doc
prettyTestVar
where
prettyTestVar :: (String, t, t) -> Sem r Doc
prettyTestVar (String
s, t
ty, t
n) = Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => f Doc -> f Doc
parens (Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
s, t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
ty, t -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty t
n])
isInfix, isPrefix, isPostfix :: Op -> Bool
isInfix :: Op -> Bool
isInfix OShouldEq{} = Bool
True
isInfix Op
op = Op
op Op -> Set Op -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` [Op] -> Set Op
forall a. Ord a => [a] -> Set a
S.fromList
[ Op
OAdd, Op
OMul, Op
ODiv, Op
OExp, Op
OMod, Op
ODivides, Op
OMultinom, Op
OEq, Op
OLt]
isPrefix :: Op -> Bool
isPrefix Op
ONeg = Bool
True
isPrefix Op
_ = Bool
False
isPostfix :: Op -> Bool
isPostfix Op
OFact = Bool
True
isPostfix Op
_ = Bool
False
instance Pretty Op where
pretty :: Op -> Sem r Doc
pretty (OForall [Type]
tys) = Sem r Doc
"∀" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," ((Type -> Sem r Doc) -> [Type] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Type]
tys) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"."
pretty (OExists [Type]
tys) = Sem r Doc
"∃" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate Sem r Doc
"," ((Type -> Sem r Doc) -> [Type] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty [Type]
tys) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"."
pretty Op
op
| Op -> Bool
isInfix Op
op = Sem r Doc
"~" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"~"
| Op -> Bool
isPrefix Op
op = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op) Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> Sem r Doc
"~"
| Op -> Bool
isPostfix Op
op = Sem r Doc
"~" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op)
| Bool
otherwise = String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Op -> String
opToStr Op
op)
opToStr :: Op -> String
opToStr :: Op -> String
opToStr = \case
Op
OAdd -> String
"+"
Op
ONeg -> String
"-"
Op
OSqrt -> String
"sqrt"
Op
OFloor -> String
"floor"
Op
OCeil -> String
"ceil"
Op
OAbs -> String
"abs"
Op
OMul -> String
"*"
Op
ODiv -> String
"/"
Op
OExp -> String
"^"
Op
OMod -> String
"mod"
Op
ODivides -> String
"divides"
Op
OMultinom -> String
"choose"
Op
OFact -> String
"!"
Op
OEq -> String
"=="
Op
OLt -> String
"<"
Op
OEnum -> String
"enumerate"
Op
OCount -> String
"count"
Op
OPower -> String
"power"
Op
OBagElem -> String
"elem_bag"
Op
OListElem -> String
"elem_list"
Op
OEachBag -> String
"each_bag"
Op
OEachSet -> String
"each_set"
Op
OFilterBag -> String
"filter_bag"
Op
OMerge -> String
"merge"
Op
OBagUnions -> String
"unions_bag"
Op
OSummary -> String
"summary"
Op
OEmptyGraph -> String
"emptyGraph"
Op
OVertex -> String
"vertex"
Op
OOverlay -> String
"overlay"
Op
OConnect -> String
"connect"
Op
OInsert -> String
"insert"
Op
OLookup -> String
"lookup"
Op
OUntil -> String
"until"
Op
OSetToList -> String
"set2list"
Op
OBagToSet -> String
"bag2set"
Op
OBagToList -> String
"bag2list"
Op
OListToSet -> String
"list2set"
Op
OListToBag -> String
"list2bag"
Op
OBagToCounts -> String
"bag2counts"
Op
OCountsToBag -> String
"counts2bag"
Op
OUnsafeCountsToBag -> String
"ucounts2bag"
Op
OMapToSet -> String
"map2set"
Op
OSetToMap -> String
"set2map"
Op
OIsPrime -> String
"isPrime"
Op
OFactor -> String
"factor"
Op
OFrac -> String
"frac"
Op
OHolds -> String
"holds"
Op
ONotProp -> String
"not"
OShouldEq Type
_ -> String
"=!="
Op
OMatchErr -> String
"matchErr"
Op
OCrash -> String
"crash"
Op
OId -> String
"id"
Op
OLookupSeq -> String
"lookupSeq"
Op
OExtendSeq -> String
"extendSeq"
OForall{} -> String
"∀"
OExists{} -> String
"∃"