Changeset 1240


Ignore:
Timestamp:
Sep 21, 2011, 5:24:43 PM (8 years ago)
Author:
sacerdot
Message:

Ported to common definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r1081 r1240  
    5858qed.
    5959
    60 definition simplify_funct ≝
    61   λid_def: ident × ?.
    62   let 〈id, def〉 ≝ id_def in
    63   let def' ≝
    64     match def with
    65     [ Internal def ⇒ Internal ? (simplify_internal def)
    66     | External def ⇒ External ? def
    67     ]
    68   in
    69     〈id, def'〉.
    70  
    71 definition tailcall_simplify ≝
    72   λp.
    73   let rtl_pr_vars' ≝ rtl_pr_vars p in
    74   let rtl_pr_functs' ≝ map ? ? simplify_funct (rtl_pr_functs p) in
    75   let rtl_pr_main' ≝ rtl_pr_main p in
    76     mk_rtl_program rtl_pr_vars' rtl_pr_functs' rtl_pr_main'.
     60definition tailcall_simplify : rtl_program → rtl_program ≝
     61 λp. transform_program … p (transf_fundef … simplify_internal).
Note: See TracChangeset for help on using the changeset viewer.