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

Safe Haskell | None

Agda.Syntax.Internal

Contents

- Definitions
- Smart constructors
- Handling blocked terms.
- Simple operations on terms and types.
- Show instances.
- Sized instances.
- KillRange instances.
- UniverseBi instances.

Synopsis

- data Term
  - = Var !Int Args
  - | Lam Hiding (Abs Term)
  - | Lit Literal
  - | Def QName Args
  - | Con QName Args
  - | Pi (Dom Type) (Abs Type)
  - | Sort Sort
  - | Level Level
  - | MetaV !MetaId Args
  - | DontCare Term
  - | Shared !(Ptr Term)
- type Args = [Arg Term]
- data Elim
  - = Apply (Arg Term)
  - | Proj QName
- data Abs a
  - = Abs {
    - absName :: String
    - unAbs :: a
    }
  - | NoAbs {
    - absName :: String
    - unAbs :: a
    }
- data Type = El {
  - getSort :: Sort
  - unEl :: Term
  }
- data Tele a
  - = EmptyTel
  - | ExtendTel a (Abs (Tele a))
- type Telescope = Tele (Dom Type)
- data Sort
  - = Type Level
  - | Prop
  - | Inf
  - | DLub Sort (Abs Sort)
- newtype Level = Max [PlusLevel]
- data PlusLevel
  - = ClosedLevel Integer
  - | Plus Integer LevelAtom
- data LevelAtom
  - = MetaLevel MetaId Args
  - | BlockedLevel MetaId Term
  - | NeutralLevel Term
  - | UnreducedLevel Term
- newtype MetaId = MetaId Nat
- data Blocked t
  - = Blocked MetaId t
  - | NotBlocked t
- data Clause = Clause {
  - clauseRange :: Range
  - clauseTel :: Telescope
  - clausePerm :: Permutation
  - clausePats :: [Arg Pattern]
  - clauseBody :: ClauseBody
  }
- data ClauseBody
  - = Body Term
  - | Bind (Abs ClauseBody)
  - | NoBody
- data Pattern
  - = VarP String
  - | DotP Term
  - | ConP QName (Maybe (Arg Type)) [Arg Pattern]
  - | LitP Literal
- patternVars :: Arg Pattern -> [Arg (Either String Term)]
- properlyMatching :: Pattern -> Bool
- ignoreSharing :: Term -> Term
- ignoreSharingType :: Type -> Type
- shared :: Term -> Term
- sharedType :: Type -> Type
- updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)
- updateSharedM :: Monad m => (Term -> m Term) -> Term -> m Term
- updateShared :: (Term -> Term) -> Term -> Term
- pointerChain :: Term -> [Ptr Term]
- compressPointerChain :: Term -> Term
- var :: Nat -> Term
- typeDontCare :: Type
- topSort :: Type
- set0 :: Type
- set :: Integer -> Type
- prop :: Type
- sort :: Sort -> Type
- varSort :: Int -> Sort
- sSuc :: Sort -> Sort
- levelSuc :: Level -> Level
- mkType :: Integer -> Sort
- impossibleTerm :: String -> Int -> Term
- blockingMeta :: Blocked t -> Maybe MetaId
- blocked :: MetaId -> a -> Blocked a
- notBlocked :: a -> Blocked a
- ignoreBlocking :: Blocked a -> a
- stripDontCare :: Term -> Term
- arity :: Type -> Nat
- argName :: Type -> String
- module Agda.Syntax.Abstract.Name
- module Agda.Utils.Pointer

# Documentation

data Term

Raw values.

`Def` is used for both defined and undefined constants. Assume there is a type declaration and a definition for every constant, even if the definition is an empty list of clauses.

Constructors

Var !Int Args | `x vs` neutral
Lam Hiding (Abs Term) | terms are beta normal
Lit Literal |
Def QName Args | `f vs`, possibly a redex

Con QName Args

    c vs

Pi (Dom Type) (Abs Type) | dependent or non-dependent function space
Sort Sort |
Level Level |
MetaV !MetaId Args |
DontCare Term | Irrelevant stuff in relevant position, but created in an irrelevant context. Basically, an internal version of the irrelevance axiom `.irrAx : .A -> A`.
Shared !(Ptr Term) | Explicit sharing

Instances

