{-# 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
  ShouldMemo (..),
  Core (..),
  Op (..),
  opArity,
  substQC,
  substsQC,
)
where

import Control.Lens.Plated
import Data.Data (Data)
import Data.Data.Lens (uniplate)
import Data.Ratio
import qualified Data.Set as S
import Disco.AST.Generic (Side, selectSide)
import Disco.Effects.LFresh
import Disco.Names (QName)
import Disco.Pretty
import Disco.Syntax.Operators (BOp (..))
import Disco.Types
import GHC.Generics
import Polysemy (Members, Sem)
import Polysemy.Reader
import Unbound.Generics.LocallyNameless hiding (LFresh, lunbind)
import Prelude hiding ((<>))
import qualified Prelude as P

data ShouldMemo = Memo | NoMemo deriving (Int -> ShouldMemo -> ShowS
[ShouldMemo] -> ShowS
ShouldMemo -> String
(Int -> ShouldMemo -> ShowS)
-> (ShouldMemo -> String)
-> ([ShouldMemo] -> ShowS)
-> Show ShouldMemo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ShouldMemo -> ShowS
showsPrec :: Int -> ShouldMemo -> ShowS
$cshow :: ShouldMemo -> String
show :: ShouldMemo -> String
$cshowList :: [ShouldMemo] -> ShowS
showList :: [ShouldMemo] -> ShowS
Show, (forall x. ShouldMemo -> Rep ShouldMemo x)
-> (forall x. Rep ShouldMemo x -> ShouldMemo) -> Generic ShouldMemo
forall x. Rep ShouldMemo x -> ShouldMemo
forall x. ShouldMemo -> Rep ShouldMemo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ShouldMemo -> Rep ShouldMemo x
from :: forall x. ShouldMemo -> Rep ShouldMemo x
$cto :: forall x. Rep ShouldMemo x -> ShouldMemo
to :: forall x. Rep ShouldMemo x -> ShouldMemo
Generic, Typeable ShouldMemo
Typeable ShouldMemo =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> ShouldMemo -> c ShouldMemo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ShouldMemo)
-> (ShouldMemo -> Constr)
-> (ShouldMemo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ShouldMemo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ShouldMemo))
-> ((forall b. Data b => b -> b) -> ShouldMemo -> ShouldMemo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r)
-> (forall u. (forall d. Data d => d -> u) -> ShouldMemo -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ShouldMemo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo)
-> Data ShouldMemo
ShouldMemo -> Constr
ShouldMemo -> DataType
(forall b. Data b => b -> b) -> ShouldMemo -> ShouldMemo
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) -> ShouldMemo -> u
forall u. (forall d. Data d => d -> u) -> ShouldMemo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ShouldMemo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ShouldMemo -> c ShouldMemo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ShouldMemo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ShouldMemo)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ShouldMemo -> c ShouldMemo
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ShouldMemo -> c ShouldMemo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ShouldMemo
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ShouldMemo
$ctoConstr :: ShouldMemo -> Constr
toConstr :: ShouldMemo -> Constr
$cdataTypeOf :: ShouldMemo -> DataType
dataTypeOf :: ShouldMemo -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ShouldMemo)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ShouldMemo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ShouldMemo)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ShouldMemo)
$cgmapT :: (forall b. Data b => b -> b) -> ShouldMemo -> ShouldMemo
gmapT :: (forall b. Data b => b -> b) -> ShouldMemo -> ShouldMemo
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ShouldMemo -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ShouldMemo -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ShouldMemo -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ShouldMemo -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ShouldMemo -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ShouldMemo -> m ShouldMemo
Data, Show ShouldMemo
Show ShouldMemo =>
(AlphaCtx -> ShouldMemo -> ShouldMemo -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> ShouldMemo -> f ShouldMemo)
-> (AlphaCtx -> NamePatFind -> ShouldMemo -> ShouldMemo)
-> (AlphaCtx -> NthPatFind -> ShouldMemo -> ShouldMemo)
-> (ShouldMemo -> DisjointSet AnyName)
-> (ShouldMemo -> All)
-> (ShouldMemo -> Bool)
-> (ShouldMemo -> NthPatFind)
-> (ShouldMemo -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> ShouldMemo -> ShouldMemo)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx
    -> ShouldMemo -> (ShouldMemo -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> ShouldMemo -> m (ShouldMemo, Perm AnyName))
