Setepenre pushed to branch master at Stefan / Typer
Commits: 0905ab89 by Pierre Delaunay at 2016-04-15T11:47:20-04:00 lexp_p_infer: Type propagation
Changes to be committed: * src/debruijn.ml: - lexp_context uses a ref cell (which solve all our synchronization problems between env and senv - new function (env_set_var_info) * src/lparse.ml: - started to propagate types and lexp_parsing at the same time - modified (_lexp_decls) to match the new environement
- - - - -
4 changed files:
- src/builtin.ml - src/debruijn.ml - src/lparse.ml - + tests/debruijn_test.ml
Changes:
===================================== src/builtin.ml ===================================== #Gitlab::Git::Diff:0x0000000718fb80
===================================== src/debruijn.ml ===================================== #Gitlab::Git::Diff:0x0000000718f658
===================================== src/lparse.ml ===================================== #Gitlab::Git::Diff:0x0000000718f158
===================================== tests/debruijn_test.ml ===================================== #Gitlab::Git::Diff:0x0000000718eb18
View it on GitLab: https://gitlab.com/monnier/typer/commit/0905ab89c1d6dc40b101b68f587c263e7131...
Afficher les réponses par date
- lexp_context uses a ref cell (which solve all our
synchronization problems between env and senv
Pourrais-tu expliquer ce changement (i.e. ce qu'il fait, et surtout quels problèmes il résout)?
Utiliser un ref-cell ici est un changement avec des conséquences assez sérieuses, donc j'aimerais m'assurer que ça se justifie,
Stefan
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.
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