Eq Term | Syntactic equality, ignores stuff below `DontCare`.
Ord Term |
Show Term |
Typeable Term |
Sized Term |
KillRange Term |
Free Term |
TermLike Term |
Subst Term |
Abstract Term |
Apply Term |
AbstractTerm Term |
PrettyTCM Term |
InstantiateFull Term |
Normalise Term |
Reduce Term |
Instantiate Term |
Match Term |
MentionsMeta Term |
EmbPrj Term |
Occurs Term |
ComputeOccurrences Term |
HasPolarity Term |
Unquote Term |
ApplyHH Term |
UReduce Term |
StripAllProjections Term |
KillVar Term |
GenC Term |
UniverseBi Args Pattern |
UniverseBi Args Term |
Reify Term Expr |
ShrinkC Term Term |
SubstHH Term (HomHet Term) |
UniverseBi [Term] Term |
UniverseBi ([Type], [Clause]) Term |

type Args = [Arg Term]

Type of argument lists.

data Elim

Eliminations, subsuming applications and projections. Used for a view which exposes the head of a neutral term.

Constructors

Apply (Arg Term) |
Proj QName | name of a record projection

Instances

Eq Elim |
Ord Elim |
Show Elim |
Subst Elim |
PrettyTCM Elim |
InstantiateFull Elim |
Normalise Elim |
Reduce Elim |
Instantiate Elim |
MentionsMeta Elim |
Reify Elim Expr |

data Abs a

Binder. `Abs`: The bound variable might appear in the body. `NoAbs` is pseudo-binder, it does not introduce a fresh variable, similar to the `const` of Haskell.

Constructors

Abs | The body has (at least) one free variable. Danger: `unAbs` doesn't shift variables properly

Fields

absName :: String
unAbs :: a

NoAbs |

Fields

absName :: String
unAbs :: a

Instances

Functor Abs |
Typeable1 Abs |
Foldable Abs |
Traversable Abs |
(Subst a, Eq a) => Eq (Abs a) |
(Subst a, Ord a) => Ord (Abs a) |
Show a => Show (Abs a) |
Sized a => Sized (Abs a) |
KillRange a => KillRange (Abs a) |
Free a => Free (Abs a) |
TermLike a => TermLike (Abs a) |
Subst a => Subst (Abs a) |
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) |
(Subst t, InstantiateFull t) => InstantiateFull (Abs t) |
(Subst t, Normalise t) => Normalise (Abs t) |
(Subst t, Reduce t) => Reduce (Abs t) |
Instantiate t => Instantiate (Abs t) |
MentionsMeta t => MentionsMeta (Abs t) |
EmbPrj a => EmbPrj (Abs a) |
(Occurs a, Subst a) => Occurs (Abs a) |
ComputeOccurrences a => ComputeOccurrences (Abs a) |
HasPolarity a => HasPolarity (Abs a) |
Unquote a => Unquote (Abs a) |
KillVar a => KillVar (Abs a) |
GenC a => GenC (Abs a) |
SubstHH a b => SubstHH (Abs a) (Abs b) |
ShrinkC a b => ShrinkC (Abs a) (Abs b) |
(Free i, Reify i a) => Reify (Abs i) (Name, a) |

data Type

Types are terms with a sort annotation.

Constructors

El |

Fields

getSort :: Sort
unEl :: Term

Instances

Eq Type |
Ord Type |
Show Type |
Typeable Type |
Error Type |
Sized Type |
KillRange Type |
Free Type |
TermLike Type |
Subst Type |
Abstract Telescope |
Abstract Type |
Apply Type |
AbstractTerm Type |
PrettyTCM Telescope |
PrettyTCM Type |
DropArgs Telescope | NOTE: This creates telescopes with unbound de Bruijn indices.
InstantiateFull Type |
Normalise Type |
Reduce Telescope |
Reduce Type |
Instantiate Telescope |
Instantiate Type |
MentionsMeta Type |
EmbPrj Telescope |
EmbPrj Type |
Occurs Type |
ComputeOccurrences Type |
HasPolarity Type |
Unquote Type |
ToTerm Type |
PrimTerm Type |
ApplyHH Type |
UReduce Type |
KillVar Telescope |
KillVar Type |
GenC Telescope |
GenC Type |
Reify Telescope Telescope |
Reify Type Expr |
ShrinkC Telescope Telescope |
ShrinkC Type Type |
SubstHH Type (HomHet Type) |
UniverseBi ([Type], [Clause]) Pattern |
UniverseBi ([Type], [Clause]) Term |

data Tele a

Sequence of types. An argument of the first type is bound in later types and so on.

Constructors

EmptyTel |
ExtendTel a (Abs (Tele a)) | `Abs` is never `NoAbs`.

Instances

