Changeset 1169


Ignore:
Timestamp:
Sep 2, 2011, 11:57:45 AM (8 years ago)
Author:
sacerdot
Message:

JointRTLtoLIN moved to Joint

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1167 r1169  
    66include "common/Registers.ma".
    77
     8record params: Type[1] ≝
     9 { acc_a_reg: Type[0]
     10 ; acc_b_reg: Type[0]
     11 ; dpl_reg: Type[0]
     12 ; dph_reg: Type[0]
     13 ; pair_reg: Type[0]
     14 ; generic_reg: Type[0]
     15 }.
     16
     17inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
     18  | joint_instr_comment: String → joint_instruction p globals
     19  | joint_instr_cost_label: costlabel → joint_instruction p globals
     20  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
     21  | joint_instr_move: pair_reg p → joint_instruction p globals
     22  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
     23  | joint_instr_push: acc_a_reg p → joint_instruction p globals
     24  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
     25  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
     26  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
     27  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
     28  | joint_instr_clear_carry: joint_instruction p globals
     29  | joint_instr_set_carry: joint_instruction p globals
     30  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
     31  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
     32  | joint_instr_call_id: ident → nat → joint_instruction p globals
     33  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
     34
     35inductive joint_statement (next: Type[0]) (p:params) (globals: list ident): Type[0] ≝
     36  | joint_st_sequential: joint_instruction p globals → next → joint_statement next p globals
     37  | joint_st_goto: label → joint_statement next p globals
     38  | joint_st_return: joint_statement next p globals.
     39
     40(* Used in LTL and LIN *) 
    841inductive registers_move: Type[0] ≝
    9   | from_acc: Register → registers_move
    10   | to_acc: Register → registers_move.
    11 
    12 inductive joint_instruction
    13   (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) (dpl_reg: Type[0])
    14   (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]) (globals: list ident): Type[0] ≝
    15   | joint_instr_comment: String → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    16   | joint_instr_cost_label: costlabel → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    17   | joint_instr_int: generic_reg → Byte → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    18   | joint_instr_move: pair_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    19   | joint_instr_pop: acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    20   | joint_instr_push: acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    21   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    22   | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    23   | joint_instr_op1: Op1 → acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    24   | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    25   | joint_instr_clear_carry: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    26   | joint_instr_set_carry: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    27   | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    28   | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    29   | joint_instr_call_id: ident → nat → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    30   | joint_instr_cond: acc_a_reg → label → joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals.
    31 
    32 inductive joint_statement
    33   (A: Type[0]) (acc_a_reg: Type[0]) (acc_b_reg: Type[0]) (dpl_reg: Type[0])
    34   (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]) (globals: list ident): Type[0] ≝
    35   | joint_st_sequential: joint_instruction acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals → A → joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    36   | joint_st_goto: label → joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals
    37   | joint_st_return: joint_statement A acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg globals.
     42 | from_acc: Register → registers_move
     43 | to_acc: Register → registers_move.
Note: See TracChangeset for help on using the changeset viewer.