Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (9 years ago)
Author:
tranquil
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r2103 r2286  
    55  λexit: label.
    66  λlbl: label.
    7   λstmt: rtl_statement globals.
    8   λgraph: codeT … (rtlntc_params globals).
     7  λstmt: joint_statement RTL globals.
     8  λgraph: codeT RTL_ntc globals.
    99  match stmt with
    10   [ sequential seq DUMMY
    11      match seq with
    12       [ extension ext ⇒
     10  [ final fin
     11     match fin with
     12      [ tailcall ext ⇒
    1313         match ext with
    14           [ rtl_st_ext_tailcall_id f args ⇒
    15               add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
    16           | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
    17               add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
    18           | _ ⇒ graph ]
     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          ]
    1919      | _ ⇒ graph ]
    2020  | _ ⇒ graph ].
     
    2323  λglobals.
    2424  λexit: label.
    25   λgraph: codeT … (rtl_params globals).
     25  λgraph: codeT RTL globals.
    2626    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2727
    2828axiom simplify_graph_preserves_labels:
    2929  ∀globals.
    30   ∀g: codeT … (rtl_params globals).
    31   ∀l: label.
     30  ∀g: codeT RTL globals.
    3231  ∀exit: label.
    33     lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
     32  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
    3433   
    3534definition simplify_internal :
    3635 ∀globals.
    37   joint_internal_function … (rtl_params globals)
    38    joint_internal_function … (rtlntc_params globals)
     36  joint_internal_function RTL globals
     37   joint_internal_function RTL_ntc globals
    3938
    4039  λglobals,def.
     
    4948qed.
    5049
    51 definition tailcall_simplify : rtl_program → rtlntc_program ≝
     50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
    5251 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracChangeset for help on using the changeset viewer.