Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r2286 r2490  
    44  λglobals.
    55  λexit: label.
    6   λlbl: label.
    76  λstmt: joint_statement RTL globals.
    8   λgraph: codeT RTL_ntc globals.
    97  match stmt with
    108  [ final fin ⇒
    119     match fin with
    12       [ tailcall ext ⇒
    13          match ext with
    14           [ rtl_tailcall_id f args ⇒
    15               add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
    16           | rtl_tailcall_ptr f1 f2 args ⇒
    17               add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
    18           ]
    19       | _ ⇒ graph ]
    20   | _ ⇒ graph ].
     10      [ TAILCALL _ f args ⇒ sequential … (CALL RTL_ntc ? f args [ ]) exit
     11      | RETURN ⇒ RETURN RTL_ntc
     12      | GOTO l ⇒ GOTO RTL_ntc l
     13      ]
     14  | sequential s next ⇒
     15    sequential RTL_ntc ?
     16    (match s return λ_.joint_step RTL_ntc globals with
     17    [ step_seq s ⇒
     18      match s return λ_.joint_seq RTL_ntc globals with
     19      [ COMMENT s ⇒ COMMENT … s
     20      | COST_LABEL l ⇒ COST_LABEL … l
     21      | MOVE m ⇒ MOVE … m
     22      | POP a ⇒ POP … a
     23      | PUSH a ⇒ PUSH … a
     24      | ADDRESS i prf dpl dph ⇒ ADDRESS … i prf dpl dph
     25      | OPACCS op a b arg1 arg2 ⇒ OPACCS … op a b arg1 arg2
     26      | OP1 op a arg ⇒ OP1 … op a arg
     27      | OP2 op a arg1 arg2 ⇒ OP2 … op a arg1 arg2
     28      | CLEAR_CARRY ⇒ CLEAR_CARRY ??
     29      | SET_CARRY ⇒ SET_CARRY ??
     30      | LOAD a dpl dph ⇒ LOAD … a dpl dph
     31      | STORE dpl dph a ⇒ STORE … dpl dph a
     32      | CALL f args dest ⇒ CALL … f args dest
     33      | extension_seq s ⇒ extension_seq … s
     34      ]
     35    | COND a ltrue ⇒ COND … a ltrue
     36    ]) next
     37  ].
     38
     39definition id_map_map : ∀tag,A,B.(A → B) → identifier_map tag A → identifier_map tag B ≝
     40λtag,A,B,f,m.
     41match m with
     42[ an_id_map m ⇒ an_id_map … (map … f m)
     43].
    2144
    2245definition simplify_graph ≝
     
    2447  λexit: label.
    2548  λgraph: codeT RTL globals.
    26     foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
     49  id_map_map … (simplify_stmt globals exit) graph.
    2750
    2851axiom simplify_graph_preserves_labels:
     
    3457definition simplify_internal :
    3558 ∀globals.
    36   joint_internal_function RTL globals →
    37    joint_internal_function RTL_ntc globals
     59  joint_closed_internal_function RTL globals →
     60   joint_closed_internal_function RTL_ntc globals
    3861
    3962  λglobals,def.
    4063    let graph ≝ simplify_graph … (joint_if_exit … def) (joint_if_code … def) in
    41       mk_joint_internal_function …
     64    «mk_joint_internal_function …
    4265       (joint_if_luniverse … def) (joint_if_runiverse … def)
    4366       (joint_if_result … def) (joint_if_params … def) (joint_if_locals … def)
    4467       (joint_if_stacksize … def) graph
    45        (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)).
    46  [ cases (joint_if_entry … def) | cases (joint_if_exit … def) ]
     68       (pi1 … (joint_if_entry … def)) (pi1 … (joint_if_exit … def)), ?».
     69 [3: cases daemon (* TODO *)
     70 | cases (joint_if_exit … def) | cases (joint_if_entry … def) ]
    4771 #l #IH @simplify_graph_preserves_labels @IH
    4872qed.
Note: See TracChangeset for help on using the changeset viewer.