Re: Internal Error:2503

[Andrzej Trybulec <trybulec@math.uw.bialystok.pl>]

On Fri, 13 Mar 1998, chen-jc wrote:

> casees. For example,the following definition causes "Internal
> Error:2503".
> -------------------------
>  definition
>  let f be FinSeq-Location;
>  func bubble-sort f -> Macro-Instruction equals
> :def4:  ::def4
>    a1:=len f ';'
>        (a3:= intloc 0) ';'
>        Times(a1,
>           a2 :=len f ';'
>           Times(a2,
>                if<0(a3,a2,
>                   a4:=a2 ';'
>                   SubFrom(a4,intloc 0) ';'
>                  (a5:=(f,a4))  ';'
>                   (a6:=(f,a2)) ';'
>                   if<0(a6,a5,swap(f,a4,a2),SCM+FSA-Stop),
>                   SCM+FSA-Stop)
> ::>                          *2503
>           )
>        );

It is a bug, a regular error should be reported.

The error is caused by free variables occurring in the term after
"equals" (a1,...,a6) that is not allowed.

When you use "means it =" the free variables are bound by default
by a universal quanrifier on the beginning of the definiens. 
So you get:

 for a1,a2,a3,a4,a5,a6 holds it = ....

it is grammaticaly correct, but it is meaningless. You cannot prove
the "existence" condition.

I guess you should use consecutive integer locations (intloc 1, ...).
But please remember that the "swap" macroinstruction needs an auxiliary 
variable and takes the first available. So you should use
 intloc 2, .... , inrloc 7 instead of a1 , ..., a6

Andrzej Trybulec