I commented out the definition because I made mine earlier before I saw your commit.
Oui, j'ai pensé.
It is true. I don't need the recursive type per se. Nevertheless, I thought it would be more efficient.
En fait, c'est le contraire: non seulement c'est di code plus compliqué, mais en plus ça ré-introduit un O(N) (quoique ce N est le nombre scopes plutôt que le nombre de variables) au lieu du O(log N) de la solution plus simple.
When we add a variable, all offsets need to be incremented by one.
Non, c'est pas nécessaire: le SMap transforme les identificateurs en "reverse debruijn-index" (i.e. comme le debuijn-index mais qui compte depuis la racine, i.e. 0 correspond au binding le plus ancien plutôt que le plus récent), donc lorsqu'on ajoute un binding, il suffit d'ajouter l'entrée correspondante dans la table et d'incrémenter le nombre associé.
Le code que j'avais ne le disait qu'implicitement:
type senv_type = (db_revindex SMap.t * db_index) let senv_lookup senv s : db_index = let (m, i) = senv in i - SMap.find s senv
qui devrait se compléter avec qqch comme:
let senv_add senv s : senv_type = let (m, i) = senv in (SMap.add s i, i + 1)
-- Stefan