Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (8 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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

    r1197 r1311  
    1 include "ASM/I8051.ma".
    21include "joint/Joint.ma".
    3 include "utilities/BitVectorTrieSet.ma".
    4 include "utilities/IdentifierTools.ma".
    5 include "common/Graphs.ma".
    6 include "common/CostLabel.ma".
    7 include "common/Registers.ma".
    8 
    9 definition registers ≝ list register.
    102
    113inductive move_registers: Type[0] ≝
     
    146                 
    157inductive 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.
     8  | ertl_st_ext_new_frame: ertl_statement_extension
     9  | ertl_st_ext_del_frame: ertl_statement_extension
     10  | ertl_st_ext_frame_size: register → ertl_statement_extension.
    1911
    20 definition 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.
     12definition ertl_params__: params__ ≝
     13 mk_params__ register register register register (move_registers × move_registers)
     14  register nat unit ertl_statement_extension.
     15definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
     16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
     17definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
     18definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
    2519
    26 definition ertl_statement ≝ joint_statement ertl_params.
     20definition ertl_statement ≝ joint_statement ertl_params_.
    2721
    28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
     22definition ertl_internal_function ≝
     23  λglobals.joint_internal_function … (ertl_params globals).
    2924
    30 record ertl_internal_function (globals: list ident): Type[0] ≝
    31 {
    32   ertl_if_luniverse: universe LabelTag;
    33   ertl_if_runiverse: universe RegisterTag;
    34   ertl_if_params: nat;
    35   ertl_if_locals: registers;
    36   ertl_if_stacksize: nat;
    37   ertl_if_graph: ertl_statement_graph globals;
    38   ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
    39   ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
    40 }.
    41 
    42 definition 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 
    57 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    58  
    59 record ertl_program (globals: list ident): Type[0] ≝
    60 {
    61   ertl_pr_vars: list (ident × nat);
    62   ertl_pr_funcs: list (ident × (ertl_function globals));
    63   ertl_pr_main: option ident
    64 }.
    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 *)
     25definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset for help on using the changeset viewer.