1
Download Le Coq` Art (V8)
Transcript
3.1. PREMIERS PAS 39 Coq permet d’ouvrir (c’est à dire rendre actives) simultanément plusieurs portées, chacune permettant d’interpréter un ensemble de notations. Ces portées sont placées sur une pile contenant au départ une portée minimale appelée core_scope définissant les notations de base de Gallina. Par ailleurs, dès que l’analyse syntaxique attend un type, une portée contenant les notations spécifiques aux types, et appelée type_scope est empilée automatiquement. La commande pour empiler une portée est “ Open Scope portée ”. Si deux portées définissant la même notation (par exemple l’opérateur ‘*’ de multiplication des nombres entiers et le produit cartésien) sont ouvertes, la portée la plus récemment ouverte masque la plus ancienne. Il peut être utile d’empiler une portée pour une seule expression. La syntaxe est alors “ exp%k ”, où k est un symbole associé à la portée à ouvrir (“delimiting key”). Cette facilité permet alors de disposer de plusieurs conventions d’écriture au sein d’une même commande, par exemple si une expression contient à la fois des nombres entiers et des nombres réels. La commande Locate permet de connaître à tout moment quelles interprétations sont associées à une notation donnée. Dans l’exemple suivant, nous demandons quelles sont les interprétations de l’opérateur infixe ‘*’ : Open Scope Z_scope. Locate ... "x * y" "x * y" "x * y" "x * y" "x * y" "_ * _". := := := := := prod x y : type_scope Ring_normalize.Pmult x y : ring_scope Pmult x y : positive_scope mult x y : nat_scope Zmult x y : Z_scope (default interpretation) Ce dialogue montre que, par défaut, la notation “x * y” doit s’interpréter comme l’application de la fonction Zmult (multiplication des nombres entiers), selon la portée Z_scope. La commande “ Print Scope ” permet de connaître toutes les notations définies par une portée, ainsi que la clef associée (champ “Delimiting key”) : Print Scope Z_scope. Scope Z_scope Delimiting key is Z Bound to class Z "- x" := Zopp x "x * y" := Zmult x y "x + y" := Zplus x y "x - y" := Zminus x y "x / y" := Zdiv x y "x < y" := Zlt x y
