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

Safe Haskell | None

Agda.Syntax.Common

Contents

- Relevance
- Function type domain
- Argument decoration
- Named arguments
- Infixity, access, abstract, etc.

Description

Some common syntactic entities are defined in this module.

Synopsis

- data Delayed
  - = Delayed
  - | NotDelayed
- data Induction
  - = Inductive
  - | CoInductive
- data Hiding
  - = Hidden
  - | Instance
  - | NotHidden
- data Relevance
  - = Relevant
  - | NonStrict
  - | Irrelevant
  - | Forced
  - | UnusedArg
- moreRelevant :: Relevance -> Relevance -> Bool
- data Dom e = Dom {
  - domHiding :: Hiding
  - domRelevance :: Relevance
  - unDom :: e
  }
- argFromDom :: Dom a -> Arg a
- domFromArg :: Arg a -> Dom a
- mapDomHiding :: (Hiding -> Hiding) -> Dom a -> Dom a
- mapDomRelevance :: (Relevance -> Relevance) -> Dom a -> Dom a
- data Arg e = Arg {
  - argHiding :: Hiding
  - argRelevance :: Relevance
  - unArg :: e
  }
- mapArgHiding :: (Hiding -> Hiding) -> Arg a -> Arg a
- mapArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg a
- makeInstance :: Arg a -> Arg a
- hide :: Arg a -> Arg a
- defaultArg :: a -> Arg a
- isHiddenArg :: Arg a -> Bool
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- data Named name a = Named {
  - nameOf :: Maybe name
  - namedThing :: a
  }
- unnamed :: a -> Named name a
- named :: name -> a -> Named name a
- type NamedArg a = Arg (Named String a)
- namedArg :: NamedArg a -> a
- defaultNamedArg :: a -> NamedArg a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- data IsInfix
  - = InfixDef
  - | PrefixDef
- data Access
  - = PrivateAccess
  - | PublicAccess
  - | OnlyQualified
- data IsAbstract
  - = AbstractDef
  - | ConcreteDef
- type Nat = Int
- type Arity = Nat
- data NameId = NameId Integer Integer
- newtype Constr a = Constr a

# Documentation

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 |

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 |

data Hiding

Constructors

Hidden |
Instance |
NotHidden |

Instances

Eq Hiding |
Ord Hiding |
Show Hiding |
Typeable Hiding |
KillRange Hiding |
EmbPrj Hiding |
Unquote Hiding |
GenC Hiding |
ShrinkC Hiding Hiding |

# 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 |
PrettyTCM Relevance |
EmbPrj Relevance |
Unquote Relevance |

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 |

Fields

domHiding :: Hiding
domRelevance :: Relevance
unDom :: e

Instances

Functor Dom |
Typeable1 Dom |
Foldable Dom |
Traversable Dom |
Abstract Telescope |
PrettyTCM Telescope |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices.
Reduce Telescope |
Instantiate Telescope |
EmbPrj Telescope |
KillVar Telescope |
GenC Telescope |
Reify Telescope Telescope |
ShrinkC Telescope Telescope |
Eq e => Eq (Dom e) |
Ord e => Ord (Dom e) |
Show a => Show (Dom a) |
Sized a => Sized (Dom a) |
KillRange a => KillRange (Dom a) |
HasRange a => HasRange (Dom a) |
Free a => Free (Dom a) |
TermLike a => TermLike (Dom a) |
Subst a => Subst (Dom a) |
AbstractTerm a => AbstractTerm (Dom a) |
(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a) |
InstantiateFull t => InstantiateFull (Dom t) |
Normalise t => Normalise (Dom t) |
Reduce t => Reduce (Dom t) |
Instantiate t => Instantiate (Dom t) |
MentionsMeta t => MentionsMeta (Dom t) |
EmbPrj a => EmbPrj (Dom a) |
Occurs a => Occurs (Dom a) |
ComputeOccurrences a => ComputeOccurrences (Dom a) |
HasPolarity a => HasPolarity (Dom a) |
KillVar a => KillVar (Dom a) |
GenC a => GenC (Dom a) |
Reify i a => Reify (Dom i) (Arg a) |
SubstHH a b => SubstHH (Dom a) (Dom b) |
ShrinkC a b => ShrinkC (Dom a) (Dom b) |

argFromDom :: Dom a -> Arg a

domFromArg :: Arg a -> Dom a

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

mapDomRelevance :: (Relevance -> Relevance) -> Dom a -> Dom a

# Argument decoration

data Arg e

A function argument can be hidden and/or irrelevant.

Constructors

Arg |

Fields

argHiding :: Hiding
argRelevance :: Relevance
unArg :: e

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

mapArgRelevance :: (Relevance -> Relevance) -> Arg a -> Arg a

makeInstance :: Arg a -> Arg a

hide :: Arg a -> Arg a

defaultArg :: a -> Arg a

isHiddenArg :: Arg a -> Bool

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

`xs `withArgsFrom` args` translates `xs` into a list of `Arg`s, 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`.

defaultNamedArg :: a -> NamedArg a

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 |

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 |
EmbPrj IsAbstract |

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 |