Functor Tele |
Typeable1 Tele |
Foldable Tele |
Traversable Tele |
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 |
(Subst a, Eq a) => Eq (Tele a) |
(Subst a, Ord a) => Ord (Tele a) |
Show a => Show (Tele a) |
Sized (Tele a) |
KillRange a => KillRange (Tele a) |
Free a => Free (Tele a) |
Subst a => Subst (Tele a) |
Subst a => Apply (Tele a) |
(Subst a, InstantiateFull a) => InstantiateFull (Tele a) |
(Subst a, Normalise a) => Normalise (Tele a) |
MentionsMeta a => MentionsMeta (Tele a) |
ComputeOccurrences a => ComputeOccurrences (Tele a) |
SubstHH a b => SubstHH (Tele a) (Tele b) |

type Telescope = Tele (Dom Type)

data Sort

Sorts.

Constructors

Type Level |
Prop |
Inf |
DLub Sort (Abs Sort) | if the free variable occurs in the second sort the whole thing should reduce to Inf, otherwise it's the normal Lub

Instances

Eq Sort |
Ord Sort |
Show Sort |
Typeable Sort |
KillRange Sort |
Free Sort |
Subst Sort |
Abstract Sort |
Apply Sort |
AbstractTerm Sort |
PrettyTCM Sort |
InstantiateFull Sort |
Normalise Sort |
Reduce Sort |
Instantiate Sort |
Match Sort |
MentionsMeta Sort |
EmbPrj Sort |
Occurs Sort |
Unquote Sort |
GenC Sort |
Reify Sort Expr |
ShrinkC Sort Sort |

newtype Level

A level is a maximum expression of 0..n plus expressions each of which is a number or an atom plus a number.

Constructors

Max [PlusLevel] |

Instances

Eq Level |
Ord Level |
Show Level |
Typeable Level |
Sized Level |
KillRange Level |
Free Level |
TermLike Level |
Subst Level |
AbstractTerm Level |
PrettyTCM Level |
InstantiateFull Level |
Normalise Level |
Reduce Level |
Instantiate Level |
Match Level |
MentionsMeta Level |
EmbPrj Level |
Occurs Level |
ComputeOccurrences Level |
HasPolarity Level |
Unquote Level |
Reify Level Expr |

data PlusLevel

Constructors

ClosedLevel Integer |
Plus Integer LevelAtom |

Instances

Eq PlusLevel |
Ord PlusLevel |
Show PlusLevel |
Typeable PlusLevel |
Sized PlusLevel |
KillRange PlusLevel |
Free PlusLevel |
TermLike PlusLevel |
Subst PlusLevel |
AbstractTerm PlusLevel |
InstantiateFull PlusLevel |
Normalise PlusLevel |
Reduce PlusLevel |
Instantiate PlusLevel |
MentionsMeta PlusLevel |
EmbPrj PlusLevel |
Occurs PlusLevel |
ComputeOccurrences PlusLevel |
HasPolarity PlusLevel |

data LevelAtom

Constructors

MetaLevel MetaId Args |
BlockedLevel MetaId Term |
NeutralLevel Term |
UnreducedLevel Term |

Instances

Eq LevelAtom |
Ord LevelAtom |
Show LevelAtom |
Typeable LevelAtom |
Sized LevelAtom |
KillRange LevelAtom |
Free LevelAtom |
TermLike LevelAtom |
Subst LevelAtom |
AbstractTerm LevelAtom |
InstantiateFull LevelAtom |
Normalise LevelAtom |
Reduce LevelAtom |
Instantiate LevelAtom |
MentionsMeta LevelAtom |
EmbPrj LevelAtom |
Occurs LevelAtom |
ComputeOccurrences LevelAtom |
HasPolarity LevelAtom |

newtype MetaId

A meta variable identifier is just a natural number.

Constructors

MetaId Nat |

Instances

Enum MetaId |
Eq MetaId |
Integral MetaId |
Num MetaId |
Ord MetaId |
Real MetaId |
Show MetaId |
Typeable MetaId |
PrettyTCM MetaId |
HasFresh MetaId FreshThings |
Reify MetaId Expr |

data Blocked t

Something where a meta variable may block reduction.

Constructors

Blocked MetaId t |
NotBlocked t |

Instances

