Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.With

Synopsis

Documentation

withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type Source

buildWithFunction Source

Arguments

:: QName	Name of the with-function.
-> Type	Types of the parent function.
-> [NamedArg Pattern]	Parent patterns.
-> 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

:: QName	f
-> Type	t
-> [NamedArg Pattern]	qs
-> Permutation	π
-> [NamedArg Pattern]	ps
-> TCM [NamedArg Pattern]	ps'

stripWithClausePatterns f t qs π ps = ps'

Δ - context bound by lhs of original function (not an argument)

f - name of with-function

t - type of the original function

qs - internal patterns for original function

π - permutation taking vars(qs) to support(Δ)

ps - patterns in with clause (eliminating type t)

ps' - patterns for with function (presumably of type Δ)

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 exprs.
-> Telescope	The arguments of the with function after the with exprs.
-> Nat	The number of with expressions.
-> [NamedArg Pattern]	The parent patterns.
-> Permutation	Permutation to split into needed and unneeded vars.
-> Permutation	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

n is the number of with arguments.

patsToElims :: Permutation -> [NamedArg Pattern] -> [Elim' DisplayTerm] Source