[pypy-svn] r19731 - pypy/dist/pypy/doc
arigo at codespeak.net
arigo at codespeak.net
Thu Nov 10 18:23:50 CET 2005
Author: arigo
Date: Thu Nov 10 18:23:47 2005
New Revision: 19731
Modified:
pypy/dist/pypy/doc/draft-dynamic-language-translation.txt
Log:
A paragraph moved, a few typos, and two minor fixes to the proof.
Modified: pypy/dist/pypy/doc/draft-dynamic-language-translation.txt
==============================================================================
--- pypy/dist/pypy/doc/draft-dynamic-language-translation.txt (original)
+++ pypy/dist/pypy/doc/draft-dynamic-language-translation.txt Thu Nov 10 18:23:47 2005
@@ -1240,8 +1240,8 @@
relation *E* identifies some of these variables as follows: if an
attribute ``attr`` is found to belong to a base class ``C``, then all
variables ``v_D.attr`` for all subclasses ``D`` of ``C`` are
- identified with ``v_C.attr``. This ensures that the instances of the
- subclasses are all given the same generic attribute defined in ``C``.
+ identified with ``v_C.attr``. This ensures that the instances of all
+ the subclasses are given the same generic attribute defined in ``C``.
Formally::
@@ -1259,7 +1259,17 @@
merge b(z) => v_C.attr
Note the similarity with the ``getitem`` and ``setitem`` of lists, in
-particular the usage of the auxiliary variable *z'*.
+particular the usage of the auxiliary variable *z'*. Also note that we
+still allow real bound methods to be handled and passed around in the
+way that is quite unique to Python: if ``meth`` is the name of a method
+of *x*, then ``y = x.meth`` is allowed, and the object *y* can be passed
+around and stored in data structures. However, in our case we do not
+allow such objects to be stored directly back into other instances (it
+is the purpose of the check in the rule for ``setattr``). This would
+create a confusion between class-level and instance-level attributes in
+a subsequent ``getattr``. It is a limitation of our annotator to not
+distinguish these two levels -- there is only one set of ``v_C.attr``
+variables for both.
The purpose of ``lookup_filter`` is to avoid losing precision in method
calls. Indeed, if ``attr`` names a method of the class ``C`` then the
@@ -1298,39 +1308,29 @@
or a superclass of ``C``, we select the ones whose class is the most
derived class thus represented. In other words, if ``C`` inherits
from ``B`` which inherits from ``A``, then potential bound method
- objects ``A.f`` would be included in the *newset* only if there is no
- ``B.g`` or ``C.h`` in *m*.
-
-Finally, note that we still allow real bound methods to be handled and
-passed around in the way that is quite unique to Python: if ``meth`` is
-the name of a method of *x*, then ``y = x.meth`` is allowed, and the
-object *y* can be passed around and stored in data structures. However,
-we do not allow such objects to be stored directly back into other
-instances (it is the purpose of the check in the rule for ``setattr``).
-This would create a confusion between class-level and instance-level
-attributes in a subsequent ``getattr``. It is a limitation of our
-annotator to not distinguish these two levels -- there is only one set
-of ``v_C.attr`` variables for both.
+ objects ``A.f`` would be included in the *newset* if and only if there
+ is no ``B.g`` or ``C.h`` in *m*.
Calls
~~~~~
-A call in the user program turns into a ``simple_call`` operation whose
-first argument is the object to call. Here is the corresponding rule --
-regrouping all cases because a single ``Pbc(set)`` annotation could mix
-several kinds of callables::
+A call in the user program is represented by a ``simple_call`` operation
+whose first argument is the object to call. Here is the corresponding
+rule -- regrouping all cases because a single ``Pbc(set)`` annotation
+could theoretically mix several kinds of callables::
- z=simple_call(x,y1,...,yn), b(x)=Pbc(set)
+ z=simple_call(x,y1,...,yn) | z', b(x)=Pbc(set)
---------------------------------------------------------------------
for each c in set:
if c is a function:
- E' = E union (z ~ returnvar_c)
+ E' = E union (z' ~ returnvar_c)
+ b' = b with (z->b(z'))
merge b(y1) => arg_c_1
...
merge b(yn) => arg_c_n
if c is a class:
- let f = c.__init__
+ let f = c.__init__ # the constructor
merge Inst(c) => z
merge Inst(c) => arg_f_1
merge b(y1) => arg_f_2
@@ -1338,7 +1338,8 @@
merge b(yn) => arg_f_(n+1)
if c is a method:
let class.f = c
- E' = E union (z ~ returnvar_f)
+ E' = E union (z' ~ returnvar_f)
+ b' = b with (z->b(z'))
merge Inst(class) => arg_f_1
merge b(y1) => arg_f_2
...
@@ -1367,12 +1368,13 @@
Generalisation
**************
-We first have to check that each rule can only turn a state *(b,E)* into
-a state *(b',E')* that is either identical or more general. Clearly,
-*E'* can only be generalised -- applying a rule can only add new
-identifications, not remove existing ones. What is left to check is
-that the annotation ``b(v)`` of each variable, when modified, can only
-become more general. We prove it in the following order:
+We first have to check that during the annotation process each rule can
+only turn a state *(b,E)* into a state *(b',E')* that is either
+identical or more general. Clearly, *E'* can only be generalised --
+applying a rule can only add new identifications, not remove existing
+ones. What is left to check is that the annotation ``b(v)`` of each
+variable, when modified, can only become more general (i.e. be
+increased, in the lattice order). We prove it in the following order:
1. the annotations of the input variables of blocks;
@@ -1388,9 +1390,10 @@
1. Input variables of blocks
The annotation of these variables are only modified by the ``phi``
- rule, which is based on ``merge``. The ``merge`` operation trivially
- guarantees the property of generalisation because it is based on the
- union operator ``\/`` of the lattice.
+ and ``simple_call`` rules, which are based on ``merge``. The
+ ``merge`` operation trivially guarantees the property of
+ generalisation because it is based on the union operator ``\/`` of
+ the lattice.
2. Auxiliary variables of operations
@@ -1420,12 +1423,13 @@
To prove our claim, first note that none of these input and result
variables is ever identified with any other variable via *E*: indeed,
- the rules described above only identify auxiliary variables and
- attribute-of-class variables with each other. It means that the only
- way the result variable *z* of an operation can be modified is
- directly by the rule or rules specific to that operation. This
- allows us to check the property of generalisation on a case-by-case
- basis.
+ the rules described above only identify auxiliary variables or
+ attribute-of-class variables with each other (the variables that
+ appear in ``List`` annotations are always auxiliary variables too).
+ It means that the only way the result variable *z* of an operation
+ can be modified is directly by the rule or rules specific to that
+ operation. This allows us to check the property of generalisation on
+ a case-by-case basis.
Most cases are easy to check. Cases like ``b' = b with (z->b(z'))``
are based on point 2 above. The only non-trivial case is in the rule
More information about the Pypy-commit
mailing list