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.