Voilà, j'espère que tout le monde voit les mails avec une police monospace. J'avais du mal à expliquer le problème. J'ai 'dessiné' les environnements un peu plus bas.
# Exemple:
Nat = inductive_ (dNat) (zero) (succ Nat);
zero = inductive-cons Nat zero; succ = inductive-cons Nat succ;
tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) | zero => 0;
one = (succ zero); two = (succ one); three = (succ two);
# Definitions
* `senv`: String environnement: map variable's name -> index * `env`: lexp environnement: map index to variable's type and expression
# Problème
Lorsqu'une variable est `lexp_parse` son type est recherché dans `env` mais l'index donné par `senv` n'est pas encore correct puisqu'il prend en compte les variables qui n'ont pas encore été `lexp`.
Le `sync_offset` que j'avais ajouté pour corriger se problème ne marche plus lorsque la propagation des types est faite en même temps. Exemple:
Environnement Top-level
.-------------------------------------------. | SENV | ENV | |-------------------------------------------| | Nat 6 | Nat (induc.., Nat) | | zero 5 | zero (cons.., Nat) | | succ 4 | succ (cons.., Nat -> Nat) | | tonum 3 | | <- lexp_parse tonum | one 2 | out of bounds | | two 1 | out of bounds | | three 0 | out of bounds | '-------------------------------------------'
Environnement lorsque `tonum` est `lexp_parse`:
.-------------------------------------------. | SENV | ENV | |-------------------------------------------| | Nat 7 | Nat (induc.., Nat) | | zero 6 | zero (cons.., Nat) | | succ 5 | succ (cons.., Nat -> Nat) | | tonum 4 | tonum(None, None) | | one 3 | x | | two 2 | out of bounds | | three 1 | out of bounds | | x 0 | out of bounds | '-------------------------------------------'
sync_offset = 7 - 3 = 4
Si on cherche `tonum`:
tonum_idx = 4 - sync_offset = 0 OK
Si on cherche `x`:
x_idx = 0 - sync_offset = -4 FAIL
Grâce à l'utilisation des ref cell, `env` et `senv` sont toujours de la même taille sauf s'il y a des noms en double, mais cella n'affecte pas la validité des indices.