Changeset 2767 for src/compiler.ma


Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2763 r2767  
    3232axiom colour_graph : coloured_graph_computer.
    3333
    34 definition back_end : RTLabs_program → pseudo_assembly_program ≝
     34definition back_end : RTLabs_program → res pseudo_assembly_program ≝
    3535λp.
    3636  let p ≝ rtlabs_to_rtl p in
     
    3939  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    4040  let p ≝ ltl_to_lin p in
    41           lin_to_asm p.
     41          opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p).
    4242
    4343include "ASM/Policy.ma".
     
    5252definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    5353λp.
    54 (*  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); *)
    5554  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
    5655  let sigma ≝ λppc. \fst sigma_pol ppc in
     
    6059include "ASM/ASMCosts.ma".
    6160
    62 (*CSC: move the next definitions, e.g. in BitVectorTrie *)
    63 definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
    64  λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
     61(*CSC: move the next definitions, e.g. in BitVectorTrie; JHM: done! *)
    6562
    66 definition strong_decidable: Prop → Type[0] ≝
    67  λP:Prop. P + ¬ P.
    68 
    69 lemma strong_decidable_in_codomain:
    70  ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
    71   strong_decidable (in_codomain A n m a).
    72  #A #n #m elim m
    73  [ normalize #a' #a inversion (a' == a) #H
    74    [ %1 %{(VEmpty …)} >(\P H) %
    75    | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
    76  | -n #n #L #R #Hl #Hr #a
    77    cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
    78    cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
    79    %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
    80    normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
    81  | #n #A %2 % * #x normalize #abs destruct ]
    82 qed.
    83 
    84 (* can now move this defn to ASM/ASMCosts.ma *)
    8563definition lift_cost_map_back_to_front :
    8664  ∀clight, code_memory, lbls.
     
    9775λp.
    9876  ! 〈init_cost,p',p〉 ← front_end p;
    99   let p ≝ back_end p in
    100     ! p ← assembler p;
     77  ! p ← back_end p;
     78  ! p ← assembler p;
    10179  let k ≝ ASM_cost_map p in
    10280  let k' ≝
Note: See TracChangeset for help on using the changeset viewer.