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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/joint_LTL_LIN_paolo.ma
r2174 r2208 1 1 include "joint/Joint_paolo.ma". 2 3 definition a_acc ≝ it.4 definition b_acc ≝ it.5 2 6 3 inductive registers_move: Type[0] ≝ 7 4  from_acc: Register → unit → registers_move 8 5  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 *) 21 9 22 10 inductive ltl_lin_seq : Type[0] ≝ … … 34 22 (* dpl_arg ≝ *) unit 35 23 (* dph_arg ≝ *) unit 36 (* snd_arg ≝ *) ltl_argument24 (* snd_arg ≝ *) hdw_argument 37 25 (* pair_move ≝ *) registers_move 38 26 (* call_args ≝ *) ℕ … … 48 36 (* localsT ≝ *) void). 49 37 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 38 interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). 39 interpretation "move to acc" 'mov a b = (MOVE ?? (to_acc a b)). 40 interpretation "move int to reg" 'mov a b = (MOVE ?? (int_to_reg a b)). 41 interpretation "move int to acc" 'mov a b = (MOVE ?? (int_to_acc a b)).
Note: See TracChangeset
for help on using the changeset viewer.