Disco.AST.Generic

Abstract syntax trees representing the generic syntax of the Disco language. Concrete AST instances may use this module as a template.

For more detail on the approach used here, see

Najd and Peyton Jones, "Trees that Grow". Journal of Universal Computer Science, vol. 23 no. 1 (2017), 42-62. https://arxiv.org/abs/1610.04799

Essentially, we define a basic generic Term_ type, with a type index to indicate what kind of term it is, i.e. what phase the term belongs to. Each constructor has a type family used to define any extra data that should go in the constructor for a particular phase; there is also one additional constructor which can be used to store arbitrary additional information, again governed by a type family. Together with the use of pattern synonyms, the result is that it looks like we have a different type for each phase, each with its own set of constructors, but in fact all use the same underlying type. Particular instantiations of the generic framework here can be found in Disco.AST.Surface, Disco.AST.Typed, and Disco.AST.Desugared.

Telescopes

data Telescope b where

A telescope is essentially a list, except that each item can bind names in the rest of the list.

Constructors

TelEmpty :: Telescope b

The empty telescope.

TelCons :: Rebind b (Telescope b) -> Telescope b

A binder of type b followed by zero or more b's. This b can bind variables in the subsequent b's.

Instances

Pretty Branch

Pretty-print a single branch in a case expression.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Branch -> Sem r Doc

HasType ABranch

Defined in Disco.AST.Typed

Methods

getType :: ABranch -> Type

setType :: Type -> ABranch -> ABranch

Subst t b => Subst t (Telescope b)

Defined in Disco.AST.Generic

Methods

isvar :: Telescope b -> Maybe (SubstName (Telescope b) t)

isCoerceVar :: Telescope b -> Maybe (SubstCoerce (Telescope b) t)

subst :: Name t -> t -> Telescope b -> Telescope b

substs :: [(Name t, t)] -> Telescope b -> Telescope b

Data b => Data (Telescope b)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Telescope b -> c (Telescope b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Telescope b)

toConstr :: Telescope b -> Constr

dataTypeOf :: Telescope b -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Telescope b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Telescope b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Telescope b -> Telescope b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Telescope b -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Telescope b -> r

gmapQ :: (forall d. Data d => d -> u) -> Telescope b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Telescope b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Telescope b -> m (Telescope b)

Show b => Show (Telescope b)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Telescope b -> ShowS

show :: Telescope b -> String

showList :: [Telescope b] -> ShowS

Generic (Telescope b)

Defined in Disco.AST.Generic

Associated Types

type Rep (Telescope b) :: Type -> Type

Methods

from :: Telescope b -> Rep (Telescope b) x

to :: Rep (Telescope b) x -> Telescope b

Alpha b => Alpha (Telescope b)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Telescope b -> Telescope b -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Telescope b -> f (Telescope b)

close :: AlphaCtx -> NamePatFind -> Telescope b -> Telescope b

open :: AlphaCtx -> NthPatFind -> Telescope b -> Telescope b

isPat :: Telescope b -> DisjointSet AnyName

isTerm :: Telescope b -> All

isEmbed :: Telescope b -> Bool

nthPatFind :: Telescope b -> NthPatFind

namePatFind :: Telescope b -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Telescope b -> Telescope b

lfreshen' :: LFresh m => AlphaCtx -> Telescope b -> (Telescope b -> Perm AnyName -> m b0) -> m b0

freshen' :: Fresh m => AlphaCtx -> Telescope b -> m (Telescope b, Perm AnyName)

acompare' :: AlphaCtx -> Telescope b -> Telescope b -> Ordering

Pretty (Telescope Guard)

Pretty-print the guards in a single branch of a case expression.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Telescope Guard -> Sem r Doc

Pretty (Telescope Qual)

Pretty-print the qualifiers in a comprehension.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Telescope Qual -> Sem r Doc

type Rep (Telescope b)

Defined in Disco.AST.Generic

type Rep (Telescope b) = D1 ('MetaData "Telescope" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "TelEmpty" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TelCons" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Rebind b (Telescope b)))))

telCons :: Alpha b => b -> Telescope b -> Telescope b

Add a new item to the beginning of a Telescope.

foldTelescope :: Alpha b => (b -> r -> r) -> r -> Telescope b -> r

Fold a telescope given a combining function and a value to use for the empty telescope. Analogous to foldr for lists.

mapTelescope :: (Alpha a, Alpha b) => (a -> b) -> Telescope a -> Telescope b

Apply a function to every item in a telescope.

traverseTelescope :: (Applicative f, Alpha a, Alpha b) => (a -> f b) -> Telescope a -> f (Telescope b)

Traverse over a telescope.

toTelescope :: Alpha b => [b] -> Telescope b

Convert a list to a telescope.

fromTelescope :: Alpha b => Telescope b -> [b]

Convert a telescope to a list.

Utility types

data Side

Injections into a sum type (inl or inr) have a "side" (L or R).

Constructors

L

R

Instances

Bounded Side

Defined in Disco.AST.Generic

Methods

minBound :: Side

maxBound :: Side

Enum Side

Defined in Disco.AST.Generic

Methods

succ :: Side -> Side

pred :: Side -> Side

toEnum :: Int -> Side

fromEnum :: Side -> Int

enumFrom :: Side -> [Side]

enumFromThen :: Side -> Side -> [Side]

enumFromTo :: Side -> Side -> [Side]

enumFromThenTo :: Side -> Side -> Side -> [Side]

Eq Side

Defined in Disco.AST.Generic

Methods

(==) :: Side -> Side -> Bool

(/=) :: Side -> Side -> Bool

Data Side

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Side -> c Side

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Side

toConstr :: Side -> Constr

dataTypeOf :: Side -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Side)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Side)

gmapT :: (forall b. Data b => b -> b) -> Side -> Side

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Side -> r

gmapQ :: (forall d. Data d => d -> u) -> Side -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Side -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Side -> m Side

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Side -> m Side

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Side -> m Side

Ord Side

Defined in Disco.AST.Generic

Methods

compare :: Side -> Side -> Ordering

(<) :: Side -> Side -> Bool

(<=) :: Side -> Side -> Bool

(>) :: Side -> Side -> Bool

(>=) :: Side -> Side -> Bool

max :: Side -> Side -> Side

min :: Side -> Side -> Side

Show Side

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Side -> ShowS

show :: Side -> String

showList :: [Side] -> ShowS

Generic Side

Defined in Disco.AST.Generic

Associated Types

type Rep Side :: Type -> Type

Methods

from :: Side -> Rep Side x

to :: Rep Side x -> Side

Alpha Side

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Side -> Side -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Side -> f Side

close :: AlphaCtx -> NamePatFind -> Side -> Side

open :: AlphaCtx -> NthPatFind -> Side -> Side

isPat :: Side -> DisjointSet AnyName

isTerm :: Side -> All

