Ignore:
Timestamp:
Feb 5, 2013, 10:49:42 PM (8 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2592 r2604  
    1717include "joint/TranslateUtils.ma".
    1818 
    19 definition translate_step_seq :
     19definition seq_embed :
    2020∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝
    2121λglobals,s.
     
    4444 label
    4545  →joint_step ERTL globals
    46    →bind_seq_block ERTLptr globals (joint_step ERTLptr globals)
     46   →bind_step_block ERTLptr globals
    4747 λglobals.λl.λs.
    48 match s with
    49 [ CALL called args dest ⇒ 
     48match s return λ_.bind_step_block ERTLptr globals with
     49[ CALL called args dest ⇒
    5050    match called with
    51     [inl id ⇒ bret … 〈[ ],CALL ERTLptr ? (inl … id) args dest〉
    52     |inr dest1 ⇒ νreg in bret … 〈[extension_seq ERTLptr ? (LOW_ADDRESS reg ?);
    53                                   PUSH … (Reg … reg);
    54                                   extension_seq ERTLptr ? (HIGH_ADDRESS reg ?);
    55                                   PUSH … (Reg … reg)],CALL ERTLptr ? (inr … dest1) args dest〉
     51    [inl id ⇒ bret … [CALL ERTLptr ? (inl … id) args dest]
     52    |inr dest1 ⇒ νreg in bret … «[λl.(extension_seq ERTLptr ? (LOW_ADDRESS reg l) : joint_step ??);
     53                                  λ_.PUSH ERTLptr … (Reg … reg);
     54                                  λl.extension_seq ERTLptr ? (HIGH_ADDRESS reg l);
     55                                  λ_.PUSH ERTLptr … (Reg … reg) ;
     56                                  λ_.CALL ERTLptr ? (inr … dest1) args dest], ?»
    5657    ]
    57 | COND reg l ⇒ bret … 〈[],COND ERTLptr ? reg l〉
    58 | step_seq x ⇒ bret … 〈[],step_seq ERTLptr ? (translate_step_seq … x)〉
    59 ].
    60 cases daemon (*TO BE COMPLETED *)
    61 qed.
     58| COND reg l ⇒ bret … [COND ERTLptr ? reg l]
     59| step_seq x ⇒ bret … [seq_embed … x]
     60]. @I qed.
    6261
    63 definition joint_fin_step_id: joint_fin_step ERTL → joint_fin_step ERTLptr ≝
     62definition fin_step_embed: joint_fin_step ERTL → joint_fin_step ERTLptr ≝
    6463λs.
    6564match s with
     
    6968].
    7069
    71 
    72 (*CSC: cut&paste from RTLtoERTL up to ERTLptr :-( keep just one copy*)
    73 definition ertl_fresh_reg:
    74  ∀globals.freshT ERTLptr globals register ≝
    75   λglobals,def.
    76     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    77     〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     70definition translate_fin_step:
     71 ∀globals.
     72 label
     73  →joint_fin_step ERTL
     74   →bind_fin_block ERTLptr globals ≝
     75 λglobals.λl.λs.bret … 〈[ ], fin_step_embed … s〉.
    7876
    7977definition translate_internal :  ∀globals: list ident.
     
    8785    (joint_if_result … int_fun)
    8886    (joint_if_params … int_fun)
    89     (joint_if_locals … int_fun)
    9087    (joint_if_stacksize … int_fun)
    91     (joint_if_entry … int_fun)
    92     (joint_if_exit … int_fun) in
     88    (joint_if_entry … int_fun) in
    9389  b_graph_translate …
    94     (ertl_fresh_reg …)
    9590    init
    9691    (translate_step …)
    97     (λ_.λstep.bret ?? 〈[],joint_fin_step_id step〉)
     92    (translate_fin_step …)
    9893    int_fun.
    9994cases daemon.
Note: See TracChangeset for help on using the changeset viewer.