tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) | zero => 0;
Vu que nos déclarations sont autorisées à être récursives, avant d'essaier de "lexp_parse" le corps de "tonum", il faut ajouter tonum dans l'environnement, et ce autant pour senv and lenv. En l'absence d'inférence de type, c'est difficile à faire vu qu'on ne connait pas le type de tonum. C'est pas grave: ça veut dire que le code ci-dessus sera rejeté. Il faut écrire tonum : Nat - > Int tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) | zero => 0; À la place.
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 | '-------------------------------------------'
Lorsqu'on entre dans "tonum", il ne devrait pas encore y avoir "three", "two", "one" dans l'environnement (ni dans lenv, ni dans senv). Donc à la place, quand on passe le corps de tonum à lexp_parse, il faut passer l'environnement suivant: .-------------------------------------------. | SENV | ENV | |-------------------------------------------| | Nat 3 | Nat (induc.., Nat) | | zero 2 | zero (cons.., Nat) | | succ 1 | succ (cons.., Nat -> Nat) | | tonum 0 | Nat -> Int | '-------------------------------------------' Et en l'absence de "tonum : Nat - > Int", on passera .-------------------------------------------. | SENV | ENV | |-------------------------------------------| | Nat 2 | Nat (induc.., Nat) | | zero 1 | zero (cons.., Nat) | | succ 0 | succ (cons.., Nat -> Nat) | '-------------------------------------------' et "tonum" n'aura simplement pas le droit d'être récursif. On veut autoriser la récursion mutuelle, mais pour l'utiliser le programmeur devrait écrire: tonum : Nat - > Int one : Nat two : Nat three : Nat tonum = lambda x -> case x | (succ y) => (1 + (tonum y)) | zero => 0; one = (succ zero); two = (succ one); three = (succ two); auquel cas, oui, "lexp_parse" recevra un environnement qui inclut one/two/three lorsqu'on descend dans le corps de tonum. Stefan