At Mon, 28 Jan 2013 15:40:34 +0000,
Francesco Mazzoli wrote:
>
> Hi Nils,
>
> Thanks for the answer.
>
> At Mon, 28 Jan 2013 16:24:16 +0100,
> Nils Anders Danielsson wrote:
> > There are several solutions:
> >
> > * One could perhaps change Agda so that overlapping patterns are
> > replaced with non-overlapping ones before the right-hand sides are
> > type-checked. (I believe that Coq does this.) For instance,
> >
> > _≟_ : (x y : Bool) → Dec (x ≡ y)
> > true ≟ true = yes refl
> > false ≟ false = yes refl
> > _ ≟ _ = no (λ ())
> >
> > could be expanded into the following, type-correct code:
> >
> > _≟_ : (x y : Bool) → Dec (x ≡ y)
> > true ≟ true = yes refl
> > false ≟ false = yes refl
> > true ≟ false = no (λ ())
> > false ≟ true = no (λ ())
>
> That would be great and would also solve the problem that you have to explicitly
> pattern match to use absurd patterns. See
> <https://personal.cis.strath.ac.uk/conor.mcbride/pub/Hmm/Hier.agda> for an
> extreme instance of this problem.
>
> > However, it's not quite clear to me what would happen if a duplicated
> > right-hand side contained a goal.
>
> I don’t get what you mean here. In my case the short version of optExp-correct:
>
> optExp-correct : ∀ {vs} e → evalExp vs e ≡ evalExp vs (optExp e)
> optExp-correct (plus (const 0) e) = optExp-correct e
> optExp-correct {vs} (plus e₁ e₂) =
> cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
> optExp-correct e = refl
>
> Would get expanded to
>
> optExp-correct : ∀ {vs} e → evalExp vs e ≡ evalExp vs (optExp e)
> optExp-correct (plus (const 0) e) = optExp-correct e
> optExp-correct {vs} (plus e₁@(const (suc _)) e₂) =
> cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
> optExp-correct {vs} (plus e₁@(var _) e₂) =
> cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
> optExp-correct {vs} (plus e₁@(plus _ _) e₂) =
> cong₂ _+_ (optExp-correct {vs} e₁) (optExp-correct e₂)
> optExp-correct (var _) = refl
> optExp-correct (const _) = refl
>
> Where I’m using haskell-style @, but in Agda you could simply desugar those to
> ‘let’s. Maybe I’m missing something...
I guess that one problem with that is that *always* expanding would slow down
things considerably when there is no need to do so. Maybe you could iteratively
try to expand until it typechecks or it can’t be expanded anymore...
Francesco