Changeset 2875
- Timestamp:
- Mar 15, 2013, 1:32:50 AM (5 years ago)
- Files:
-
- 11 edited
Legend:
- Unmodified
- Added
- Removed
-
driver/backendPrinter.ml
r2868 r2875 221 221 222 222 let print_program pass (program : Extracted.Preamble.__) = 223 let beprint pcs = 224 print_graph (pcs (Extracted.Types.fst (Obj.magic program))) in 223 225 let lines = 224 226 match pass with 225 227 | Extracted.Compiler.Rtl_separate_pass -> 226 Extracted.RTL_printer.print_RTL_program rTL_printing_params228 beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params) 227 229 | Extracted.Compiler.Rtl_uniq_pass -> 228 Extracted.RTL_printer.print_RTL_program rTL_printing_params230 beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params) 229 231 | Extracted.Compiler.Ertl_pass -> 230 Extracted.ERTL_printer.print_ERTL_program eRTL_printing_params232 beprint (Extracted.ERTL_printer.print_ERTL_program eRTL_printing_params) 231 233 | Extracted.Compiler.Ertlptr_pass -> 232 Extracted.ERTLptr_printer.print_ERTLptr_program eRTLptr_printing_params 234 beprint 235 (Extracted.ERTLptr_printer.print_ERTLptr_program eRTLptr_printing_params) 233 236 | Extracted.Compiler.Ltl_pass -> 234 Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params 235 | _ -> (fun _ -> Extracted.List.Nil) 237 beprint 238 (Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params) 239 | Extracted.Compiler.Object_code_pass -> 240 ASMPrinter.print_program (Extracted.ASM.oc (Obj.magic program)) 241 | _ -> "" 236 242 in 237 "\n" ^ print_graph (lines (Extracted.Types.fst (Obj.magic program)))^ "\n"243 "\n" ^ lines ^ "\n" -
driver/build
r2856 r2875 12 12 ocamlc -I ../Deliverables/D2.2/8051/lib -c -g error.ml 13 13 ocamlc -I ../Deliverables/D2.2/8051/lib -c -g *.ml 14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo IntelHex.cmo clightPrinter.cmo backendPrinter.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo IntelHex.cmo clightPrinter.cmo ASMPrinter.cmo backendPrinter.cmo error.cmo cerco.cmo -o cerco -
driver/cerco.ml
r2874 r2875 29 29 | Extracted.Compiler.Ltl_pass -> "Ltl_pass" 30 30 | Extracted.Compiler.Lin_pass -> "Lin_pass" 31 | Extracted.Compiler.Assembly_pass -> "Assembly_pass" 32 | Extracted.Compiler.Object_code_pass -> "Object_code_pass" 31 33 ;; 32 34 -
extracted/compiler.ml
r2873 r2875 258 258 | Ltl_pass 259 259 | Lin_pass 260 | Assembly_pass 261 | Object_code_pass 260 262 261 263 (** val pass_rect_Type4 : 262 264 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 263 -> 'a1 -> pass -> 'a1 **)264 let rec pass_rect_Type4 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass = function265 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **) 266 let rec pass_rect_Type4 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function 265 267 | Clight_pass -> h_clight_pass 266 268 | Clight_switch_removed_pass -> h_clight_switch_removed_pass … … 275 277 | Ltl_pass -> h_ltl_pass 276 278 | Lin_pass -> h_lin_pass 279 | Assembly_pass -> h_assembly_pass 280 | Object_code_pass -> h_object_code_pass 277 281 278 282 (** val pass_rect_Type5 : 279 283 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 280 -> 'a1 -> pass -> 'a1 **)281 let rec pass_rect_Type5 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass = function284 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **) 285 let rec pass_rect_Type5 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function 282 286 | Clight_pass -> h_clight_pass 283 287 | Clight_switch_removed_pass -> h_clight_switch_removed_pass … … 292 296 | Ltl_pass -> h_ltl_pass 293 297 | Lin_pass -> h_lin_pass 298 | Assembly_pass -> h_assembly_pass 299 | Object_code_pass -> h_object_code_pass 294 300 295 301 (** val pass_rect_Type3 : 296 302 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 297 -> 'a1 -> pass -> 'a1 **)298 let rec pass_rect_Type3 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass = function303 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **) 304 let rec pass_rect_Type3 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function 299 305 | Clight_pass -> h_clight_pass 300 306 | Clight_switch_removed_pass -> h_clight_switch_removed_pass … … 309 315 | Ltl_pass -> h_ltl_pass 310 316 | Lin_pass -> h_lin_pass 317 | Assembly_pass -> h_assembly_pass 318 | Object_code_pass -> h_object_code_pass 311 319 312 320 (** val pass_rect_Type2 : 313 321 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 314 -> 'a1 -> pass -> 'a1 **)315 let rec pass_rect_Type2 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass = function322 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **) 323 let rec pass_rect_Type2 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function 316 324 | Clight_pass -> h_clight_pass 317 325 | Clight_switch_removed_pass -> h_clight_switch_removed_pass … … 326 334 | Ltl_pass -> h_ltl_pass 327 335 | Lin_pass -> h_lin_pass 336 | Assembly_pass -> h_assembly_pass 337 | Object_code_pass -> h_object_code_pass 328 338 329 339 (** val pass_rect_Type1 : 330 340 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 331 -> 'a1 -> pass -> 'a1 **)332 let rec pass_rect_Type1 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass = function341 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **) 342 let rec pass_rect_Type1 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function 333 343 | Clight_pass -> h_clight_pass 334 344 | Clight_switch_removed_pass -> h_clight_switch_removed_pass … … 343 353 | Ltl_pass -> h_ltl_pass 344 354 | Lin_pass -> h_lin_pass 355 | Assembly_pass -> h_assembly_pass 356 | Object_code_pass -> h_object_code_pass 345 357 346 358 (** val pass_rect_Type0 : 347 359 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 348 -> 'a1 -> pass -> 'a1 **)349 let rec pass_rect_Type0 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass = function360 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **) 361 let rec pass_rect_Type0 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function 350 362 | Clight_pass -> h_clight_pass 351 363 | Clight_switch_removed_pass -> h_clight_switch_removed_pass … … 360 372 | Ltl_pass -> h_ltl_pass 361 373 | Lin_pass -> h_lin_pass 374 | Assembly_pass -> h_assembly_pass 375 | Object_code_pass -> h_object_code_pass 362 376 363 377 (** val pass_inv_rect_Type4 : 364 378 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ 365 379 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 366 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) 367 let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 = 368 let hcut = pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 hterm in 380 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) 381 -> 'a1 **) 382 let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 = 383 let hcut = 384 pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm 385 in 369 386 hcut __ 370 387 … … 372 389 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ 373 390 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 374 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) 375 let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 = 376 let hcut = pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 hterm in 391 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) 392 -> 'a1 **) 393 let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 = 394 let hcut = 395 pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm 396 in 377 397 hcut __ 378 398 … … 380 400 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ 381 401 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 382 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) 383 let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 = 384 let hcut = pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 hterm in 402 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) 403 -> 'a1 **) 404 let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 = 405 let hcut = 406 pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm 407 in 385 408 hcut __ 386 409 … … 388 411 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ 389 412 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 390 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) 391 let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 = 392 let hcut = pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 hterm in 413 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) 414 -> 'a1 **) 415 let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 = 416 let hcut = 417 pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm 418 in 393 419 hcut __ 394 420 … … 396 422 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ 397 423 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 398 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) 399 let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 = 400 let hcut = pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 hterm in 424 (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) 425 -> 'a1 **) 426 let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 = 427 let hcut = 428 pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm 429 in 401 430 hcut __ 402 431 … … 416 445 | Ertlptr_pass -> Obj.magic (fun _ dH -> dH) 417 446 | Ltl_pass -> Obj.magic (fun _ dH -> dH) 418 | Lin_pass -> Obj.magic (fun _ dH -> dH)) y 447 | Lin_pass -> Obj.magic (fun _ dH -> dH) 448 | Assembly_pass -> Obj.magic (fun _ dH -> dH) 449 | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y 419 450 420 451 (** val pass_jmdiscr : pass -> pass -> __ **) … … 433 464 | Ertlptr_pass -> Obj.magic (fun _ dH -> dH) 434 465 | Ltl_pass -> Obj.magic (fun _ dH -> dH) 435 | Lin_pass -> Obj.magic (fun _ dH -> dH)) y 466 | Lin_pass -> Obj.magic (fun _ dH -> dH) 467 | Assembly_pass -> Obj.magic (fun _ dH -> dH) 468 | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y 436 469 437 470 type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod … … 510 543 let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 } 511 544 in 512 let { Types.fst = eta2 9104; Types.snd = max_stack } =545 let { Types.fst = eta2; Types.snd = max_stack } = 513 546 ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2 514 547 in 515 let { Types.fst = p3; Types.snd = stack_cost } = eta2 9104in548 let { Types.fst = p3; Types.snd = stack_cost } = eta2 in 516 549 let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in 517 550 let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in … … 525 558 (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge) 526 559 (LINToASM.lin_to_asm p4))) (fun p5 -> 560 let i5 = observe Assembly_pass p5 in 527 561 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst = 528 562 p5; Types.snd = stack_cost }; Types.snd = max_stack })) … … 541 575 542 576 (** val assembler : 543 ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **) 544 let assembler p = 577 observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code 578 Errors.res **) 579 let assembler observe p = 545 580 Obj.magic 546 581 (Monad.m_bind0 (Monad.max_def Errors.res0) … … 550 585 let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in 551 586 let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in 552 Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma pol))))) 587 let p0 = Assembly.assembly p sigma pol in 588 let i = Obj.magic observe Object_code_pass (Types.pi1 p0) in 589 Obj.magic (Errors.OK (Types.pi1 p0)))) 553 590 554 591 open AbstractStatus … … 586 623 Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> 587 624 compiler_output -> 'a1 **) 588 let rec compiler_output_rect_Type4 h_mk_compiler_output x_ 25364=625 let rec compiler_output_rect_Type4 h_mk_compiler_output x_198 = 589 626 let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost = 590 627 c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight = 591 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_ 25364628 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_198 592 629 in 593 630 h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0 … … 598 635 Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> 599 636 compiler_output -> 'a1 **) 600 let rec compiler_output_rect_Type5 h_mk_compiler_output x_2 5366=637 let rec compiler_output_rect_Type5 h_mk_compiler_output x_200 = 601 638 let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost = 602 639 c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight = 603 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_2 5366640 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_200 604 641 in 605 642 h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0 … … 610 647 Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> 611 648 compiler_output -> 'a1 **) 612 let rec compiler_output_rect_Type3 h_mk_compiler_output x_2 5368=649 let rec compiler_output_rect_Type3 h_mk_compiler_output x_202 = 613 650 let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost = 614 651 c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight = 615 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_2 5368652 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_202 616 653 in 617 654 h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0 … … 622 659 Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> 623 660 compiler_output -> 'a1 **) 624 let rec compiler_output_rect_Type2 h_mk_compiler_output x_2 5370=661 let rec compiler_output_rect_Type2 h_mk_compiler_output x_204 = 625 662 let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost = 626 663 c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight = 627 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_2 5370664 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_204 628 665 in 629 666 h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0 … … 634 671 Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> 635 672 compiler_output -> 'a1 **) 636 let rec compiler_output_rect_Type1 h_mk_compiler_output x_2 5372=673 let rec compiler_output_rect_Type1 h_mk_compiler_output x_206 = 637 674 let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost = 638 675 c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight = 639 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_2 5372676 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_206 640 677 in 641 678 h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0 … … 646 683 Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> 647 684 compiler_output -> 'a1 **) 648 let rec compiler_output_rect_Type0 h_mk_compiler_output x_2 5374=685 let rec compiler_output_rect_Type0 h_mk_compiler_output x_208 = 649 686 let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost = 650 687 c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight = 651 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_2 5374688 c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_208 652 689 in 653 690 h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0 … … 735 772 Monad.m_bind3 (Monad.max_def Errors.res0) 736 773 (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack -> 737 Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))738 ( fun p2 ->774 Monad.m_bind0 (Monad.max_def Errors.res0) 775 (Obj.magic (assembler observe p1)) (fun p2 -> 739 776 let k = ASMCostsSplit.aSM_cost_map p2 in 740 777 let k' = -
extracted/compiler.mli
r2842 r2875 258 258 | Ltl_pass 259 259 | Lin_pass 260 | Assembly_pass 261 | Object_code_pass 260 262 261 263 val pass_rect_Type4 : 262 264 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 263 -> 'a1 -> pass -> 'a1265 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 264 266 265 267 val pass_rect_Type5 : 266 268 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 267 -> 'a1 -> pass -> 'a1269 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 268 270 269 271 val pass_rect_Type3 : 270 272 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 271 -> 'a1 -> pass -> 'a1273 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 272 274 273 275 val pass_rect_Type2 : 274 276 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 275 -> 'a1 -> pass -> 'a1277 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 276 278 277 279 val pass_rect_Type1 : 278 280 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 279 -> 'a1 -> pass -> 'a1281 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 280 282 281 283 val pass_rect_Type0 : 282 284 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 283 -> 'a1 -> pass -> 'a1285 -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 284 286 285 287 val pass_inv_rect_Type4 : 286 288 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 287 289 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 288 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1290 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 289 291 290 292 val pass_inv_rect_Type3 : 291 293 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 292 294 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 293 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1295 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 294 296 295 297 val pass_inv_rect_Type2 : 296 298 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 297 299 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 298 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1300 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 299 301 300 302 val pass_inv_rect_Type1 : 301 303 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 302 304 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 303 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1305 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 304 306 305 307 val pass_inv_rect_Type0 : 306 308 pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 307 309 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 308 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1310 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 309 311 310 312 val pass_discr : pass -> pass -> __ … … 353 355 354 356 val assembler : 355 ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res 357 observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code 358 Errors.res 356 359 357 360 open AbstractStatus -
extracted/semantics.ml
r2873 r2875 316 316 317 317 open LIN_semantics 318 319 open Interpret2 318 320 319 321 type preclassified_system_pass = … … 324 326 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> 325 327 preclassified_system_pass -> 'a1 **) 326 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_ 26392=327 let pcs_pcs = x_ 26392in h_mk_preclassified_system_pass pcs_pcs __328 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 = 329 let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __ 328 330 329 331 (** val preclassified_system_pass_rect_Type5 : 330 332 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> 331 333 preclassified_system_pass -> 'a1 **) 332 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_ 26394=333 let pcs_pcs = x_ 26394in h_mk_preclassified_system_pass pcs_pcs __334 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 = 335 let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __ 334 336 335 337 (** val preclassified_system_pass_rect_Type3 : 336 338 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> 337 339 preclassified_system_pass -> 'a1 **) 338 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_ 26396=339 let pcs_pcs = x_ 26396in h_mk_preclassified_system_pass pcs_pcs __340 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 = 341 let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __ 340 342 341 343 (** val preclassified_system_pass_rect_Type2 : 342 344 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> 343 345 preclassified_system_pass -> 'a1 **) 344 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_ 26398=345 let pcs_pcs = x_ 26398in h_mk_preclassified_system_pass pcs_pcs __346 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 = 347 let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __ 346 348 347 349 (** val preclassified_system_pass_rect_Type1 : 348 350 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> 349 351 preclassified_system_pass -> 'a1 **) 350 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_ 26400=351 let pcs_pcs = x_ 26400in h_mk_preclassified_system_pass pcs_pcs __352 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 = 353 let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __ 352 354 353 355 (** val preclassified_system_pass_rect_Type0 : 354 356 Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) -> 355 357 preclassified_system_pass -> 'a1 **) 356 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_ 26402=357 let pcs_pcs = x_ 26402in h_mk_preclassified_system_pass pcs_pcs __358 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 = 359 let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __ 358 360 359 361 (** val pcs_pcs : … … 405 407 Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1) 406 408 409 exception NotImplementedYet 410 407 411 (** val preclassified_system_of_pass : 408 Compiler.pass -> preclassified_system_pass **)412 Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **) 409 413 let preclassified_system_of_pass = function 410 | Compiler.Clight_pass -> Clight_classified_system.clight_pcs 411 | Compiler.Clight_switch_removed_pass -> Clight_classified_system.clight_pcs 412 | Compiler.Clight_label_pass -> Clight_classified_system.clight_pcs 413 | Compiler.Clight_simplified_pass -> Clight_classified_system.clight_pcs 414 | Compiler.Cminor_pass -> Cminor_classified_system.cminor_pcs 415 | Compiler.Rtlabs_pass -> RTLabs_classified_system.rTLabs_pcs 414 | Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs) 415 | Compiler.Clight_switch_removed_pass -> 416 (fun x -> Clight_classified_system.clight_pcs) 417 | Compiler.Clight_label_pass -> 418 (fun x -> Clight_classified_system.clight_pcs) 419 | Compiler.Clight_simplified_pass -> 420 (fun x -> Clight_classified_system.clight_pcs) 421 | Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs) 422 | Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs) 416 423 | Compiler.Rtl_separate_pass -> 417 Joint_fullexec.joint_preclassified_system 418 (SemanticsUtils.sem_graph_params_to_sem_params 419 RTL_semantics.rTL_semantics_separate) 424 (fun x -> 425 Joint_fullexec.joint_preclassified_system 426 (SemanticsUtils.sem_graph_params_to_sem_params 427 RTL_semantics.rTL_semantics_separate)) 420 428 | Compiler.Rtl_uniq_pass -> 421 Joint_fullexec.joint_preclassified_system 422 (SemanticsUtils.sem_graph_params_to_sem_params 423 RTL_semantics.rTL_semantics_unique) 429 (fun x -> 430 Joint_fullexec.joint_preclassified_system 431 (SemanticsUtils.sem_graph_params_to_sem_params 432 RTL_semantics.rTL_semantics_unique)) 424 433 | Compiler.Ertl_pass -> 425 Joint_fullexec.joint_preclassified_system 426 (SemanticsUtils.sem_graph_params_to_sem_params 427 ERTL_semantics.eRTL_semantics) 434 (fun x -> 435 Joint_fullexec.joint_preclassified_system 436 (SemanticsUtils.sem_graph_params_to_sem_params 437 ERTL_semantics.eRTL_semantics)) 428 438 | Compiler.Ertlptr_pass -> 429 Joint_fullexec.joint_preclassified_system 430 (SemanticsUtils.sem_graph_params_to_sem_params 431 ERTLptr_semantics.eRTLptr_semantics) 439 (fun x -> 440 Joint_fullexec.joint_preclassified_system 441 (SemanticsUtils.sem_graph_params_to_sem_params 442 ERTLptr_semantics.eRTLptr_semantics)) 432 443 | Compiler.Ltl_pass -> 433 Joint_fullexec.joint_preclassified_system 434 (SemanticsUtils.sem_graph_params_to_sem_params 435 LTL_semantics.lTL_semantics) 444 (fun x -> 445 Joint_fullexec.joint_preclassified_system 446 (SemanticsUtils.sem_graph_params_to_sem_params 447 LTL_semantics.lTL_semantics)) 436 448 | Compiler.Lin_pass -> 437 Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics 449 (fun x -> 450 Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics) 451 | Compiler.Assembly_pass -> (fun prog -> raise NotImplementedYet) 452 | Compiler.Object_code_pass -> 453 (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog)) 438 454 439 455 (** val run_and_print : … … 443 459 Types.unit0 **) 444 460 let run_and_print pass prog n print_pass print_event print_error print_exit = 445 let pcs = preclassified_system_of_pass pass in 461 try 462 let pcs = preclassified_system_of_pass pass prog in 446 463 let prog0 = prog in 447 464 let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0 in … … 460 477 | Errors.Error msg -> print_error msg) 461 478 | Errors.Error msg -> print_error msg) 462 479 with 480 NotImplementedYet -> Types.It 481 -
extracted/semantics.mli
r2867 r2875 316 316 317 317 open LIN_semantics 318 319 open Interpret2 318 320 319 321 type preclassified_system_pass = … … 377 379 SmallstepExec.trans_system 378 380 379 val preclassified_system_of_pass : Compiler.pass -> preclassified_system_pass 381 val preclassified_system_of_pass : 382 Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass 380 383 381 384 val run_and_print : -
src/ASM/Interpret2.ma
r2764 r2875 17 17 18 18 definition mk_fullexec_of_abstract_status: 19 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in 20 ≝ λS,as_eval,as_init. 21 mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 19 ∀program: Type[0]. 20 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in 21 ≝ λprogram,S,as_eval,as_init. 22 mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 22 23 (λ_.return as_init). 23 24 24 25 definition mk_preclassified_system_of_abstract_status: 25 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system 26 ≝ λS,as_eval,as_init. 26 ∀program: Type[0]. 27 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system 28 ≝ λprogram,S,as_eval,as_init. 27 29 mk_preclassified_system 28 (mk_fullexec_of_abstract_status S as_eval as_init)30 (mk_fullexec_of_abstract_status program S as_eval as_init) 29 31 (λ_.λst. ¬(is_none … (as_label … st))) 30 32 (λ_.as_classify S) … … 39 41 let cm ≝ load_code_memory (oc c) in 40 42 mk_preclassified_system_of_abstract_status 43 labelled_object_code 41 44 (ASM_abstract_status cm (costlabels c)) 42 45 (λst. return (execute_1 … st)) -
src/compiler.ma
r2841 r2875 29 29 | ertlptr_pass: pass 30 30 | ltl_pass: pass 31 | lin_pass: pass. 31 | lin_pass: pass 32 | assembly_pass: pass 33 | object_code_pass: pass. 32 34 33 35 definition with_stack_model : Type[0] → Type[0] ≝ … … 48 50 | ertlptr_pass ⇒ with_stack_model ertlptr_program 49 51 | ltl_pass ⇒ with_stack_model ltl_program 50 | lin_pass ⇒ with_stack_model lin_program ]. 52 | lin_pass ⇒ with_stack_model lin_program 53 | assembly_pass ⇒ pseudo_assembly_program 54 | object_code_pass ⇒ labelled_object_code ]. 51 55 52 56 definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit. … … 109 113 let st ≝ lookup_stack_cost … p in 110 114 let i ≝ observe lin_pass 〈p,st〉 in 111 ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; 115 ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; 116 let i ≝ observe assembly_pass p in 112 117 return 〈p,stack_cost,max_stack〉. 113 118 … … 115 120 include "ASM/Policy.ma". 116 121 117 definition assembler : pseudo_assembly_program → res labelled_object_code ≝ 118 λp. 122 definition assembler : 123 observe_pass → pseudo_assembly_program → res labelled_object_code ≝ 124 λobserve,p. 119 125 ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p); 120 126 let sigma ≝ λppc. \fst sigma_pol ppc in 121 127 let pol ≝ λppc. \snd sigma_pol ppc in 122 OK ? (assembly p sigma pol). 128 let p ≝ assembly p sigma pol in 129 let i ≝ observe object_code_pass p in 130 OK ? p. 123 131 124 132 (* Cost lifting *) … … 148 156 ! 〈init_cost,p',p〉 ← front_end observe p; 149 157 ! 〈p,stack_cost,max_stack〉 ← back_end observe p; 150 ! p ← assembler p;158 ! p ← assembler observe p; 151 159 let k ≝ ASM_cost_map p in 152 160 let k' ≝ -
src/correctness.ma
r2852 r2875 109 109 ∃n1,n2. 110 110 observables Clight_pcs (c_labelled_clight … p) m1 m2 = 111 observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2 111 observables (OC_preclassified_system (c_labelled_object_code … p)) 112 (c_labelled_object_code … p) n1 n2 112 113 ∧ 113 114 minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status). -
src/semantics.ma
r2841 r2875 9 9 include "LTL/LTL_semantics.ma". 10 10 include "LIN/LIN_semantics.ma". 11 include "ASM/Interpret2.ma". 11 12 12 13 record preclassified_system_pass (P:pass) : Type[2] ≝ … … 16 17 17 18 definition preclassified_system_of_pass: 18 ∀pass. preclassified_system_pass pass ≝19 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝ 19 20 λpass. 20 match pass with21 [ clight_pass ⇒ mk_preclassified_system_pass … Clight_pcs …22 | clight_switch_removed_pass ⇒ mk_preclassified_system_pass … Clight_pcs …23 | clight_label_pass ⇒ mk_preclassified_system_pass … Clight_pcs …24 | clight_simplified_pass ⇒ mk_preclassified_system_pass … Clight_pcs …25 | cminor_pass ⇒ mk_preclassified_system_pass … Cminor_pcs …26 | rtlabs_pass ⇒ mk_preclassified_system_pass … RTLabs_pcs …21 match pass return λpass.syntax_of_pass pass → preclassified_system_pass pass with 22 [ clight_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … 23 | clight_switch_removed_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … 24 | clight_label_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … 25 | clight_simplified_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs … 26 | cminor_pass ⇒ λ_.mk_preclassified_system_pass … Cminor_pcs … 27 | rtlabs_pass ⇒ λ_.mk_preclassified_system_pass … RTLabs_pcs … 27 28 | rtl_separate_pass ⇒ 28 mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …29 λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) … 29 30 | rtl_uniq_pass ⇒ 30 mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …31 λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) … 31 32 | ertl_pass ⇒ 32 mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …33 λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) … 33 34 | ertlptr_pass ⇒ 34 mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …35 λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) … 35 36 | ltl_pass ⇒ 36 mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …37 λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) … 37 38 | lin_pass ⇒ 38 mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ? 39 λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ? 40 | assembly_pass ⇒ 41 ? 42 | object_code_pass ⇒ 43 λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) … 39 44 ]. 40 % 45 try % cases daemon 41 46 qed. 42 47 … … 46 51 ≝ 47 52 λpass,prog,n,print_pass,print_event,print_error,print_exit. 48 let pcs ≝ preclassified_system_of_pass pass in53 let pcs ≝ preclassified_system_of_pass pass prog in 49 54 let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in 50 55 let g ≝ make_global … pcs prog in
Note: See TracChangeset
for help on using the changeset viewer.