Agda-2.4.2.3: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Common

Contents

Description

Some common syntactic entities are defined in this module.

Synopsis

Delayed

data Delayed

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 

Induction

Hiding

data Hiding

Constructors

Hidden 
Instance 
NotHidden 

Instances

class LensHiding a where

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

Minimal complete definition

getHiding

Methods

getHiding :: a -> Hiding

setHiding :: Hiding -> a -> a

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

mergeHiding :: LensHiding a => WithHiding a -> a

Monoidal composition of Hiding information in some data.

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 Big

An constructor argument is big if the sort of its type is bigger than the sort of the data type. Only parameters (and maybe forced arguments) are allowed to be big. List : Set -> Set nil : (A : Set) -> List A A is big in constructor nil as the sort Set1 of its type Set is bigger than the sort Set of the data type List.

Constructors

Big 
Small 

Instances

data Relevance

A function argument can be relevant or irrelevant. See Agda.TypeChecking.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 Big

The argument can be skipped during equality checking because its value is already determined by the type. If a constructor argument is big, it has to be regarded absent, otherwise we get into paradoxes.

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

class LensRelevance a where

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

Minimal complete definition

getRelevance

Methods

getRelevance :: a -> Relevance

setRelevance :: Relevance -> a -> a

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

moreRelevant :: Relevance -> Relevance -> Bool

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

Argument decoration

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

Arguments

data Arg c e

Constructors

Arg 

Fields

argInfo :: ArgInfo c
 
unArg :: e
 

Instances

IsPrefixOf Args 
UniverseBi Args Pattern 
UniverseBi Args Term 
Functor (Arg c) 
Foldable (Arg c) 
Traversable (Arg c) 
Decoration (Arg c) 
Pretty a => Pretty (Arg a) 
ExprLike a => ExprLike (Arg a) 
SubstExpr a => SubstExpr (Arg a) 
AllNames a => AllNames (Arg a) 
Free a => Free (Arg a) 
TermLike a => TermLike (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) 
FoldRigid a => FoldRigid (Arg a) 
Occurs a => Occurs (Arg a) 
NoProjectedVar a => NoProjectedVar (Arg a) 
HasPolarity a => HasPolarity (Arg a) 
ComputeOccurrences a => ComputeOccurrences (Arg a) 
UReduce a => UReduce (Arg a) 
Unquote a => Unquote (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.

AmbMatch a b => AmbMatch (Arg a) (Arg b) 
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) 
(KillRange c, KillRange a) => KillRange (Arg c a) 
SetRange a => SetRange (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) 
LabelPatVars a b i => LabelPatVars (Arg c a) (Arg c b) i 

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

argColors :: Arg c a -> [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

Minimal complete definition

underscore

Methods

underscore :: a

isUnderscore :: a -> Bool

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

TeleNoAbs Telescope 
TeleNoAbs ListTel 
Abstract Telescope 
KillVar Telescope 
GenC Telescope 
AddContext Telescope 
PrettyTCM Telescope 
EmbPrj Telescope 
Reduce Telescope 
Instantiate Telescope 
DropArgs Telescope

NOTE: This creates telescopes with unbound de Bruijn indices.

ShrinkC Telescope Telescope 
Reify Telescope Telescope 
Functor (Dom c) 
Foldable (Dom c) 
Traversable (Dom c) 
Decoration (Dom c) 
SgTel (Dom (ArgName, Type)) 
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) 
FoldRigid a => FoldRigid (Dom a) 
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) 
(KillRange c, KillRange a) => KillRange (Dom c a) 
HasRange a => HasRange (Dom c a) 
LensRelevance (Dom c e) 
LensHiding (Dom c e) 
SgTel (ArgName, Dom Type) 
LensSort a => LensSort (Dom c a) 
(GetDefs c, GetDefs a) => GetDefs (Dom c a) 
(GenC c, GenC a) => GenC (Dom c a) 
AddContext ([Name], Dom Type) 
AddContext ([WithHiding 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 a -> [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

Functor (Named name) 
Show a => Show (Named_ a) 
Foldable (Named name) 
Traversable (Named name) 
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) 
(KillRange name, KillRange a) => KillRange (Named name a) 
SetRange a => SetRange (Named name a) 
HasRange a => HasRange (Named name a) 
ExprLike a => ExprLike (Named name a) 
IsProjP a => IsProjP (Named n a) 
SubstExpr a => SubstExpr (Named name a) 
AllNames a => AllNames (Named name a) 
ExprLike a => ExprLike (Named x 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) 
LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i 

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.

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
 

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.

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 

data Access

Access modifier.

Constructors

PrivateAccess 
PublicAccess 
OnlyQualified

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

data IsInstance

Is this definition eligible for instance search?

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 

newtype Constr a

Constructors

Constr a 

Interaction meta variables

Termination

data TerminationCheck m

Termination check? (Default = True).

Constructors

TerminationCheck

Run the termination checker.

NoTerminationCheck

Skip termination checking (unsafe).

NonTerminating

Treat as non-terminating.

Terminating

Treat as terminating (unsafe). Same effect as NoTerminationCheck.

TerminationMeasure !Range m

Skip termination checking but use measure instead.