Changeset 1091 for Deliverables


Ignore:
Timestamp:
Jul 28, 2011, 12:14:17 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into id-lookup-branch

Location:
Deliverables/D3.3/id-lookup-branch
Files:
7 edited
2 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

    • Property svn:mergeinfo set to
      /srcmergedeligible
  • Deliverables/D3.3/id-lookup-branch/ASM

    • Property svn:mergeinfo changed
      /src/ASM (added)merged: 1089
  • Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma

    r1075 r1091  
    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
  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTLToLTL.ma

    r1084 r1091  
    22include "ERTL/ERTLToLTLI.ma".
    33include "LTL/LTL.ma".
     4
     5definition translate_internal ≝
     6  λf.
     7  λint_fun: ertl_internal_function.
     8    mk_ltl_internal_function ?
     9      (ertl_if_luniverse int_fun)
     10      (ertl_if_runiverse int_fun)
     11      (ertl_if_stacksize int_fun)
     12      (ertl_if_graph int_fun)
     13      ?
     14      ?.
    415
    516definition translate_funct ≝
  • Deliverables/D3.3/id-lookup-branch/LIN/JointLTLLIN.ma

    r1082 r1091  
    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.
  • Deliverables/D3.3/id-lookup-branch/LTL/LTL.ma

    r1082 r1091  
    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).
  • Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma

    r1071 r1091  
    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.