Changeset 1077 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Jul 19, 2011, 12:23:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1073 r1077 4 4 include "common/FrontEndOps.ma". 5 5 include "common/Graphs.ma". 6 7 axiom graph_add_lookup:8 ∀g: graph rtl_statement.9 ∀l: label.10 ∀s: rtl_statement.11 ∀to_insert: label.12 lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.13 6 14 7 definition add_graph ≝ … … 32 25 [1: @LABEL 33 26 2: cases(HYP) 34 generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l); 27 generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l); 28 normalize nodelta; 35 29 /2/ 36 30 ] … … 39 33 [1: @LABEL 40 34 2: cases(HYP) 41 generalize in match (graph_add_lookup (rtl_if_graph p) LABEL stmt l); 35 generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l); 36 normalize nodelta; 42 37 /2/ 43 38 ] … … 1222 1217 qed. 1223 1218 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 1219 (* XXX: we use a "hack" here to circumvent the proof obligations required to 1231 1220 create res, an empty internal_function record. we insert into our graph … … 1260 1249 mk_rtl_internal_function luniverse' runiverse' result' params' 1261 1250 locals' stack_size' graph' ? ? in 1262 fold ? ? ? (translate_stmt lenv) (f_graph def) res.1251 foldi ? ? ? (translate_stmt lenv) (f_graph def) res. 1263 1252 [1: % 1264 1253 [1: @entry' 1265 1254 2: normalize nodelta; 1266 @(graph_add ? (f_entry def) ?)1267 1255 @graph_add_lookup 1256 @graph_add 1268 1257 ] 1269 1258 2: % 1270 1259 [1: @exit' 1271 2: /2/ 1260 2: normalize nodelta; 1261 @graph_add 1272 1262 ] 1273 1263 ] … … 1281 1271 ]. 1282 1272 1273 (* XXX: change, we need to propagate the region information, not ignore it *) 1283 1274 definition init_data_to_nat ≝ 1284 1275 λi: init_data.
Note: See TracChangeset
for help on using the changeset viewer.