{-# 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 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

-- | 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
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

-- | 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 = 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
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

-- | 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

    -- | 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
  | -- | unsafe set of counts -> bag, assumes all are distinct
    OUnsafeCountsToBag
  | -- | 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
    OShouldLt Type
  | -- | 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
  | -- | Not the Boolean `And`, but instead a propositional BOp
    -- | Should only be seen and used with Props.
    OAnd
  | -- | Not the Boolean `Or`, but instead a propositional BOp
    -- | Should only be seen and used with Props.
    OOr
  | -- | Not the Boolean `Impl`, but instead a propositional BOp
    -- | Should only be seen and used with Props.
    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)

-- | 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 = 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"