Changeset 2208 for src/LIN


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (7 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_paolo.ma

    r2174 r2208  
    11include "joint/Joint_paolo.ma".
    2 
    3 definition a_acc ≝ it.
    4 definition b_acc ≝ it.
    52
    63inductive registers_move: Type[0] ≝
    74 | from_acc: Register → unit → registers_move
    85 | to_acc: unit → Register → registers_move
    9  | int_to_reg : Register → Byte → registers_move
    10  | int_to_acc : unit → Byte → registers_move.
    11 
    12 inductive ltl_argument : Type[0] ≝
    13  | Reg : Register → ltl_argument
    14  | Imm : Byte → ltl_argument.
    15 
    16 coercion reg_ltl_argument : ∀r : Register.ltl_argument ≝ Reg on _r : Register to ltl_argument.
    17 coercion int_ltl_argument : ∀b : Byte.ltl_argument ≝ Imm on _b : Byte to ltl_argument.
    18 
    19 notation "𝐀" with precedence 90 for @{a_acc}.
    20 notation "𝐁" with precedence 90 for @{b_acc}.
     6 | int_to_reg : Register → beval → registers_move
     7 | int_to_acc : unit → beval → registers_move.
     8(* the last is redudant, but kept for notation's sake *)
    219
    2210inductive ltl_lin_seq : Type[0] ≝
     
    3422    (* dpl_arg   ≝ *) unit
    3523    (* dph_arg   ≝ *) unit
    36     (* snd_arg   ≝ *) ltl_argument
     24    (* snd_arg   ≝ *) hdw_argument
    3725    (* pair_move ≝ *) registers_move
    3826    (* call_args ≝ *) ℕ
     
    4836      (* localsT ≝ *) void).
    4937
    50 interpretation "from accumulator" 'mov a b = (MOVE ?? (from_acc a b)).
    51 interpretation "to accumulator" 'mov a b = (MOVE ?? (to_acc a b)).
    52 interpretation "int to register" 'mov a b = (MOVE ?? (int_to_reg a b)).
    53 interpretation "int to accumulator" 'mov a b = (MOVE ?? (int_to_acc a b)).
    54 definition nat_to_byte : ℕ → Byte ≝ nat_to_bv 8.
    55 coercion nat_as_byte : ∀n : ℕ.Byte ≝ nat_to_byte on _n : ℕ to Byte.
    56 
     38interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
     39interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)).
     40interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)).
     41interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracChangeset for help on using the changeset viewer.