Changeset 2675 for src/ERTLptr
 Timestamp:
 Feb 18, 2013, 6:26:22 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptr.ma
r2674 r2675 39 39 definition translate_step: 40 40 ∀globals. 41 unit → 41 42 label 42 43 →joint_step ERTL globals 43 44 →bind_step_block ERTLptr globals ≝ 44 λglobals.λ l.λs.45 λglobals.λ_.λl.λs. 45 46 match s return λ_.bind_step_block ERTLptr globals with 46 47 [ CALL called args dest ⇒ … … 68 69 definition translate_fin_step: 69 70 ∀globals. 71 unit → 70 72 label 71 73 →joint_fin_step ERTL 72 74 →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〉. 89 76 90 77 definition 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.