Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (10 years ago)
Author:
campbell
Message:

Merge trunk to branch.

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

Legend:

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

  • Deliverables/D3.3/id-lookup-branch/ERTL/ERTL.ma

    r1153 r1197  
    11include "ASM/I8051.ma".
     2include "joint/Joint.ma".
    23include "utilities/BitVectorTrieSet.ma".
    34include "utilities/IdentifierTools.ma".
     
    89definition registers ≝ list register.
    910
    10 inductive ertl_statement: Type[0] ≝
    11   | ertl_st_skip: label → ertl_statement
    12   | ertl_st_comment: String → label → ertl_statement
    13   | ertl_st_cost: costlabel → label → ertl_statement
    14   | ertl_st_get_hdw: register → Register → label → ertl_statement
    15   | ertl_st_set_hdw: Register → register → label → ertl_statement
    16   | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
    17   | ertl_st_new_frame: label → ertl_statement
    18   | ertl_st_del_frame: label → ertl_statement
    19   | ertl_st_frame_size: register → label → ertl_statement
    20   | ertl_st_pop: register → label → ertl_statement
    21   | ertl_st_push: register → label → ertl_statement
    22   | ertl_st_addr: register → register → ident → label → ertl_statement
    23 (* XXX: changed from O'Caml
    24   | ertl_st_addr_h: register → ident → label → ertl_statement
    25   | ertl_st_addr_l: register → ident → label → ertl_statement
    26 *)
    27   | ertl_st_int: register → Byte → label → ertl_statement
    28   | ertl_st_move: register → register → label → ertl_statement
    29   | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    30 (* XXX: changed from O'Caml
    31   | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
    32   | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
    33 *)
    34   | ertl_st_op1: Op1 → register → register → label → ertl_statement
    35   | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    36   | ertl_st_clear_carry: label → ertl_statement
    37   | ertl_st_set_carry: label → ertl_statement
    38   | ertl_st_load: register → register → register → label → ertl_statement
    39   | ertl_st_store: register → register → register → label → ertl_statement
    40   | ertl_st_call_id: ident → nat → label → ertl_statement
    41   | ertl_st_cond: register → label → label → ertl_statement
    42   | ertl_st_return: ertl_statement.
     11inductive move_registers: Type[0] ≝
     12  | pseudo: register → move_registers
     13  | hardware: Register → move_registers.
     14                 
     15inductive ertl_statement_extension: Type[0] ≝
     16  | ertl_st_ext_new_frame: label → ertl_statement_extension
     17  | ertl_st_ext_del_frame: label → ertl_statement_extension
     18  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    4319
    44 definition ertl_statement_graph ≝ graph ertl_statement.
     20definition ertl_params: params ≝
     21 mk_params
     22   register register register register
     23     (move_registers × move_registers) register
     24       ertl_statement_extension unit (list register) nat.
    4525
    46 record ertl_internal_function: Type[0] ≝
     26definition ertl_statement ≝ joint_statement ertl_params.
     27
     28definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
     29
     30record ertl_internal_function (globals: list ident): Type[0] ≝
    4731{
    4832  ertl_if_luniverse: universe LabelTag;
     
    5135  ertl_if_locals: registers;
    5236  ertl_if_stacksize: nat;
    53   ertl_if_graph: ertl_statement_graph;
     37  ertl_if_graph: ertl_statement_graph globals;
    5438  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    5539  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    5640}.
    5741
    58 definition ertl_function ≝ fundef ertl_internal_function.
     42definition set_luniverse ≝
     43  λglobals  : list ident.
     44  λint_fun  : ertl_internal_function globals.
     45  λluniverse: universe LabelTag.
     46  let runiverse ≝ ertl_if_runiverse globals int_fun in
     47  let params    ≝ ertl_if_params globals int_fun in
     48  let locals    ≝ ertl_if_locals globals int_fun in
     49  let stacksize ≝ ertl_if_stacksize globals int_fun in
     50  let graph     ≝ ertl_if_graph globals int_fun in
     51  let entry     ≝ ertl_if_entry globals int_fun in
     52  let exit      ≝ ertl_if_exit globals int_fun in
     53    mk_ertl_internal_function globals
     54      luniverse runiverse params locals
     55      stacksize graph entry exit.
     56
     57definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    5958 
    60 record ertl_program: Type[0] ≝
     59record ertl_program (globals: list ident): Type[0] ≝
    6160{
    6261  ertl_pr_vars: list (ident × nat);
    63   ertl_pr_funcs: list (ident × ertl_function);
     62  ertl_pr_funcs: list (ident × (ertl_function globals));
    6463  ertl_pr_main: option ident
    6564}.
     65
     66
     67(* XXX: changed from O'Caml
     68  | ertl_st_addr_h: register → ident → label → ertl_statement
     69  | ertl_st_addr_l: register → ident → label → ertl_statement
     70*)
     71
     72(* XXX: changed from O'Caml
     73  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
     74  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
     75*)
Note: See TracChangeset for help on using the changeset viewer.