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

Safe HaskellNone

Agda.Syntax.Common

Contents

Description

Some common syntactic entities are defined in this module.

Synopsis

Documentation

data Delayed

Used to specify whether something should be delayed.

Constructors

Delayed 
NotDelayed 

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

moreRelevant :: Relevance -> Relevance -> Bool

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

Function type domain

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

Instances

argFromDom :: Dom a -> Arg a

domFromArg :: Arg a -> Dom a

mapDomHiding :: (Hiding -> Hiding) -> Dom a -> Dom a

Argument decoration

data Arg e

A function argument can be hidden and/or irrelevant.

Constructors

Arg 

Instances

Functor Arg 
Typeable1 Arg 
Foldable Arg 
Traversable Arg 
UniverseBi Args Pattern 
UniverseBi Args Term 
Eq a => Eq (Arg a) 
Ord e => Ord (Arg e) 
Show a => Show (Arg a) 
Sized a => Sized (Arg a) 
Pretty e => Pretty (Arg e) 
KillRange a => KillRange (Arg a) 
HasRange a => HasRange (Arg a) 
Free a => Free (Arg a) 
TermLike a => TermLike (Arg a) 
Subst a => Subst (Arg a) 
AbstractTerm a => AbstractTerm (Arg a) 
Alpha a => Alpha (Arg a) 
Rename a => Rename (Arg a) 
(ReifyWhen a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a) 
InstantiateFull t => InstantiateFull (Arg t) 
Normalise t => Normalise (Arg t) 
Reduce t => Reduce (Arg t) 
Instantiate t => Instantiate (Arg t) 
Match a => Match (Arg a) 
DotVars a => DotVars (Arg a) 
MentionsMeta t => MentionsMeta (Arg t) 
EmbPrj a => EmbPrj (Arg a) 
Occurs a => Occurs (Arg a) 
ComputeOccurrences a => ComputeOccurrences (Arg a) 
HasPolarity a => HasPolarity (Arg a) 
Unquote a => Unquote (Arg a) 
StripAllProjections a => StripAllProjections (Arg a) 
KillVar a => KillVar (Arg a) 
GenC a => GenC (Arg a) 
LowerMeta a => LowerMeta (Arg a) 
ToConcrete a c => ToConcrete (Arg a) (Arg c) 
ToAbstract c a => ToAbstract (Arg c) (Arg a) 
ReifyWhen i a => Reify (Arg i) (Arg a)

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

Reify i a => Reify (Dom i) (Arg a) 
ReifyWhen i a => ReifyWhen (Arg i) (Arg a) 
SubstHH a b => SubstHH (Arg a) (Arg b) 
ShrinkC a b => ShrinkC (Arg a) (Arg b) 

mapArgHiding :: (Hiding -> Hiding) -> Arg a -> Arg a

makeInstance :: Arg a -> Arg a

hide :: Arg a -> Arg a

defaultArg :: a -> Arg a

withArgsFrom :: [a] -> [Arg b] -> [Arg 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.

Named arguments

data Named name a

Constructors

Named 

Fields

nameOf :: Maybe name
 
namedThing :: a
 

Instances

Typeable2 Named 
Functor (Named name) 
Foldable (Named name) 
Traversable (Named name) 
(Eq name, Eq a) => Eq (Named name a) 
(Ord name, Ord a) => Ord (Named name a) 
Show a => Show (Named String a) 
Sized a => Sized (Named name a) 
Pretty e => Pretty (Named String e) 
KillRange a => KillRange (Named name a) 
HasRange a => HasRange (Named name a) 
(Eq n, Alpha a) => Alpha (Named n a) 
Rename a => Rename (Named n a) 
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named String a) 
DotVars a => DotVars (Named s a) 
(EmbPrj s, EmbPrj t) => EmbPrj (Named s t) 
LowerMeta a => LowerMeta (Named name a) 
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) 
ReifyWhen i a => ReifyWhen (Named n i) (Named n a) 

unnamed :: a -> Named name a

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

type NamedArg a = Arg (Named String a)

Only Hidden arguments can have names.

namedArg :: NamedArg a -> a

Get the content of a NamedArg.

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

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

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.

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