The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri,  8 Mar 2013 09:51:55 +0100 (CET),
"fengsheng" 
<fsheng1990 AT 163.com>
 a écrit :

> 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?
> 
> Here is a link of my problem.
> http://www.cis.upenn.edu/~bcpierce/sf/ImpParser.html

Have you modified the sources of SF you downloaded (for instance to
test some examples/try to do some exercise). I do not remember if SF
has "holes" in it, you are requested to fill in. If no, I think a good
practice is to not touch the files and do the exercices in other files
(requiring the required files of course).

Taking a look at your link, I think that the following error may have
occured:

→ you didn't carefully copy/paste (the first ":= 3" turned into a "::=
ANum 2" while the second one turned into a "::= ANum 3", and clearly
that should have more annoyed me than your identifier indexation)
→ the tokenization function is wrong, try to change (in a separate file
requiring all the needed stuff, so that you don't risk to alter the
original files)

Definition parse (str : string) : optionE (com * list token) :=
  let tokens := tokenize str in
  parseSequencedCommand bignumber (build_symtable tokens 0) tokens.

with

Definition parse (str : string)
: optionE (list token * (com * list token)) :=
  let tokens := tokenize str in
  (tokens,
   parseSequencedCommand bignumber (build_symtable tokens 0) tokens).
To check that you have no lower case string between x and y

→ isLowerAlpha is wrong, allowing ":=", "3" or ";" to be considered as
lower case and thus as an ident (not likely to happen if only variables
can be identifiers as it would have lead to a syntax error in the
program to be parsed…)

→ The Coq nat notations have been modified so "S O" is printed "2" and
so on (but it would be quite weird, and I am not sure it is possible
with the Notation command…)