isEmbed :: Side -> Bool

nthPatFind :: Side -> NthPatFind

namePatFind :: Side -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Side -> Side

lfreshen' :: LFresh m => AlphaCtx -> Side -> (Side -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Side -> m (Side, Perm AnyName)

acompare' :: AlphaCtx -> Side -> Side -> Ordering

Pretty Side

Defined in Disco.AST.Generic

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Side -> Sem r Doc

Subst t Side

Defined in Disco.AST.Generic

Methods

isvar :: Side -> Maybe (SubstName Side t)

isCoerceVar :: Side -> Maybe (SubstCoerce Side t)

subst :: Name t -> t -> Side -> Side

substs :: [(Name t, t)] -> Side -> Side

type Rep Side

Defined in Disco.AST.Generic

type Rep Side = D1 ('MetaData "Side" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "L" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "R" 'PrefixI 'False) (U1 :: Type -> Type))

selectSide :: Side -> a -> a -> a

Use a Side to select one of two arguments (the first argument for L, and the second for R).

fromSide :: Side -> Bool

Convert a Side to a boolean.

data Container where

An enumeration of the different kinds of containers in disco: lists, bags, and sets.

Constructors

ListContainer :: Container

BagContainer :: Container

SetContainer :: Container

Instances

Enum Container

Defined in Disco.AST.Generic

Methods

succ :: Container -> Container

pred :: Container -> Container

toEnum :: Int -> Container

fromEnum :: Container -> Int

enumFrom :: Container -> [Container]

enumFromThen :: Container -> Container -> [Container]

enumFromTo :: Container -> Container -> [Container]

enumFromThenTo :: Container -> Container -> Container -> [Container]

Eq Container

Defined in Disco.AST.Generic

Methods

(==) :: Container -> Container -> Bool

(/=) :: Container -> Container -> Bool

Data Container

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Container -> c Container

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Container

toConstr :: Container -> Constr

dataTypeOf :: Container -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Container)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Container)

gmapT :: (forall b. Data b => b -> b) -> Container -> Container

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Container -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Container -> r

gmapQ :: (forall d. Data d => d -> u) -> Container -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Container -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Container -> m Container

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Container -> m Container

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Container -> m Container

Show Container

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Container -> ShowS

show :: Container -> String

showList :: [Container] -> ShowS

Generic Container

Defined in Disco.AST.Generic

Associated Types

type Rep Container :: Type -> Type

Methods

from :: Container -> Rep Container x

to :: Rep Container x -> Container

Alpha Container

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Container -> Container -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Container -> f Container

close :: AlphaCtx -> NamePatFind -> Container -> Container

open :: AlphaCtx -> NthPatFind -> Container -> Container

isPat :: Container -> DisjointSet AnyName

isTerm :: Container -> All

isEmbed :: Container -> Bool

nthPatFind :: Container -> NthPatFind

namePatFind :: Container -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Container -> Container

lfreshen' :: LFresh m => AlphaCtx -> Container -> (Container -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Container -> m (Container, Perm AnyName)

acompare' :: AlphaCtx -> Container -> Container -> Ordering

Subst t Container

Defined in Disco.AST.Generic

Methods

isvar :: Container -> Maybe (SubstName Container t)

isCoerceVar :: Container -> Maybe (SubstCoerce Container t)

subst :: Name t -> t -> Container -> Container

substs :: [(Name t, t)] -> Container -> Container

type Rep Container

Defined in Disco.AST.Generic

type Rep Container = D1 ('MetaData "Container" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "ListContainer" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BagContainer" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SetContainer" 'PrefixI 'False) (U1 :: Type -> Type)))

data Ellipsis t where

An ellipsis is an "omitted" part of a literal container (such as a list or set), of the form .. t. We don't have open-ended ellipses since everything is evaluated eagerly and hence containers must be finite.

Constructors

Until :: t -> Ellipsis t

Until represents an ellipsis with a given endpoint, as in [3 .. 20].

Instances

Functor Ellipsis

Defined in Disco.AST.Generic

Methods

fmap :: (a -> b) -> Ellipsis a -> Ellipsis b

(<$) :: a -> Ellipsis b -> Ellipsis a

Foldable Ellipsis

Defined in Disco.AST.Generic

Methods

fold :: Monoid m => Ellipsis m -> m

foldMap :: Monoid m => (a -> m) -> Ellipsis a -> m

foldMap' :: Monoid m => (a -> m) -> Ellipsis a -> m

foldr :: (a -> b -> b) -> b -> Ellipsis a -> b

foldr' :: (a -> b -> b) -> b -> Ellipsis a -> b

foldl :: (b -> a -> b) -> b -> Ellipsis a -> b

foldl' :: (b -> a -> b) -> b -> Ellipsis a -> b

foldr1 :: (a -> a -> a) -> Ellipsis a -> a

foldl1 :: (a -> a -> a) -> Ellipsis a -> a

toList :: Ellipsis a -> [a]

null :: Ellipsis a -> Bool

length :: Ellipsis a -> Int

elem :: Eq a => a -> Ellipsis a -> Bool

maximum :: Ord a => Ellipsis a -> a

minimum :: Ord a => Ellipsis a -> a

sum :: Num a => Ellipsis a -> a

product :: Num a => Ellipsis a -> a

Traversable Ellipsis

Defined in Disco.AST.Generic

Methods

traverse :: Applicative f => (a -> f b) -> Ellipsis a -> f (Ellipsis b)

sequenceA :: Applicative f => Ellipsis (f a) -> f (Ellipsis a)

mapM :: Monad m => (a -> m b) -> Ellipsis a -> m (Ellipsis b)

sequence :: Monad m => Ellipsis (m a) -> m (Ellipsis a)

Subst a t => Subst a (Ellipsis t)

Defined in Disco.AST.Generic

Methods

isvar :: Ellipsis t -> Maybe (SubstName (Ellipsis t) a)

isCoerceVar :: Ellipsis t -> Maybe (SubstCoerce (Ellipsis t) a)

subst :: Name a -> a -> Ellipsis t -> Ellipsis t

substs :: [(Name a, a)] -> Ellipsis t -> Ellipsis t

Data t => Data (Ellipsis t)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ellipsis t -> c (Ellipsis t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ellipsis t)

toConstr :: Ellipsis t -> Constr

dataTypeOf :: Ellipsis t -> DataType

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Ellipsis t))

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Ellipsis t))

gmapT :: (forall b. Data b => b -> b) -> Ellipsis t -> Ellipsis t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ellipsis t -> r

gmapQ :: (forall d. Data d => d -> u) -> Ellipsis t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ellipsis t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ellipsis t -> m (Ellipsis t)

Show t => Show (Ellipsis t)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Ellipsis t -> ShowS

show :: Ellipsis t -> String

showList :: [Ellipsis t] -> ShowS

Generic (Ellipsis t)