-> (AlphaCtx -> ShouldMemo -> ShouldMemo -> Ordering)
-> Alpha ShouldMemo
AlphaCtx -> Perm AnyName -> ShouldMemo -> ShouldMemo
AlphaCtx -> NamePatFind -> ShouldMemo -> ShouldMemo
AlphaCtx -> NthPatFind -> ShouldMemo -> ShouldMemo
AlphaCtx -> ShouldMemo -> ShouldMemo -> Bool
AlphaCtx -> ShouldMemo -> ShouldMemo -> Ordering
ShouldMemo -> Bool
ShouldMemo -> All
ShouldMemo -> NamePatFind
ShouldMemo -> NthPatFind
ShouldMemo -> DisjointSet AnyName
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) -> ShouldMemo -> f ShouldMemo
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ShouldMemo -> m (ShouldMemo, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ShouldMemo -> (ShouldMemo -> Perm AnyName -> m b) -> m b
$caeq' :: AlphaCtx -> ShouldMemo -> ShouldMemo -> Bool
aeq' :: AlphaCtx -> ShouldMemo -> ShouldMemo -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> ShouldMemo -> f ShouldMemo
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> ShouldMemo -> f ShouldMemo
$cclose :: AlphaCtx -> NamePatFind -> ShouldMemo -> ShouldMemo
close :: AlphaCtx -> NamePatFind -> ShouldMemo -> ShouldMemo
$copen :: AlphaCtx -> NthPatFind -> ShouldMemo -> ShouldMemo
open :: AlphaCtx -> NthPatFind -> ShouldMemo -> ShouldMemo
$cisPat :: ShouldMemo -> DisjointSet AnyName
isPat :: ShouldMemo -> DisjointSet AnyName
$cisTerm :: ShouldMemo -> All
isTerm :: ShouldMemo -> All
$cisEmbed :: ShouldMemo -> Bool
isEmbed :: ShouldMemo -> Bool
$cnthPatFind :: ShouldMemo -> NthPatFind
nthPatFind :: ShouldMemo -> NthPatFind
$cnamePatFind :: ShouldMemo -> NamePatFind
namePatFind :: ShouldMemo -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> ShouldMemo -> ShouldMemo
swaps' :: AlphaCtx -> Perm AnyName -> ShouldMemo -> ShouldMemo
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ShouldMemo -> (ShouldMemo -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ShouldMemo -> (ShouldMemo -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ShouldMemo -> m (ShouldMemo, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ShouldMemo -> m (ShouldMemo, Perm AnyName)
$cacompare' :: AlphaCtx -> ShouldMemo -> ShouldMemo -> Ordering
acompare' :: AlphaCtx -> ShouldMemo -> ShouldMemo -> Ordering
Alpha)

-- | AST for the desugared, untyped core language.
data Core where
  -- | A variable.
  CVar :: QName Core -> Core
  -- | A rational number.
  CNum :: 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 :: ShouldMemo -> 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
$cshowsPrec :: Int -> Core -> ShowS
showsPrec :: Int -> Core -> ShowS
$cshow :: Core -> String
show :: Core -> String
$cshowList :: [Core] -> ShowS
showList :: [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
$cfrom :: forall x. Core -> Rep Core x
from :: forall x. Core -> Rep Core x
$cto :: forall x. Rep Core x -> Core
to :: forall x. Rep Core x -> Core
Generic, Typeable Core
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 -> Constr
Core -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Core -> c Core
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Core
$ctoConstr :: Core -> Constr
toConstr :: Core -> Constr
$cdataTypeOf :: Core -> DataType
dataTypeOf :: Core -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Core)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Core)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Core)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Core)
$cgmapT :: (forall b. Data b => b -> b) -> Core -> Core
gmapT :: (forall b. Data b => b -> b) -> Core -> Core
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Core -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Core -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Core -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Core -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Core -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m Core
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Core -> m 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 -> Perm AnyName -> Core -> Core
AlphaCtx -> NamePatFind -> Core -> Core
AlphaCtx -> NthPatFind -> Core -> Core
AlphaCtx -> Core -> Core -> Bool
AlphaCtx -> Core -> Core -> Ordering
Core -> Bool
Core -> All
Core -> NamePatFind
Core -> NthPatFind
Core -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> Core -> Core -> Bool
aeq' :: AlphaCtx -> Core -> Core -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Core -> f Core
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Core -> f Core
$cclose :: AlphaCtx -> NamePatFind -> Core -> Core
close :: AlphaCtx -> NamePatFind -> Core -> Core
$copen :: AlphaCtx -> NthPatFind -> Core -> Core
open :: AlphaCtx -> NthPatFind -> Core -> Core
$cisPat :: Core -> DisjointSet AnyName
isPat :: Core -> DisjointSet AnyName
$cisTerm :: Core -> All
isTerm :: Core -> All
$cisEmbed :: Core -> Bool
isEmbed :: Core -> Bool
$cnthPatFind :: Core -> NthPatFind
nthPatFind :: Core -> NthPatFind
$cnamePatFind :: Core -> NamePatFind
namePatFind :: Core -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Core -> Core
swaps' :: AlphaCtx -> Perm AnyName -> Core -> Core
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Core -> (Core -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Core -> (Core -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Core -> m (Core, Perm AnyName)
$cacompare' :: AlphaCtx -> Core -> Core -> Ordering
acompare' :: AlphaCtx -> Core -> Core -> Ordering
Alpha)

instance Plated Core where
  plate :: Traversal' Core Core
plate = (Core -> f Core) -> Core -> f Core
forall a. Data a => Traversal' a a
Traversal' Core Core
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
  | -- | Comparison assertion
    OShould BOp 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
  | OSeed
  | ORandom
  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
$cshowsPrec :: Int -> Op -> ShowS
showsPrec :: Int -> Op -> ShowS
$cshow :: Op -> String
show :: Op -> String
$cshowList :: [Op] -> ShowS
showList :: [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
$cfrom :: forall x. Op -> Rep Op x
from :: forall x. Op -> Rep Op x
$cto :: forall x. Rep Op x -> Op
to :: forall x. Rep Op x -> Op
Generic, Typeable Op
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 -> Constr
Op -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Op -> c Op
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Op
$ctoConstr :: Op -> Constr
toConstr :: Op -> Constr
$cdataTypeOf :: Op -> DataType
dataTypeOf :: Op -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Op)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)
$cgmapT :: (forall b. Data b => b -> b) -> Op -> Op
gmapT :: (forall b. Data b => b -> b) -> Op -> Op
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Op -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Op -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m Op
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Op -> m 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 -> Perm AnyName -> Op -> Op
AlphaCtx -> NamePatFind -> Op -> Op
AlphaCtx -> NthPatFind -> Op -> Op
AlphaCtx -> Op -> Op -> Bool
AlphaCtx -> Op -> Op -> Ordering
Op -> Bool
Op -> All
Op -> NamePatFind
Op -> NthPatFind
Op -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> Op -> Op -> Bool
aeq' :: AlphaCtx -> Op -> Op -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Op -> f Op
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Op -> f Op
$cclose :: AlphaCtx -> NamePatFind -> Op -> Op
close :: AlphaCtx -> NamePatFind -> Op -> Op
$copen :: AlphaCtx -> NthPatFind -> Op -> Op
open :: AlphaCtx -> NthPatFind -> Op -> Op
$cisPat :: Op -> DisjointSet AnyName
isPat :: Op -> DisjointSet AnyName
$cisTerm :: Op -> All
isTerm :: Op -> All
$cisEmbed :: Op -> Bool
isEmbed :: Op -> Bool
$cnthPatFind :: Op -> NthPatFind
nthPatFind :: Op -> NthPatFind
$cnamePatFind :: Op -> NamePatFind
namePatFind :: Op -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Op -> Op
swaps' :: AlphaCtx -> Perm AnyName -> Op -> Op
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Op -> (Op -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Op -> (Op -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Op -> m (Op, Perm AnyName)
$cacompare' :: AlphaCtx -> Op -> Op -> Ordering
acompare' :: AlphaCtx -> Op -> Op -> Ordering
Alpha, Op -> Op -> Bool
(Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
/= :: 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
$ccompare :: Op -> Op -> Ordering
compare :: Op -> Op -> Ordering
$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
>= :: Op -> Op -> Bool
$cmax :: Op -> Op -> Op
max :: Op -> Op -> Op
$cmin :: Op -> Op -> Op
min :: Op -> Op -> 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 :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
pretty = \case
    CVar QName Core
qn -> QName Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
QName Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty QName Core
qn
    CNum 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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
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 ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r)) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"/" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
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 ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c1 Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (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 -> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (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 -> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op)
    CConst Op
op -> Op -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Op -> Sem r (Doc ann)
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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Side -> Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Side -> a -> a -> a
selectSide Side
s Sem r (Doc ann)
"left" Sem r (Doc ann)
"right" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
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
      Bind (Name Core) Core
-> ((Name Core, Core) -> Sem r (Doc ann)) -> Sem r (Doc ann)
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 ann)) -> Sem r (Doc ann))
-> ((Name Core, Core) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \(Name Core
x, Core
lc) -> do
        Bind (Name Core) Core
-> ((Name Core, Core) -> Sem r (Doc ann)) -> Sem r (Doc ann)
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 ann)) -> Sem r (Doc ann))
-> ((Name Core, Core) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \(Name Core
y, Core
rc) -> do
          Int -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
nest Int
2 (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
            Sem r (Doc ann)
"case"
              Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c
              Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"of {"
              Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
                [ PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"left" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Name Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Core
x) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"->" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
lc
                , PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"right" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Name Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name Core
y) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann)
"->" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
rc
                ]
              Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a.
