Changeset 759 for src/ERTL


Ignore:
Timestamp:
Apr 18, 2011, 5:32:46 PM (10 years ago)
Author:
mulligan
Message:

More work on the RTL to ERTL pass.

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r756 r759  
    1414
    1515inductive ertl_statement: Type[0] ≝
    16   | ertl_st_skip: ident → ertl_statement
    17   | ertl_st_comment: String → ident → ertl_statement
    18   | ertl_st_cost: costlabel → ident → ertl_statement
    19   | ertl_st_get_hdw: register → abstract_register → ident → ertl_statement
    20   | ertl_st_set_hdw: abstract_register → register → ident → ertl_statement
    21   | ertl_st_hdw_to_hdw: register → register → ident → ertl_statement
    22   | ertl_st_new_frame: ident → ertl_statement
    23   | ertl_st_del_frame: ident → ertl_statement
    24   | ertl_st_frame_size: abstract_register → ident → ertl_statement
    25   | ertl_st_pop: abstract_register → ident → ertl_statement
    26   | ertl_st_push: abstract_register → ident → ertl_statement
    27   | ertl_st_addr_h: abstract_register → ident → ident → ertl_statement
    28   | ertl_st_addr_l: abstract_register → ident → ident → ertl_statement
    29   | ertl_st_int: abstract_register → Byte → ident → ertl_statement
    30   | ertl_st_move: abstract_register → abstract_register → ident → ertl_statement
    31   | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → ident → ertl_statement
    32   | ertl_st_op1: Op1 → abstract_register → abstract_register → ident → ertl_statement
    33   | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → ident → ertl_statement
    34   | ertl_st_clear_carry: ident → ertl_statement
    35   | ertl_st_load: abstract_register → abstract_register → abstract_register → ident → ertl_statement
    36   | ertl_st_store: abstract_register → abstract_register → abstract_register → ident → ertl_statement
    37   | ertl_st_call_id: ident → Byte → ident → ertl_statement
    38   | ertl_st_cond_acc: abstract_register → ident → ident → ertl_statement
     16  | ertl_st_skip: label → ertl_statement
     17  | ertl_st_comment: String → label → ertl_statement
     18  | ertl_st_cost: costlabel → label → ertl_statement
     19  | ertl_st_get_hdw: register → abstract_register → label → ertl_statement
     20  | ertl_st_set_hdw: abstract_register → register → label → ertl_statement
     21  | ertl_st_hdw_to_hdw: register → register → label → ertl_statement
     22  | ertl_st_new_frame: label → ertl_statement
     23  | ertl_st_del_frame: label → ertl_statement
     24  | ertl_st_frame_size: abstract_register → label → ertl_statement
     25  | ertl_st_pop: abstract_register → label → ertl_statement
     26  | ertl_st_push: abstract_register → label → ertl_statement
     27  | ertl_st_addr_h: abstract_register → label → label → ertl_statement
     28  | ertl_st_addr_l: abstract_register → label → label → ertl_statement
     29  | ertl_st_int: abstract_register → Byte → label → ertl_statement
     30  | ertl_st_move: abstract_register → abstract_register → label → ertl_statement
     31  | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → label → ertl_statement
     32  | ertl_st_op1: Op1 → abstract_register → abstract_register → label → ertl_statement
     33  | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → label → ertl_statement
     34  | ertl_st_clear_carry: label → ertl_statement
     35  | ertl_st_load: abstract_register → abstract_register → abstract_register → label → ertl_statement
     36  | ertl_st_store: abstract_register → abstract_register → abstract_register → label → ertl_statement
     37  | ertl_st_call_id: label → Byte → label → ertl_statement
     38  | ertl_st_cond_acc: abstract_register → label → label → ertl_statement
    3939  | ertl_st_return: abstract_registers → ertl_statement.
    4040
     
    4848  ertl_if_locals: registers;
    4949  ertl_if_graph: ertl_statement_graph;
    50   ertl_if_entry: ident;
    51   ertl_if_exit: ident
     50  ertl_if_entry: label;
     51  ertl_if_exit: label
    5252}.
     53
     54definition ertl_if_params: ertl_internal_function → nat.
     55  # E
     56  cases E
     57  # H1 # H2 # H3 # H4 # H5 # H6 # H7
     58  @ H3
     59qed.
    5360
    5461inductive ertl_function: Type[0] ≝
     
    6067  ertl_pr_vars: list (ident × nat);
    6168  ertl_pr_funcs: list (ident × ertl_function);
    62   ertl_pr_main: option ident
     69  ertl_pr_main: option label
    6370}.
    6471
  • src/ERTL/ERTLToLTL.ma

    r757 r759  
    22include "LTL/LTL.ma".
    33 
    4 axiom translate_ERTL_func:
     4axiom translate_ertl_func:
    55  ∀globals: list ident.
    66    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
Note: See TracChangeset for help on using the changeset viewer.