Agda.Syntax.Common

Some common syntactic entities are defined in this module.

Delayed

data Delayed

Used to specify whether something should be delayed.

Constructors

Delayed

NotDelayed

Instances

Eq Delayed

Ord Delayed

Show Delayed

Typeable Delayed

KillRange Delayed

EmbPrj Delayed

Induction

data Induction

Constructors

Inductive

CoInductive

Instances

Eq Induction

Ord Induction

Show Induction

Typeable Induction

Arbitrary Induction

CoArbitrary Induction

Pretty Induction

KillRange Induction

HasRange Induction

EmbPrj Induction

Hiding

data Hiding

Constructors

Hidden

Instance

NotHidden

Instances

Eq Hiding

Ord Hiding

Show Hiding

Typeable Hiding

KillRange Hiding

LensHiding Hiding

GenC Hiding

EmbPrj Hiding

Unquote Hiding

ShrinkC Hiding Hiding

class LensHiding a where

A lens to access the Hiding attribute in data structures. Minimal implementation: getHiding and one of setHiding or mapHiding.

Methods

getHiding :: a -> Hiding

setHiding :: Hiding -> a -> a

mapHiding :: (Hiding -> Hiding) -> a -> a

Instances

LensHiding Hiding

LensHiding (ArgInfo c)

LensHiding (FlexibleVar a)

LensHiding (Dom c e)

LensHiding (Arg c e)

isHidden :: LensHiding a => a -> Bool

isHidden does not apply to Instance, only to Hidden.

notHidden :: LensHiding a => a -> Bool

Visible (NotHidden) arguments are notHidden. (DEPRECATED, use visible.)

visible :: LensHiding a => a -> Bool

NotHidden arguments are visible.

notVisible :: LensHiding a => a -> Bool

Instance and Hidden arguments are notVisible.

hide :: LensHiding a => a -> a

makeInstance :: LensHiding a => a -> a

Relevance

data Relevance

A function argument can be relevant or irrelevant. See Irrelevance.

Constructors

Relevant

The argument is (possibly) relevant at compile-time.

NonStrict

The argument may never flow into evaluation position. Therefore, it is irrelevant at run-time. It is treated relevantly during equality checking.

Irrelevant

The argument is irrelevant at compile- and runtime.

Forced

The argument can be skipped during equality checking because its value is already determined by the type.

UnusedArg

The polarity checker has determined that this argument is unused in the definition. It can be skipped during equality checking but should be mined for solutions of meta-variables with relevance UnusedArg

Instances

Bounded Relevance

Enum Relevance

Eq Relevance

Ord Relevance

Show Relevance

Typeable Relevance

Arbitrary Relevance

Pretty Relevance

KillRange Relevance

LensRelevance Relevance

PrettyTCM Relevance

EmbPrj Relevance

Unquote Relevance

class LensRelevance a where

A lens to access the Relevance attribute in data structures. Minimal implementation: getRelevance and one of setRelevance or mapRelevance.

Methods

getRelevance :: a -> Relevance

setRelevance :: Relevance -> a -> a

mapRelevance :: (Relevance -> Relevance) -> a -> a

Instances

LensRelevance Relevance

LensRelevance (ArgInfo c)

LensRelevance (Dom c e)

LensRelevance (Arg c e)

isRelevant :: LensRelevance a => a -> Bool

isIrrelevant :: LensRelevance a => a -> Bool

moreRelevant :: Relevance -> Relevance -> Bool

Information ordering. Relevant `moreRelevant` UnusedArg `moreRelevant` Forced `moreRelevant` NonStrict `moreRelevant` Irrelevant

Argument decoration

data ArgInfo c

A function argument can be hidden and/or irrelevant.

Constructors

ArgInfo

Fields

argInfoHiding :: Hiding

argInfoRelevance :: Relevance

argInfoColors :: [c]

Instances

Functor ArgInfo

Typeable1 ArgInfo

Foldable ArgInfo

Traversable ArgInfo

Unquote ArgInfo

ToTerm ArgInfo

ToAbstract ArgInfo ArgInfo

Reify ArgInfo ArgInfo

