Changeset 1307 for src/RTLabs


Ignore:
Timestamp:
Oct 6, 2011, 2:08:53 PM (8 years ago)
Author:
mulligan
Message:

adding translate_cst

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1306 r1307  
    127127  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
    128128
    129 (*CSC: XXXXX *)
    130 axiom translate_cst:
    131   ∀globals.
    132   ∀cst: constant.
    133   ∀destrs: list register.
    134   ∀start_lbl: label.
    135   ∀dest_lbl: label.
    136   ∀def: rtl_internal_function globals.
    137     rtl_internal_function globals.
    138 
     129let rec translate_cst
     130  (globals: list ident) (cst: constant) (destrs: list register)
     131    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
     132      on cst: rtl_internal_function globals ≝
     133  match cst with
     134  [ Ointconst size const ⇒
     135    match destrs with
     136    [ nil        ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
     137    | cons hd tl ⇒ ?
     138    ]
     139  | Ofloatconst float ⇒ ⊥
     140  | Oaddrsymbol id offset ⇒ ?
     141  | Oaddrstack offset ⇒ ?
     142  ].
     143  [5: cases not_implemented (* XXX: float, error_float in o'caml *)
     144  ].
     145 
    139146definition translate_move_internal ≝
    140147  λglobals.
     
    10291036  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
    10301037    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
     1038    (* XXX: should we be ignoring this? *)
    10311039  | St_load ignore addr destr lbl' ⇒
    10321040    translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
     1041    (* XXX: should we be ignoring this? *)
    10331042  | St_store ignore addr srcr lbl' ⇒
    10341043    translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
  • src/RTLabs/syntax.ma

    r1224 r1307  
    1 
    21include "basics/logic.ma".
    32
Note: See TracChangeset for help on using the changeset viewer.