Ignore:
Timestamp:
Sep 26, 2011, 3:59:28 PM (8 years ago)
Author:
sacerdot
Message:

Making RTL syntax an instance of Joint.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r1240 r1270  
    22
    33definition simplify_stmt ≝
     4  λglobals.
    45  λexit: label.
    56  λlbl: label.
    6   λstmt.
    7   λgraph: rtl_statement_graph.
     7  λstmt: rtl_statement globals.
     8  λgraph: codeT … (rtl_params globals).
    89  match stmt with
    9   [ rtl_st_tailcall_id f args ⇒
    10       add ? ? graph lbl (rtl_st_call_id f args [ ] exit)
    11   | rtl_st_tailcall_ptr f1 f2 args ⇒
    12       add ? ? graph lbl (rtl_st_call_ptr f1 f2 args [ ] exit)
    13   | _ ⇒ graph
    14   ].
     10  [ joint_st_sequential seq DUMMY ⇒
     11     match seq with
     12      [ joint_instr_extension ext ⇒
     13         match ext with
     14          [ rtl_st_ext_tailcall_id f args ⇒
     15              add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit)
     16          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
     17              add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtl_st_ext_call_ptr f1 f2 args [ ])) exit)
     18          | _ ⇒ graph ]
     19      | _ ⇒ graph ]
     20  | _ ⇒ graph ].
    1521
    1622definition simplify_graph ≝
     23  λglobals.
    1724  λexit: label.
    18   λgraph: rtl_statement_graph.
    19     foldi ? ? ? (simplify_stmt exit) graph graph.
     25  λgraph: codeT … (rtl_params globals).
     26    foldi ? ? ? (simplify_stmt globals exit) graph graph.
    2027
    2128axiom simplify_graph_preserves_labels:
    22   ∀g: rtl_statement_graph.
     29  ∀globals.
     30  ∀g: codeT … (rtl_params globals).
    2331  ∀l: label.
    2432  ∀exit: label.
    25     lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.
     33    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
    2634   
    27 definition simplify_internal ≝
    28   λdef.
    29     let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    30     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    31     let rtl_if_result' ≝ rtl_if_result def in
    32     let rtl_if_params' ≝ rtl_if_params def in
    33     let rtl_if_locals' ≝ rtl_if_locals def in
    34     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    35     let rtl_if_graph' ≝ simplify_graph (rtl_if_exit def) (rtl_if_graph def) in
    36     let rtl_if_entry' ≝ rtl_if_entry def in
    37     let rtl_if_exit' ≝ rtl_if_exit def in
    38       mk_rtl_internal_function
    39         rtl_if_luniverse' rtl_if_runiverse'
    40         rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
    41         rtl_if_graph' ? ?.
    42   normalize nodelta
    43   [1: cases rtl_if_entry'
    44       #ENTRY #ENTRY_PRF
    45       %
    46       [1: @ENTRY
    47       |2: @simplify_graph_preserves_labels
    48           @ENTRY_PRF
    49       ]
    50   |2: cases rtl_if_exit'
    51       #EXIT #EXIT_PRF
    52       %
    53       [1: @EXIT
    54       |2: @simplify_graph_preserves_labels
    55           @EXIT_PRF
    56       ]
    57   ]
     35definition simplify_internal :
     36 ∀globals.
     37  joint_internal_function … (rtl_params globals) →
     38   joint_internal_function … (rtl_params globals)
     39
     40  λglobals,def.
     41    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
     42      mk_joint_internal_function …
     43       (joint_if_luniverse … def) (joint_if_runiverse … def)
     44       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
     45       (joint_if_stacksize … def) graph
     46       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
     47 [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
     48 #l #IH @simplify_graph_preserves_labels @IH
    5849qed.
    5950
    6051definition tailcall_simplify : rtl_program → rtl_program ≝
    61  λp. transform_program … p (transf_fundef … simplify_internal).
     52 λp. transform_program … p (transf_fundef … (simplify_internal …)).
Note: See TracChangeset for help on using the changeset viewer.