Re: [Typer] déclaration lexp_parsing - Typer

20 Mai 2016


      ...
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)  (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]
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