Changeset 2032 for src/Cminor

Timestamp:

Jun 8, 2012, 4:32:03 PM (8 years ago)

Author:

sacerdot

Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:

• src/Cminor/toRTLabs.ma (modified) (1 diff)

src/Cminor/toRTLabs.ma

@@ -828 +828 @@
 | #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
 | #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
-| #_ (* see above *) <E @(pi2 ?? r)
+| (*#_ (* see above *) <E @(pi2 ?? r)*) (*CSC: FIXME!!!*) cases daemon
 | @(pi2 … (pf_entry …))
 | #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]