Changeset 1529 for src/RTLabs

Timestamp:

Nov 22, 2011, 12:28:04 PM (8 years ago)

Author:

campbell

Message:

Update RTLabs to RTL with unary operation types.

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (10 diffs)

src/RTLabs/RTLabsToRTL.ma

@@ -431 +431 @@
 definition translate_op1 ≝
   λglobals: list ident.
-  λop1: unary_operation.
+  λty, ty'.
+  λop1: unary_operation ty ty'.
   λdestrs: list register.
   λsrcrs: list register.
@@ -439 +440 @@
   λdef: rtl_internal_function globals.
   match op1 with
-  [ Ocastint src_sign src_size _ _ ⇒
+  [ Ocastint src_size src_sign _ _ ⇒
     let dest_size ≝ |destrs| * 8 in
     let src_size ≝ bitsize_of_intsize src_size in
       translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
-  | Onegint ⇒
+  | Onegint _ _ ⇒
       translate_negint globals destrs srcrs start_lbl dest_lbl def prf
-  | Onotbool ⇒
+  | Onotbool _ _ _ _ ⇒
       translate_notbool globals destrs srcrs start_lbl dest_lbl def
-  | Onotint ⇒
+  | Onotint _ _ ⇒
     let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
     let l ≝ map2 … f destrs srcrs prf in
       adds_graph rtl_params1 globals l start_lbl dest_lbl def
-  | Optrofint r ⇒
+  | Optrofint _ _ r ⇒
       translate_move globals destrs srcrs start_lbl dest_lbl def
-  | Ointofptr r ⇒
+  | Ointofptr _ _ r ⇒
       translate_move globals destrs srcrs start_lbl dest_lbl def
-  | Oid ⇒
+  | Oid _ ⇒
       translate_move globals destrs srcrs start_lbl dest_lbl def
   | _ ⇒ ? (* float operations implemented in runtime *)
@@ -860 +861 @@
   [2: >tmp_destrs_proof @prf_destrs
   |1: normalize nodelta
-      generalize in match srcrs12_proof
+      generalize in match srcrs12_proof;
       #HYP >rev_length >rev_length @HYP
   ]
@@ -971 +972 @@
       add_translates rtl_params1 globals [
         translate_ne globals destrs srcrs1 srcrs2;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
@@ -979 +980 @@
       add_translates rtl_params1 globals [
         translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     | Cge ⇒
       add_translates rtl_params1 globals [
         translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     ]
@@ -992 +993 @@
       add_translates rtl_params1 globals [
         translate_ne globals destrs srcrs1 srcrs2;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
@@ -1000 +1001 @@
       add_translates rtl_params1 globals [
         translate_lt globals destrs destrs_prf srcrs2 srcrs1;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     | Cge ⇒
       add_translates rtl_params1 globals [
         translate_lt globals destrs destrs_prf srcrs1 srcrs2;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     ]
@@ -1013 +1014 @@
       add_translates rtl_params1 globals [
         translate_ne globals destrs srcrs1 srcrs2;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
@@ -1021 +1022 @@
       add_translates rtl_params1 globals [
         translate_lt globals destrs destrs_prf srcrs2 srcrs1;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     | Cge ⇒
       add_translates rtl_params1 globals [
         translate_lt globals destrs destrs_prf srcrs1 srcrs2;
-        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
+        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
       ] start_lbl dest_lbl def
     ]
@@ -1168 +1169 @@
   | St_const destr cst lbl' ⇒
     translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
-  | St_op1 op1 destr srcr lbl' ⇒
-    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
+  | St_op1 ty ty' op1 destr srcr lbl' ⇒
+    translate_op1 globals ty ty' op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
   | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
     translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def