Changeset 2005
 Timestamp:
 May 29, 2012, 2:51:06 PM (6 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1948 r2005 1155 1155 ) ≝ 1156 1156 λ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) × ℕ. 1159 1159 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in 1160 1160 ppc = prefix ∧ … … 1164 1164 program 1165 1165 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. 1166 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in1166 let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in 1167 1167 let 〈label,instr〉 ≝ x in 1168 1168 let labels ≝ … … 1176 1176  _ ⇒ costs ] in 1177 1177 〈labels,costs,S ppc〉 1178 ) 〈(empty_map …),(Stub ??),0〉) .1179 [ 2:normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH21178 ) 〈(empty_map …),(Stub ??),0〉)). 1179 [ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2 1180 1180 labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %] 1181 1181 inversion label [#EQ  #l #EQ] … … 1226 1226 list Byte × (BitVectorTrie costlabel 16) ≝ 1227 1227 λp. 1228 let 〈preamble, instr_list〉 ≝ p in1229 1228 λsigma. 1230 1229 λpolicy. 1230 let 〈preamble, instr_list〉 ≝ p in 1231 1231 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 1232 1232 let datalabels ≝ construct_datalabels preamble in … … 1234 1234 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 1235 1235 let result ≝ 1236 foldl_strong1236 pi1 ?? (foldl_strong 1237 1237 (option Identifier × pseudo_instruction) 1238 1238 (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))). … … 1252 1252 let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in 1253 1253 〈new_pc, 〈new_ppc, (code @ program)〉〉) 1254 〈(zero ?), 〈(zero ?), [ ]〉〉 1254 〈(zero ?), 〈(zero ?), [ ]〉〉) 1255 1255 in 1256 1256 〈\snd (\snd result), 
src/ASM/Util.ma
r1964 r2005 266 266 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 267 267  cons hd' tl' ⇒ 268 let 〈cleft, cright〉 ≝ reduce_strong A B tl tl'in268 let 〈cleft, cright〉 ≝ pi1 ?? (reduce_strong A B tl tl') in 269 269 let 〈commonl, restl〉 ≝ cleft in 270 270 let 〈commonr, restr〉 ≝ cright in
Note: See TracChangeset
for help on using the changeset viewer.