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