B. SPECIFICATION LSP & REPL🔗

Le protocole LSP et le REPL ne sont pas deux outils ajoutés à K7PL après coup : ce sont le système déjà construit, rendu visible en temps réel plutôt qu'à la seule compilation. Cette annexe en esquisse une première spécification, entièrement dérivée des mécanismes établis.

Le serveur LSP expose quatre services, chacun une lecture directe d'un mécanisme des chapitres précédents. La complétion propose, pour un trou _ laissé dans le texte, les termes que le narrowing (chapitre 3, §3.3) accepte à cette position — le trou étant le point le moins précis du treillis \sqsubseteq pour le type attendu, la complétion n'est que la recherche, dans ce même treillis, des raffinements qui satisfont la contrainte. Sur un raffinement laissé en trou, le compilateur ne remplace jamais silencieusement le trou : il calcule les bornes nécessaires à la sûreté mémoire et retourne un diagnostic proposant (and (>= 0) (< length)), que le développeur doit recopier lui-même dans le texte source, pour que la contrainte reste auditable plutôt qu'implicite. Le diagnostic accompagne un rejet de la tranche minimale de dérivation (chapitre 3, §3.3) qui l'explique, plutôt que du seul message d'erreur.

La visualisation traduit une machine à états composable (chapitre 4, §4.5) en diagramme, puisque sa description est déjà celle d'un graphe. Le refactoring, enfin, n'autorise un remplacement de fragment de programme que lorsque la relation de substituabilité généralisée du chapitre 3 (§3.3) — préconditions affaiblies, postconditions renforcées — est vérifiée entre l'ancien et le nouveau fragment, jamais sur la seule ressemblance syntaxique.

{deftype safe-index Int64
  "Index sécurisé."
  :where _}

Figure 13 :

Les quatre services du LSP, chacun ancré dans un mécanisme déjà construit

Les quatre services et le mécanisme du manuscrit dont chacun n'est qu'une lecture.

Le REPL est le mode d'évaluation interactif de K7PL. Chaque expression y est compilée par le mode JIT (chapitre 6, §6.1), seul contexte où ce mode est autorisé. Son résultat s'affiche sous forme tabulaire plutôt que comme une valeur imprimée, conformément à l'ontologie du chapitre 2 selon laquelle un tableau n'est jamais qu'une fonction depuis un type fini. Le prompt suit le format utilisateur@domaine[cible][branche]: λ expr, où cible et branche situent la session dans la topologie d'acteurs (chapitre 4, §4.5) sur laquelle elle opère.

Le Replay Debugger prolonge ce même REPL vers le passé d'une exécution plutôt que vers son futur. Il charge le journal Cap'n Proto d'un acteur (chapitre 4, §4.5) et rejoue la séquence de messages à travers ses gestionnaires purs, la pureté garantissant que ce rejeu reproduit fidèlement l'original. Les commandes play, pause, stop, next, previous et les deux défilements rapides — avant, arrière — parcourent cette séquence exactement comme un lecteur multimédia parcourt un flux enregistré, sans qu'aucune instrumentation n'ait dû être ajoutée après coup au programme observé.