[PVS-Help] Re: PVS Grammar in BNF

[Joseph Kiniry <kiniry@acm.org>]

Hi Nat,

On 19 May 2005, at 11:09, Nathaniel Ayewah wrote:

> Is there a plain Backus-Naur Form (not extended bnf) grammar for PVS?
> I've tried converting the extended grammar to bnf and compiling the
> grammar with a LALR parser and had many shift-reduce conflicts.
>
> For example, when parsing a TheoryDecl, how can the parser  
> differentiate
> between a list of Ids (as in TypeDecl) and a list of IdOps (as in
> VarDecl)?

The PVS grammar is the most context-sensitive grammar I have ever  
tried to parse.  I think that you will find that, even once you  
introduce quite a bit of type and expression context to your LALR  
parser, you will still see lots of conflicts.  Parsing PVS outside of  
PVS is not for the faint-hearted.  May I ask what your needs are wrt  
parsing PVS?

Joe
---
Joseph Kiniry
Department of Computer Science
University College Dublin
http://secure.ucd.ie/