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