Changeset 2702 for src/compiler.ma


Ignore:
Timestamp:
Feb 22, 2013, 3:27:16 PM (8 years ago)
Author:
sacerdot
Message:
  1. proof closed in ASM/UtilBranch
  2. more passes integrated in the compiler.ma
  3. some work on commenting out broken proofs in linearise.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2700 r2702  
    4444definition costlabel_map ≝ BitVectorTrie costlabel 16.
    4545
    46 axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
    47 
    48 (* Only sloow include "ASM/Policy.ma".
    49 *)include "ASM/PolicyStep.ma". include "arithmetics/nat.ma". axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
     46include "ASM/Policy.ma".
     47(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
     48   file to compile
     49  include "ASM/PolicyStep.ma".
     50  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
    5051 option (Σsigma_policy:(Word → Word) × (Word → bool).
    5152   let 〈sigma,policy〉≝ sigma_policy in
    52    sigma_policy_specification 〈\fst program,\snd program〉 sigma policy).
     53   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
    5354
    5455definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
     
    5859  let p' ≝ 〈preamble, list_instr〉 in
    5960  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
    60   let sigma ≝ λppc. \fst (sigma_pol ppc) in
    61   let pol ≝ λppc. \snd (sigma_pol ppc) in
     61  let sigma ≝ λppc. \fst sigma_pol ppc in
     62  let pol ≝ λppc. \snd sigma_pol ppc in
    6263  OK ? (assembly p sigma pol).
    6364cases daemon
     
    9293  return 〈p, ❬p', k'❭〉.
    9394  cases daemon
    94   qed.
     95qed.
Note: See TracChangeset for help on using the changeset viewer.