Référence Fix

La liste de ce qui s'écrit dans un programme .fix aujourd'hui — forme exacte, exemple, et sortie. Document de consultation : prends la section qui t'intéresse.

Lancer Fix

fix [--test] [--strict-types] [--strict-subtype] [--help] [--version] <fichier.fix>
fix --tour

Fix charge le fichier, calcule son point fixe, puis ouvre une invite ?- :

$ fix examples/graph.fix
Fix v3.1.0 — 3 faits, 2 règles → fixpoint : 9 faits
?- path(a, X).
X = b
X = c
X = d
?- quit

(La bannière compte les faits et règles de ton programme — le catalogue de messages d'erreur préchargé au démarrage n'y figure pas, comme il est masqué de :listing.)

Le typage est nominal, fort et vérifié par défaut : un écart de type est une erreur de compilation — le programme ne se charge pas. Ce comportement n'est pas débrayable.

Sous-commande : fix enroll [--hub <url>] enrôle la machine auprès du hub de licence (gatx) quand la clé locale est absente. L'URL du hub vient de --hub, sinon de la variable d'environnement GATX_HUB. Sans licence valide, fix refuse de démarrer — le portillon s'exécute avant toute lecture de programme.

Un programme sans signature (sig) reste accepté tel quel : le Datalog nu tourne, en monde ouvert. Le contrôle strict ne porte que sur les prédicats typés. Le strict suit les déclarations, pas la proximité : un constructeur d'un type déclaré est vérifié en interne partout où il apparaît (ses champs doivent être conformes — fold(7) est refusé si fold attend un selects), mais sa présence n'étend pas le contrôle au prédicat non signé qui le porte. Seul un vrai conflit (deux valeurs de types incompatibles à la même position d'un prédicat non signé) est refusé.

Réponses possibles à une requête : une substitution par solution (X = b), true. (requête close vraie), ou false. (aucune solution).

Les commandes du REPL

Une entrée peut s'étaler sur plusieurs lignes : tant que la clause n'est pas terminée (.), l'invite passe à ... et Fix attend la suite.

:assert est typé comme le reste : une clause mal typée est refusée, la session reste dans son état précédent. Sur un programme avec négation ou agrégat non-idempotent, :assert/:retract repassent par un recalcul stratifié complet (voir la négation).

Tester un programme (--test)

Un test est un fait ou une règle test/2 ordinaire : test(Nom, Attente). fix --test fichier.fix calcule le point fixe, puis tranche chaque test par présence du fait dans la base dérivée.

majeur(alice).

test(alice_majeure, holds) :- majeur(alice).
test(alice_absente, fails) :- majeur(alice).   % échoue, exprès

$ fix --test exemple.fix
suite (principal)
  ✗ alice_absente : majeur(alice) a tenu (attendu : échec)
  ✓ alice_majeure
─────────────────────────────────
1 suite(s) · 1 passé(s) · 1 échoué(s)

Les tests sont groupés par suite = module — un test déclaré dans un module apparaît sous le nom du module, un test au niveau principal sous (principal). Deux attentes différentes sous le même nom → verdict ambigu. Code de sortie : 0 si aucun échec/cassé/ambigu (les skip et différés ne font pas échouer) — utilisable directement en CI.

Un test dont le corps référence un prédicat inconnu est signalé ⚠ CASSÉ au lieu d'échouer silencieusement.

Le cœur logique

Fait — un atome vrai.

edge(a, b).

Règle — la tête est vraie si le corps l'est.

path(X, Z) :- path(X, Y), path(Y, Z).

Requête — au REPL.

?- path(a, d).
true.

Commentaire — % jusqu'à la fin de ligne.

% ceci est un commentaire

Variables — majuscule initiale. Joker : _ (anonyme, frais à chaque occurrence) ou _Nom (nommé, réutilisable).

is_circle(S) :- shape(S, circle, _Rayon).

Identifiants (atomes, prédicats, types) — minuscule initiale, puis lettres non accentuées, chiffres et _ : livre passe, livré est une erreur de syntaxe.

Types, signatures, kinds

Type algébrique (ADT) — paramétrable. Le paramètre s'écrit en MAJUSCULE (T — c'est une variable de type ; une minuscule désigne un type nommé, un lieur minuscule est refusé).

