Changeset 1282 for src/LIN


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/LIN/LINToASM.ma

    r1275 r1282  
    3131  let generated ≝
    3232    match instr with
    33     [ joint_st_sequential instr' _ ⇒
     33    [ sequential instr' _ ⇒
    3434      match instr' with
    35       [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    36       | joint_instr_cond acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     35      [ COST_LABEL lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     36      | COND acc_a_reg lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3737      | _ ⇒ set_empty ?
    3838      ]
    39     | joint_st_return ⇒ set_empty ?
    40     | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
     39    | RETURN ⇒ set_empty ?
     40    | GOTO lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
    4141  in
    4242  match label with
     
    8787  λstatement: pre_lin_statement globals_old.
    8888  match statement with
    89   [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    90   | joint_st_return ⇒ Instruction (RET ?)
    91   | joint_st_sequential instr _ ⇒
     89  [ GOTO lbl ⇒ Jmp (word_of_identifier ? lbl)
     90  | RETURN ⇒ Instruction (RET ?)
     91  | sequential instr _ ⇒
    9292      match instr with
    93       [ joint_instr_extension ext ⇒ ⊥
    94       | joint_instr_comment comment ⇒ Comment comment
    95       | joint_instr_cost_label lbl ⇒ Cost (word_of_identifier ? lbl)
    96       | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
    97       | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
    98       | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    99       | joint_instr_call_id f _ _ ⇒ Call (word_of_identifier ? f)
    100       | joint_instr_opaccs accs _ _ _ _ ⇒
     93      [ extension ext ⇒ ⊥
     94      | COMMENT comment ⇒ Comment comment
     95      | COST_LABEL lbl ⇒ Cost (word_of_identifier ? lbl)
     96      | POP _ ⇒ Instruction (POP ? accumulator_address)
     97      | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
     98      | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
     99      | CALL_ID f _ _ ⇒ Call (word_of_identifier ? f)
     100      | OPACCS accs _ _ _ _ ⇒
    101101        match accs with
    102102        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    103103        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    104104        ]
    105       | joint_instr_op1 op1 _ _ ⇒
     105      | OP1 op1 _ _ ⇒
    106106        match op1 with
    107107        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    108108        | Inc ⇒ Instruction (INC ? ACC_A)
    109109        ]
    110       | joint_instr_op2 op2 _ _ reg ⇒
     110      | OP2 op2 _ _ reg ⇒
    111111        match op2 with
    112112        [ Add ⇒
     
    189189          ] (subaddressing_modein … reg')
    190190        ]
    191       | joint_instr_int reg byte ⇒
     191      | INT reg byte ⇒
    192192        let reg' ≝ register_address reg in
    193193          match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    202202          | _ ⇒ λother: False. ⊥
    203203          ] (subaddressing_modein … reg')
    204       | joint_instr_move regs ⇒
     204      | MOVE regs ⇒
    205205         match regs with
    206206          [ from_acc reg ⇒
     
    230230               | _ ⇒ λother: False. ⊥
    231231               ] (subaddressing_modein … reg')]
    232       | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    233       | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    234       | joint_instr_address addr proof _ _ ⇒
     232      | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     233      | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     234      | ADDRESS addr proof _ _ ⇒
    235235        let look ≝ association addr globals (prf ? proof) in
    236236          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    237       | joint_instr_cond _ lbl ⇒
     237      | COND _ lbl ⇒
    238238        (* dpm: this should be handled in translate_code! *)
    239239        Instruction (JNZ ? (word_of_identifier ? lbl))
    240       | joint_instr_set_carry
     240      | SET_CARRY
    241241        Instruction (SETB ? CARRY)
    242242      ]
Note: See TracChangeset for help on using the changeset viewer.