Defined in Disco.AST.Generic

Associated Types

type Rep (Ellipsis t) :: Type -> Type

Methods

from :: Ellipsis t -> Rep (Ellipsis t) x

to :: Rep (Ellipsis t) x -> Ellipsis t

Alpha t => Alpha (Ellipsis t)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Ellipsis t -> f (Ellipsis t)

close :: AlphaCtx -> NamePatFind -> Ellipsis t -> Ellipsis t

open :: AlphaCtx -> NthPatFind -> Ellipsis t -> Ellipsis t

isPat :: Ellipsis t -> DisjointSet AnyName

isTerm :: Ellipsis t -> All

isEmbed :: Ellipsis t -> Bool

nthPatFind :: Ellipsis t -> NthPatFind

namePatFind :: Ellipsis t -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Ellipsis t -> Ellipsis t

lfreshen' :: LFresh m => AlphaCtx -> Ellipsis t -> (Ellipsis t -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Ellipsis t -> m (Ellipsis t, Perm AnyName)

acompare' :: AlphaCtx -> Ellipsis t -> Ellipsis t -> Ordering

type Rep (Ellipsis t)

Defined in Disco.AST.Generic

type Rep (Ellipsis t) = D1 ('MetaData "Ellipsis" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "Until" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t)))

Term

data Term_ e where

The base generic AST representing terms in the disco language. e is a type index indicating the kind of term, i.e. the phase (for example, surface, typed, or desugared). Type families like X_TVar and so on use the phase index to determine what extra information (if any) should be stored in each constructor. For example, in the typed phase many constructors store an extra type, giving the type of the term.

Constructors

TVar_ :: X_TVar e -> Name (Term_ e) -> Term_ e

A term variable.

TPrim_ :: X_TPrim e -> Prim -> Term_ e

A primitive, i.e. a constant which is interpreted specially at runtime. See Disco.Syntax.Prims.

TLet_ :: X_TLet e -> Bind (Telescope (Binding_ e)) (Term_ e) -> Term_ e

A (non-recursive) let expression, let x1 = t1, x2 = t2, ... in t.

TParens_ :: X_TParens e -> Term_ e -> Term_ e

Explicit parentheses. We need to keep track of these in the surface syntax in order to syntactically distinguish multiplication and function application. However, note that these disappear after the surface syntax phase.

TUnit_ :: X_TUnit e -> Term_ e

The unit value, (), of type Unit.

TBool_ :: X_TBool e -> Bool -> Term_ e

A boolean value.

TNat_ :: X_TNat e -> Integer -> Term_ e

A natural number.

TRat_ :: X_TRat e -> Rational -> Term_ e

A nonnegative rational number, parsed as a decimal. (Note syntax like 3/5 does not parse as a rational, but rather as the application of a division operator to two natural numbers.)

TChar_ :: X_TChar e -> Char -> Term_ e

A literal unicode character, e.g. d.

TString_ :: X_TString e -> [Char] -> Term_ e

A string literal, e.g. "disco".

TAbs_ :: Quantifier -> X_TAbs e -> Binder_ e (Term_ e) -> Term_ e

A binding abstraction, of the form Q vars. expr where Q is a quantifier and vars is a list of bound variables and optional type annotations. In particular, this could be a lambda abstraction, i.e. an anonymous function (e.g. x, (y:N). 2x + y), a universal quantifier (forall x, (y:N). x^2 + y > 0), or an existential quantifier (exists x, (y:N). x^2 + y == 0).

TApp_ :: X_TApp e -> Term_ e -> Term_ e -> Term_ e

Function application, t1 t2.

TTup_ :: X_TTup e -> [Term_ e] -> Term_ e

An n-tuple, (t1, ..., tn).

TCase_ :: X_TCase e -> [Branch_ e] -> Term_ e

A case expression.

TChain_ :: X_TChain e -> Term_ e -> [Link_ e] -> Term_ e

A chained comparison, consisting of a term followed by one or more "links", where each link is a comparison operator and another term.

TTyOp_ :: X_TTyOp e -> TyOp -> Type -> Term_ e

An application of a type operator.

TContainer_ :: X_TContainer e -> Container -> [(Term_ e, Maybe (Term_ e))] -> Maybe (Ellipsis (Term_ e)) -> Term_ e

A containter literal (set, bag, or list).

TContainerComp_ :: X_TContainerComp e -> Container -> Bind (Telescope (Qual_ e)) (Term_ e) -> Term_ e

A container comprehension.

TAscr_ :: X_TAscr e -> Term_ e -> PolyType -> Term_ e

Type ascription, (Term_ e : type).

XTerm_ :: X_Term e -> Term_ e

A data constructor with an extension descriptor that a "concrete" implementation of a generic AST may use to carry extra information.

Instances

Pretty Branch

Pretty-print a single branch in a case expression.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Branch -> Sem r Doc

Pretty Term

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Term -> Sem r Doc

Pretty ATerm

Defined in Disco.AST.Typed

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => ATerm -> Sem r Doc

HasType ABranch

Defined in Disco.AST.Typed

Methods

getType :: ABranch -> Type

setType :: Type -> ABranch -> ABranch

HasType ATerm

Defined in Disco.AST.Typed

Methods

getType :: ATerm -> Type

setType :: Type -> ATerm -> ATerm

HasType DTerm

Defined in Disco.AST.Desugared

Methods

getType :: DTerm -> Type

setType :: Type -> DTerm -> DTerm

(Typeable e, ForallTerm (Subst Type) e, ForallTerm Alpha e) => Subst Type (Term_ e)

Defined in Disco.AST.Generic

Methods

isvar :: Term_ e -> Maybe (SubstName (Term_ e) Type)

isCoerceVar :: Term_ e -> Maybe (SubstCoerce (Term_ e) Type)

subst :: Name Type -> Type -> Term_ e -> Term_ e

substs :: [(Name Type, Type)] -> Term_ e -> Term_ e

(Data e, Typeable e, ForallTerm Data e) => Data (Term_ e)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term_ e -> c (Term_ e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Term_ e)

toConstr :: Term_ e -> Constr

dataTypeOf :: Term_ e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Term_ e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Term_ e))

gmapT :: (forall b. Data b => b -> b) -> Term_ e -> Term_ e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term_ e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term_ e -> r