type statut = ouvert | en_cours | clos.
type list(T) = nil | cons(T, list(T)).

Signature — les types des arguments d'un prédicat.

sig(etat, [statut]).
sig(edge, [noeud, noeud]).

Kind — ce qu'on a le droit de faire d'un type. Inféré, jamais déclaré : il n'y a rien à écrire. Fix classe chaque type d'après sa forme — number (calcul), enum (valeurs nommées), record (structure à champs), adt (mixte), numeric_record (structure et calcul) — et vérifie chaque opération contre cette classe (un calcul sur un type non calculable est refusé : règle mal typée). Tu croises ces noms dans les messages d'erreur et via kind_of/2, pas dans ton code. Le rôle du garde-fou : explications/kinds.md.

Type ouvert vs fermé. Déclarer un type t = a | b. (avec ses membres) ferme le type : seuls a et b sont admis, tout autre atome est refusé à la compilation. Un nom de type utilisé dans un sig sans déclaration type reste ouvert : toute valeur cohérente avec l'usage passe. Un paramètre de type (le T de list(T)) est une variable de type universelle, résolue à l'instanciation.

Règles de types (TLLP) · le kind est inféré, pas programmé

has_type/2 (type, niveau L₁) accepte des règles : tu peux affiner un type par une règle ordinaire.

Inférer un type (niveau L₁) — un type affiné, défini par une règle :

has_type(S, critique) :- latence(S, L), L > 30.

Le kind, lui, ne se programme PAS par règle (doctrine kind inféré-only, BUG-024). Le kind d'un type est fonction de sa déclaration (type … = …), jamais d'une règle. Une clause de tête kind_of/2 plate compile et s'évalue comme un prédicat ordinaire, mais elle est inerte pour le kindage — elle n'élargit ni ne modifie le kind d'aucun type. Une clause kind_of récursive (kind_of(list(T), adt) :- kind_of(T, _).) est, elle, refusée par la garde de terminaison (règle croissante kind_of). (Cette voie « KLLP » a été retirée : elle laissait une règle élargir un enum et y glisser un nombre — un trou de soundness.)

⚠️ Une règle has_type qui construit un terme en tête (has_type(cons(H, T), …) :- has_type(T, …)) reste rejetée par la garde de terminaison. Les règles has_type plates (comme critique) et l'interrogation (?- kind_of(T, K).) fonctionnent pleinement. Pour typer des termes structurés, déclare un ADT (les faits ground sont vérifiés) ou relie les types dans un prédicat dédié — voir explications/rdt.md.

Interroger un kind — déclarer un type peuple kind_of/2, que tu peux interroger directement, avec le nom lisible du kind :

?- kind_of(statut, K).
K = enum

kind_of est la surface interrogeable des kinds — le pendant L₂ de has_type.

Types dépendants (RDT)

Un type peut porter une valeur comme indice ; l'indice se calcule.

has_type(v1, vec(int, 3)).      % le 3 est une valeur, portée par le type

La contrainte entre indices s'écrit dans une règle has_type/result_type ordinaire, avec les builtins relationnels. Exemples complets (concaténation qui calcule la longueur, produit matriciel qui refuse les dimensions incompatibles) : explications/rdt.md.

Arithmétique

Builtins relationnels (tournent dans plusieurs sens) :

Comparaisons (gardes) : X > Y, X < Y, X >= Y, X =< Y, X = Y, X != Y. Il n'y a pas de forme évaluée Z is Expr : le calcul s'écrit relationnellement, add(X, Y, Z) plutôt que Z is X + Y.

