Changeset 2997 for extracted/toRTLabs.ml
 Timestamp:
 Mar 28, 2013, 10:27:41 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r2974 r2997 121 121 List.foldr (fun idt rsengen > 122 122 let { Types.fst = id; Types.snd = ty } = idt in 123 let { Types.fst = eta 166; Types.snd = gen0 } = rsengen in124 let { Types.fst = rs; Types.snd = en0 } = eta 166in123 let { Types.fst = eta651; Types.snd = gen0 } = rsengen in 124 let { Types.fst = rs; Types.snd = en0 } = eta651 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_ 207=144 let rec fixed_rect_Type4 h_mk_fixed x_1096 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_ 207146 x_1096 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_ 209=153 let rec fixed_rect_Type5 h_mk_fixed x_1098 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_ 209155 x_1098 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_ 211=162 let rec fixed_rect_Type3 h_mk_fixed x_1100 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_ 211164 x_1100 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_ 213=171 let rec fixed_rect_Type2 h_mk_fixed x_1102 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_ 213173 x_1102 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_ 215=180 let rec fixed_rect_Type1 h_mk_fixed x_1104 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_ 215182 x_1104 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_ 217=189 let rec fixed_rect_Type0 h_mk_fixed x_1106 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_ 217191 x_1106 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_ 233=260 let gm_map = x_ 233in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_1122 = 260 let gm_map = x_1122 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_ 235=267 let gm_map = x_ 235in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_1124 = 267 let gm_map = x_1124 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_ 237=274 let gm_map = x_ 237in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_1126 = 274 let gm_map = x_1126 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_ 239=281 let gm_map = x_ 239in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_1128 = 281 let gm_map = x_1128 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_ 241=288 let gm_map = x_ 241in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_1130 = 288 let gm_map = x_1130 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_ 243=295 let gm_map = x_ 243in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_1132 = 295 let gm_map = x_1132 in h_mk_goto_map gm_map __ __ 296 296 297 297 (** val gm_map : … … 399 399 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 400 400 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 401 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn402 > 'a1 **)403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_ 261=401 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 402 partial_fn > 'a1 **) 403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_1150 = 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_ 261408 x_1150 409 409 in 410 410 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ 411 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 411 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __ 412 412 413 413 (** val partial_fn_rect_Type5 : … … 417 417 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 418 418 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 419 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn420 > 'a1 **)421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_ 263=419 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 420 partial_fn > 'a1 **) 421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_1152 = 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_ 263426 x_1152 427 427 in 428 428 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ 429 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 429 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __ 430 430 431 431 (** val partial_fn_rect_Type3 : … … 435 435 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 436 436 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 437 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn438 > 'a1 **)439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_ 265=437 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 438 partial_fn > 'a1 **) 439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_1154 = 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_ 265444 x_1154 445 445 in 446 446 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ 447 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 447 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __ 448 448 449 449 (** val partial_fn_rect_Type2 : … … 453 453 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 454 454 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 455 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn456 > 'a1 **)457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_ 267=455 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 456 partial_fn > 'a1 **) 457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_1156 = 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_ 267462 x_1156 463 463 in 464 464 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ 465 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 465 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __ 466 466 467 467 (** val partial_fn_rect_Type1 : … … 471 471 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 472 472 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 473 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn474 > 'a1 **)475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_ 269=473 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 474 partial_fn > 'a1 **) 475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_1158 = 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_ 269480 x_1158 481 481 in 482 482 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ 483 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 483 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __ 484 484 485 485 (** val partial_fn_rect_Type0 : … … 489 489 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 490 490 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 491 Graphs.label Types.sig0 > Graphs.label Types.sig0 > 'a1) > partial_fn492 > 'a1 **)493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_ 271=491 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 492 partial_fn > 'a1 **) 493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_1160 = 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_ 271498 x_1160 499 499 in 500 500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ 501 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 501 pf_stacksize0 pf_graph0 __ pf_gotos0 pf_labels0 __ pf_entry0 pf_exit0 __ 502 502 503 503 (** val pf_labgen : fixed > partial_fn > Identifiers.universe **) … … 556 556 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 557 557 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 558 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 'a1 **) 558 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > __ > 'a1) > 559 'a1 **) 559 560 let partial_fn_inv_rect_Type4 x1 hterm h1 = 560 561 let hcut = partial_fn_rect_Type4 x1 h1 hterm in hcut __ … … 566 567 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 567 568 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 568 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 'a1 **) 569 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > __ > 'a1) > 570 'a1 **) 569 571 let partial_fn_inv_rect_Type3 x1 hterm h1 = 570 572 let hcut = partial_fn_rect_Type3 x1 h1 hterm in hcut __ … … 576 578 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 577 579 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 578 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 'a1 **) 580 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > __ > 'a1) > 581 'a1 **) 579 582 let partial_fn_inv_rect_Type2 x1 hterm h1 = 580 583 let hcut = partial_fn_rect_Type2 x1 h1 hterm in hcut __ … … 586 589 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 587 590 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 588 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 'a1 **) 591 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > __ > 'a1) > 592 'a1 **) 589 593 let partial_fn_inv_rect_Type1 x1 hterm h1 = 590 594 let hcut = partial_fn_rect_Type1 x1 h1 hterm in hcut __ … … 596 600 Nat.nat > RTLabs_syntax.statement Graphs.graph > __ > goto_map > 597 601 PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 > __ > 598 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > 'a1) > 'a1 **) 602 Graphs.label Types.sig0 > Graphs.label Types.sig0 > __ > __ > 'a1) > 603 'a1 **) 599 604 let partial_fn_inv_rect_Type0 x1 hterm h1 = 600 605 let hcut = partial_fn_rect_Type0 x1 h1 hterm in hcut __ … … 607 612 pf_labels = a100; pf_entry = a12; pf_exit = a13 } = x 608 613 in 609 Obj.magic (fun _ dH > dH __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y 614 Obj.magic (fun _ dH > dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) 615 y 610 616 611 617 (** val fn_contains_rect_Type4 : … … 874 880 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 875 881 fn_con_because > 'a1 **) 876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_ 347 = function882 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1237 = function 877 883  Fn_con_eq f > h_fn_con_eq f 878 884  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 884 890 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 885 891 fn_con_because > 'a1 **) 886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_ 354 = function892 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1244 = function 887 893  Fn_con_eq f > h_fn_con_eq f 888 894  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 894 900 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 895 901 fn_con_because > 'a1 **) 896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_ 361 = function902 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1251 = function 897 903  Fn_con_eq f > h_fn_con_eq f 898 904  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 904 910 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 905 911 fn_con_because > 'a1 **) 906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_ 368 = function912 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1258 = function 907 913  Fn_con_eq f > h_fn_con_eq f 908 914  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 914 920 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 915 921 fn_con_because > 'a1 **) 916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_ 375 = function922 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1265 = function 917 923  Fn_con_eq f > h_fn_con_eq f 918 924  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 924 930 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 925 931 fn_con_because > 'a1 **) 926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_ 382 = function932 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_1272 = function 927 933  Fn_con_eq f > h_fn_con_eq f 928 934  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 1234 1240 pf_stacksize = f.pf_stacksize; pf_graph = 1235 1241 (Identifiers.add PreIdentifiers.LabelTag f.pf_graph l 1236 RTLabs_syntax.St_return); pf_gotos =1242 (RTLabs_syntax.St_skip l)); pf_gotos = 1237 1243 (Identifiers.add PreIdentifiers.LabelTag (gm_map fx f.pf_graph f.pf_gotos) 1238 1244 l dest); pf_labels = (Types.pi1 f.pf_labels); pf_entry = l; pf_exit = … … 1339 1345 let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in 1340 1346 let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in 1341 (let { Types.fst = eta 393; Types.snd = reggen1 } =1347 (let { Types.fst = eta878; Types.snd = reggen1 } = 1342 1348 populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0 1343 1349 f.Cminor_syntax.f_params 1344 1350 in 1345 let { Types.fst = params; Types.snd = env1 } = eta 393in1351 let { Types.fst = params; Types.snd = env1 } = eta878 in 1346 1352 (fun _ > 1347 (let { Types.fst = eta 392; Types.snd = reggen2 } =1353 (let { Types.fst = eta877; Types.snd = reggen2 } = 1348 1354 populate_env env1 reggen1 f.Cminor_syntax.f_vars 1349 1355 in 1350 let { Types.fst = locals0; Types.snd = env0 } = eta 392in1356 let { Types.fst = locals0; Types.snd = env0 } = eta877 in 1351 1357 (fun _ > 1352 1358 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset
for help on using the changeset viewer.