Changeset 1281 for src/LIN/LIN.ma

Timestamp:

Sep 28, 2011, 11:08:37 PM (8 years ago)

Author:

sacerdot

Message:

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

File:

• src/LIN/LIN.ma (modified) (2 diffs)

src/LIN/LIN.ma

@@ -2 +2 @@
 include "utilities/lists.ma".
 
-definition lin_params_: params_ ≝
- mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) unit.
+definition lin_params__: params__ ≝
+ mk_params__ unit unit unit unit registers_move Register nat unit False.
+definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit.
+definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit.
+definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit.
 
 definition pre_lin_statement ≝ joint_statement lin_params_.
@@ -21 +24 @@
 definition lin_params: ∀globals. params globals ≝
  λglobals.
-  mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code)
+  mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code)
    (λcode:Σcode.?. λl.
     find ?? (λs. let 〈l',x〉 ≝ s in