Changeset 1089


Ignore:
Timestamp:
Jul 27, 2011, 5:50:25 PM (9 years ago)
Author:
mulligan
Message:

more changes from earlier in the week

Location:
src
Files:
1 added
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1075 r1089  
    6666| RegisterB: Register
    6767| RegisterDPL: Register
    68 | RegisterDPH: Register.
     68| RegisterDPH: Register
     69| RegisterCarry: Register.
    6970
    7071definition nat_of_register: Register → nat ≝
     
    107108  | RegisterDPL ⇒ 34
    108109  | RegisterDPH ⇒ 35
     110  | RegisterCarry ⇒ 36 (* was -1, increment as needed *)
    109111  ].
    110112 
     
    230232  register_DPL_value: option Byte;
    231233  register_DPH_value: option Byte
     234  (* carry only used in liveness analysis *)
    232235}.
    233236
  • src/LIN/JointLTLLIN.ma

    r1082 r1089  
    22include "ASM/I8051.ma".
    33include "common/CostLabel.ma".
     4include "common/Graphs.ma".
    45include "common/AST.ma".
    56include "common/Registers.ma".
    67
    78inductive joint_instruction (globals: list ident): Type[0] ≝
     9  | joint_instr_skip: joint_instruction globals
    810  | joint_instr_comment: String → joint_instruction globals
    911  | joint_instr_cost_label: costlabel → joint_instruction globals
     
    1820  | joint_instr_op2: Op2 → Register → joint_instruction globals
    1921  | joint_instr_clear_carry: joint_instruction globals
     22  | joint_instr_set_carry: joint_instruction globals
    2023  | joint_instr_load: joint_instruction globals
    2124  | joint_instr_store: joint_instruction globals
    22   | joint_instr_call_id: ident → joint_instruction globals
    23   | joint_instr_cond_acc: ident → joint_instruction globals.
     25  | joint_instr_call_id: label → joint_instruction globals
     26  | joint_instr_cond_acc: label → joint_instruction globals.
    2427
    2528inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
    2629  | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
    27   | joint_st_goto: ident → joint_statement A globals
    2830  | joint_st_return: joint_statement A globals.
  • src/LTL/LTL.ma

    r1082 r1089  
    33include "LIN/LIN.ma".
    44
    5 definition ltl_statement ≝ joint_statement ident.
     5definition ltl_statement ≝ joint_statement label.
    66 
    77definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  • src/RTL/RTL.ma

    r1071 r1089  
    2626  | rtl_st_cond: register → label → label → rtl_statement
    2727  | rtl_st_set_carry: label → rtl_statement
    28   | rtl_st_return: rtl_statement. (* XXX: change from o'caml *)
     28  | rtl_st_return: label → rtl_statement.
    2929 
    3030definition rtl_statement_graph ≝ graph rtl_statement.
Note: See TracChangeset for help on using the changeset viewer.