gmapQ :: (forall d. Data d => d -> u) -> Term_ e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term_ e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term_ e -> m (Term_ e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term_ e -> m (Term_ e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term_ e -> m (Term_ e)

ForallTerm Show e => Show (Term_ e)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Term_ e -> ShowS

show :: Term_ e -> String

showList :: [Term_ e] -> ShowS

Generic (Term_ e)

Defined in Disco.AST.Generic

Associated Types

type Rep (Term_ e) :: Type -> Type

Methods

from :: Term_ e -> Rep (Term_ e) x

to :: Rep (Term_ e) x -> Term_ e

(Data e, ForallTerm Data e) => Plated (Term_ e)

Defined in Disco.AST.Generic

Methods

plate :: Traversal' (Term_ e) (Term_ e)

(Typeable e, ForallTerm Alpha e) => Alpha (Term_ e)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Term_ e -> Term_ e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Term_ e -> f (Term_ e)

close :: AlphaCtx -> NamePatFind -> Term_ e -> Term_ e

open :: AlphaCtx -> NthPatFind -> Term_ e -> Term_ e

isPat :: Term_ e -> DisjointSet AnyName

isTerm :: Term_ e -> All

isEmbed :: Term_ e -> Bool

nthPatFind :: Term_ e -> NthPatFind

namePatFind :: Term_ e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Term_ e -> Term_ e

lfreshen' :: LFresh m => AlphaCtx -> Term_ e -> (Term_ e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Term_ e -> m (Term_ e, Perm AnyName)

acompare' :: AlphaCtx -> Term_ e -> Term_ e -> Ordering

Pretty (Name a, Bind [Pattern] Term)

Pretty-print a single clause in a definition.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => (Name a, Bind [Pattern] Term) -> Sem r Doc

type Rep (Term_ e)

Defined in Disco.AST.Generic

type Rep (Term_ e) = D1 ('MetaData "Term_" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) ((((C1 ('MetaCons "TVar_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TVar e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name (Term_ e)))) :+: C1 ('MetaCons "TPrim_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TPrim e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prim))) :+: (C1 ('MetaCons "TLet_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TLet e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Bind (Telescope (Binding_ e)) (Term_ e)))) :+: (C1 ('MetaCons "TParens_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TParens e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e))) :+: C1 ('MetaCons "TUnit_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TUnit e)))))) :+: ((C1 ('MetaCons "TBool_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TBool e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "TNat_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TNat e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer))) :+: (C1 ('MetaCons "TRat_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TRat e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: (C1 ('MetaCons "TChar_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TChar e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Char)) :+: C1 ('MetaCons "TString_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TString e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Char])))))) :+: (((C1 ('MetaCons "TAbs_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantifier) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TAbs e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Binder_ e (Term_ e))))) :+: C1 ('MetaCons "TApp_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TApp e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e))))) :+: (C1 ('MetaCons "TTup_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TTup e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term_ e])) :+: (C1 ('MetaCons "TCase_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TCase e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Branch_ e])) :+: C1 ('MetaCons "TChain_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TChain e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Link_ e])))))) :+: ((C1 ('MetaCons "TTyOp_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TTyOp e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TyOp) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "TContainer_" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TContainer e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Container)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Term_ e, Maybe (Term_ e))]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Ellipsis (Term_ e))))))) :+: (C1 ('MetaCons "TContainerComp_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TContainerComp e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Container) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Bind (Telescope (Qual_ e)) (Term_ e))))) :+: (C1 ('MetaCons "TAscr_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TAscr e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PolyType))) :+: C1 ('MetaCons "XTerm_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_Term e))))))))

type family X_TVar e

Instances

type X_TVar UD

Defined in Disco.AST.Surface

type X_TVar UD = ()

type family X_TPrim e

Instances

type X_TPrim UD

Defined in Disco.AST.Surface

type X_TPrim UD = ()

type family X_TLet e

Instances

type X_TLet UD

Defined in Disco.AST.Surface

type X_TLet UD = ()

type family X_TParens e

Instances

type X_TParens UD

Defined in Disco.AST.Surface

type X_TParens UD = ()

type family X_TUnit e

Instances

type X_TUnit UD

Defined in Disco.AST.Surface

type X_TUnit UD = ()

type family X_TBool e

Instances

type X_TBool UD

Defined in Disco.AST.Surface

type X_TBool UD = ()

type family X_TNat e

Instances

type X_TNat UD

Defined in Disco.AST.Surface

type X_TNat UD = ()

type family X_TRat e

Instances

type X_TRat UD

Defined in Disco.AST.Surface

type X_TRat UD = ()

type family X_TChar e

Instances

type X_TChar UD

Defined in Disco.AST.Surface

type X_TChar UD = ()

type family X_TString e

Instances

type X_TString UD

Defined in Disco.AST.Surface

type X_TString UD = ()

type family X_TAbs e

Instances

type X_TAbs UD

Defined in Disco.AST.Surface

type X_TAbs UD = ()

type family X_TApp e

Instances

type X_TApp UD

Defined in Disco.AST.Surface

type X_TApp UD = ()

type family X_TTup e

Instances

type X_TTup UD

Defined in Disco.AST.Surface

type X_TTup UD = ()

type family X_TCase e

Instances

type X_TCase UD

Defined in Disco.AST.Surface

type X_TCase UD = ()

type family X_TChain e

Instances

type X_TChain UD

Defined in Disco.AST.Surface

type X_TChain UD = ()

type family X_TTyOp e

Instances

type X_TTyOp UD

Defined in Disco.AST.Surface

type X_TTyOp UD = ()

type family X_TContainer e

Instances

type X_TContainer UD

Defined in Disco.AST.Surface

type X_TContainer UD = ()

type family X_TContainerComp e

Instances

type X_TContainerComp UD

Defined in Disco.AST.Surface

type X_TContainerComp UD = ()

type family X_TAscr e

Instances

type X_TAscr UD

Defined in Disco.AST.Surface

type X_TAscr UD = ()

type family X_Term e

Instances

type X_Term UD

Defined in Disco.AST.Surface

type X_Term UD = ()

type ForallTerm (a :: * -> Constraint) e = (a (X_TVar e), a (X_TPrim e), a (X_TLet e), a (X_TParens e), a (X_TUnit e), a (X_TBool e), a (X_TNat e), a (X_TRat e), a (X_TChar e), a (X_TString e), a (X_TAbs e), a (X_TApp e), a (X_TCase e), a (X_TTup e), a (X_TChain e), a (X_TTyOp e), a (X_TContainer e), a (X_TContainerComp e), a (X_TAscr e), a (X_Term e), a (Qual_ e), a (Guard_ e), a (Link_ e), a (Binding_ e), a (Pattern_ e), a (Binder_ e (Term_ e)))

Link

data Link_ e where

A "link" is a comparison operator and a term; a single term followed by a sequence of links makes up a comparison chain, such as 2 < x < y < 10.

Constructors

TLink_ :: X_TLink e -> BOp -> Term_ e -> Link_ e

Note that although the type of TLink_ says it can hold any BOp, it should really only hold comparison operators.

Instances

ForallLink (Subst Type) e => Subst Type (Link_ e)

Defined in Disco.AST.Generic

Methods

isvar :: Link_ e -> Maybe (SubstName (Link_ e) Type)

isCoerceVar :: Link_ e -> Maybe (SubstCoerce (Link_ e) Type)

subst :: Name Type -> Type -> Link_ e -> Link_ e

substs :: [(Name Type, Type)] -> Link_ e -> Link_ e

(Typeable e, Data e, ForallLink Data e) => Data (Link_ e)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Link_ e -> c (Link_ e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Link_ e)

toConstr :: Link_ e -> Constr

dataTypeOf :: Link_ e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Link_ e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Link_ e))

