The Coq mailing list

[盛枫 <13761090639 AT 163.com>]

But I'm still a little confused.Look at the following example:

Eval compute in parse "

    x := 3;

    IF (x <= 4 && not (x <= 0)) 

    THEN y := 0

    ELSE z := 1

    END".

(*

====>

  SomeE

         (Id 0 ::= ANum 3;

          IFB BAnd (BLe (AId (Id 0)) (ANum 4))

                (BNot (BLe (AId (Id 0)) (ANum 0))) THEN Id 4 ::= ANum 0

          ELSE Id 5 ::= ANum 1 FI, [])

     : optionE (com * list token)

*)

Basically, it takes the list of tokens, like

(["x", ":=", "3", ";", "IF", "(", "x", "<=", "4", "&&", "not", "(",
        "x", "<=", "0", ")", ")", "THEN", "y", ":=", "0", "ELSE", "y", ":=",
        "1", "END"])

filters out nonalphabetic ones:
  ["x", "x", "x", "y", "z"]

numbers each element of the list
  ["x", "x","x", "y", "z"]
   0    1    2    3    4

From the result, We see y is mapped to 4 and z is mapped to 5 which is different with above.

At 2013-03-09 02:32:55,"Vilhelm Sjöberg" <vilhelm AT cis.upenn.edu> wrote:

>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

来自网易手机号码邮箱了解更多