Functor Blocked |
Typeable1 Blocked |
Applicative Blocked |
Foldable Blocked |
Traversable Blocked |
Eq t => Eq (Blocked t) |
Ord t => Ord (Blocked t) |
Show t => Show (Blocked t) |
KillRange a => KillRange (Blocked a) |
Subst t => Subst (Blocked t) |
Apply t => Apply (Blocked t) |
PrettyTCM a => PrettyTCM (Blocked a) |
Instantiate a => Instantiate (Blocked a) |
ShrinkC a b => ShrinkC (Blocked a) (Blocked b) |

# Definitions

data Clause

A clause is a list of patterns and the clause body should `Bind`.

The telescope contains the types of the pattern variables and the permutation is how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the patterns.

    clauseTel ~ permute clausePerm (patternVars clausPats)

For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!

Constructors

Clause |

Fields

clauseRange :: Range
clauseTel :: Telescope
clausePerm :: Permutation
clausePats :: [Arg Pattern]
clauseBody :: ClauseBody

Instances

Show Clause |
Typeable Clause |
HasRange Clause |
Abstract Clause |
Abstract FunctionInverse |
Apply Clause |
Apply FunctionInverse |
PrettyTCM NamedClause |
DropArgs Clause | NOTE: does not work for recursive functions.
DropArgs FunctionInverse |
InstantiateFull Clause |
InstantiateFull FunctionInverse |
EmbPrj Clause |
EmbPrj FunctionInverse |
Occurs Clause |
ComputeOccurrences Clause |
Reify NamedClause Clause |
UniverseBi ([Type], [Clause]) Pattern |
UniverseBi ([Type], [Clause]) Term |

data ClauseBody

Constructors

Body Term |
Bind (Abs ClauseBody) |
NoBody | for absurd clauses.

Instances

Show ClauseBody |
Typeable ClauseBody |
Free ClauseBody |
Subst ClauseBody |
Abstract ClauseBody |
Apply ClauseBody |
PrettyTCM ClauseBody |
DropArgs ClauseBody | NOTE: does not go into the body, so does not work for recursive functions.
InstantiateFull ClauseBody |
Normalise ClauseBody |
EmbPrj ClauseBody |
Reify ClauseBody RHS |

data Pattern

Patterns are variables, constructors, or wildcards. `QName` is used in `ConP` rather than `Name` since a constructor might come from a particular namespace. This also meshes well with the fact that values (i.e. the arguments we are matching with) use `QName`.

Constructors

VarP String |
DotP Term |
ConP QName (Maybe (Arg Type)) [Arg Pattern] | The type is ``Just` t`' iff the pattern is a record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (`clauseTel`).
LitP Literal |

Instances

Show Pattern |
Typeable Pattern |
Subst Pattern |
InstantiateFull Pattern |
Normalise Pattern |
EmbPrj Pattern |
UniverseBi Args Pattern |
UniverseBi ([Type], [Clause]) Pattern |

patternVars :: Arg Pattern -> [Arg (Either String Term)]

Extract pattern variables in left-to-right order. A `DotP` is also treated as variable (see docu for `Clause`).

properlyMatching :: Pattern -> Bool

Does the pattern perform a match that could fail?

# Smart constructors

ignoreSharing :: Term -> Term

ignoreSharingType :: Type -> Type

shared :: Term -> Term

sharedType :: Type -> Type

updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)

Typically m would be TCM and f would be Blocked.

updateSharedM :: Monad m => (Term -> m Term) -> Term -> m Term

updateShared :: (Term -> Term) -> Term -> Term

pointerChain :: Term -> [Ptr Term]

compressPointerChain :: Term -> Term

var :: Nat -> Term

An unapplied variable.

typeDontCare :: Type

A dummy type.

topSort :: Type

Top sort (Setomega).

set0 :: Type

set :: Integer -> Type

prop :: Type

sort :: Sort -> Type

varSort :: Int -> Sort

sSuc :: Sort -> Sort

Get the next higher sort.

levelSuc :: Level -> Level

mkType :: Integer -> Sort

impossibleTerm :: String -> Int -> Term

# Handling blocked terms.

blockingMeta :: Blocked t -> Maybe MetaId

blocked :: MetaId -> a -> Blocked a

notBlocked :: a -> Blocked a

ignoreBlocking :: Blocked a -> a

# Simple operations on terms and types.

stripDontCare :: Term -> Term

Removing a topmost `DontCare` constructor.

arity :: Type -> Nat

Doesn't do any reduction.

argName :: Type -> String

Suggest a name for the first argument of a function of the given type.

# Show instances.

# Sized instances.

# KillRange instances.

# UniverseBi instances.

module Agda.Syntax.Abstract.Name

module Agda.Utils.Pointer