Changeset 3059 for extracted/toRTLabs.ml
 Timestamp:
 Apr 2, 2013, 1:25:09 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r3043 r3059 121 121 List.foldr (fun idt rsengen > 122 122 let { Types.fst = id; Types.snd = ty } = idt in 123 let { Types.fst = eta2 943; Types.snd = gen0 } = rsengen in124 let { Types.fst = rs; Types.snd = en0 } = eta2 943in123 let { Types.fst = eta2859; Types.snd = gen0 } = rsengen in 124 let { Types.fst = rs; Types.snd = en0 } = eta2859 in 125 125 let { Types.fst = r; Types.snd = gen' } = 126 126 Identifiers.fresh PreIdentifiers.RegisterTag gen0 … … 142 142 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 143 143 fixed > 'a1 **) 144 let rec fixed_rect_Type4 h_mk_fixed x_15 539=144 let rec fixed_rect_Type4 h_mk_fixed x_15483 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_15 539146 x_15483 147 147 in 148 148 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 151 151 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 152 152 fixed > 'a1 **) 153 let rec fixed_rect_Type5 h_mk_fixed x_15 541=153 let rec fixed_rect_Type5 h_mk_fixed x_15485 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_15 541155 x_15485 156 156 in 157 157 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 160 160 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 161 161 fixed > 'a1 **) 162 let rec fixed_rect_Type3 h_mk_fixed x_15 543=162 let rec fixed_rect_Type3 h_mk_fixed x_15487 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_15 543164 x_15487 165 165 in 166 166 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 169 169 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 170 170 fixed > 'a1 **) 171 let rec fixed_rect_Type2 h_mk_fixed x_15 545=171 let rec fixed_rect_Type2 h_mk_fixed x_15489 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_15 545173 x_15489 174 174 in 175 175 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 178 178 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 179 179 fixed > 'a1 **) 180 let rec fixed_rect_Type1 h_mk_fixed x_15 547=180 let rec fixed_rect_Type1 h_mk_fixed x_15491 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_15 547182 x_15491 183 183 in 184 184 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 187 187 (Identifiers.identifier_set > env > AST.typ Types.option > 'a1) > 188 188 fixed > 'a1 **) 189 let rec fixed_rect_Type0 h_mk_fixed x_15 549=189 let rec fixed_rect_Type0 h_mk_fixed x_15493 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_15 549191 x_15493 192 192 in 193 193 h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0 … … 257 257 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 258 258 > goto_map > 'a1 **) 259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_155 65=260 let gm_map = x_155 65in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15509 = 260 let gm_map = x_15509 in h_mk_goto_map gm_map __ __ 261 261 262 262 (** val goto_map_rect_Type5 : … … 264 264 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 265 265 > goto_map > 'a1 **) 266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_155 67=267 let gm_map = x_155 67in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15511 = 267 let gm_map = x_15511 in h_mk_goto_map gm_map __ __ 268 268 269 269 (** val goto_map_rect_Type3 : … … 271 271 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 272 272 > goto_map > 'a1 **) 273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_155 69=274 let gm_map = x_155 69in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15513 = 274 let gm_map = x_15513 in h_mk_goto_map gm_map __ __ 275 275 276 276 (** val goto_map_rect_Type2 : … … 278 278 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 279 279 > goto_map > 'a1 **) 280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_155 71=281 let gm_map = x_155 71in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15515 = 281 let gm_map = x_15515 in h_mk_goto_map gm_map __ __ 282 282 283 283 (** val goto_map_rect_Type1 : … … 285 285 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 286 286 > goto_map > 'a1 **) 287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_155 73=288 let gm_map = x_155 73in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15517 = 288 let gm_map = x_15517 in h_mk_goto_map gm_map __ __ 289 289 290 290 (** val goto_map_rect_Type0 : … … 292 292 (PreIdentifiers.identifier Identifiers.identifier_map > __ > __ > 'a1) 293 293 > goto_map > 'a1 **) 294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_155 75=295 let gm_map = x_155 75in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15519 = 295 let gm_map = x_15519 in h_mk_goto_map gm_map __ __ 296 296 297 297 (** val gm_map : … … 401 401 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 402 402 partial_fn > 'a1 **) 403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_155 93=403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15537 = 404 404 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 405 405 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 406 406 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 407 407 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 408 x_155 93408 x_15537 409 409 in 410 410 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 419 419 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 420 420 partial_fn > 'a1 **) 421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_155 95=421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15539 = 422 422 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 423 423 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 424 424 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 425 425 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 426 x_155 95426 x_15539 427 427 in 428 428 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 437 437 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 438 438 partial_fn > 'a1 **) 439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_155 97=439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15541 = 440 440 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 441 441 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 442 442 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 443 443 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 444 x_155 97444 x_15541 445 445 in 446 446 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 455 455 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 456 456 partial_fn > 'a1 **) 457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_155 99=457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15543 = 458 458 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 459 459 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 460 460 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 461 461 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 462 x_155 99462 x_15543 463 463 in 464 464 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 473 473 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 474 474 partial_fn > 'a1 **) 475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15 601=475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15545 = 476 476 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 477 477 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 478 478 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 479 479 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 480 x_15 601480 x_15545 481 481 in 482 482 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 491 491 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 492 492 partial_fn > 'a1 **) 493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15 603=493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15547 = 494 494 let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params = 495 495 pf_params0; pf_locals = pf_locals0; pf_result = pf_result0; 496 496 pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0; 497 497 pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } = 498 x_15 603498 x_15547 499 499 in 500 500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 880 880 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 881 881 fn_con_because > 'a1 **) 882 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 80= function882 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15624 = function 883 883  Fn_con_eq f > h_fn_con_eq f 884 884  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 890 890 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 891 891 fn_con_because > 'a1 **) 892 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 87= function892 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15631 = function 893 893  Fn_con_eq f > h_fn_con_eq f 894 894  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 900 900 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 901 901 fn_con_because > 'a1 **) 902 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_156 94= function902 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15638 = function 903 903  Fn_con_eq f > h_fn_con_eq f 904 904  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 910 910 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 911 911 fn_con_because > 'a1 **) 912 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15 701= function912 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15645 = function 913 913  Fn_con_eq f > h_fn_con_eq f 914 914  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 920 920 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 921 921 fn_con_because > 'a1 **) 922 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15 708= function922 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15652 = function 923 923  Fn_con_eq f > h_fn_con_eq f 924 924  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 930 930 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 931 931 fn_con_because > 'a1 **) 932 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15 715= function932 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15659 = function 933 933  Fn_con_eq f > h_fn_con_eq f 934 934  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 1345 1345 let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in 1346 1346 let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in 1347 (let { Types.fst = eta3 170; Types.snd = reggen1 } =1347 (let { Types.fst = eta3086; Types.snd = reggen1 } = 1348 1348 populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0 1349 1349 f.Cminor_syntax.f_params 1350 1350 in 1351 let { Types.fst = params; Types.snd = env1 } = eta3 170in1351 let { Types.fst = params; Types.snd = env1 } = eta3086 in 1352 1352 (fun _ > 1353 (let { Types.fst = eta3 169; Types.snd = reggen2 } =1353 (let { Types.fst = eta3085; Types.snd = reggen2 } = 1354 1354 populate_env env1 reggen1 f.Cminor_syntax.f_vars 1355 1355 in 1356 let { Types.fst = locals0; Types.snd = env0 } = eta3 169in1356 let { Types.fst = locals0; Types.snd = env0 } = eta3085 in 1357 1357 (fun _ > 1358 1358 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset
for help on using the changeset viewer.