Safe Haskell | None |
---|---|

Language | Haskell98 |

- withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type
- buildWithFunction :: QName -> Type -> [NamedArg Pattern] -> Permutation -> Nat -> Nat -> [SpineClause] -> TCM [SpineClause]
- stripWithClausePatterns :: 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

:: 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

:: 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). @

:: 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