[Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker

[Sergei Meshveliani]

On Thu, 2013-09-19 at 14:34 +0200, Nils Anders Danielsson wrote:
> On 2013-09-17 15:09, Sergei Meshveliani wrote:
> > But I need a general understanding:  when to use `with' and when to
> > use `case'.
> 
> When you use with Agda creates a helper function. As part of the
> creation of this function Agda performs the following steps:
> 
> * Normalise the context and goal type.
> 
> * For each term that you abstract over: Normalise the term, find all
>    syntactic occurrences of the normal form in the (normalised) context
>    and goal type, and replace these occurrences by a fresh variable.
> 
> These steps can be expensive.


What does this mean "to abstract over a term" ?
Is this to convert a term  t   to   λ (x → t)  for a variable  x  in t ?

Consider the example:

  f : ℕ → ℕ
  f x = <a complex implementation>

  h = <another complex implementation>

  g x  with  f x ≤? 2
  ... | yes p =  h p
  ... | no _  =  0

  g' x = case  f x ≤? 2  of \ { (yes p) → h p
    	       	              ; (no _)  → 0   }

1) Here  "with  f x ≤? 2"  is said to produce some abstraction over the
term  (f x ≤? 2).
Right?  How does it look this abstraction?

2) Do you say that if  f  and  h  have a large code, then type-checking
of  g  will often cost much more than type-checking  g'  ?

3) The checker makes something with the occurrences of  f  and  h  in
the body of  g  and  g'.
Do you say that these occurrences are processed in very different way in
g  and in  g' ?

Thanks to people for explanation,

------
Sergei