gmapT :: (forall b. Data b => b -> b) -> Link_ e -> Link_ e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Link_ e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Link_ e -> r

gmapQ :: (forall d. Data d => d -> u) -> Link_ e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Link_ e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Link_ e -> m (Link_ e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Link_ e -> m (Link_ e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Link_ e -> m (Link_ e)

ForallLink Show e => Show (Link_ e)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Link_ e -> ShowS

show :: Link_ e -> String

showList :: [Link_ e] -> ShowS

Generic (Link_ e)

Defined in Disco.AST.Generic

Associated Types

type Rep (Link_ e) :: Type -> Type

Methods

from :: Link_ e -> Rep (Link_ e) x

to :: Rep (Link_ e) x -> Link_ e

(Typeable e, Show (Link_ e), ForallLink Alpha e) => Alpha (Link_ e)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Link_ e -> Link_ e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Link_ e -> f (Link_ e)

close :: AlphaCtx -> NamePatFind -> Link_ e -> Link_ e

open :: AlphaCtx -> NthPatFind -> Link_ e -> Link_ e

isPat :: Link_ e -> DisjointSet AnyName

isTerm :: Link_ e -> All

isEmbed :: Link_ e -> Bool

nthPatFind :: Link_ e -> NthPatFind

namePatFind :: Link_ e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Link_ e -> Link_ e

lfreshen' :: LFresh m => AlphaCtx -> Link_ e -> (Link_ e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Link_ e -> m (Link_ e, Perm AnyName)

acompare' :: AlphaCtx -> Link_ e -> Link_ e -> Ordering

type Rep (Link_ e)

Defined in Disco.AST.Generic

type Rep (Link_ e) = D1 ('MetaData "Link_" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "TLink_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_TLink e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BOp) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e)))))

type family X_TLink e

Instances

type X_TLink UD

Defined in Disco.AST.Surface

type X_TLink UD = ()

type ForallLink (a :: * -> Constraint) e = (a (X_TLink e), a (Term_ e))

Qual

data Qual_ e where

A container comprehension consists of a head term and then a list of qualifiers. Each qualifier either binds a variable to some collection or consists of a boolean guard.

Constructors

QBind_ :: X_QBind e -> Name (Term_ e) -> Embed (Term_ e) -> Qual_ e

A binding qualifier (i.e. x in t).

QGuard_ :: X_QGuard e -> Embed (Term_ e) -> Qual_ e

A boolean guard qualfier (i.e. x + y > 4).

Instances

Pretty Qual

Pretty-print a single qualifier in a comprehension.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Qual -> Sem r Doc

ForallQual (Subst Type) e => Subst Type (Qual_ e)

Defined in Disco.AST.Generic

Methods

isvar :: Qual_ e -> Maybe (SubstName (Qual_ e) Type)

isCoerceVar :: Qual_ e -> Maybe (SubstCoerce (Qual_ e) Type)

subst :: Name Type -> Type -> Qual_ e -> Qual_ e

substs :: [(Name Type, Type)] -> Qual_ e -> Qual_ e

(Typeable e, Data e, ForallQual Data e) => Data (Qual_ e)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Qual_ e -> c (Qual_ e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Qual_ e)

toConstr :: Qual_ e -> Constr

dataTypeOf :: Qual_ e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Qual_ e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Qual_ e))

gmapT :: (forall b. Data b => b -> b) -> Qual_ e -> Qual_ e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Qual_ e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Qual_ e -> r

gmapQ :: (forall d. Data d => d -> u) -> Qual_ e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Qual_ e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Qual_ e -> m (Qual_ e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Qual_ e -> m (Qual_ e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Qual_ e -> m (Qual_ e)

ForallQual Show e => Show (Qual_ e)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Qual_ e -> ShowS

show :: Qual_ e -> String

showList :: [Qual_ e] -> ShowS

Generic (Qual_ e)

Defined in Disco.AST.Generic

Associated Types

type Rep (Qual_ e) :: Type -> Type

Methods

from :: Qual_ e -> Rep (Qual_ e) x

to :: Rep (Qual_ e) x -> Qual_ e

(Typeable e, ForallQual Alpha e) => Alpha (Qual_ e)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Qual_ e -> Qual_ e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Qual_ e -> f (Qual_ e)

close :: AlphaCtx -> NamePatFind -> Qual_ e -> Qual_ e

open :: AlphaCtx -> NthPatFind -> Qual_ e -> Qual_ e

isPat :: Qual_ e -> DisjointSet AnyName

isTerm :: Qual_ e -> All

isEmbed :: Qual_ e -> Bool

nthPatFind :: Qual_ e -> NthPatFind

namePatFind :: Qual_ e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Qual_ e -> Qual_ e

lfreshen' :: LFresh m => AlphaCtx -> Qual_ e -> (Qual_ e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Qual_ e -> m (Qual_ e, Perm AnyName)

acompare' :: AlphaCtx -> Qual_ e -> Qual_ e -> Ordering

Pretty (Telescope Qual)

Pretty-print the qualifiers in a comprehension.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Telescope Qual -> Sem r Doc

type Rep (Qual_ e)

Defined in Disco.AST.Generic

type Rep (Qual_ e) = D1 ('MetaData "Qual_" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "QBind_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_QBind e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name (Term_ e))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Embed (Term_ e))))) :+: C1 ('MetaCons "QGuard_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_QGuard e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Embed (Term_ e)))))

type family X_QBind e

Instances

type X_QBind UD

Defined in Disco.AST.Surface

type X_QBind UD = ()

type family X_QGuard e

Instances

type X_QGuard UD

Defined in Disco.AST.Surface

type X_QGuard UD = ()

type ForallQual (a :: * -> Constraint) e = (a (X_QBind e), a (X_QGuard e), a (Term_ e))

Binding

data Binding_ e

A binding is a name along with its definition, and optionally its type.

Constructors

Binding_ (Maybe (Embed PolyType)) (Name (Term_ e)) (Embed (Term_ e))

Instances

Pretty Binding

Pretty-print a binding, i.e. a pairing of a name (with optional type annotation) and term.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Binding -> Sem r Doc

Subst Type (Term_ e) => Subst Type (Binding_ e)

Defined in Disco.AST.Generic

Methods

isvar :: Binding_ e -> Maybe (SubstName (Binding_ e) Type)

isCoerceVar :: Binding_ e -> Maybe (SubstCoerce (Binding_ e) Type)

subst :: Name Type -> Type -> Binding_ e -> Binding_ e

substs :: [(Name Type, Type)] -> Binding_ e -> Binding_ e

(Typeable e, Data e, ForallTerm Data e) => Data (Binding_ e)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binding_ e -> c (Binding_ e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Binding_ e)

toConstr :: Binding_ e -> Constr

dataTypeOf :: Binding_ e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Binding_ e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Binding_ e))

gmapT :: (forall b. Data b => b -> b) -> Binding_ e -> Binding_ e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binding_ e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binding_ e -> r

gmapQ :: (forall d. Data d => d -> u) -> Binding_ e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binding_ e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binding_ e -> m (Binding_ e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binding_ e -> m (Binding_ e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binding_ e -> m (Binding_ e)

ForallTerm Show e => Show (Binding_ e)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Binding_ e -> ShowS

show :: Binding_ e -> String

showList :: [Binding_ e] -> ShowS

Generic (Binding_ e)

Defined in Disco.AST.Generic

Associated Types

type Rep (Binding_ e) :: Type -> Type

Methods

from :: Binding_ e -> Rep (Binding_ e) x

to :: Rep (Binding_ e) x -> Binding_ e

(Typeable e, Show (Binding_ e), Alpha (Term_ e)) => Alpha (Binding_ e)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Binding_ e -> Binding_ e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Binding_ e -> f (Binding_ e)

close :: AlphaCtx -> NamePatFind -> Binding_ e -> Binding_ e

open :: AlphaCtx -> NthPatFind -> Binding_ e -> Binding_ e

isPat :: Binding_ e -> DisjointSet AnyName

isTerm :: Binding_ e -> All

isEmbed :: Binding_ e -> Bool

nthPatFind :: Binding_ e -> NthPatFind

namePatFind :: Binding_ e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Binding_ e -> Binding_ e

lfreshen' :: LFresh m => AlphaCtx -> Binding_ e -> (Binding_ e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Binding_ e -> m (Binding_ e, Perm AnyName)

acompare' :: AlphaCtx -> Binding_ e -> Binding_ e -> Ordering

type Rep (Binding_ e)

Defined in Disco.AST.Generic

type Rep (Binding_ e) = D1 ('MetaData "Binding_" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "Binding_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Embed PolyType))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name (Term_ e))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Embed (Term_ e))))))

Branch

type Branch_ e = Bind (Telescope (Guard_ e)) (Term_ e)

A branch of a case is a list of guards with an accompanying term. The guards scope over the term. Additionally, each guard scopes over subsequent guards.

Guard

data Guard_ e where

Guards in case expressions.

Constructors

GBool_ :: X_GBool e -> Embed (Term_ e) -> Guard_ e

Boolean guard (if test)

GPat_ :: X_GPat e -> Embed (Term_ e) -> Pattern_ e -> Guard_ e

Pattern guard (when term = pat)

GLet_ :: X_GLet e -> Binding_ e -> Guard_ e

Let (let x = term)

Instances

Pretty Guard

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Guard -> Sem r Doc

Pretty Branch

Pretty-print a single branch in a case expression.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Branch -> Sem r Doc

HasType ABranch

Defined in Disco.AST.Typed

Methods

getType :: ABranch -> Type

setType :: Type -> ABranch -> ABranch

ForallGuard (Subst Type) e => Subst Type (Guard_ e)

Defined in Disco.AST.Generic

Methods

isvar :: Guard_ e -> Maybe (SubstName (Guard_ e) Type)

isCoerceVar :: Guard_ e -> Maybe (SubstCoerce (Guard_ e) Type)

subst :: Name Type -> Type -> Guard_ e -> Guard_ e

substs :: [(Name Type, Type)] -> Guard_ e -> Guard_ e

(Typeable e, Data e, ForallGuard Data e) => Data (Guard_ e)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Guard_ e -> c (Guard_ e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Guard_ e)

toConstr :: Guard_ e -> Constr

dataTypeOf :: Guard_ e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Guard_ e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Guard_ e))

gmapT :: (forall b. Data b => b -> b) -> Guard_ e -> Guard_ e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Guard_ e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Guard_ e -> r

gmapQ :: (forall d. Data d => d -> u) -> Guard_ e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Guard_ e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Guard_ e -> m (Guard_ e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Guard_ e -> m (Guard_ e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Guard_ e -> m (Guard_ e)

ForallGuard Show e => Show (Guard_ e)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Guard_ e -> ShowS

show :: Guard_ e -> String

showList :: [Guard_ e] -> ShowS

Generic (Guard_ e)

Defined in Disco.AST.Generic

Associated Types

type Rep (Guard_ e) :: Type -> Type

Methods

from :: Guard_ e -> Rep (Guard_ e) x

to :: Rep (Guard_ e) x -> Guard_ e

(Typeable e, Show (Guard_ e), ForallGuard Alpha e) => Alpha (Guard_ e)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Guard_ e -> Guard_ e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Guard_ e -> f (Guard_ e)

close :: AlphaCtx -> NamePatFind -> Guard_ e -> Guard_ e

open :: AlphaCtx -> NthPatFind -> Guard_ e -> Guard_ e

isPat :: Guard_ e -> DisjointSet AnyName

isTerm :: Guard_ e -> All

isEmbed :: Guard_ e -> Bool

nthPatFind :: Guard_ e -> NthPatFind

namePatFind :: Guard_ e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Guard_ e -> Guard_ e

lfreshen' :: LFresh m => AlphaCtx -> Guard_ e -> (Guard_ e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Guard_ e -> m (Guard_ e, Perm AnyName)

acompare' :: AlphaCtx -> Guard_ e -> Guard_ e -> Ordering

Pretty (Telescope Guard)

Pretty-print the guards in a single branch of a case expression.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Telescope Guard -> Sem r Doc

type Rep (Guard_ e)

Defined in Disco.AST.Generic

type Rep (Guard_ e) = D1 ('MetaData "Guard_" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "GBool_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_GBool e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Embed (Term_ e)))) :+: (C1 ('MetaCons "GPat_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_GPat e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Embed (Term_ e))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)))) :+: C1 ('MetaCons "GLet_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_GLet e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Binding_ e)))))

type family X_GBool e

Instances

type X_GBool UD

Defined in Disco.AST.Surface

type X_GBool UD = ()

type family X_GPat e

Instances

type X_GPat UD

Defined in Disco.AST.Surface

type X_GPat UD = ()

type family X_GLet e

Instances

type X_GLet UD

Defined in Disco.AST.Surface

type X_GLet UD = ()

type ForallGuard (a :: * -> Constraint) e = (a (X_GBool e), a (X_GPat e), a (X_GLet e), a (Term_ e), a (Pattern_ e), a (Binding_ e))

Pattern

data Pattern_ e where

Patterns.

Constructors

PVar_ :: X_PVar e -> Name (Term_ e) -> Pattern_ e

Variable pattern: matches anything and binds the variable.

PWild_ :: X_PWild e -> Pattern_ e

Wildcard pattern _: matches anything.

PAscr_ :: X_PAscr e -> Pattern_ e -> Type -> Pattern_ e

Type ascription pattern pat : ty.

PUnit_ :: X_PUnit e -> Pattern_ e

Unit pattern (): matches ().

PBool_ :: X_PBool e -> Bool -> Pattern_ e

Literal boolean pattern.

PTup_ :: X_PTup e -> [Pattern_ e] -> Pattern_ e

Tuple pattern (pat1, .. , patn).

PInj_ :: X_PInj e -> Side -> Pattern_ e -> Pattern_ e

Injection pattern (inl pat or inr pat).

PNat_ :: X_PNat e -> Integer -> Pattern_ e

Literal natural number pattern.

PChar_ :: X_PChar e -> Char -> Pattern_ e

Unicode character pattern

PString_ :: X_PString e -> String -> Pattern_ e

String pattern.

PCons_ :: X_PCons e -> Pattern_ e -> Pattern_ e -> Pattern_ e

Cons pattern p1 :: p2.

PList_ :: X_PList e -> [Pattern_ e] -> Pattern_ e

List pattern [p1, .., pn].

PAdd_ :: X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e

Addition pattern, p + t or t + p

PMul_ :: X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e

Multiplication pattern, p * t or t * p

PSub_ :: X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e

Subtraction pattern, p - t

PNeg_ :: X_PNeg e -> Pattern_ e -> Pattern_ e

Negation pattern, -p

PFrac_ :: X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e

Fraction pattern, p1/p2

XPattern_ :: X_Pattern e -> Pattern_ e

Expansion slot.

Instances

Pretty Pattern

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => Pattern -> Sem r Doc

HasType APattern

Defined in Disco.AST.Typed

Methods

getType :: APattern -> Type

setType :: Type -> APattern -> APattern

HasType DPattern

Defined in Disco.AST.Desugared

Methods

getType :: DPattern -> Type

setType :: Type -> DPattern -> DPattern

ForallPattern (Subst Type) e => Subst Type (Pattern_ e)

Defined in Disco.AST.Generic

Methods

isvar :: Pattern_ e -> Maybe (SubstName (Pattern_ e) Type)

isCoerceVar :: Pattern_ e -> Maybe (SubstCoerce (Pattern_ e) Type)

subst :: Name Type -> Type -> Pattern_ e -> Pattern_ e

substs :: [(Name Type, Type)] -> Pattern_ e -> Pattern_ e

(Typeable e, Data e, ForallPattern Data e) => Data (Pattern_ e)

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern_ e -> c (Pattern_ e)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern_ e)

