Changeset 2208 for src/LIN

Timestamp:

Jul 18, 2012, 1:26:43 PM (8 years ago)

Author:

tranquil

Message:

• moving some code around
• changed immediates to hold beval in general, not only bytes
• fixed RTLabsToRTL after redefinitions in front end

File:

• src/LIN/joint_LTL_LIN_paolo.ma (modified) (3 diffs)

src/LIN/joint_LTL_LIN_paolo.ma

@@ -1 +1 @@
 include "joint/Joint_paolo.ma".
-
-definition a_acc ≝ it.
-definition b_acc ≝ it.
 
 inductive registers_move: Type[0] ≝
  | from_acc: Register → unit → registers_move
  | to_acc: unit → Register → registers_move
- | int_to_reg : Register → Byte → registers_move
- | int_to_acc : unit → Byte → registers_move.
-
-inductive ltl_argument : Type[0] ≝
- | Reg : Register → ltl_argument
- | Imm : Byte → ltl_argument.
-
-coercion reg_ltl_argument : ∀r : Register.ltl_argument ≝ Reg on _r : Register to ltl_argument.
-coercion int_ltl_argument : ∀b : Byte.ltl_argument ≝ Imm on _b : Byte to ltl_argument.
-
-notation "𝐀" with precedence 90 for @{a_acc}.
-notation "𝐁" with precedence 90 for @{b_acc}.
+ | int_to_reg : Register → beval → registers_move
+ | int_to_acc : unit → beval → registers_move.
+(* the last is redudant, but kept for notation's sake *)
 
 inductive ltl_lin_seq : Type[0] ≝
@@ -34 +22 @@
     (* dpl_arg   ≝ *) unit
     (* dph_arg   ≝ *) unit
-    (* snd_arg   ≝ *) ltl_argument
+    (* snd_arg   ≝ *) hdw_argument
     (* pair_move ≝ *) registers_move
     (* call_args ≝ *) ℕ
@@ -48 +36 @@
       (* localsT ≝ *) void).
 
-interpretation "from accumulator" 'mov a b = (MOVE ?? (from_acc a b)).
-interpretation "to accumulator" 'mov a b = (MOVE ?? (to_acc a b)).
-interpretation "int to register" 'mov a b = (MOVE ?? (int_to_reg a b)).
-interpretation "int to accumulator" 'mov a b = (MOVE ?? (int_to_acc a b)).
-definition nat_to_byte : ℕ → Byte ≝ nat_to_bv 8.
-coercion nat_as_byte : ∀n : ℕ.Byte ≝ nat_to_byte on _n : ℕ to Byte.
-
+interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
+interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
+interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
+interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).