Changeset 2730 for extracted/toRTLabs.ml
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toRTLabs.ml
r2717 r2730 121 121 List.foldr (fun idt rsengen > 122 122 let { Types.fst = id; Types.snd = ty } = idt in 123 let { Types.fst = eta 2892; Types.snd = gen0 } = rsengen in124 let { Types.fst = rs; Types.snd = en0 } = eta 2892in123 let { Types.fst = eta991; Types.snd = gen0 } = rsengen in 124 let { Types.fst = rs; Types.snd = en0 } = eta991 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_ 15317=144 let rec fixed_rect_Type4 h_mk_fixed x_3346 = 145 145 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 146 x_ 15317146 x_3346 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_ 15319=153 let rec fixed_rect_Type5 h_mk_fixed x_3348 = 154 154 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 155 x_ 15319155 x_3348 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_ 15321=162 let rec fixed_rect_Type3 h_mk_fixed x_3350 = 163 163 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 164 x_ 15321164 x_3350 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_ 15323=171 let rec fixed_rect_Type2 h_mk_fixed x_3352 = 172 172 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 173 x_ 15323173 x_3352 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_ 15325=180 let rec fixed_rect_Type1 h_mk_fixed x_3354 = 181 181 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 182 x_ 15325182 x_3354 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_ 15327=189 let rec fixed_rect_Type0 h_mk_fixed x_3356 = 190 190 let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } = 191 x_ 15327191 x_3356 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_ 15343=260 let gm_map = x_ 15343in h_mk_goto_map gm_map __ __259 let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_3372 = 260 let gm_map = x_3372 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_ 15345=267 let gm_map = x_ 15345in h_mk_goto_map gm_map __ __266 let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_3374 = 267 let gm_map = x_3374 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_ 15347=274 let gm_map = x_ 15347in h_mk_goto_map gm_map __ __273 let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_3376 = 274 let gm_map = x_3376 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_ 15349=281 let gm_map = x_ 15349in h_mk_goto_map gm_map __ __280 let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_3378 = 281 let gm_map = x_3378 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_ 15351=288 let gm_map = x_ 15351in h_mk_goto_map gm_map __ __287 let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_3380 = 288 let gm_map = x_3380 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_ 15353=295 let gm_map = x_ 15353in h_mk_goto_map gm_map __ __294 let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_3382 = 295 let gm_map = x_3382 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_ 15371=403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_3400 = 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_ 15371408 x_3400 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_ 15373=421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_3402 = 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_ 15373426 x_3402 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_ 15375=439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_3404 = 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_ 15375444 x_3404 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_ 15377=457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_3406 = 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_ 15377462 x_3406 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_ 15379=475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_3408 = 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_ 15379480 x_3408 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_ 15381=493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_3410 = 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_ 15381498 x_3410 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_ 15457= function876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_3486 = 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_ 15464= function886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_3493 = 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_ 15471= function896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_3500 = 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_ 15478= function906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_3507 = 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_ 15485= function916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_3514 = 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_ 15492= function926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_3521 = 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 3119; Types.snd = reggen1 } =1334 (let { Types.fst = eta1218; 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 3119in1338 let { Types.fst = params; Types.snd = env1 } = eta1218 in 1339 1339 (fun _ > 1340 (let { Types.fst = eta 3118; Types.snd = reggen2 } =1340 (let { Types.fst = eta1217; 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 3118in1343 let { Types.fst = locals0; Types.snd = env0 } = eta1217 in 1344 1344 (fun _ > 1345 1345 (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset
for help on using the changeset viewer.