Ich war völlig erstaunt, wie Coqs Parser implementiert ist. z.B.
Es ist so verrückt, dass der Parser in Ordnung scheint, ein Lexem zu nehmen, indem er einen Notationsbefehl gibt, und der nachfolgende Parser ist in der Lage, jeden Ausdruck so zu analysieren, wie er ist. Was es bedeutet, ist, dass die Grammatik kontextsensitiv sein muss. Aber das ist so flexibel, dass es absolut mein Verständnis übersteigt.
Irgendwelche Hinweise darauf, wie diese Art von Parser theoretisch machbar ist? Wie sollte es funktionieren? Alle Materialien oder Kenntnisse würden funktionieren. Ich versuche nur, über diese Art von Parser im Allgemeinen zu lernen. Danke.
Bitte bitte mich nicht, Coqs Quelle selbst zu lesen. Ich möchte die Idee im Allgemeinen, aber nicht eine spezifische Implementierung überprüfen.
Tatsächlich ist dieses Notationssystem sehr mächtig und wahrscheinlich einer der Gründe für den Erfolg von Coq. In der Praxis ist dies eine Quelle für viele Komplikationen im Quellcode. Ich denke, @ejgallego sollte Ihnen mehr darüber erzählen können, aber hier ist eine kurze Erklärung:
Zu Beginn wurden Coqs Dokumente Satz für Satz (Sätze sind durch Punkte getrennt) von coqtop ausgewertet. Einige Befehle können Notationen definieren, und diese ändern die Parserregeln, wenn sie ausgewertet werden. Daher werden spätere Sätze mit einem etwas anderen Parser ausgewertet.
Seit Version 8.5 gibt es auch einen Mechanismus (das STM), um ein Dokument vollständig auszuwerten (viele Sätze parallel), aber es gibt einen speziellen Mechanismus für die Handhabung dieser Notationsbefehle (im Grunde müssen Sie auf diese warten) ausgewertet werden, bevor Sie den Rest des Dokuments weiter analysieren und auswerten können.)
Im Gegensatz zu einer normalen Programmiersprache, in der der Compiler ein Dokument übernimmt, lege es durch den Lexer, dann den Parser (parse das gesamte Dokument auf einmal) und habe dann eine AST, um dem Typer oder zu geben In anderen späteren Phasen wird in Coq jeder Befehl separat analysiert und ausgewertet. Daher muss man nicht auf komplexe kontextabhängige Grammatiken zurückgreifen ...
Ich werde meine zwei Cent fallen lassen, um @ Zimmi48s ausgezeichnete Antwort zu ergänzen.
Coq verfügt in der Tat über einen erweiterbaren Parser, wobei TTBOMK hauptsächlich von Hugo Herbelin entwickelt wurde, der auf dem erweiterbaren Analysesystem CAMLP4 / CAMLP5 von Daniel de Rauglaudre aufbaut. Beide sind die kanonischen Quellen für Informationen über den Parser, ich werde versuchen, zusammenzufassen, was ich weiß, aber beachte in der Tat, dass meine Erfahrung mit dem System kurz ist.
Das CAMLPX-System unterstützt grundsätzlich jede LL1-Grammatik. Coq stellt dem Benutzer die Gesamtheit der Grammatikregeln zur Verfügung, so dass der Benutzer sie neu definieren kann. Dies ist der Basismechanismus, auf dem erweiterbare Grammatiken aufgebaut sind. Notationen werden im Metasyntax -Modul in Parsing-Regeln kompiliert und in einem späteren Beitrag ausgefaltet. Verarbeitungsphase. Und das ist wirklich AFAICT.
Das System selbst hat sich in der gesamten 8.x-Reihe nicht sehr verändert, @ Zimmi48s Kommentare beziehen sich eher auf die interne Verarbeitung von Befehlen nach Parsing. Ich habe kürzlich gelernt, dass Coq v7 ein noch leistungsfähigeres System zur Modifikation des Parsers hat.
In Worten von Hugo Herbelin "ist die Kunst des erweiterbaren Parsens ein delikates" und tatsächlich ist es das, aber Coq hat eine ziemlich gute Umsetzung davon erreicht.