{-# 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 Unbound.Generics.LocallyNameless hiding (LFresh, lunbind)
import Prelude hiding ((<>))
import qualified Prelude as P
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
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
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. 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
RationalDisplay -> DataType
RationalDisplay -> Constr
(forall b. Data b => b -> b) -> RationalDisplay -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u.
Int -> (forall d. Data d => d -> u) -> RationalDisplay -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> RationalDisplay -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> RationalDisplay -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RationalDisplay -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Eq 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
Ord, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> RationalDisplay -> m (RationalDisplay, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> RationalDisplay -> m (RationalDisplay, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
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 = 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
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. 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
Core -> DataType
Core -> Constr
(forall b. Data b => b -> b) -> Core -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Core -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Core -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Core -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Core -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha)
instance Plated Core where
plate :: Traversal' Core Core
plate = 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
|
OShouldLt Type
|
OMatchErr
|
OCrash
|
OId
|
OLookupSeq
|
OExtendSeq
|
OAnd
|
OOr
|
OImpl
deriving (Int -> Op -> ShowS
[Op] -> ShowS
Op -> String
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. 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
Op -> DataType
Op -> Constr
(forall b. Data b => b -> b) -> Op -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Show 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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Op -> Op -> Bool
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
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
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 = forall a. Plated a => (a -> a) -> a -> a
transform forall a b. (a -> b) -> a -> b
$ \case
CVar QName Core
y
| QName Core
x 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 = forall a. Plated a => (a -> a) -> a -> a
transform forall a b. (a -> b) -> a -> b
$ \case
CVar QName Core
y -> case 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 :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
pretty = \case
CVar QName Core
qn -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty QName Core
qn
CNum RationalDisplay
_ Rational
r
| forall a. Ratio a -> a
denominator Rational
r forall a. Eq a => a -> a -> Bool
== Integer
1 -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show (forall a. Ratio a -> a
numerator Rational
r))
| Bool
otherwise -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show (forall a. Ratio a -> a
numerator Rational
r)) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"/" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (forall a. Show a => a -> String
show (forall a. Ratio a -> a
denominator Rational
r))
CApp (CConst Op
op) (CPair Core
c1 Core
c2)
| Op -> Bool
isInfix Op
op -> forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c1 forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c2)
CApp (CConst Op
op) Core
c
| Op -> Bool
isPrefix Op
op -> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c
| Op -> Bool
isPostfix Op
op -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op)
CConst Op
op -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Op
op
CInj Side
s Core
c -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$ forall a. Side -> a -> a -> a
selectSide Side
s Sem r (Doc ann)
"left" Sem r (Doc ann)
"right" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c)
CCase Core
c Bind (Name Core) Core
l Bind (Name Core) Core
r -> do
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 forall a b. (a -> b) -> a -> b
$ \(Name Core
x, Core
lc) -> do
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 forall a b. (a -> b) -> a -> b
$ \(Name Core
y, Core
rc) -> do
forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 forall a b. (a -> b) -> a -> b
$
Sem r (Doc ann)
"case"
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"of {"
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
[ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"left" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Core
x) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"->" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
lc
, forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"right" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Core
y) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"->" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
rc
]
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Sem r (Doc ann)
"}"
Core
CUnit -> Sem r (Doc ann)
"unit"
CPair Core
c1 Core
c2 -> forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c1 forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
", " forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c2)
CProj Side
s Core
c -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$ forall a. Side -> a -> a -> a
selectSide Side
s Sem r (Doc ann)
"fst" Sem r (Doc ann)
"snd" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c)
CAbs Bind [Name Core] Core
lam -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$ do
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 forall a b. (a -> b) -> a -> b
$ \([Name Core]
xs, Core
body) -> Sem r (Doc ann)
"λ" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Name Core]
xs) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"." forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
body)
CApp Core
c1 Core
c2 -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c1) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c2)
CTest [(String, Type, Name Core)]
xs Core
c -> Sem r (Doc ann)
"test" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[(String, Type, Name Core)] -> Sem r (Doc ann)
prettyTestVars [(String, Type, Name Core)]
xs forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c
CType Type
ty -> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Type
ty
CDelay Bind [Name Core] [Core]
d -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA forall a b. (a -> b) -> a -> b
$ do
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 forall a b. (a -> b) -> a -> b
$ \([Name Core]
xs, [Core]
bodies) ->
Sem r (Doc ann)
"delay" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Name Core]
xs) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"." forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ([Core] -> Core
toTuple [Core]
bodies)
CForce Core
c -> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"force" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c)
toTuple :: [Core] -> Core
toTuple :: [Core] -> Core
toTuple = 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 ann)
prettyTestVars :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
[(String, Type, Name Core)] -> Sem r (Doc ann)
prettyTestVars = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {r :: EffectRow} {t} {t} {ann}.
(Member (Reader PA) r, Member LFresh r, Pretty t, Pretty t) =>
(String, t, t) -> Sem r (Doc ann)
prettyTestVar
where
prettyTestVar :: (String, t, t) -> Sem r (Doc ann)
prettyTestVar (String
s, t
ty, t
n) = forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," [forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s, forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
ty, forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
n])
isInfix, isPrefix, isPostfix :: Op -> Bool
isInfix :: Op -> Bool
isInfix OShouldEq {} = Bool
True
isInfix OShouldLt {} = Bool
True
isInfix Op
op =
Op
op
forall a. Ord a => a -> Set a -> Bool
`S.member` 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, Op
OAnd, Op
OOr, Op
OImpl]
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 :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Op -> Sem r (Doc ann)
pretty (OForall [Type]
tys) = Sem r (Doc ann)
"∀" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Type]
tys) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
pretty (OExists [Type]
tys) = Sem r (Doc ann)
"∃" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Type]
tys) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"."
pretty Op
op
| Op -> Bool
isInfix Op
op = Sem r (Doc ann)
"~" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"~"
| Op -> Bool
isPrefix Op
op = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"~"
| Op -> Bool
isPostfix Op
op = Sem r (Doc ann)
"~" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op)
| Bool
otherwise = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
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
"=!="
OShouldLt 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
"∃"
Op
OAnd -> String
"and"
Op
OOr -> String
"or"
Op
OImpl -> String
"implies"