 Timestamp:
 Sep 21, 2011, 5:24:43 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r1081 r1240 58 58 qed. 59 59 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'. 60 definition 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.