Je ne comprends de quelle lookup il s'agit. Est-ce que cela devrait ressembler à cela ?
let env_lookup_type ctx (v : vref): lexp = let (_, idx) = v in let (_, _, _, ltp) = _env_lookup ctx v in unsusp_all (Susp (ltp, (S.shift (idx + 1))))
Plus ou moins, oui. Sauf que celui-ci est pour "lookup_type", où il n'y a pas le même problème de récursion, et donc c'est toujours "idx + 1" sans jamais avoir un "offset". Et que le unsusp devra aussi être fait ailleurs de toute façon, donc il n'est pas probablement pas nécessaire de le faire ici.
Stefan
2016-05-20 14:37 GMT-04:00 Stefan Monnier monnier@iro.umontreal.ca:
Voici l'état de l’environnement à l’évaluation:
| Position | roffset | Nat | 13 | Nat | 1 | inductive_ (dNat) (succNat[0]) (zero): Type[30] | zero | 12 | zero | 0 | inductive-cons Nat[0] zero: Nat[0] | succ | 11 | succ | 0 | inductive-cons Nat[1] succ: Nat[0] -> Nat[1] | to-num | 10 | to-num | 1 | lambda (x : Nat[ | one | 9 | one | 0 | (succ[1] zero[2]):
Nat[1]
| two | 8 | two | 0 | (succ[2] one[0]): Nat[1] | three | 7 | three | 0 | (succ[3] two[0]): Nat[1] | plus | 6 | plus | 1 | lambda (x : Nat[7]) -> | n1 | 5 | n1 | 0 | (to-num[4] zero[6]):Int[32] | n2 | 4 | n2 | 0 | (to-num[5] one[4]):
Int[32]
| n3 | 3 | n3 | 0 | (to-num[6] two[4]):Int[32]
| m1 | 2 | m1 | 0 | (to-num[7] (plus[3]zero[9] two[5])): Int[32] | m2 | 1 | m2 | 0 | (to-num[8] (plus[4]
two[6]
zero[10])): Int[32] | m3 | 0 | m3 | 0 | (to-num[9] (plus[5]
two[7]
one[8])): Int[32]
J'ai pas regardé tout en détail, mais à première vue ça semble OK.
L'évaluation de `one = succ zero` ne marche pas (retourne l'item 2 du contexte global)
Hmm.. je ne suis pas sûr de comprendre ce que tu entends par "L'évaluation de `one = succ zero`". Si tu fait un `lookup "one"` (i.e. `lookup #9`) dans l'environnement ci-dessus, tu devrais obtenir qqch de la forme
Susp (S.shift 10) (succ[1] zero[2])
Et si tu utilises "unsusp" assez de fois, cela devrait se réduire à
(succ[11] zero[12])
Pour résoudre le problème il faudrait garder en mémoire le chemin
d’accès.
i.e one[9] -> (9 + zero[2]) + 1 = 12
Le "Susp" ajouté par le "lookup" devrait faire ce travail.
Stefan
-- Pierre Delaunay