Changeset 1252 for src/RTL


Ignore:
Timestamp:
Sep 22, 2011, 2:49:18 PM (8 years ago)
Author:
sacerdot
Message:

graph_params added to joint/Joint.ma, together with useful common setters/getters

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1250 r1252  
    33include "common/Identifiers.ma".
    44include "ERTL/ERTL.ma".
    5 include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
    6                      
    7 definition add_graph ≝
    8   λglobals.λl: label.λstmt.λp: joint_internal_function … (ertl_params globals).
    9    let code ≝ add … (joint_if_code … p) l stmt in
    10     mk_joint_internal_function … (ertl_params globals)
    11      (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    12      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    13      code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
    14   normalize nodelta;
    15   [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
    16   #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
    17 qed.
    185                           
    196definition fresh_label ≝
     
    2512  match e with
    2613  [ joint_st_goto _ ⇒ joint_st_goto … l
    27   | joint_st_return ⇒ joint_st_return …
    28   | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l
    29   | joint_st_extension ].
    30   | ertl_st_comment s _ ⇒ ertl_st_comment s l
    31   | ertl_st_cost c _ ⇒ ertl_st_cost c l
    32   | ertl_st_get_hdw r1 r2 _ ⇒ ertl_st_get_hdw r1 r2 l
    33   | ertl_st_set_hdw r1 r2 _ ⇒ ertl_st_set_hdw r1 r2 l
    34   | ertl_st_hdw_to_hdw r1 r2 _ ⇒ ertl_st_hdw_to_hdw r1 r2 l
    35   | ertl_st_new_frame _ ⇒ ertl_st_new_frame l
    36   | ertl_st_del_frame _ ⇒ ertl_st_del_frame l
    37   | ertl_st_frame_size r _ ⇒ ertl_st_frame_size r l
    38   | ertl_st_pop r _ ⇒ ertl_st_pop r l
    39   | ertl_st_push r _ ⇒ ertl_st_push r l
    40   | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
    41   | ertl_st_int r i _ ⇒ ertl_st_int r i l
    42   | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    43   | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
    44   | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    45   | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
    46   | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
    47   | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
    48   | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
    49   | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
    50   | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
    51   | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
    52   | ertl_st_return ⇒ ertl_st_return
    53   ].
    54  
     14  | joint_st_return ⇒ joint_st_return ??
     15  | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l].
     16
     17(* 
    5518let rec adds_graph
    5619  (stmt_list: list ertl_statement) (start_lbl: label)
     
    8548    ]
    8649  ].
     50*)
    8751
    8852axiom register_fresh: universe RegisterTag → register.
Note: See TracChangeset for help on using the changeset viewer.