Skip to Content.
Sympa Menu

coq-club - Re:Re: [Coq-Club] ImpParser,Lexing and parsing in coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re:Re: [Coq-Club] ImpParser,Lexing and parsing in coq


Chronological Thread 
  • From: 盛枫 <13761090639 AT 163.com>
  • To: Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re:Re: [Coq-Club] ImpParser,Lexing and parsing in coq
  • Date: Sat, 9 Mar 2013 11:34:01 +0800 (CST)

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


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



Archive powered by MHonArc 2.6.18.

Top of Page