Arguments

Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2024-02-07.

module reflection.arguments where
Imports 
open import foundation.universe-levels

Idea

An argument to a function is a term together with some information about it. The argument has three properties:

  1. Visibility: whether they are visible, hidden, or an instance
  2. Relevance: whether they are relevant or not (see, docs)
  3. Quantity: whether they are run-time relevant or not (see, docs)

The properties of Relevance-Argument-Agda and Quantity-Argument-Agda are combined in one, called Modality-Argument-Agda.

For concrete examples, see reflection.definitions.

Definitions

data Visibility-Argument-Agda : UU lzero where
  visible-Visibility-Argument-Agda : Visibility-Argument-Agda
  hidden-Visibility-Argument-Agda : Visibility-Argument-Agda
  instance-Visibility-Argument-Agda : Visibility-Argument-Agda

data Relevance-Argument-Agda : UU lzero where
  relevant-Relevance-Argument-Agda : Relevance-Argument-Agda
  irrelevant-Relevance-Argument-Agda : Relevance-Argument-Agda

data Quantity-Argument-Agda : UU lzero where
  zero-Quantity-Argument-Agda : Quantity-Argument-Agda
  omega-Quantity-Argument-Agda : Quantity-Argument-Agda

data Modality-Argument-Agda : UU lzero where
  cons-Modality-Argument-Agda :
    Relevance-Argument-Agda → Quantity-Argument-Agda → Modality-Argument-Agda

data Info-Argument-Agda : UU lzero where
  cons-Info-Argument-Agda :
    Visibility-Argument-Agda → Modality-Argument-Agda → Info-Argument-Agda

data Argument-Agda {l : Level} (A : UU l) : UU l where
  cons-Argument-Agda : Info-Argument-Agda → A → Argument-Agda A
Bindings 
{-# BUILTIN HIDING Visibility-Argument-Agda #-}
{-# BUILTIN VISIBLE visible-Visibility-Argument-Agda #-}
{-# BUILTIN HIDDEN hidden-Visibility-Argument-Agda #-}
{-# BUILTIN INSTANCE instance-Visibility-Argument-Agda #-}

{-# BUILTIN RELEVANCE Relevance-Argument-Agda #-}
{-# BUILTIN RELEVANT relevant-Relevance-Argument-Agda #-}
{-# BUILTIN IRRELEVANT irrelevant-Relevance-Argument-Agda #-}

{-# BUILTIN QUANTITY Quantity-Argument-Agda #-}
{-# BUILTIN QUANTITY-0 zero-Quantity-Argument-Agda #-}
{-# BUILTIN QUANTITY-ω omega-Quantity-Argument-Agda #-}

{-# BUILTIN MODALITY Modality-Argument-Agda #-}
{-# BUILTIN MODALITY-CONSTRUCTOR cons-Modality-Argument-Agda #-}

{-# BUILTIN ARGINFO Info-Argument-Agda #-}
{-# BUILTIN ARGARGINFO cons-Info-Argument-Agda #-}

{-# BUILTIN ARG Argument-Agda #-}
{-# BUILTIN ARGARG cons-Argument-Agda #-}

Helpers

We create helper patterns for the two most common type of arguments.

-- visible-Argument-Agda : {l : Level} {A : UU l} → A → Argument-Agda A
pattern visible-Argument-Agda t =
  cons-Argument-Agda
    ( cons-Info-Argument-Agda
      ( visible-Visibility-Argument-Agda)
      ( cons-Modality-Argument-Agda
        ( relevant-Relevance-Argument-Agda)
        ( omega-Quantity-Argument-Agda)))
    ( t)

-- hidden-Argument-Agda : {l : Level} {A : UU l} → A → Argument-Agda A
pattern hidden-Argument-Agda t =
  cons-Argument-Agda
    ( cons-Info-Argument-Agda
      ( hidden-Visibility-Argument-Agda)
      ( cons-Modality-Argument-Agda
        ( relevant-Relevance-Argument-Agda)
        ( omega-Quantity-Argument-Agda)))
    ( t)

Recent changes