Member (Reader PA) r =>
PA -> Sem r a -> Sem r a
setPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c1 Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
", " Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Side -> Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Side -> a -> a -> a
selectSide Side
s Sem r (Doc ann)
"fst" Sem r (Doc ann)
"snd" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c)
    CAbs ShouldMemo
_ Bind [Name Core] Core
lam -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ do
      Bind [Name Core] Core
-> (([Name Core], Core) -> Sem r (Doc ann)) -> Sem r (Doc ann)
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 ann)) -> Sem r (Doc ann))
-> (([Name Core], Core) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \([Name Core]
xs, Core
body) -> Sem r (Doc ann)
"λ" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," ((Name Core -> Sem r (Doc ann)) -> [Name Core] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Name Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Name Core]
xs) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"." Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
lt (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Core
c1) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
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" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> [(String, Type, Name Core)] -> Sem r (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 Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (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 -> Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
initPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ do
      Bind [Name Core] [Core]
-> (([Name Core], [Core]) -> Sem r (Doc ann)) -> Sem r (Doc ann)
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 ann)) -> Sem r (Doc ann))
-> (([Name Core], [Core]) -> Sem r (Doc ann)) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ \([Name Core]
xs, [Core]
bodies) ->
        Sem r (Doc ann)
"delay" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," ((Name Core -> Sem r (Doc ann)) -> [Name Core] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Name Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Name Core -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Name Core]
xs) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"." Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (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 -> PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> Sem r (Doc ann) -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"force" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
Sem r (Doc ann) -> Sem r (Doc ann)
rt (Core -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Core -> Sem r (Doc ann)
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 = (Core -> Core -> Core) -> Core -> [Core] -> Core
forall a b. (a -> b -> b) -> b -> [a] -> b
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 = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
brackets (Sem r (Doc ann) -> Sem r (Doc ann))
-> ([(String, Type, Name Core)] -> Sem r (Doc ann))
-> [(String, Type, Name Core)]
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> ([(String, Type, Name Core)] -> [Sem r (Doc ann)])
-> [(String, Type, Name Core)]
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, Type, Name Core) -> Sem r (Doc ann))
-> [(String, Type, Name Core)] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (String, Type, Name Core) -> Sem r (Doc ann)
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) = Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann. Functor f => f (Doc ann) -> f (Doc ann)
parens (Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," [String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text String
s, t -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
t -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty t
ty, t -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
t -> Sem r (Doc ann)
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 OShould {} = 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, 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)
"∀" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," ((Type -> Sem r (Doc ann)) -> [Type] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Type]
tys) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
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)
"∃" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann) -> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Monad f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
intercalate Sem r (Doc ann)
"," ((Type -> Sem r (Doc ann)) -> [Type] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Type -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty [Type]
tys) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
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)
"~" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"~"
    | Op -> Bool
isPrefix Op
op = String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
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)
"~" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (Op -> String
opToStr Op
op)
    | Bool
otherwise = String -> Sem r (Doc ann)
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"
  OShould BOp
Eq Type
_ -> String
"=!="
  OShould BOp
Neq Type
_ -> String
"=!!="
  OShould BOp
Lt Type
_ -> String
"!<"
  OShould BOp
Gt Type
_ -> String
"!>"
  OShould BOp
Leq Type
_ -> String
"!<="
  OShould BOp
Geq Type
_ -> String
"!>="
  OShould BOp
Divides Type
_ -> String
"!|"
  OShould BOp
_ 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"
  Op
ORandom -> String
"random"
  Op
OSeed -> String
"seed"