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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.With

Synopsis

- splitTelForWith :: Telescope -> Type -> [EqualityView] -> [Term] -> (Telescope, Telescope, Permutation, Type, [EqualityView], [Term])
- withFunctionType :: Telescope -> [Term] -> [EqualityView] -> Telescope -> Type -> TCM (Type, Nat)
- countWithArgs :: [EqualityView] -> Nat
- withArguments :: [Term] -> [EqualityView] -> [Term]
- buildWithFunction :: [Name] -> QName -> QName -> Type -> Telescope -> [NamedArg DeBruijnPattern] -> Nat -> Substitution -> Permutation -> Nat -> Nat -> [SpineClause] -> TCM [SpineClause]
- stripWithClausePatterns :: [Name] -> QName -> QName -> Type -> Telescope -> [NamedArg DeBruijnPattern] -> Nat -> Permutation -> [NamedArg Pattern] -> TCM ([ProblemEq], [NamedArg Pattern])
- withDisplayForm :: QName -> QName -> Telescope -> Telescope -> Nat -> [NamedArg DeBruijnPattern] -> Permutation -> Permutation -> TCM DisplayForm
- patsToElims :: [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm]

# Documentation

splitTelForWith Source #

Arguments

:: Telescope | `Δ` context of types and with-arguments.
-> Type | `Δ ⊢ t` type of rhs.
-> [EqualityView] | `Δ ⊢ as` types of with arguments.
-> [Term] | `Δ ⊢ vs` with arguments. Output:

-> (Telescope, Telescope, Permutation, Type, [EqualityView], [Term])

(`Δ₁`,`Δ₂`,`π`,`t'`,`as'`,`vs'`) where

`Δ₁`
  part of context needed for with arguments and their types.
`Δ₂`
  part of context not needed for with arguments and their types.
`π`
  permutation from Δ to Δ₁Δ₂ as returned by `splitTelescope`.
`Δ₁Δ₂ ⊢ t'`
  type of rhs under `π`
`Δ₁ ⊢ as'`
  types with with-arguments depending only on `Δ₁`.
`Δ₁ ⊢ vs'`
  with-arguments under `π`.

Split pattern variables according to with-expressions.

withFunctionType Source #

Arguments

:: Telescope | `Δ₁` context for types of with types.
-> [Term] | `Δ₁,Δ₂ ⊢ vs : raise Δ₂ as` with and rewrite-expressions.
-> [EqualityView] | `Δ₁ ⊢ as` types of with and rewrite-expressions.
-> Telescope | `Δ₁ ⊢ Δ₂` context extension to type with-expressions.
-> Type | `Δ₁,Δ₂ ⊢ b` type of rhs.
-> TCM (Type, Nat) | `Δ₁ → wtel → Δ₂′ → b′` such that `[vs/wtel]wtel = as` and `[vs/wtel]Δ₂′ = Δ₂` and `[vs/wtel]b′ = b`. Plus the final number of with-arguments.

Abstract with-expressions `vs` to generate type for with-helper function.

Each `EqualityType`, coming from a `rewrite`, will turn into 2 abstractions.

countWithArgs :: [EqualityView] -> Nat Source #

withArguments :: [Term] -> [EqualityView] -> [Term] Source #

From a list of `with` and `rewrite` expressions and their types, compute the list of final `with` expressions (after expanding the `rewrite`s).

buildWithFunction Source #

Arguments

:: [Name] | Names of the module parameters of the parent function.
-> QName | Name of the parent function.
-> QName | Name of the with-function.
-> Type | Types of the parent function.
-> Telescope | Context of parent patterns.
-> [NamedArg DeBruijnPattern] | Parent patterns.
-> Nat | Number of module parameters in parent patterns
-> Substitution | Substitution from parent lhs to with function lhs
-> Permutation | Final permutation.
-> Nat | Number of needed vars.
-> Nat | Number of with expressions.
-> [SpineClause] | With-clauses.
-> TCM [SpineClause] | With-clauses flattened wrt. parent patterns.

Compute the clauses for the with-function given the original patterns.

stripWithClausePatterns Source #

Arguments

:: [Name] | `cxtNames` names of the module parameters of the parent function
-> QName | `parent` name of the parent function.
-> QName | `f` name of with-function.
-> Type | `t` top-level type of the original function.
-> Telescope | `Δ` context of patterns of parent function.
-> [NamedArg DeBruijnPattern] | `qs` internal patterns for original function.
-> Nat | `npars` number of module parameters in `qs`.
-> Permutation | `π` permutation taking `vars(qs)` to `support(Δ)`.
-> [NamedArg Pattern] | `ps` patterns in with clause (eliminating type `t`).
-> TCM ([ProblemEq], [NamedArg Pattern]) | `ps'` patterns for with function (presumably of type `Δ`).

    stripWithClausePatterns cxtNames parent f t Δ qs np π ps = ps'

Example:

      record Stream (A : Set) : Set where
        coinductive
        constructor delay
        field       force : A × Stream A

      record SEq (s t : Stream A) : Set where
        coinductive
        field
          ~force : let a , as = force s
                       b , bs = force t
                   in  a ≡ b × SEq as bs

      test : (s : Nat × Stream Nat) (t : Stream Nat) → SEq (delay s) t → SEq t (delay s)
      ~force (test (a     , as) t p) with force t
      ~force (test (suc n , as) t p) | b , bs = ?

With function:

      f : (t : Stream Nat) (w : Nat × Stream Nat) (a : Nat) (as : Stream Nat)
          (p : SEq (delay (a , as)) t) → (fst w ≡ a) × SEq (snd w) as

      Δ  = t a as p   -- reorder to bring with-relevant (= needed) vars first
      π  = a as t p → Δ
      qs = (a     , as) t p ~force
      ps = (suc n , as) t p ~force
      ps' = (suc n) as t p

Resulting with-function clause is:

      f t (b , bs) (suc n) as t p

Note: stripWithClausePatterns factors `ps` through `qs`, thus

      ps = qs[ps']

where `[..]` is to be understood as substitution. The projection patterns have vanished from `ps'` (as they are already in `qs`).

withDisplayForm Source #

Arguments

:: QName | The name of parent function.
-> QName | The name of the `with`-function.
-> Telescope | `Δ₁` The arguments of the `with` function before the `with` expressions.
-> Telescope | `Δ₂` The arguments of the `with` function after the `with` expressions.
-> Nat | `n` The number of `with` expressions.
-> [NamedArg DeBruijnPattern] | `qs` The parent patterns.
-> Permutation | `perm` Permutation to split into needed and unneeded vars.
-> Permutation | `lhsPerm` Permutation reordering the variables in parent patterns.
-> TCM DisplayForm |

Construct the display form for a with function. It will display applications of the with function as applications to the original function. For instance,

        aux a b c

as

        f (suc a) (suc b) | c

patsToElims :: [NamedArg DeBruijnPattern] -> [Elim' DisplayTerm] Source #