Radu:

1) Please add this to the manual as well

2) Can you remind us why we need the ground parser?  Can't that just be a special case of the rule parser?  Please explain that in the manual, too.

Grigore


________________________________
From: Radu Mereuta [notifications@github.com]
Sent: Tuesday, March 04, 2014 5:55 PM
To: kframework/k
Cc: Rosu, Grigore
Subject: Re: [k] Added many documentation comments; added a "nodoc" tag. (#264)


In include/builtins/k-reference.k:

> +but not 'A-'.
> +
> +\verb^Lexer{...}^ and \verb^-/-^ are the main way of specifying a lexical rule,
> +but if your expression is simple enough, you may write directly
> +\verb^Token{...}^. This will try to infer automatically the follow restriction
> +(if needed). Looking back at the rule for \#Id, it will be equivalent to:
> +
> +\begin{verbatim}
> +syntax #Id ::= Lexer{[a-zA-Z][a-zA-Z0-9]*}
> +syntax #Id -/- [a-zA-Z0-9]
> +\end{verbatim}
> +
> +Note that this works for simple expressions that have a repeated character set
> +at the end. If you want to specify something more complex, you will have to use
> +\verb^Lexer{...}^ and specify the follow restriction.
> +


There are 3 parser generated at kompile time:
1. program parser. It takes the exact syntax of the syntax module and generates parser from that
2. rule parser. It takes all the syntax declarations from all included modules and mix it with K (cells, meta-variables, lists, bags...etc), except for Ids
3. ground parser. Just like the above, except for meta-variables, which are replaced with Ids

Now, one can annotate a production with one of the following:
notInRules, notInGround, notInPrograms to specify to komple that you don't want those productions to be included in a specific parser. This is usually useful for avoiding ambiguities. Most common case is Ids with meta-variables.

Something else to add would be 'onlyLabel' which should be considered deprecated and has the same value as notInRules and notInGround, if used at the same time.

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/264/files#r10281700>.