Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (8 years ago)
Author:
tranquil
Message:
  • 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall_paolo.ma

    r2162 r2214  
    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
    1010  [ final fin ⇒
     
    1313         match ext with
    1414          [ rtl_tailcall_id f args ⇒
    15               add … graph lbl (sequential … (CALL_ID rtlntc_params ? f args [ ]) exit)
     15              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
    1616          | rtl_tailcall_ptr f1 f2 args ⇒
    17               add … graph lbl (sequential rtlntc_params ? (rtl_call_ptr f1 f2 args [ ] : ext_call rtlntc_params) exit)
     17              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
    1818          ]
    1919      | _ ⇒ 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.
     30  ∀g: codeT RTL globals.
    3131  ∀exit: label.
    3232  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
     
    3434definition simplify_internal :
    3535 ∀globals.
    36   joint_internal_function globals rtl_params →
    37    joint_internal_function globals rtlntc_params
     36  joint_internal_function RTL globals →
     37   joint_internal_function RTL_ntc globals
    3838
    3939  λglobals,def.
     
    4848qed.
    4949
    50 definition tailcall_simplify : rtl_program → rtlntc_program ≝
     50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
    5151 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
Note: See TracChangeset for help on using the changeset viewer.