Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.With

Synopsis

splitTelForWith :: Telescope -> Type -> [Arg (Term, EqualityView)] -> (Telescope, Telescope, Permutation, Type, [Arg (Term, EqualityView)])
withFunctionType :: Telescope -> [Arg (Term, EqualityView)] -> Telescope -> Type -> [(Int, (Term, Term))] -> TCM (Type, Nat)
countWithArgs :: [EqualityView] -> Nat
withArguments :: [Arg (Term, EqualityView)] -> TCM [Arg 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.
-> [Arg (Term, EqualityView)]	`Δ ⊢ vs : as` with arguments and their types. Output:
-> (Telescope, Telescope, Permutation, Type, [Arg (Term, EqualityView)])	(`Δ₁`,`Δ₂`,`π`,`t'`,`vtys'`) 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 `π` `Δ₁ ⊢ vtys'` with-arguments and their types under `π`.

Split pattern variables according to with-expressions.

withFunctionType Source #

Arguments

:: Telescope	`Δ₁` context for types of with types.
-> [Arg (Term, EqualityView)]	`Δ₁,Δ₂ ⊢ vs : raise Δ₂ as` with and rewrite-expressions and their type.
-> Telescope	`Δ₁ ⊢ Δ₂` context extension to type with-expressions.
-> Type	`Δ₁,Δ₂ ⊢ b` type of rhs.
-> [(Int, (Term, Term))]	@Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b boundary.
-> 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 :: [Arg (Term, EqualityView)] -> TCM [Arg Term] Source #

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

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 #