Changeset 1282 for src/joint/Joint.ma


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.

File:
1 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] ≝
Note: See TracChangeset for help on using the changeset viewer.