Salut Vincent,
Voici une première ébauche de la description du problème&solution dont
je t'ai parlé, je commence avec une récapitulation pour les gens du "Cc":
Avec les index de deBruijn, on a le problème que lorsqu'on fait un
"lookup", tel que typiquement dans `lctx_lookup_type`, on doit faire:
mkSusp t (S.shift (i + 1))
Quand on a de la chance et que le type en question est fermé, ce shift
va traverser `t` récursivement (et lazily) pour finalement ne
rien faire. C'est pas idéal, mais c'est pas le plus grave.
Le plus grave, c'est quand ce type n'est pas complètement fermé (ce qui
est le cas courant, après tout, il suffit qu'il y a une référence à un
autre type prédéfini comme `Type`, `Int`, `Bool`, `List, `TypeLevel`,
...), on va non seulement traverser `t` mais le résultat sera différent
selon la taille actuelle du `lctx`, donc on se retrouve avec un type
comme `List` représenté de manière (légèrement) différente à chaque
profondeur, donc notre hash-consing ne peut pas les mettre ensemble.
Dans un système comme Coq, ils évitent en partie ce problème parce que
`List` n'est pas dans l'environnement `lctx` mais dans un environnement
global.
L'idée pour résoudre ce problème de performance et d'utiliser un mélange
de deBruijn index et deBruijn level. En gros l'idée serait
la suivante. On aurait nos termes représentés comme suit:
type Term
| Lambda Term
| App Term Term
| LVar Nat
| IVar Nat
| LocallyIndexed Term
Où le `Var` a été dupliqué en un cas `IVar i` si c'est un index et `LVar l`
si c'est un level (lorsque l'environnement a une longueur de N, `LVar
i` ≃ `IVar (N - i)`), et on a un nouveau nœud `LocallyIndexed e` qui signifie
que toutes les variables libres de `e` sont des `LVar` et toutes les
variables non-libres de `e` sont des `IVar`.
Comme ça, maintenant, quand on ajoute `x : τ` dans le `lctx` on peut
en fait y mettre `x : LocallyIndexed τ'` de sorte que dans le
`lctx_lookup_type` on a plus besoin du shift parce qu'un shift de
`LocallyIndexed e` renvoie simplement `LocallyIndexed e`.
Mais il faut maintenant réviser nos substitutions explicites.
E.g. on aura probablement besoin d'une substitution pour "fermer":
LocallyIndexed τ[σf] ≃ τ
une autre pour ouvrir:
LocallyIndexed τ ≃ τ[σo]
et des règles pour les composer (et bien sûr une/des règles pour
éliminer les shifts quand ils arrivent sur un `LocallyIndexed`).
Stefan