coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
来自网易手机号码邮箱了解更多
- [Coq-Club] ImpParser,Lexing and parsing in coq, fengsheng, 03/08/2013
- Re: [Coq-Club] ImpParser,Lexing and parsing in coq, AUGER Cédric, 03/08/2013
- Re: [Coq-Club] ImpParser,Lexing and parsing in coq, Vilhelm Sjöberg, 03/08/2013
- Re:Re: [Coq-Club] ImpParser,Lexing and parsing in coq, 盛枫, 03/09/2013
- Re: [Coq-Club] ImpParser,Lexing and parsing in coq, AUGER Cédric, 03/11/2013
- Re:Re: [Coq-Club] ImpParser,Lexing and parsing in coq, 盛枫, 03/09/2013
Archive powered by MHonArc 2.6.18.