source: src/RTL/RTLTailcall_paolo.ma @ 2214

Last change on this file since 2214 was 2214, checked in by tranquil, 8 years ago
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File size: 1.7 KB
Line 
1include "RTL/RTL_paolo.ma".
2
3definition simplify_stmt ≝
4  λglobals.
5  λexit: label.
6  λlbl: label.
7  λstmt: joint_statement RTL globals.
8  λgraph: codeT RTL_ntc globals.
9  match stmt with
10  [ final fin ⇒
11     match fin with
12      [ tailcall ext ⇒
13         match ext with
14          [ rtl_tailcall_id f args ⇒
15              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
16          | rtl_tailcall_ptr f1 f2 args ⇒
17              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
18          ]
19      | _ ⇒ graph ]
20  | _ ⇒ graph ].
21
22definition simplify_graph ≝
23  λglobals.
24  λexit: label.
25  λgraph: codeT RTL globals.
26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
27
28axiom simplify_graph_preserves_labels:
29  ∀globals.
30  ∀g: codeT RTL globals.
31  ∀exit: label.
32  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
33   
34definition simplify_internal :
35 ∀globals.
36  joint_internal_function RTL globals →
37   joint_internal_function RTL_ntc globals
38
39  λglobals,def.
40    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
41      mk_joint_internal_function …
42       (joint_if_luniverse … def) (joint_if_runiverse … def)
43       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
44       (joint_if_stacksize … def) graph
45       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
46 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
47 #l #IH @simplify_graph_preserves_labels @IH
48qed.
49
50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
51 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracBrowser for help on using the repository browser.