Changeset 2743 for extracted/toRTLabs.ml
 Timestamp:
 Feb 27, 2013, 9:27:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r2730 r2743 121 121 List.foldr (fun idt rsengen > 122 122 let { Types.fst = id; Types.snd = ty } = idt in 123 let { Types.fst = eta 991; Types.snd = gen0 } = rsengen in124 let { Types.fst = rs; Types.snd = en0 } = eta 991in123 let { Types.fst = eta2917; Types.snd = gen0 } = rsengen in 124 let { Types.fst = rs; Types.snd = en0 } = eta2917 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_ 3346=144 let rec fixed_rect_Type4 h_mk_fixed x_15343 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_ 3346146 x_15343 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_ 3348=153 let rec fixed_rect_Type5 h_mk_fixed x_15345 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_ 3348155 x_15345 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_ 3350=162 let rec fixed_rect_Type3 h_mk_fixed x_15347 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_ 3350164 x_15347 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_ 3352=171 let rec fixed_rect_Type2 h_mk_fixed x_15349 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_ 3352173 x_15349 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_ 3354=180 let rec fixed_rect_Type1 h_mk_fixed x_15351 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_ 3354182 x_15351 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_ 3356=189 let rec fixed_rect_Type0 h_mk_fixed x_15353 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_ 3356191 x_15353 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 g0 h_mk_goto_map x_ 3372=260 let gm_map = x_ 3372in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_15369 = 260 let gm_map = x_15369 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 g0 h_mk_goto_map x_ 3374=267 let gm_map = x_ 3374in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_15371 = 267 let gm_map = x_15371 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 g0 h_mk_goto_map x_ 3376=274 let gm_map = x_ 3376in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_15373 = 274 let gm_map = x_15373 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 g0 h_mk_goto_map x_ 3378=281 let gm_map = x_ 3378in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_15375 = 281 let gm_map = x_15375 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 g0 h_mk_goto_map x_ 3380=288 let gm_map = x_ 3380in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_15377 = 288 let gm_map = x_15377 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 g0 h_mk_goto_map x_ 3382=295 let gm_map = x_ 3382in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_15379 = 295 let gm_map = x_15379 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) > partial_fn 402 402 > 'a1 **) 403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_ 3400=403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15397 = 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_ 3400408 x_15397 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) > partial_fn 420 420 > 'a1 **) 421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_ 3402=421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15399 = 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_ 3402426 x_15399 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) > partial_fn 438 438 > 'a1 **) 439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_ 3404=439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15401 = 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_ 3404444 x_15401 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) > partial_fn 456 456 > 'a1 **) 457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_ 3406=457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15403 = 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_ 3406462 x_15403 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) > partial_fn 474 474 > 'a1 **) 475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_ 3408=475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15405 = 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_ 3408480 x_15405 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) > partial_fn 492 492 > 'a1 **) 493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_ 3410=493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15407 = 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_ 3410498 x_15407 499 499 in 500 500 h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __ … … 874 874 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 875 875 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_ 3486= function876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15483 = function 877 877  Fn_con_eq f > h_fn_con_eq f 878 878  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 884 884 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 885 885 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_ 3493= function886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15490 = function 887 887  Fn_con_eq f > h_fn_con_eq f 888 888  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 894 894 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 895 895 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_ 3500= function896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15497 = function 897 897  Fn_con_eq f > h_fn_con_eq f 898 898  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 904 904 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 905 905 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_ 3507= function906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15504 = function 907 907  Fn_con_eq f > h_fn_con_eq f 908 908  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 914 914 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 915 915 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_ 3514= function916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15511 = function 917 917  Fn_con_eq f > h_fn_con_eq f 918 918  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 924 924 Cminor_syntax.stmt > partial_fn Types.sig0 > 'a1) > partial_fn > 925 925 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_ 3521= function926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15518 = function 927 927  Fn_con_eq f > h_fn_con_eq f 928 928  Fn_con_sig (f1, f2, f3) > h_fn_con_sig f1 f2 __ f3 … … 1332 1332 let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in 1333 1333 let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in 1334 (let { Types.fst = eta 1218; Types.snd = reggen1 } =1334 (let { Types.fst = eta3144; Types.snd = reggen1 } = 1335 1335 populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0 1336 1336 f.Cminor_syntax.f_params 1337 1337 in 1338 let { Types.fst = params; Types.snd = env1 } = eta 1218in1338 let { Types.fst = params; Types.snd = env1 } = eta3144 in 1339 1339 (fun _ > 1340 (let { Types.fst = eta 1217; Types.snd = reggen2 } =1340 (let { Types.fst = eta3143; Types.snd = reggen2 } = 1341 1341 populate_env env1 reggen1 f.Cminor_syntax.f_vars 1342 1342 in 1343 let { Types.fst = locals0; Types.snd = env0 } = eta 1217in1343 let { Types.fst = locals0; Types.snd = env0 } = eta3143 in 1344 1344 (fun _ > 1345 1345 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset
for help on using the changeset viewer.