Ignore:
Timestamp:
Jul 20, 2011, 11:26:21 AM (10 years ago)
Author:
mulligan
Message:

completed rtl-ertl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r1080 r1081  
    11include "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.
    102
    113definition simplify_stmt ≝
     
    2113  | _ ⇒ graph
    2214  ].
    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
    3216definition simplify_graph ≝
    33   λexit.
     17  λexit: label.
    3418  λgraph: rtl_statement_graph.
    35     map_fold ? ? (lift_option3 ? ? ? ? (simplify_stmt exit)) graph graph.
     19    foldi ? ? ? (simplify_stmt exit) graph graph.
     20
     21axiom 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 ?.
    3626   
    3727definition simplify_internal ≝
     
    5040        rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
    5141        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  ]
     58qed.
    5359
    5460definition simplify_funct ≝
     
    5763  let def' ≝
    5864    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'〉.
    6370 
    6471definition tailcall_simplify ≝
Note: See TracChangeset for help on using the changeset viewer.