ConvColor ArgInfo ArgInfo

Eq c => Eq (ArgInfo c)

Ord c => Ord (ArgInfo c)

Show c => Show (ArgInfo c)

KillRange c => KillRange (ArgInfo c)

LensRelevance (ArgInfo c)

LensHiding (ArgInfo c)

GetDefs c => GetDefs (ArgInfo c)

EmbPrj c => EmbPrj (ArgInfo c)

SynEq c => SynEq (ArgInfo c)

ToConcrete (ArgInfo ac) ArgInfo

mapArgInfoColors :: ([c] -> [c']) -> ArgInfo c -> ArgInfo c'

defaultArgInfo :: ArgInfo c

Arguments

data Arg c e

Constructors

Arg

Fields

argInfo :: ArgInfo c

unArg :: e

Instances

Typeable2 Arg

IsPrefixOf Args

UniverseBi Args Pattern

UniverseBi Args Term

Functor (Arg c)

Foldable (Arg c)

Traversable (Arg c)

Pretty e => Pretty (Arg e)

Pretty a => Pretty (Arg a)

Decoration (Arg c)

Free a => Free (Arg a)

TermLike a => TermLike (Arg a)

ExprLike a => ExprLike (Arg a)

Subst a => Subst (Arg a)

AbstractTerm a => AbstractTerm (Arg a)

KillVar a => KillVar (Arg a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

MentionsMeta t => MentionsMeta (Arg t)

InstantiateFull t => InstantiateFull (Arg t)

Normalise t => Normalise (Arg t)

Simplify t => Simplify (Arg t)

Reduce t => Reduce (Arg t)

Instantiate t => Instantiate (Arg t)

Match a => Match (Arg a)

Injectible a => Injectible (Arg a)

Evaluate a => Evaluate (Arg a)

Occurs a => Occurs (Arg a)

NoProjectedVar a => NoProjectedVar (Arg a)

HasPolarity a => HasPolarity (Arg a)

ComputeOccurrences a => ComputeOccurrences (Arg a)

Unquote a => Unquote (Arg a)

UReduce a => UReduce (Arg a)

ShrinkC a b => ShrinkC (Arg a) (Arg b)

ToAbstract c a => ToAbstract (Arg c) (Arg a)

ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a)

Reify i a => Reify (Dom i) (Arg a)

Reify i a => Reify (Arg i) (Arg a)

Skip reification of implicit and irrelevant args if option is off.

SubstHH a b => SubstHH (Arg a) (Arg b)

ConvColor (Arg e) (Arg e)

(Eq a, Eq c) => Eq (Arg c a)

(Ord c, Ord e) => Ord (Arg c e)

(Show a, Show c) => Show (Arg c a)

Sized a => Sized (Arg c a)

(KillRange c, KillRange a) => KillRange (Arg c a)

HasRange a => HasRange (Arg c a)

LensRelevance (Arg c e)

LensHiding (Arg c e)

IsProjP a => IsProjP (Arg c a)

ExprLike a => ExprLike (Arg c a)

TODO: currently does not go into colors.

(GetDefs c, GetDefs a) => GetDefs (Arg c a)

(GenC c, GenC a) => GenC (Arg c a)

IsInstantiatedMeta a => IsInstantiatedMeta (Arg c a)

(EmbPrj a, EmbPrj c) => EmbPrj (Arg c a)

ExpandPatternSynonyms a => ExpandPatternSynonyms (Arg c a)

(SynEq a, SynEq c) => SynEq (Arg c a)

ToConcrete a c => ToConcrete (Arg ac a) (Arg c)

mapArgInfo :: (ArgInfo c -> ArgInfo c') -> Arg c a -> Arg c' a

argColors :: Arg c e -> [c]

mapArgColors :: ([c] -> [c']) -> Arg c a -> Arg c' a

setArgColors :: [c] -> Arg c' a -> Arg c a

defaultArg :: a -> Arg c a

defaultColoredArg :: ([c], a) -> Arg c a

noColorArg :: Hiding -> Relevance -> a -> Arg c a

withArgsFrom :: [a] -> [Arg c b] -> [Arg c a]

xs `withArgsFrom` args translates xs into a list of Args, using the elements in args to fill in the non-unArg fields.

Precondition: The two lists should have equal length.

withNamedArgsFrom :: [a] -> [NamedArg c b] -> [NamedArg c a]

Names

class Eq a => Underscore a where

Methods

underscore :: a

isUnderscore :: a -> Bool

Instances

Underscore String

Underscore ByteString

Underscore Doc

Underscore QName

Underscore Name

Underscore Expr

Function type domain

data Dom c e

Similar to Arg, but we need to distinguish an irrelevance annotation in a function domain (the domain itself is not irrelevant!) from an irrelevant argument.

Dom is used in Pi of internal syntax, in Context and Telescope. Arg is used for actual arguments (Var, Con, Def etc.) and in Abstract syntax and other situations.

Constructors

Dom

Fields

domInfo :: ArgInfo c

unDom :: e

Instances

Typeable2 Dom

TeleNoAbs Telescope

TeleNoAbs ListTel

Abstract Telescope

KillVar Telescope

GenC Telescope

AddContext Telescope

PrettyTCM Telescope

EmbPrj Telescope

DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

Reduce Telescope

Instantiate Telescope

ShrinkC Telescope Telescope

Reify Telescope Telescope

Functor (Dom c)

Foldable (Dom c)

Traversable (Dom c)

Decoration (Dom c)

Free a => Free (Dom a)

TermLike a => TermLike (Dom a)

Subst a => Subst (Dom a)

AbstractTerm a => AbstractTerm (Dom a)

KillVar a => KillVar (Dom a)

AddContext (Dom (String, Type))

AddContext (Dom (Name, Type))

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

MentionsMeta t => MentionsMeta (Dom t)

InstantiateFull t => InstantiateFull (Dom t)

Normalise t => Normalise (Dom t)

Simplify t => Simplify (Dom t)

Reduce t => Reduce (Dom t)

Instantiate t => Instantiate (Dom t)

Occurs a => Occurs (Dom a)

HasPolarity a => HasPolarity (Dom a)

ComputeOccurrences a => ComputeOccurrences (Dom a)

ShrinkC a b => ShrinkC (Dom a) (Dom b)

Reify i a => Reify (Dom i) (Arg a)

SubstHH a b => SubstHH (Dom a) (Dom b)

ConvColor (Dom e) (Dom e)

(Eq c, Eq e) => Eq (Dom c e)

(Ord c, Ord e) => Ord (Dom c e)

(Show a, Show c) => Show (Dom c a)

Sized a => Sized (Dom c a)

(KillRange c, KillRange a) => KillRange (Dom c a)

HasRange a => HasRange (Dom c a)

LensRelevance (Dom c e)

LensHiding (Dom c e)

(GetDefs c, GetDefs a) => GetDefs (Dom c a)

(GenC c, GenC a) => GenC (Dom c a)

AddContext ([Name], Dom Type)

AddContext (String, Dom Type)

AddContext (Name, Dom Type)

(EmbPrj a, EmbPrj c) => EmbPrj (Dom c a)

(SynEq a, SynEq c) => SynEq (Dom c a)

mapDomInfo :: (ArgInfo c -> ArgInfo c') -> Dom c a -> Dom c' a

domColors :: Dom c e -> [c]

argFromDom :: Dom c a -> Arg c a

domFromArg :: Arg c a -> Dom c a

defaultDom :: a -> Dom c a

Named arguments

data Named name a

Something potentially carrying a name.

Constructors

Named

Fields

nameOf :: Maybe name

namedThing :: a

Instances

Typeable2 Named

Functor (Named name)

Show a => Show (Named_ a)

Foldable (Named name)

Traversable (Named name)

Pretty e => Pretty (Named_ e)

Decoration (Named name)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a)

(Eq name, Eq a) => Eq (Named name a)

(Ord name, Ord a) => Ord (Named name a)

Sized a => Sized (Named name a)

(KillRange name, KillRange a) => KillRange (Named name a)

HasRange a => HasRange (Named name a)

IsProjP a => IsProjP (Named n a)

ExprLike a => ExprLike (Named x a)

ExprLike a => ExprLike (Named name a)

Subst a => Subst (Named name a)

(EmbPrj s, EmbPrj t) => EmbPrj (Named s t)

ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a)

InstantiateFull t => InstantiateFull (Named name t)

Normalise t => Normalise (Named name t)

Simplify t => Simplify (Named name t)

ToConcrete a c => ToConcrete (Named name a) (Named name c)

ToAbstract c a => ToAbstract (Named name c) (Named name a)

Reify i a => Reify (Named n i) (Named n a)

type Named_ = Named RString

Standard naming.

unnamed :: a -> Named name a

named :: name -> a -> Named name a

type NamedArg c a = Arg c (Named_ a)

Only Hidden arguments can have names.

namedArg :: NamedArg c a -> a

Get the content of a NamedArg.

defaultNamedArg :: a -> NamedArg c a

updateNamedArg :: (a -> b) -> NamedArg c a -> NamedArg c b

The functor instance for NamedArg would be ambiguous, so we give it another name here.

Range decoration.

data Ranged a

Thing with range info.

Constructors

Ranged

Fields

rangeOf :: Range

rangedThing :: a

Instances

Functor Ranged

Typeable1 Ranged

Foldable Ranged

Traversable Ranged

Decoration Ranged

UniverseBi Declaration RString

Eq a => Eq (Ranged a)

Ord a => Ord (Ranged a)

Show a => Show (Ranged a)

Show a => Show (Named_ a)

Pretty e => Pretty (Named_ e)

KillRange (Ranged a)

HasRange (Ranged a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

EmbPrj a => EmbPrj (Ranged a)

ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a)

unranged :: a -> Ranged a

Thing with no range info.

Raw names (before parsing into name parts).

type RawName = String

A RawName is some sort of string.

rawNameToString :: RawName -> String

stringToRawName :: String -> RawName

type RString = Ranged RawName

String with range info.

Infixity, access, abstract, etc.

data IsInfix

Functions can be defined in both infix and prefix style. See LHS.

Constructors

InfixDef

PrefixDef

Instances

Eq IsInfix

Ord IsInfix

Show IsInfix

Typeable IsInfix

data Access

Access modifier.

Constructors

PrivateAccess

PublicAccess

OnlyQualified

Visible from outside, but not exported when opening the module Used for qualified constructors.

Instances

Eq Access

Ord Access

Show Access

Typeable Access

EmbPrj Access

data IsAbstract

Abstract or concrete

Constructors

AbstractDef

ConcreteDef

Instances

Eq IsAbstract

Ord IsAbstract

Show IsAbstract

Typeable IsAbstract

KillRange IsAbstract

EmbPrj IsAbstract

data IsInstance

Is this definition eligible for instance search?

Constructors

InstanceDef

NotInstanceDef

Instances

Eq IsInstance

Ord IsInstance

Show IsInstance

Typeable IsInstance

type Nat = Int

type Arity = Nat

data NameId

The unique identifier of a name. Second argument is the top-level module identifier.

Constructors

NameId Integer Integer

Instances

Enum NameId

Eq NameId

Ord NameId

Show NameId

Typeable NameId

Hashable NameId

EmbPrj NameId

HasFresh NameId FreshThings

newtype Constr a

Constructors

Constr a

Instances

ToConcrete (Constr Constructor) Declaration

Interaction meta variables

newtype InteractionId

Constructors

InteractionId

Fields

interactionId :: Nat

Instances

Enum InteractionId

Eq InteractionId

Integral InteractionId

Num InteractionId

Ord InteractionId

Read InteractionId

Real InteractionId

Show InteractionId

KillRange InteractionId

HasFresh InteractionId FreshThings

ToConcrete InteractionId Expr

Termination

data TerminationCheck m

Termination check? (Default = True).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

TerminationMeasure !Range m

Skip termination checking but use measure instead.

Instances

Typeable1 TerminationCheck

Eq m => Eq (TerminationCheck m)

Show m => Show (TerminationCheck m)

KillRange m => KillRange (TerminationCheck m)