dict type the t_symbol(function is used to match both symbols (identifiersand keywords if the key given to dict get(isn' in the dictionary the default value (in this case "symbol"is returnedotherwise the key' corresponding token name is returned notice also that unlike in previous lexerswe don' change the ply lex lextoken' value attributebut we do change its type attribute to be either "symbolor the appropriate keyword token name all the other tokens are matched by simple regexes--all of which happen to match one or two literal characters in all the previous ply examples the lexer alone has been sufficient for our parsing needs but for the first-order logic bnf we need to use ply' parser as well as its lexer to do the parsing setting up ply parser is quite straightforward--and unlike pyparsing we don' have to reformulate our bnf to match certain patterns but can use the bnf directly for each bnf definitionwe create function with name prefixed by p_ and whose docstring contains the bnf statement the function is designed to process as the parser parsesit calls the function with the matching bnf statement and passes it single argument of type ply yacc yaccproduction the argument is given the name (following the ply examplesnaming conventionswhen bnf statement includes alternativesit is possible to create just one function to handle them allalthough in most cases it is clearer to create one function per alternative or set of structurally similar alternatives we will look at each of the parser functionsstarting with the one for handling quantifiers def p_formula_quantifier( )"""formula forall symbol colon formula exists symbol colon formula"" [ [ [ ] [ ] [ ]the docstring contains the bnf statement that the function corresponds tobut using rather than ::to mean is defined by note that the words in the bnf are either tokens that the lexer matches or nonterminals ( formulathat the bnf matches one ply quirk to be aware of is that if we have alternatives as we have hereeach one must be on separate line in the docstring sequence types the bnf' definition of the formula nonterminal involves many alternativesbut here we have used just the parts that are concerned with quantifiers--we will handle the other alternatives in other functions the argument of type ply yacc yaccproduction supports python' sequence apiwith each item corresponding to an item in the bnf so in all casesp[ corresponds to the nonterminal that is being defined (in this case formula)with the other items matching the parts on the right-hand side herep[ matches one of the symbols "existsor "forall" [ matches the quantified identifier (typicallyx or ) [ matches the colon token ( literal which we ignore)and [ matches the formula that is quantified this is recursive definitionso the [ item