Safe Haskell  None 

Language  Haskell98 
 splitTelForWith :: Telescope > Type > [EqualityView] > [Term] > (Telescope, Telescope, Permutation, Type, [EqualityView], [Term])
 withFunctionType :: Telescope > [Term] > [EqualityView] > Telescope > Type > TCM (Type, Nat)
 withArguments :: [Term] > [EqualityView] > [Term]
 buildWithFunction :: QName > QName > Type > [NamedArg Pattern] > Permutation > Nat > Nat > [SpineClause] > TCM [SpineClause]
 stripWithClausePatterns :: QName > QName > Type > [NamedArg Pattern] > Permutation > [NamedArg Pattern] > TCM [NamedArg Pattern]
 withDisplayForm :: QName > QName > Telescope > Telescope > Nat > [NamedArg Pattern] > Permutation > Permutation > TCM DisplayForm
 patsToElims :: Permutation > [NamedArg Pattern] > [Elim' DisplayTerm]
Documentation
:: Telescope 

> Type 

> [EqualityView] 

> [Term] 

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

Split pattern variables according to withexpressions.
:: Telescope 

> [Term] 

> [EqualityView] 

> Telescope 

> Type 

> TCM (Type, Nat) 

Abstract withexpressions vs
to generate type for withhelper function.
Each EqualityType
, coming from a rewrite
, will turn into 2 abstractions.
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).
:: QName  Name of the parent function. 
> QName  Name of the withfunction. 
> Type  Types of the parent function. 
> [NamedArg Pattern]  Parent patterns. 
> Permutation  Final permutation. 
> Nat  Number of needed vars. 
> Nat  Number of with expressions. 
> [SpineClause]  Withclauses. 
> TCM [SpineClause]  Withclauses flattened wrt. parent patterns. 
Compute the clauses for the withfunction given the original patterns.
stripWithClausePatterns Source #
:: QName  Name of the parent function. 
> QName  Name of withfunction. 
> Type 

> [NamedArg Pattern] 

> Permutation 

> [NamedArg Pattern] 

> TCM [NamedArg Pattern] 

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)
tosupport(Δ)
. 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 withrelevant (= 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 withfunction 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
).
:: QName  The name of parent function. 
> QName  The name of the 
> Telescope 

> Telescope 

> Nat 

> [NamedArg Pattern] 

> Permutation 

> Permutation 

> 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 :: Permutation > [NamedArg Pattern] > [Elim' DisplayTerm] Source #