toConstr :: Pattern_ e -> Constr

dataTypeOf :: Pattern_ e -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern_ e))

dataCast2 :: Typeable t => (forall d e0. (Data d, Data e0) => c (t d e0)) -> Maybe (c (Pattern_ e))

gmapT :: (forall b. Data b => b -> b) -> Pattern_ e -> Pattern_ e

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern_ e -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern_ e -> r

gmapQ :: (forall d. Data d => d -> u) -> Pattern_ e -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern_ e -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern_ e -> m (Pattern_ e)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern_ e -> m (Pattern_ e)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern_ e -> m (Pattern_ e)

ForallPattern Show e => Show (Pattern_ e)

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Pattern_ e -> ShowS

show :: Pattern_ e -> String

showList :: [Pattern_ e] -> ShowS

Generic (Pattern_ e)

Defined in Disco.AST.Generic

Associated Types

type Rep (Pattern_ e) :: Type -> Type

Methods

from :: Pattern_ e -> Rep (Pattern_ e) x

to :: Rep (Pattern_ e) x -> Pattern_ e

(Typeable e, Show (Pattern_ e), ForallPattern Alpha e) => Alpha (Pattern_ e)

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Pattern_ e -> Pattern_ e -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Pattern_ e -> f (Pattern_ e)

