Changeset 2032 for src/RTLabs/RTLabsToRTL_paolo.ma

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/RTLabs/RTLabsToRTL_paolo.ma (modified) (1 diff)

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -119 +119 @@
   [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
 [ %[@[int]] //
-| %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) normalize //
-| %[@(let 〈h1,l〉 ≝ split ? 8 … int in
-      let 〈h2,l〉 ≝ split ? 8 … l in
-      let 〈h3,l〉 ≝ split ? 8 … l in
+| %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) normalize //
+| %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in
+      let 〈h2,l〉 ≝ vsplit ? 8 … l in
+      let 〈h3,l〉 ≝ vsplit ? 8 … l in
        [l;h3;h2;h1])]
-  cases (split ????) #h1 #l normalize
-  cases (split ????) #h2 #l normalize
-  cases (split ????) // ]
+  cases (vsplit ????) #h1 #l normalize
+  cases (vsplit ????) #h2 #l normalize
+  cases (vsplit ????) // ]
 qed.