Déclarations

En-tête de module et import

space outils::calcul;
use core::types::option::{Option, option_some};
use outils::conversion as conversion;

space accepte un chemin. use peut importer un module ou un chemin, définir un alias avec as, importer un groupe de noms entre accolades ou demander un glob avec *. Les noms qualifiés utilisent ::. La résolution concrète dépend de la racine du projet et des chemins de modules configurés.

Valeurs et types nommés

export const REPONSE: i64 = 42;
static COMPTEUR: i64 = 0;
type Identifiant = u64;
opaque Jeton;

const et static déclarent des valeurs de module initialisées par une expression. type donne un alias à un type ; opaque annonce un type dont la représentation n’est pas exposée. Les règles détaillées de visibilité et de mutabilité se vérifient dans les étapes sémantiques du compilateur.

Formes et choix

form Point {
    x: i64,
    y: i64,
}

pick Etat {
    Inactif,
    Pret,
    Erreur(i64),
}

Une form contient des champs nommés. Un pick décrit des variantes, et la grammaire permet de placer des types entre parenthèses après une variante. Dans le langage courant, on emploie souvent les formes comme valeurs composées et les choix pour représenter des états exclusifs.

Procédures

export proc ajouter_un(valeur: i64) -> i64
    requires valeur < 100;
    ensures result == valeur + 1;
{
    return valeur + 1;
}

Une procédure peut déclarer des paramètres typés, un type de retour, des paramètres génériques, une clause where et plusieurs contrats requires/ensures. Le corps est un bloc. Les paramètres n’ont pas de valeur par défaut dans la grammaire actuelle.

Traits et implémentations

Un trait contient des déclarations liées à un contrat de comportement. Un impl regroupe les déclarations d’implémentation pour un type et éventuellement un trait. Les méthodes peuvent employer &self ou &mut self ; la bibliothèque core en fournit des signatures. La liaison effective des implémentations de traits et le dispatch générique ne sont pas complets dans le compilateur d’après la documentation de core.

export trait Display {
    proc fmt(&self, formatter: &mut Formatter) -> bool;
}

Frontières, macros et tests

• extern "bibliotheque" proc nom(...); déclare une procédure dont le corps est fourni à l’extérieur.
• intrinsic nom(...); réserve l’implémentation au compilateur ou au runtime.
• macro nom(...) { ... } déclare une macro selon la grammaire.
• test "nom" { ... } déclare un bloc de test.

Les modificateurs prévus avant une déclaration comprennent pub, export, async, unsafe et comptime. La syntaxe reconnue ne garantit pas que chaque modificateur soit pris en charge de bout en bout.

Vérification par construction

Construction	EBNF	Analyseur	Compilation constatée
space / use	Décrites.	Acceptées par les tests d’import/parité.	Import et appel qualifié compilés et exécutés dans llvm_imports_runtime.vit.
export	Décrit, y compris les listes et glob.	Exercé dans les fixtures d’import/export.	Des imports/exports de modules sont exécutés ; l’alias d’export emprunte le frontend de compatibilité. Chaque forme de réexport n’est pas validée.
const / static	Décrites.	Une constante importée est exercée ; aucune fixture ciblée relevée pour static.	Constantes utilisées par les tests d’import ; génération/exécution de static non prouvée ici.
type / opaque	Décrites.	Pas de fixture ciblée retenue pour un alias de type ou une déclaration opaque.	Non établi par les tests de compilation et d’exécution audités.
form sans paramètre générique	Décrite.	Acceptée par fixtures grammaire, parité et frontend natif.	Champs scalaires, imbriqués et tableaux : IR natif, C17 et exécution vérifiés.
form<T>	Décrite.	Le cas test atteint la génération C.	Rejetée au backend avec VITTE_BACKEND_E_CODEGEN dans le test ciblé.
pick et variantes à charge utile	Décrites.	Acceptées par fixtures grammaire, parité et frontend natif.	Variantes simples et charges utiles compilées et exécutées avec le backend natif.
proc	Décrite, avec paramètres et retour.	Acceptée dans les cas de parité, séma et frontend natif.	Compilée et exécutée dans plusieurs fixtures.
requires / ensures	Décrites.	Vérifiées par test sémantique.	contracts_ok.vit passe par compatibilité, compile et s’exécute.
trait / impl / génériques / where	Décrits.	Le README du parseur bootstrap les documente ; pas de fixture runtime ciblée dans cet audit.	Compilation de bout en bout non prouvée ; core signale des limites de liaison.
extern / intrinsic / macro	Décrites.	Non vérifiées par une fixture ciblée retenue.	Non prouvées en génération et exécution.
test	Décrite.	Une déclaration test est acceptée par le test d’émetteur de compatibilité.	L’émetteur C est testé ; la déclaration n’est pas exécutée comme un test Vitte.
Attributs et modificateurs	Les modificateurs cités dans l’EBNF sont décrits ; les attributs en sont absents.	La parité accepte un attribut de procédure ; les modificateurs ne sont pas tous couverts.	Support du backend non établi pour l’ensemble.

Voir la matrice complète avec les fichiers de preuve et les commandes exécutées. Source syntaxique : grammaire EBNF.