J'ai été entièrement étonné par la façon dont l'analyseur de Coq est implémenté. par exemple.

https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html#lab347

C'est tellement fou que l'analyseur semble correct pour prendre n'importe quel lexème en donnant une commande de notation et l'analyseur ultérieur est capable d'analyser n'importe quelle expression telle quelle. Donc, ce que cela signifie, c'est que la grammaire doit être sensible au contexte. Mais c'est si flexible que cela dépasse absolument ma compréhension.

Des conseils sur la façon dont ce type d'analyseur est théoriquement faisable? Comment cela devrait-il fonctionner? Tout matériel ou connaissance fonctionnerait. J'essaie juste d'en savoir plus sur ce type d'analyseur en général. Merci.

Ne me demandez pas de lire moi-même la source de Coq. Je veux vérifier l'idée en général mais pas une mise en œuvre spécifique.

10
Jason Hu 3 avril 2017 à 15:26

2 réponses

Meilleure réponse

En effet, ce système de notation est très puissant et c'était probablement l'une des raisons du succès de Coq. En pratique, c'est une source de beaucoup de complications dans le code source. Je pense que @ejgallego devrait pouvoir vous en dire plus mais voici une explication rapide:

  • Au début, les documents de Coq étaient évalués phrase par phrase (les phrases sont séparées par des points) par coqtop. Certaines commandes peuvent définir des notations et celles-ci modifient les règles d'analyse lorsqu'elles sont évaluées. Ainsi, les phrases ultérieures sont évaluées avec un analyseur légèrement différent.

  • Depuis la version 8.5, il existe également un mécanisme (le STM) pour évaluer complètement un document (de nombreuses phrases en parallèle) mais il existe un mécanisme spécial pour gérer ces commandes de notation (en gros, il faut attendre qu'elles soient évaluées avant de pouvoir continuer analyse et évaluation du reste du document).

Ainsi, contrairement à un langage de programmation normal, où le compilateur prendra un document, le passera à travers le lexer, puis l'analyseur (analyser le document complet en une seule fois), et ensuite aura un AST à donner au typeur ou à d'autres étapes ultérieures , dans Coq, chaque commande est analysée et évaluée séparément. Ainsi, il n'est pas nécessaire de recourir à des grammaires contextuelles complexes ...

12
Zimm i48 3 avril 2017 à 12:54

Je vais laisser tomber mes deux cents pour compléter l'excellente réponse de @ Zimmi48.

Coq dispose en effet d'un analyseur extensible, dont TTBOMK est principalement l'œuvre d'Hugo Herbelin, construit sur le système d'analyse extensible CAMLP4 / CAMLP5 de Daniel de Rauglaudre. Les deux sont les sources canoniques d'informations sur l'analyseur, je vais essayer de résumer ce que je sais mais notons en effet que mon expérience avec le système est courte.

Le système CAMLPX prend essentiellement en charge toute grammaire LL1. Coq expose à l'utilisateur l'ensemble des règles de grammaire, permettant à l'utilisateur de les redéfinir. C'est le mécanisme de base sur lequel sont construites les grammaires extensibles. Les notations sont compilées en règles d'analyse dans le module Metasyntax, et déroulé dans une dernière phase de post-traitement. Et c'est vraiment AFAICT.

Le système lui-même n'a pas beaucoup changé dans toute la série 8.x, les commentaires de @ Zimmi48 sont plus liés au traitement interne des commandes après l'analyse. J'ai récemment appris que Coq v7 avait un système encore plus puissant pour modifier l'analyseur.

Pour reprendre les mots d'Hugo Herbelin, «l'art de l'analyse extensible est délicat» et c'est effectivement le cas, mais Coq en a réalisé une assez bonne implémentation.

10
Anton Trunov 19 mars 2018 à 21:28