close :: AlphaCtx -> NamePatFind -> Pattern_ e -> Pattern_ e

open :: AlphaCtx -> NthPatFind -> Pattern_ e -> Pattern_ e

isPat :: Pattern_ e -> DisjointSet AnyName

isTerm :: Pattern_ e -> All

isEmbed :: Pattern_ e -> Bool

nthPatFind :: Pattern_ e -> NthPatFind

namePatFind :: Pattern_ e -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Pattern_ e -> Pattern_ e

lfreshen' :: LFresh m => AlphaCtx -> Pattern_ e -> (Pattern_ e -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Pattern_ e -> m (Pattern_ e, Perm AnyName)

acompare' :: AlphaCtx -> Pattern_ e -> Pattern_ e -> Ordering

Pretty (Name a, Bind [Pattern] Term)

Pretty-print a single clause in a definition.

Defined in Disco.AST.Surface

Methods

pretty :: forall (r :: EffectRow). Members '[Reader PA, LFresh] r => (Name a, Bind [Pattern] Term) -> Sem r Doc

type Rep (Pattern_ e)

Defined in Disco.AST.Generic

type Rep (Pattern_ e) = D1 ('MetaData "Pattern_" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) ((((C1 ('MetaCons "PVar_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PVar e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name (Term_ e)))) :+: C1 ('MetaCons "PWild_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PWild e)))) :+: (C1 ('MetaCons "PAscr_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PAscr e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))) :+: C1 ('MetaCons "PUnit_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PUnit e))))) :+: ((C1 ('MetaCons "PBool_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PBool e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "PTup_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PTup e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern_ e]))) :+: (C1 ('MetaCons "PInj_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PInj e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Side) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)))) :+: (C1 ('MetaCons "PNat_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PNat e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "PChar_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PChar e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Char)))))) :+: (((C1 ('MetaCons "PString_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PString e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "PCons_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PCons e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e))))) :+: (C1 ('MetaCons "PList_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PList e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pattern_ e])) :+: C1 ('MetaCons "PAdd_" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PAdd e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Side)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e)))))) :+: ((C1 ('MetaCons "PMul_" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PMul e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Side)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e)))) :+: C1 ('MetaCons "PSub_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PSub e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term_ e))))) :+: (C1 ('MetaCons "PNeg_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PNeg e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e))) :+: (C1 ('MetaCons "PFrac_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_PFrac e)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern_ e)))) :+: C1 ('MetaCons "XPattern_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (X_Pattern e))))))))

type family X_PVar e

Instances

type X_PVar UD

Defined in Disco.AST.Surface

type X_PVar UD = ()

type family X_PWild e

Instances

type X_PWild UD

Defined in Disco.AST.Surface

type X_PWild UD = ()

type family X_PAscr e

Instances

type X_PAscr UD

Defined in Disco.AST.Surface

type X_PAscr UD = ()

type family X_PUnit e

Instances

type X_PUnit UD

Defined in Disco.AST.Surface

type X_PUnit UD = ()

type family X_PBool e

Instances

type X_PBool UD

Defined in Disco.AST.Surface

type X_PBool UD = ()

type family X_PTup e

Instances

type X_PTup UD

Defined in Disco.AST.Surface

type X_PTup UD = ()

type family X_PInj e

Instances

type X_PInj UD

Defined in Disco.AST.Surface

type X_PInj UD = ()

type family X_PNat e

Instances

type X_PNat UD

Defined in Disco.AST.Surface

type X_PNat UD = ()

type family X_PChar e

Instances

type X_PChar UD

Defined in Disco.AST.Surface

type X_PChar UD = ()

type family X_PString e

Instances

type X_PString UD

Defined in Disco.AST.Surface

type X_PString UD = ()

type family X_PCons e

Instances

type X_PCons UD

Defined in Disco.AST.Surface

type X_PCons UD = ()

type family X_PList e

Instances

type X_PList UD

Defined in Disco.AST.Surface

type X_PList UD = ()

type family X_PAdd e

Instances

type X_PAdd UD

Defined in Disco.AST.Surface

type X_PAdd UD = ()

type family X_PMul e

Instances

type X_PMul UD

Defined in Disco.AST.Surface

type X_PMul UD = ()

type family X_PSub e

Instances

type X_PSub UD

Defined in Disco.AST.Surface

type X_PSub UD = ()

type family X_PNeg e

Instances

type X_PNeg UD

Defined in Disco.AST.Surface

type X_PNeg UD = ()

type family X_PFrac e

Instances

type X_PFrac UD

Defined in Disco.AST.Surface

type X_PFrac UD = ()

type family X_Pattern e

Instances

type X_Pattern UD

Defined in Disco.AST.Surface

type X_Pattern UD = Void

type ForallPattern (a :: * -> Constraint) e = (a (X_PVar e), a (X_PWild e), a (X_PAscr e), a (X_PUnit e), a (X_PBool e), a (X_PNat e), a (X_PChar e), a (X_PString e), a (X_PTup e), a (X_PInj e), a (X_PCons e), a (X_PList e), a (X_PAdd e), a (X_PMul e), a (X_PSub e), a (X_PNeg e), a (X_PFrac e), a (X_Pattern e), a (Term_ e))

Quantifiers

data Quantifier

A quantifier: λ, ∀, or ∃

Constructors

Lam

Ex

All

Instances

Eq Quantifier

Defined in Disco.AST.Generic

Methods

(==) :: Quantifier -> Quantifier -> Bool

(/=) :: Quantifier -> Quantifier -> Bool

Data Quantifier

Defined in Disco.AST.Generic

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantifier -> c Quantifier

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantifier

toConstr :: Quantifier -> Constr

dataTypeOf :: Quantifier -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantifier)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantifier)

