Agda.TypeChecking.With

Documentation

splitTelForWith

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

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

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

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

buildWithFunction

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

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

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]