Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 -> List1 SpineClause -> TCM (List1 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 |
|
-> [Arg (Term, EqualityView)] |
|
-> (Telescope, Telescope, Permutation, Type, [Arg (Term, EqualityView)]) | (
|
Split pattern variables according to with-expressions.
:: Telescope |
|
-> [Arg (Term, EqualityView)] |
|
-> Telescope |
|
-> Type |
|
-> [(Int, (Term, Term))] | @Δ₁,Δ₂ ⊢ [(i,(u0,u1))] : b boundary. |
-> TCM (Type, Nat) |
|
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 rewrite
s).
:: [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. |
-> List1 SpineClause | With-clauses. |
-> TCM (List1 SpineClause) | With-clauses flattened wrt. parent patterns. |
Compute the clauses for the with-function 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 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
).
:: 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 #