Bonjour,
je viens d'ajouter le commit qui implémente le parsing des déclarations comme nous en avons parlé, aujourd'hui.
Comme attendu, cela ne marche pas.
Voici l'état de l’environnement à l’évaluation:
| Position | roffset | Nat | 13 | Nat | 1 | inductive_ (dNat) (succ Nat[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]
L'évaluation de `one = succ zero` ne marche pas (retourne l'item 2 du contexte global)
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
Est-ce que vous avez des proposition pour faire cela ?