The Coq mailing list

[Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>]

On Fri, Mar 08, 2013 at 09:51:55AM +0100, fengsheng wrote:
> Hello everyone:
>      I'm studying the [Software Foundations] written by Benjamin C. Pierce.
> I was confused when I was reading the chapter [ImpParser,Lexing and parsing 
> in
> coq].
> Eval compute in parse "
>     x := 3;
>     IF x <= 1
>        THEN y := 3
>        ELSE z := 4
>     END".
> (*
> ====>
>     SomeE
>          (Id 0 ::= ANum 2;
>           IFB BLe (AId (Id 0)) (ANum 1) THEN Id 2 ::= ANum 3
>           ELSE Id 3 ::= ANum 4 FI, [])
> *)
> The Id 2 is followed by the Id 0.But there is no other variable between
> them.Where is the Id 1?Later I found every time the expression was used, the
> symtable would be called and the index plus one.Is it the reason about the
> problem? How to solve this bug?

Yes, the reason is the (rather hacky) way that build_symtable is written.

Basically, it takes the list of tokens, like
  ["x", ":=", "3", ";", "IF", "x", "<=", "1", "THEN", "y", ":=", "3",
   "ELSE", "z", ":=", "4", "END"]
filters out nonalphabetic ones:
  ["x", "x", "y", "z"]
numbers each element of the list
  ["x", "x", "y", "z"]
   0    1    2    3
and maps each string to the number of the first place it occurs in the list.
(so x is mapped to 0 and y is mapped to 2).

My reason for writing it this way was that it's arbitrary exactly which number
gets used for a given symbol, and this way the function implementation is
short...

Also, this implementation is very inefficient, since it will search through 
the
tokenized program from the beginning each time it looks up a variable. A more
realistic implementation would use an efficient datastructure, like the FMap
from Coq's standard library, and that would take care of the "duplicate 
number"
issue also.

Vilhelm Sjoberg