Changeset 1081 for src/RTL/RTLTailcall.ma
 Timestamp:
 Jul 20, 2011, 11:26:21 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLTailcall.ma
r1080 r1081 1 1 include "RTL/RTL.ma". 2 3 (* dpm: this should not be option, fix *)4 axiom map_fold:5 ∀A, B: Type[0].6 ∀f: label → A → B → option B.7 ∀m: rtl_statement_graph.8 ∀b: B.9 B.10 2 11 3 definition simplify_stmt ≝ … … 21 13  _ ⇒ graph 22 14 ]. 23 24 definition lift_option3: ∀A, B, C, D. ∀f: A → B → C → D. A → B → C → option D ≝ 25 λA, B, C, D: Type[0]. 26 λf: A → B → C → D. 27 λa: A. 28 λb: B. 29 λc: C. 30 Some ? (f a b c). 31 15 32 16 definition simplify_graph ≝ 33 λexit .17 λexit: label. 34 18 λgraph: rtl_statement_graph. 35 map_fold ? ? (lift_option3 ? ? ? ? (simplify_stmt exit)) graph graph. 19 foldi ? ? ? (simplify_stmt exit) graph graph. 20 21 axiom simplify_graph_preserves_labels: 22 ∀g: rtl_statement_graph. 23 ∀l: label. 24 ∀exit: label. 25 lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?. 36 26 37 27 definition simplify_internal ≝ … … 50 40 rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize' 51 41 rtl_if_graph' ? ?. 52 [1: normalize nodelta; 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 ] 58 qed. 53 59 54 60 definition simplify_funct ≝ … … 57 63 let def' ≝ 58 64 match def with 59 [ rtl_f_internal def ⇒ rtl_f_internal (simplify_internal def) 60  rtl_f_external def ⇒ rtl_f_external def 61 ] in 62 〈id, def'〉. 65 [ Internal def ⇒ Internal ? (simplify_internal def) 66  External def ⇒ External ? def 67 ] 68 in 69 〈id, def'〉. 63 70 64 71 definition tailcall_simplify ≝
Note: See TracChangeset
for help on using the changeset viewer.