Safe Haskell  None 

Language  Haskell2010 
Synopsis
 splitTelForWith :: Telescope > Type > [WithHiding (Term, EqualityView)] > (Telescope, Telescope, Permutation, Type, [WithHiding (Term, EqualityView)])
 withFunctionType :: Telescope > [WithHiding (Term, EqualityView)] > Telescope > Type > TCM (Type, Nat)
 countWithArgs :: [EqualityView] > Nat
 withArguments :: [WithHiding (Term, EqualityView)] > [WithHiding 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
:: Telescope 

> Type 

> [WithHiding (Term, EqualityView)] 

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

Split pattern variables according to withexpressions.
:: Telescope 

> [WithHiding (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.
countWithArgs :: [EqualityView] > Nat Source #
withArguments :: [WithHiding (Term, EqualityView)] > [WithHiding 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).
:: [Name]  Names of the module parameters of the parent function. 
> QName  Name of the parent function. 
> QName  Name of the withfunction. 
> 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]  Withclauses. 
> TCM [SpineClause]  Withclauses flattened wrt. parent patterns. 
Compute the clauses for the withfunction given the original patterns.
stripWithClausePatterns Source #
:: [Name] 

> QName 

> QName 

> Type 

> Telescope 

> [NamedArg DeBruijnPattern] 

> Nat 

> Permutation 

> [NamedArg Pattern] 

> TCM ([ProblemEq], [NamedArg Pattern]) 

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 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 DeBruijnPattern] 

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