ef(T, EF) :- es(T, ES), dur(T, D), add(ES, D, EF).

Les builtins et les gardes acceptent les flottants comme les entiers (add(1.5, 1.5, D) → D = 3.0 ; M > 2.0).

Nombres : entiers (42, -7) et flottants (3.14, -2.5e3). NaN et Inf sont refusés — un flottant Fix est toujours fini, et un calcul qui déborde ne produit pas de fait (la règle ne s'applique pas) plutôt qu'un résultat faux.

Agrégation

agg(Résultat, Opérateur, Variable, Source), comme but de corps : replie Variable sur toutes les solutions de Source (un littéral), groupées par les variables de tête, et lie Résultat.

best_score(P, B) :- agg(B, max, S, score(P, S)).

Opérateurs : min, max, sum, count, product, avg (avg produit un flottant, count un nombre quel que soit le type de la source). En récursion, seuls les opérateurs idempotents (min, max) sont permis.

La tête se signe comme tout prédicat — position résultat de type numérique (sig(best_score, [joueur, points])). Le détail, et le pourquoi (monoïdes, strates) : explications/agregation.md.

Une valeur agrégée se propage comme n'importe quelle autre : tu peux la faire transiter par un prédicat intermédiaire (une garde dans un prédicat séparé) et l'interroger — la limitation qui l'empêchait est corrigée (BUG-033).

Négation

not dans un corps de règle — négation stratifiée (univers typé fini ; les cycles négatifs sont rejetés à la compilation). Le pourquoi (complément, strates) : explications/negation.md.

orphelin(C) :- compte(C, P), not client(P).

Contrainte de déni — constraint <but>. déclare une configuration interdite.

constraint parent(X, X).

Régime : une violation héritée au chargement est un diagnostic — la session s'ouvre avec un ⚠ visible et reste utilisable (répare par :retract, la sentinelle est interrogeable : ?- constraint_violation. — PAS ?- false. : false reste un atome utilisateur ordinaire, disponible pour tes propres types) ; un :assert qui introduirait une violation est refusé (MOD-ERR-CONSTRAINT-VIOLATED, session intacte). L'état existant se signale, la dégradation nouvelle se bloque.

Modules

module(infra, [impacte/2]).
    % ... faits et règles internes ...
end_module.

use_module(infra).

Appel qualifié dans un corps de règle (alerte(S) :- infra::impacte(S, db).) comme en requête directe (?- infra::impacte(web, X).). Après use_module, la forme non qualifiée marche aussi. Un prédicat non exporté est invisible de l'extérieur (prédicat non exporté : infra::depend/2). Détails : explications/modules.md.

Déclarations propres à Fix

Dual et Generalize (ILP) — ⛔ DÉSACTIVÉES (2026-07-06, pull-driven). Ces deux déclarations sont refusées à la compilation (MOD-ERR-FEATURE-DISABLED) : leur réalisation « collapse en place » cassait la clôture du point fixe et le typage (BUG-018/045/046/047). Elles ne seront redéveloppées que sur besoin réel, et alors en dérivation join-only (spec 26, statut_surface ; backlog DUAL-REACTIVATION / GENERALIZE).

En attendant, le max/min par clé s'écrit en agg/4 explicite (la voie sûre et théorisée) :

mesure_max(C, M) :- agg(M, max, V, mesure(C, V)).
mesure_min(C, M) :- agg(M, min, V, mesure(C, V)).

Syntaxe de surface — définir la notation d'un langage (AST ↔ texte, bidirectionnel). Le type porte la structure, la clause de syntaxe habille un constructeur — explication complète : explications/syntaxe.md.

module(er, []).   % le langage er COMPLET : son AST ET sa syntaxe, au même endroit
  type list(T) = nil | cons(T, list(T)).       % liste GÉNÉRIQUE (type paramétré)
  type atype   = string | int | bool.          % FERMÉ : le vocabulaire de types du DSL
  type attr_t  = attr(aname, atype).           % aname OUVERT (nom), atype fermé (type)
  type ent_t   = ent(ename, list(attr_t)).     % ename OUVERT · liste = list(attr_t)
  ent(N, L) := "entity" N "fields" L "end".   % puis la syntaxe
end_module.

lire / ecrire — le pont texte ↔ terme, en requête uniquement (jamais dans une règle — refus MOD-ERR-LIRE-ECRIRE-IN-RULE : une règle qui fabrique du texte à chaque tour peut ne jamais terminer). Signatures symétriques, 4ᵉ argument unifié (variable → liaison ; lié → test) :

?- lire(er, ent_t, "entity person fields [ attr name string ] end", M).
M = ent(person, cons(attr(name, string), nil))

%% pipeline complet texte → AST → transformation → texte, en UNE requête
%% (forme segmentée : les lire d'abord, les littéraux ensuite, les ecrire en fin)
?- lire(er, ent_t, "entity person fields [ attr name string ] end", M),
   classe(C),
   ecrire(uml, cls_t, C, S).
S = class person members [ field name string ] end

Le texte est un atome quoté "…" ; le type racine doit être déclaré (type ent_t = ent(...)). Erreur de parse = message catalogué avec position (→ :help serialisation). Exemple jouable : :demo serialisation, ou charge examples/er-to-uml.fix.

Diagnostics et messages

Quand un programme .fix contient une erreur (type, prédicat sans signature, syntaxe, module introuvable…), Fix affiche un message clair, dans la langue de la session — français au REPL, anglais via MCP :

$ fix mauvais.fix
fix: fait mal typé : `bar(a, b, c)`
    `bar` a 3 argument(s), mais sa signature en attend 2.
    Corrige : ajuste l'appel, ou la signature sig(`bar`, [...]).
    → :help types

Les gabarits de messages vivent dans un catalogue interrogeable, chargé dès le démarrage. Tu peux le consulter :

?- error_template(type_error, fr, T).
T = le prédicat {} attend {}, reçu {}

?- error_severity(type_error, S).
S = fatal

…et l'enrichir d'une langue, sans une ligne de Rust :

:assert error_template(type_error, de, "Prädikat {} erwartet {}, erhielt {}").

La langue courante est portée par le fait lang(L) (REPL : lang(fr), MCP : lang(en)). Les trous {} du gabarit sont remplis dans l'ordre des arguments.

Chaque refus routé se termine par → :help <sujet> — le pointeur vers sa fiche, jamais présent sur un succès. Comprendre ce que chaque famille de refus te dit — et le réflexe pour y répondre : explications/erreurs.md.

Fix comme serveur MCP

Le binaire fix-mcp expose le solveur en serveur MCP (stdio) — la même session que le REPL, pilotable par un agent. Huit outils, calqués sur les commandes du REPL : load, query, assert, retract, listing, reload, save, help. help(topic?) répond depuis la même doc-KB que :help/ :help <sujet> en JSON structuré — c'est la porte à utiliser quand un refus se termine par → :help <sujet> (ce suffixe est une convention texte REPL ; :help <sujet> n'est pas un but Fix, ne pas le passer tel quel à query).

Activation par projet (opt-in, jamais automatique) :

./install.sh mcp-on     # écrit .mcp.json pour CE projet
./install.sh mcp-off    # le retire

Les erreurs sortent en anglais via MCP (fait lang(en)) et en JSON structuré (code textuel + message + position), prêt à consommer par l'agent — en français et en texte au REPL. Voir Diagnostics et messages.

Interdit par construction

Ces formes n'existent pas — par cohérence avec le modèle (ordre des règles sans importance, monotonie du point fixe) :

• le cut (!) et la négation par l'échec (\+) ;
• assert / retract dans les règles ;
• l'ordre significatif des clauses ;
• l'ordre supérieur (call/1, apply/2).

→ Pour le pourquoi derrière tout ça : Comprendre. Pour débuter en douceur : Apprendre.