 Timestamp:
 Apr 1, 2013, 9:14:03 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r3039 r3057 664 664 let labels ≝ \fst (create_label_cost_map instr_list) in 665 665 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 666 let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x ( lookup_labels x) in666 let lookup_datalabels ≝ λx. lookup_def … (construct_datalabels preamble) x (sigma (lookup_labels x)) in 667 667 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 668 668 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in … … 837 837 let datalabels ≝ construct_datalabels preamble in 838 838 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 839 let lookup_datalabels ≝ λx.lookup_def … datalabels x ( lookup_labels x) in839 let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in 840 840 ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < instr_list. 841 841 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in … … 856 856 let datalabels ≝ construct_datalabels preamble in 857 857 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 858 let lookup_datalabels ≝ λx.lookup_def … datalabels x ( lookup_labels x) in858 let lookup_datalabels ≝ λx.lookup_def … datalabels x (sigma (lookup_labels x)) in 859 859 let 〈next_pc,revcode〉 ≝ pi1 … ( 860 860 foldl_strong
Note: See TracChangeset
for help on using the changeset viewer.