Changeset 1282 for src/joint


Ignore:
Timestamp:
Sep 28, 2011, 11:50:32 PM (8 years ago)
Author:
sacerdot
Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1280 r1282  
    3030
    3131inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
    32   | joint_instr_comment: String → joint_instruction p globals
    33   | joint_instr_cost_label: costlabel → joint_instruction p globals
    34   | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
    35   | joint_instr_move: pair_reg p → joint_instruction p globals
    36   | joint_instr_pop: acc_a_reg p → joint_instruction p globals
    37   | joint_instr_push: acc_a_reg p → joint_instruction p globals
    38   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    39   | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
    40   | joint_instr_op1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    41   | joint_instr_op2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
    42   | joint_instr_clear_carry: joint_instruction p globals
    43   | joint_instr_set_carry: joint_instruction p globals
    44   | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
    45   | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    46   | joint_instr_call_id: ident → call_args p → call_dest p → joint_instruction p globals
    47   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
    48   | joint_instr_extension: extend_statements p → joint_instruction p globals.
     32  | COMMENT: String → joint_instruction p globals
     33  | COST_LABEL: costlabel → joint_instruction p globals
     34  | INT: generic_reg p → Byte → joint_instruction p globals
     35  | MOVE: pair_reg p → joint_instruction p globals
     36  | POP: acc_a_reg p → joint_instruction p globals
     37  | PUSH: acc_a_reg p → joint_instruction p globals
     38  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
     39  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
     40  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     41  | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
     42  | CLEAR_CARRY: joint_instruction p globals
     43  | SET_CARRY: joint_instruction p globals
     44  | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
     45  | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
     46  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
     47  | COND: acc_a_reg p → label → joint_instruction p globals
     48  | extension: extend_statements p → joint_instruction p globals.
    4949
    5050inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    51   | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    52   | joint_st_goto: label → joint_statement p globals
    53   | joint_st_return: joint_statement p globals.
     51  | sequential: joint_instruction p globals → succ p → joint_statement p globals
     52  | GOTO: label → joint_statement p globals
     53  | RETURN: joint_statement p globals.
    5454
    5555record params0: Type[1] ≝
  • src/joint/TranslateUtils.ma

    r1280 r1282  
    4242  λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.
    4343  match e with
    44   [ joint_st_goto _ ⇒ joint_st_goto … l
    45   | joint_st_return ⇒ joint_st_return ??
    46   | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr l].
     44  [ GOTO _ ⇒ GOTO … l
     45  | RETURN ⇒ RETURN ??
     46  | sequential instr _ ⇒ sequential … globals instr l].
    4747
    4848(*CSC: bad programming habit: the code below puts everywhere a fake
     
    5656    on stmt_list ≝
    5757  match stmt_list with
    58   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
     58  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    5959  | cons stmt stmt_list ⇒
    6060    match stmt_list with
     
    7474    on translate_list ≝
    7575  match translate_list with
    76   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
     76  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    7777  | cons trans translate_list ⇒
    7878    match translate_list with
Note: See TracChangeset for help on using the changeset viewer.