source: src/RTL/RTLTailcall.ma @ 2486

Last change on this file since 2486 was 2286, checked in by tranquil, 9 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 1.7 KB
RevLine 
[784]1include "RTL/RTL.ma".
2
3definition simplify_stmt ≝
[1270]4  λglobals.
[784]5  λexit: label.
6  λlbl: label.
[2286]7  λstmt: joint_statement RTL globals.
8  λgraph: codeT RTL_ntc globals.
[784]9  match stmt with
[2286]10  [ final fin ⇒
11     match fin with
12      [ tailcall ext ⇒
[1270]13         match ext with
[2286]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          ]
[1270]19      | _ ⇒ graph ]
20  | _ ⇒ graph ].
[1081]21
[784]22definition simplify_graph ≝
[1270]23  λglobals.
[1081]24  λexit: label.
[2286]25  λgraph: codeT RTL globals.
[1275]26    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
[1081]27
28axiom simplify_graph_preserves_labels:
[1270]29  ∀globals.
[2286]30  ∀g: codeT RTL globals.
[1081]31  ∀exit: label.
[2286]32  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
[784]33   
[1270]34definition simplify_internal :
35 ∀globals.
[2286]36  joint_internal_function RTL globals →
37   joint_internal_function RTL_ntc globals
[1270]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
[1081]48qed.
[784]49
[2286]50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
[2103]51 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracBrowser for help on using the repository browser.