[Agda] tweaking evaluation

[Peter Selinger]

This may be a newbie question. I have a program whose type-checking
requires the evaluation of some moderately large terms. The fact that
Agda uses normal order (or call-by-name) evaluation makes the
evaluations very slow. Is there a way to force certain terms to be
evaluated to normal form?

Here's a toy example (adapted from
http://stackoverflow.com/questions/21210569/is-the-evaluation-strategy-of-agda-specified-anywhere):

  open import Data.Product
  open import Relation.Binary.PropositionalEquality

  -- using a unary implementation of ℕ for illustration purposes.
  data ℕ : Set where
    zero : ℕ
    suc  : ℕ → ℕ

  {-# BUILTIN NATURAL ℕ #-}

  infixl 4 _+_
  infixl 5 _*_
  infixr 6 _^_

  _+_ : (m n : ℕ) → ℕ
  zero  + n = n
  suc m + n = suc (m + n)

  _*_ : (m n : ℕ) → ℕ
  zero  * n = zero
  suc m * n = n + m * n

  _^_ : (m n : ℕ) → ℕ
  m ^ zero = suc zero
  m ^ suc n = m * m ^ n

  -- naive diagonal function
  Δ : {A : Set} -> A -> A × A
  Δ x = (x , x)

  -- checking takes about 11 seconds
  slow : 2 ^ 13 * 0 ≡ 0
  slow = refl

  -- takes about 22 seconds
  slower : Δ (2 ^ 13 * 0) ≡ Δ 0
  slower = refl

Naturally, "slower" takes about twice as long to type-check than
"slow". 

It is stated here that using "with" on an expression causes the
expression to be evaluated to normal form:
https://lists.chalmers.se/pipermail/agda/2012/004443.html

Therefore, I figured the following could be a way to speed up the
diagonal function:

  -- better diagonal function?
  Δ' : {A : Set} -> A -> A × A
  Δ' x with x
  Δ' x | y = (y , y)

However, this doesn't work at all, as the result still takes 22
seconds to evaluate:
  
  -- takes about 22 seconds
  slower' : Δ' (2 ^ 13 * 0) ≡ Δ' 0
  slower' = refl

Is there a way to force some term to be evaluated strictly?

Thanks, -- Peter