gmapT :: (forall b. Data b => b -> b) -> Quantifier -> Quantifier

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantifier -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantifier -> r

gmapQ :: (forall d. Data d => d -> u) -> Quantifier -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantifier -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier

Ord Quantifier

Defined in Disco.AST.Generic

Methods

compare :: Quantifier -> Quantifier -> Ordering

(<) :: Quantifier -> Quantifier -> Bool

(<=) :: Quantifier -> Quantifier -> Bool

(>) :: Quantifier -> Quantifier -> Bool

(>=) :: Quantifier -> Quantifier -> Bool

max :: Quantifier -> Quantifier -> Quantifier

min :: Quantifier -> Quantifier -> Quantifier

Show Quantifier

Defined in Disco.AST.Generic

Methods

showsPrec :: Int -> Quantifier -> ShowS

show :: Quantifier -> String

showList :: [Quantifier] -> ShowS

Generic Quantifier

Defined in Disco.AST.Generic

Associated Types

type Rep Quantifier :: Type -> Type

Methods

from :: Quantifier -> Rep Quantifier x

to :: Rep Quantifier x -> Quantifier

Alpha Quantifier

Defined in Disco.AST.Generic

Methods

aeq' :: AlphaCtx -> Quantifier -> Quantifier -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Quantifier -> f Quantifier

close :: AlphaCtx -> NamePatFind -> Quantifier -> Quantifier

open :: AlphaCtx -> NthPatFind -> Quantifier -> Quantifier

isPat :: Quantifier -> DisjointSet AnyName

isTerm :: Quantifier -> All

isEmbed :: Quantifier -> Bool

nthPatFind :: Quantifier -> NthPatFind

namePatFind :: Quantifier -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Quantifier -> Quantifier

lfreshen' :: LFresh m => AlphaCtx -> Quantifier -> (Quantifier -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Quantifier -> m (Quantifier, Perm AnyName)

acompare' :: AlphaCtx -> Quantifier -> Quantifier -> Ordering

Subst Type Quantifier

Defined in Disco.AST.Generic

Methods

isvar :: Quantifier -> Maybe (SubstName Quantifier Type)

isCoerceVar :: Quantifier -> Maybe (SubstCoerce Quantifier Type)

subst :: Name Type -> Type -> Quantifier -> Quantifier

substs :: [(Name Type, Type)] -> Quantifier -> Quantifier

type Rep Quantifier

Defined in Disco.AST.Generic

type Rep Quantifier = D1 ('MetaData "Quantifier" "Disco.AST.Generic" "disco-0.1.5-Dj6M4uP9IofLLslCWcCyVQ" 'False) (C1 ('MetaCons "Lam" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Ex" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "All" 'PrefixI 'False) (U1 :: Type -> Type)))

type Binder_ e a = Bind (X_Binder e) a

A binder represents the stuff between the quantifier and the body of a lambda, ∀, or ∃ abstraction, as in x : N, r : F.

type family X_Binder e

A type family specifying what the binder in an abstraction can be. Should have at least variables in it, but how many variables and what other information is carried along may vary.

Instances

type X_Binder UD

Defined in Disco.AST.Surface

type X_Binder UD = [Pattern]

Property

type Property_ e = Term_ e

A property is just a term (of type Prop).

Orphan instances

Alpha Void

Methods

aeq' :: AlphaCtx -> Void -> Void -> Bool

fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> Void -> f Void

close :: AlphaCtx -> NamePatFind -> Void -> Void

open :: AlphaCtx -> NthPatFind -> Void -> Void

isPat :: Void -> DisjointSet AnyName

isTerm :: Void -> All

isEmbed :: Void -> Bool

nthPatFind :: Void -> NthPatFind

namePatFind :: Void -> NamePatFind

swaps' :: AlphaCtx -> Perm AnyName -> Void -> Void

lfreshen' :: LFresh m => AlphaCtx -> Void -> (Void -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Void -> m (Void, Perm AnyName)

acompare' :: AlphaCtx -> Void -> Void -> Ordering