Changeset 1073
 Timestamp:
 Jul 15, 2011, 5:38:37 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1071 r1073 29 29 rtl_if_stacksize' rtl_if_graph' ? ?. 30 30 [1: cases(rtl_if_entry') 31 #LABEL #HYP 32 % 31 #LABEL #HYP % 33 32 [1: @LABEL 34 33 2: cases(HYP) 35 #STMT 36 #FRST_PRF 37 % 38 [1: @STMT 39 2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt) 40 ] 34 generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l); 35 /2/ 41 36 ] 42 37 2: cases(rtl_if_exit') 38 #LABEL #HYP % 39 [1: @LABEL 40 2: cases(HYP) 41 generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l); 42 /2/ 43 ] 44 ] 45 qed. 43 46 44 47 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝ … … 1219 1222 qed. 1220 1223 1224 axiom graph_add: 1225 ∀g: graph rtl_statement. 1226 ∀l: label. 1227 ∀s: rtl_statement. 1228 lookup ? ? (add ? ? g l s) l ≠ None ?. 1229 1230 (* XXX: we use a "hack" here to circumvent the proof obligations required to 1231 create res, an empty internal_function record. we insert into our graph 1232 the start and end nodes to ensure that they are in, and place dummy 1233 skip instructions at these nodes. *) 1221 1234 definition translate_internal ≝ 1222 1235 λdef. … … 1240 1253 let locals' ≝ locals in 1241 1254 let stack_size' ≝ f_stacksize def in 1242 let graph' ≝ empty_map ? ? in1243 1255 let entry' ≝ f_entry def in 1244 1256 let exit' ≝ f_exit def in 1257 let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in 1258 let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in 1245 1259 let res ≝ 1246 1260 mk_rtl_internal_function luniverse' runiverse' result' params' 1247 locals' stack_size' graph' entry' exit'in1261 locals' stack_size' graph' ? ? in 1248 1262 fold ? ? ? (translate_stmt lenv) (f_graph def) res. 1263 [1: % 1264 [1: @entry' 1265 2: normalize nodelta; 1266 @(graph_add ? (f_entry def) ?) 1267 @graph_add_lookup 1268 ] 1269 2: % 1270 [1: @exit' 1271 2: /2/ 1272 ] 1273 ] 1274 qed. 1249 1275 1250 1276 definition translate_fun_def ≝
Note: See TracChangeset
for help on using the changeset viewer.