Changeset 2675 for src/ERTLptr


Ignore:
Timestamp:
Feb 18, 2013, 6:26:22 PM (7 years ago)
Author:
tranquil
Message:
  • a generic graph program transformation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2674 r2675  
    3939definition translate_step:
    4040 ∀globals.
     41 unit →
    4142 label
    4243  →joint_step ERTL globals
    4344   →bind_step_block ERTLptr globals ≝
    44  λglobals.λl.λs.
     45 λglobals.λ_.λl.λs.
    4546match s return λ_.bind_step_block ERTLptr globals with
    4647[ CALL called args dest ⇒
     
    6869definition translate_fin_step:
    6970 ∀globals.
     71 unit →
    7072 label
    7173  →joint_fin_step ERTL
    7274   →bind_fin_block ERTLptr globals ≝
    73  λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
    74 
    75 definition translate_internal :  ∀globals: list ident.
    76   joint_closed_internal_function ERTL globals →
    77   joint_closed_internal_function ERTLptr globals ≝
    78   λglobals,int_fun.
    79   (* initialize internal function *)
    80   b_graph_translate ERTL ERTLptr globals
    81     (joint_if_result … int_fun)
    82     (joint_if_params … int_fun)
    83     (joint_if_stacksize … int_fun)
    84     (translate_step …)
    85     (translate_fin_step …)
    86     int_fun.
    87 cases daemon.
    88 qed.
     75 λglobals.λ_.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
    8976
    9077definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    91   λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
     78  b_graph_transform_program ERTL ERTLptr (λ_.unit)
     79  (λglobals,int_fun.
     80    〈〈joint_if_result … int_fun,
     81      joint_if_params … int_fun,
     82      joint_if_stacksize … int_fun〉,
     83    it〉)
     84  translate_step
     85  translate_fin_step.
Note: See TracChangeset for help on using the changeset viewer.