J’ai attaché 2 fichiers, `update.patch` qui contient les modifications que j’ai effectuées depuis le dernier patch et `full.patch` qui contient tout. Pour résumer rapidement les changements dans `update.patch`: - Le changement de nom `Interval` en `I` - L’argument (f : I ≡> t) dans `Eq_eq` a été rendu effaçable, par conséquent la preuve d’égalité dans Eq_uneq est aussi effaçable. - L'equivalence η des fonctions, ce qui nous permet d’écrire Eq_funext : (f : ? -> ?) => (g : ? -> ?) => ((x : ?) -> Eq (f x) (g x)) -> Eq f g; A part l’ajout du traitement de η dans `conv_p`, c’était aussi nécessaire d’ajouter la même logique dans l’unification des lambdas. Dans la fonction `unify’`, est-ce que c’est nécessaire de traiter les branches dans cet ordre? Par exemple, est-ce que ce serait correct de traiter d’abord les Vars avant les Lambdas? - Petite amélioration du printer: - Eval.print_eval_result prend un `ltype` optionnel comme paramètre, c’est utile notamment pour mieux afficher les expressions du type Eq et les fonctions qui ont des paramètres effaçables. - la REPL garde le type des expressions après l’appel à `check` et les fournit à Eval.print_eval_result Et voila. James Le 24 juin 2023 à 11:01, Stefan Monnier <monnier@iro.umontreal.ca> a écrit : Pas sûr si c'est mieux, mais tu devrais pouvoir faire ce qu'on fait pour les booléens (via `predef_names` in `src/builtin.ml`). Comme discuté, je pense que ce serait pas trivial d'implémenter ça car le type `Interval` et les fonctions `eq_eq` et `eq_uneq` sont référencés dans des endroits où on a pas accès au contexte d’élaboration (ce qui est nécessaire pour utiliser la fonction `get_predef`). OK, je suis allé voir pourquoi on a besoin du elab_context: let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) with Not_found -> log_raise_error {|"%s" was not predefined|} name [...ailleurs...] let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n donc on a besoin du elab_context parce que `DB.get_size` prend un `elab_context` pour en extraire le `n` qui contient la taille du `lexp_context`, mais on pourrait aussi le calculer sur la base du `lexp_context`, sauf que c'est O(log N) au lieu de O(1). :-( Et tout ça pour faire un `S.shift` que l'on pourrait complètement éviter en évitant les indices de DeBruijn dans les predefs :-) Je remarque cependant que t'as seulement besoin de `DB.eq_eq` (qui remplace `DB.eq_refl`) mais pas de `DB.eq_uneq`, donc on peut éliminer la définition en OCaml du type de `eq_uneq`. Stefan