{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE DeriveDataTypeable       #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE OverloadedStrings        #-}
{-# LANGUAGE UndecidableInstances     #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.AST.Core
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Abstract syntax trees representing the desugared, untyped core
-- language for Disco.
-----------------------------------------------------------------------------

module Disco.AST.Core
       ( -- * Core AST
         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

-- | A type of flags specifying whether to display a rational number
--   as a fraction or a decimal.
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

-- | The 'Monoid' instance for 'RationalDisplay' corresponds to the
--   idea that the result should be displayed as a decimal if any
--   decimal literals are used in the input; otherwise, the default is
--   to display as a fraction.  So the identity element is 'Fraction',
--   and 'Decimal' always wins when combining.
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.<>)

-- | AST for the desugared, untyped core language.
data Core where
  -- | A variable.
  CVar :: QName Core -> Core
  -- | A rational number.
  CNum :: RationalDisplay -> Rational -> Core
  -- | A built-in constant.
  CConst :: Op -> Core
  -- | An injection into a sum type, i.e. a value together with a tag
  --   indicating which element of a sum type we are in.  For example,
  --   false is represented by @CSum L CUnit@; @right(v)@ is
  --   represented by @CSum R v@.  Note we do not need to remember
  --   which type the constructor came from; if the program
  --   typechecked then we will never end up comparing constructors
  --   from different types.
  CInj :: Side -> Core -> Core
  -- | A primitive case expression on a value of a sum type.
  CCase :: Core -> Bind (Name Core) Core -> Bind (Name Core) Core -> Core
  -- | The unit value.
  CUnit :: Core
  -- | A pair of values.
  CPair :: Core -> Core -> Core
  -- | A projection from a product type, i.e. @fst@ or @snd@.
  CProj :: Side -> Core -> Core
  -- | An anonymous function.
  CAbs :: Bind [Name Core] Core -> Core
  -- | Function application.
  CApp :: Core -> Core -> Core
  -- | A "test frame" under which a test case is run. Records the
  --   types and legible names of the variables that should
  --   be reported to the user if the test fails.
  CTest :: [(String, Type, Name Core)] -> Core -> Core
  -- | A type.
  CType :: Type -> Core
  -- | Introduction form for a lazily evaluated value of type Lazy T
  --   for some type T.  We can have multiple bindings to multiple
  --   terms to create a simple target for compiling mutual recursion.
  CDelay :: Bind [Name Core] [Core] -> Core
  -- | Force evaluation of a lazy value.
  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

-- | Operators that can show up in the core language.  Note that not
--   all surface language operators show up here, since some are
--   desugared into combinators of the operators here.
data Op
  = -- | Addition (@+@)
    OAdd
  | -- | Arithmetic negation (@-@)
    ONeg
  | -- | Integer square root (@sqrt@)
    OSqrt
  | -- | Floor of fractional type (@floor@)
    OFloor
  | -- | Ceiling of fractional type (@ceiling@)
    OCeil
  | -- | Absolute value (@abs@)
    OAbs
  | -- | Multiplication (@*@)
    OMul
  | -- | Division (@/@)
    ODiv
  | -- | Exponentiation (@^@)
    OExp
  | -- | Modulo (@mod@)
    OMod
  | -- | Divisibility test (@|@)
    ODivides
  | -- | Multinomial coefficient (@choose@)
    OMultinom
  | -- | Factorial (@!@)
    OFact
  | -- | Equality test (@==@)
    OEq
  | -- | Less than (@<@)
    OLt
  | -- Type operators

    -- | Enumerate the values of a type.
    OEnum
  | -- | Count the values of a type.
    OCount
  | -- Container operations

    -- | Size of two sets (@size@)
    OSize
  | -- | Power set/bag of a given set/bag
    --   (@power@).
    OPower
  | -- | Set/bag element test.
    OBagElem
  | -- | List element test.
    OListElem
  | -- | Map a function over a bag.  Carries the
    --   output type of the function.
    OEachBag
  | -- | Map a function over a set. Carries the
    --   output type of the function.
    OEachSet
  | -- | Filter a bag.
    OFilterBag
  | -- | Merge two bags/sets.
    OMerge
  | -- | Bag join, i.e. union a bag of bags.
    OBagUnions
  | -- | Adjacency List of given graph
    OSummary
  | -- | Empty graph
    OEmptyGraph
  | -- | Construct a vertex with given value
    OVertex
  | -- | Graph overlay
    OOverlay
  | -- | Graph connect
    OConnect
  | -- | Map insert
    OInsert
  | -- | Map lookup
    OLookup
  | -- Ellipses

    -- | Continue until end, @[x, y, z .. e]@
    OUntil
  | -- Container conversion

    -- | set -> list conversion (sorted order).
    OSetToList
  | -- | bag -> set conversion (forget duplicates).
    OBagToSet
  | -- | bag -> list conversion (sorted order).
    OBagToList
  | -- | list -> set conversion (forget order, duplicates).
    OListToSet
  | -- | list -> bag conversion (forget order).
    OListToBag
  | -- | bag -> set of counts
    OBagToCounts
  | -- | set of counts -> bag
    OCountsToBag
  | -- | Map k v -> Set (k × v)
    OMapToSet
  | -- | Set (k × v) -> Map k v
    OSetToMap
  | -- Number theory primitives

    -- | Primality test
    OIsPrime
  | -- | Factorization
    OFactor
  | -- | Turn a rational into a (num, denom) pair
    OFrac
  | -- Propositions

    -- | Universal quantification. Applied to a closure
    --   @t1, ..., tn -> Prop@ it yields a @Prop@.
    OForall [Type]
  | -- | Existential quantification. Applied to a closure
    --   @t1, ..., tn -> Prop@ it yields a @Prop@.
    OExists [Type]
  | -- | Convert Prop -> Bool via exhaustive search.
    OHolds
  | -- | Flip success and failure for a prop.
    ONotProp
  | -- | Equality assertion, @=!=@
    OShouldEq Type
  | -- Other primitives

    -- | Error for non-exhaustive pattern match
    OMatchErr
  | -- | Crash with a user-supplied message
    OCrash
  | -- | No-op/identity function
    OId
  | -- | Lookup OEIS sequence
    OLookupSeq
  | -- | Extend a List via OEIS
    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
$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
$cOSize :: 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)

-- | Get the arity (desired number of arguments) of a function
--   constant.  A few constants have arity 0; everything else is
--   uncurried and hence has arity 1.
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
OSize        -> String
"size"
  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
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
"∃"