Changeset 2875 for src/compiler.ma


Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2841 r2875  
    2929 | ertlptr_pass: pass
    3030 | ltl_pass: pass
    31  | lin_pass: pass.
     31 | lin_pass: pass
     32 | assembly_pass: pass
     33 | object_code_pass: pass.
    3234
    3335definition with_stack_model : Type[0] → Type[0] ≝
     
    4850  | ertlptr_pass ⇒ with_stack_model ertlptr_program
    4951  | 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 ].
    5155
    5256definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
     
    109113  let st ≝ lookup_stack_cost … p in
    110114  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
    112117   return 〈p,stack_cost,max_stack〉.
    113118
     
    115120include "ASM/Policy.ma".
    116121
    117 definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    118 λp.
     122definition assembler :
     123 observe_pass → pseudo_assembly_program → res labelled_object_code ≝
     124λobserve,p.
    119125  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
    120126  let sigma ≝ λppc. \fst sigma_pol ppc in
    121127  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.
    123131
    124132(* Cost lifting *)
     
    148156  ! 〈init_cost,p',p〉 ← front_end observe p;
    149157  ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
    150   ! p ← assembler p;
     158  ! p ← assembler observe p;
    151159  let k ≝ ASM_cost_map p in
    152160  let k' ≝
Note: See TracChangeset for help on using the changeset viewer.