Documentation

Split pattern variables according to with-expressions.

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

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

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

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

stripWithClausePatterns parent 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 >

Note:Def" class="lincodeTypeChee> (as tl#t:Phase">Phase-(d colspan="2"> jse">ypeChhhhhhhhhd by lhs801; b & -> b empty with clhhhhd-Base.hlan="2">Bool)ss="link">Source (phlan="2">tbly ofase">Phase-lass="caption">M"Agda-Syneneeded>

Sourc">Pr splitt>ypeChhhhethods">e="cies/basd>Sourceclass="sr/baseihee> (phlan /a> a) stitu#t:UnquoteM">Unquocrete-Namess"Agda-TypeCheckince t sd>M">Unqutd can cltors.htm>