Changeset 2570 for src/ERTLptr


Ignore:
Timestamp:
Jan 5, 2013, 1:41:13 PM (7 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place

Location:
src/ERTLptr
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2566 r2570  
    1717include "joint/TranslateUtils.ma".
    1818
     19definition translate_step_seq :
     20∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝
     21λglobals,s.
     22match s with
     23[COMMENT s ⇒ COMMENT ERTLptr … s
     24|COST_LABEL c ⇒ COST_LABEL ERTLptr … c
     25|MOVE a  ⇒ MOVE ERTLptr … a
     26|POP a ⇒ POP ERTLptr … a
     27|PUSH a ⇒ PUSH ERTLptr … a
     28|ADDRESS i H reg1 reg2 ⇒ ADDRESS ERTLptr … i H reg1 reg2
     29|OPACCS op reg1 reg2 reg3 reg4 ⇒ OPACCS ERTLptr … op reg1 reg2 reg3 reg4
     30|OP1 op reg1 reg2 ⇒ OP1 ERTLptr … op reg1 reg2
     31|OP2 op reg1 reg2 arg ⇒ OP2 ERTLptr … op reg1 reg2 arg
     32|CLEAR_CARRY ⇒ CLEAR_CARRY ERTLptr ?
     33|SET_CARRY ⇒ SET_CARRY ERTLptr ?
     34|LOAD reg1 reg2 reg3 ⇒ LOAD ERTLptr … reg1 reg2 reg3
     35|STORE arg1 arg2 reg ⇒ STORE ERTLptr … arg1 arg2 reg
     36|extension_seq s ⇒ extension_seq ERTLptr … (ertlptr_ertl s)
     37].
     38
     39
    1940(* PAOLO: implement the b_graph_translate2 that expects functions that
    2041   return not (list instr * instr) but (list (label → instr) * instr) *)
     
    2445  →joint_step ERTL globals
    2546   →bind_seq_block ERTLptr globals (joint_step ERTLptr globals) ≝
    26  λglobals.λl.λs.?.
    27 cases s
    28 [ #called #args #dest cases called
    29   [ (*#_*) #id % %{[]} %1 [%1{id}] assumption
    30   | (*#pc*) #dest1 %2 #reg %1 @(〈[?;?;?;?], ?〉)
    31     [ @extension_seq @(LOW_ADDRESS reg ?(*pc*)) cases daemon
    32     | @(PUSH … (Reg … reg))
    33     | @extension_seq @(HIGH_ADDRESS reg ?(*pc*)) cases daemon
    34     | @(PUSH … (Reg … reg))
    35     | %1 [%2{dest1}] assumption
    36     ]]
    37 | (*#_*) #reg #l %{[]} %2 assumption
    38 | (*#_*) #X %1 %{[]} %3 cases X
    39   try (#a #b #c #d #e) try (#a #b #c #d) try (#a #b #c) try (#a #b) try #a
    40   [%1|%2|%3|%4|%5|%6|%7|%8|%9|%10|%11|%12|%13|%14] try assumption
    41   %1 @a ]
    42 qed.
     47 λglobals.λl.λs.
     48match s with
     49[ CALL called args dest ⇒
     50    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〉
     56    ]
     57| COND reg l ⇒ bret … 〈[],COND ERTLptr ? reg l〉
     58| step_seq x ⇒ bret … 〈[],step_seq ERTLptr ? (translate_step_seq … x)〉
     59].
     60cases daemon (*TO BE COMPLETED *)
     61qed.
    4362
    44 definition joint_fin_step_id: joint_fin_step ERTL → joint_fin_step ERTLptr.
    45  * [#l %1 @l | %2 | #H #arg #arg' %3 assumption ]
    46 qed.
     63definition joint_fin_step_id: joint_fin_step ERTL → joint_fin_step ERTLptr ≝
     64λs.
     65match s with
     66[GOTO l ⇒ GOTO ERTLptr … l
     67|RETURN  ⇒ RETURN ERTLptr
     68|TAILCALL H arg arg' ⇒ TAILCALL ERTLptr … H arg arg'
     69].
     70
    4771
    4872(*CSC: cut&paste from RTLtoERTL up to ERTLptr :-( keep just one copy*)
Note: See TracChangeset for help on using the changeset viewer.