Changeset 782 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Apr 28, 2011, 5:36:33 PM (9 years ago)
Author:
mulligan
Message:

More work on rtl-ertl pass from today, plus resolved conflict.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r777 r782  
    2121  | ertl_st_pop: register → label → ertl_statement
    2222  | ertl_st_push: register → label → ertl_statement
    23   | ertl_st_addr_h: register → label → label → ertl_statement
    24   | ertl_st_addr_l: register → label → label → ertl_statement
     23  | ertl_st_addr_h: register → ident → label → ertl_statement
     24  | ertl_st_addr_l: register → ident → label → ertl_statement
    2525  | ertl_st_int: register → Byte → label → ertl_statement
    2626  | ertl_st_move: register → register → label → ertl_statement
     
    3131  | ertl_st_load: register → register → register → label → ertl_statement
    3232  | ertl_st_store: register → register → register → label → ertl_statement
    33   | ertl_st_call_id: label → Byte → label → ertl_statement
     33  | ertl_st_call_id: ident → Byte → label → ertl_statement
    3434  | ertl_st_cond_acc: register → label → label → ertl_statement
    3535  | ertl_st_return: registers → ertl_statement.
     
    4343  ertl_if_params: nat;
    4444  ertl_if_locals: registers;
     45  ertl_if_stacksize: nat;
    4546  ertl_if_graph: ertl_statement_graph;
    4647  ertl_if_entry: label;
     
    5152  # E
    5253  cases E
    53   # H1 # H2 # H3 # H4 # H5 # H6 # H7
     54  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
    5455  @ H3
    5556qed.
    5657
     58definition ertl_if_stacksize: ertl_internal_function → nat.
     59  # E
     60  cases E
     61  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
     62  @ H5
     63qed.
     64
    5765inductive ertl_function: Type[0] ≝
    58   | ertl_fu_internal: ertl_internal_function → ertl_function
    59   | ertl_fu_external: external_function → ertl_function.
     66  | ertl_f_internal: ertl_internal_function → ertl_function
     67  | ertl_f_external: external_function → ertl_function.
    6068 
    6169record ertl_program: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.