Changeset 1307 for src/RTLabs
- Timestamp:
- Oct 6, 2011, 2:08:53 PM (9 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLAbstoRTL.ma
r1306 r1307 127 127 λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl. 128 128 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 129 let 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 139 146 definition translate_move_internal ≝ 140 147 λglobals. … … 1029 1036 | St_op2 op2 destr srcr1 srcr2 lbl' ⇒ 1030 1037 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? *) 1031 1039 | St_load ignore addr destr lbl' ⇒ 1032 1040 translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def 1041 (* XXX: should we be ignoring this? *) 1033 1042 | St_store ignore addr srcr lbl' ⇒ 1034 1043 translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def -
src/RTLabs/syntax.ma
r1224 r1307 1 2 1 include "basics/logic.ma". 3 2
Note: See TracChangeset
for help on using the changeset viewer.