[Agda] Computation and patterns in called functions

[Francesco Mazzoli]

At Mon, 28 Jan 2013 17:19:22 +0100,
Nils Anders Danielsson wrote:
> Should
> 
>    _≟_ : (x y : Bool) → Dec (x ≡ y)
>    true  ≟ true  = yes refl
>    false ≟ false = yes refl
>    _     ≟ _     = ?
> 
> be expanded into
> 
>    _≟_ : (x y : Bool) → Dec (x ≡ y)
>    true  ≟ true  = yes refl
>    false ≟ false = yes refl
>    true  ≟ false = ?
>    false ≟ true  = ?
> 
> ?

Sorry, I usually call those ‘holes’.

That is indeed a tricky situation.  Off the top of my head a possibility would
be to reduce the terms dependent on the to-be-expanded things as long as the
reduced terms are def. equal across all the branches of the expanded
constructors, so that the matched things can be re-abstracted.  So in that
context you’ll still have ‘.b₁’ and ‘.b₂’, but also a ‘no p’.  In my example,
‘optExp’ would reduce to ‘plus (optExp e₁) (optExp e₂)’, but not more, because
then the reduced terms would change depending on the value of the ‘e’s.

Francesco