Changeset 2005


Ignore:
Timestamp:
May 29, 2012, 2:51:06 PM (5 years ago)
Author:
boender
Message:
  • minor changes to make things compile with a clean checkout
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1948 r2005  
    11551155  ) ≝
    11561156  λprogram.
    1157   \fst (foldl_strong (option Identifier × pseudo_instruction)
    1158   (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × nat.
     1157  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
     1158  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × .
    11591159    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    11601160    ppc = |prefix| ∧
     
    11641164  program
    11651165  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
    1166    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
     1166   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
    11671167   let 〈label,instr〉 ≝ x in
    11681168   let labels ≝
     
    11761176     | _ ⇒ costs ] in
    11771177      〈labels,costs,S ppc〉
    1178    ) 〈(empty_map …),(Stub ??),0〉).
    1179 [2: normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
     1178   ) 〈(empty_map …),(Stub ??),0〉)).
     1179[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2
    11801180  -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
    11811181 inversion label [#EQ | #l #EQ]
     
    12261226      list Byte × (BitVectorTrie costlabel 16) ≝
    12271227  λp.
    1228   let 〈preamble, instr_list〉 ≝ p in
    12291228  λsigma.
    12301229  λpolicy.
     1230  let 〈preamble, instr_list〉 ≝ p in
    12311231  let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
    12321232  let datalabels ≝ construct_datalabels preamble in
     
    12341234  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
    12351235  let result ≝
    1236      foldl_strong
     1236     pi1 ?? (foldl_strong
    12371237      (option Identifier × pseudo_instruction)
    12381238      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
     
    12521252        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
    12531253         〈new_pc, 〈new_ppc, (code @ program)〉〉)
    1254       〈(zero ?), 〈(zero ?), [ ]〉〉
     1254      〈(zero ?), 〈(zero ?), [ ]〉〉)
    12551255    in
    12561256     〈\snd (\snd result),
  • src/ASM/Util.ma

    r1964 r2005  
    266266    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
    267267    | cons hd' tl' ⇒
    268       let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in
     268      let 〈cleft, cright〉 ≝ pi1 ?? (reduce_strong A B tl tl') in
    269269      let 〈commonl, restl〉 ≝ cleft in
    270270      let 〈commonr, restr〉 ≝ cright in
Note: See TracChangeset for help on using the changeset viewer.