Changeset 3029
 Timestamp:
 Mar 29, 2013, 9:47:49 AM (4 years ago)
 Location:
 extracted
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aSMCosts.ml
r2999 r3029 127 127 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 128 128 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 129 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 130 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 129 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 130 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 131 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 132 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 133 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 134 (Nat.S (Nat.S (Nat.S (Nat.S 135 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 131 136 (List.Cons ((ASM.DIRECT 132 137 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S … … 139 144 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 140 145 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 141 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 142 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 146 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 147 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 148 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 149 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 150 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 151 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 152 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 143 153 (List.Cons ((ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), 144 154 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons … … 492 502  Nat.S program_size' > 493 503 (fun _ > 494 (let { Types.fst = eta 24755; Types.snd = ticks } =504 (let { Types.fst = eta83; Types.snd = ticks } = 495 505 Fetch.fetch prog.ASM.cm program_counter' 496 506 in 497 let { Types.fst = instruction; Types.snd = program_counter'' } = 498 eta24755 507 let { Types.fst = instruction; Types.snd = program_counter'' } = eta83 499 508 in 500 509 (fun _ > 
extracted/lINToASM.ml
r3023 r3029 143 143 Identifiers.identifier_map > __ > Positive.pos > 'a1) > aSM_universe 144 144 > 'a1 **) 145 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_ 263 =145 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 = 146 146 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 147 147 ident_map0; label_map = label_map0; address_map = address_map0; 148 fresh_cost_label = fresh_cost_label0 } = x_ 263148 fresh_cost_label = fresh_cost_label0 } = x_3 149 149 in 150 150 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 157 157 Identifiers.identifier_map > __ > Positive.pos > 'a1) > aSM_universe 158 158 > 'a1 **) 159 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_ 265 =159 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 = 160 160 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 161 161 ident_map0; label_map = label_map0; address_map = address_map0; 162 fresh_cost_label = fresh_cost_label0 } = x_ 265162 fresh_cost_label = fresh_cost_label0 } = x_5 163 163 in 164 164 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 171 171 Identifiers.identifier_map > __ > Positive.pos > 'a1) > aSM_universe 172 172 > 'a1 **) 173 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_ 267 =173 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 = 174 174 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 175 175 ident_map0; label_map = label_map0; address_map = address_map0; 176 fresh_cost_label = fresh_cost_label0 } = x_ 267176 fresh_cost_label = fresh_cost_label0 } = x_7 177 177 in 178 178 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 185 185 Identifiers.identifier_map > __ > Positive.pos > 'a1) > aSM_universe 186 186 > 'a1 **) 187 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_ 269 =187 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 = 188 188 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 189 189 ident_map0; label_map = label_map0; address_map = address_map0; 190 fresh_cost_label = fresh_cost_label0 } = x_ 269190 fresh_cost_label = fresh_cost_label0 } = x_9 191 191 in 192 192 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 199 199 Identifiers.identifier_map > __ > Positive.pos > 'a1) > aSM_universe 200 200 > 'a1 **) 201 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_ 271 =201 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 = 202 202 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 203 203 ident_map0; label_map = label_map0; address_map = address_map0; 204 fresh_cost_label = fresh_cost_label0 } = x_ 271204 fresh_cost_label = fresh_cost_label0 } = x_11 205 205 in 206 206 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 213 213 Identifiers.identifier_map > __ > Positive.pos > 'a1) > aSM_universe 214 214 > 'a1 **) 215 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_ 273 =215 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 = 216 216 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 217 217 ident_map0; label_map = label_map0; address_map = address_map0; 218 fresh_cost_label = fresh_cost_label0 } = x_ 273218 fresh_cost_label = fresh_cost_label0 } = x_13 219 219 in 220 220 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 … … 320 320 let globals_addr_internal = fun res_offset x_size > 321 321 let { Types.fst = res; Types.snd = offset } = res_offset in 322 let { Types.fst = eta 11; Types.snd = data } = x_size in323 let { Types.fst = x; Types.snd = region } = eta 11in322 let { Types.fst = eta6; Types.snd = data } = x_size in 323 let { Types.fst = x; Types.snd = region } = eta6 in 324 324 { Types.fst = 325 325 (Identifiers.add PreIdentifiers.SymbolTag res x … … 352 352 (Identifiers.empty_map PreIdentifiers.LabelTag) 353 353 in 354 let { Types.fst = eta 12; Types.snd = lmap0 } =354 let { Types.fst = eta7; Types.snd = lmap0 } = 355 355 match Identifiers.lookup PreIdentifiers.LabelTag lmap l with 356 356  Types.None > … … 364 364 lmap } 365 365 in 366 let { Types.fst = id; Types.snd = univ } = eta 12in366 let { Types.fst = id; Types.snd = univ } = eta7 in 367 367 { Types.fst = { id_univ = univ; current_funct = current; ident_map = 368 368 u.ident_map; label_map = … … 377 377 Obj.magic (fun u > 378 378 let imap = u.ident_map in 379 let { Types.fst = eta 13; Types.snd = imap0 } =379 let { Types.fst = eta8; Types.snd = imap0 } = 380 380 match Identifiers.lookup PreIdentifiers.SymbolTag imap i with 381 381  Types.None > … … 389 389 imap } 390 390 in 391 let { Types.fst = id; Types.snd = univ } = eta 13in391 let { Types.fst = id; Types.snd = univ } = eta8 in 392 392 { Types.fst = { id_univ = univ; current_funct = u.current_funct; 393 393 ident_map = imap0; label_map = u.label_map; address_map = u.address_map; … … 597 597 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 598 598 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 599 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 600 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 599 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 600 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 601 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 602 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 603 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 604 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 605 Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 601 606  I8051.RegisterDPH > 602 607 (fun _ > ASM.DIRECT … … 611 616 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 612 617 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 613 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 614 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 618 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 619 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 620 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 621 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 622 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 623 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 624 Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 615 625  I8051.RegisterCarry > 616 626 (fun _ > ASM.DIRECT … … 1008 1018 (identifier_of_label globals lbl) (fun lbl' > 1009 1019 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp 1010 (ASM.toASM_ident PreIdentifiers. LabelTag lbl')))1020 (ASM.toASM_ident PreIdentifiers.ASMTag lbl'))) 1011 1021  Joint.RETURN > 1012 1022 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction … … 1078 1088 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1079 1089 > 'a1 **) 1080 let rec init_mutable_rect_Type4 h_mk_init_mutable x_ 290 =1090 let rec init_mutable_rect_Type4 h_mk_init_mutable x_30 = 1081 1091 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1082 built0 } = x_ 2901092 built0 } = x_30 1083 1093 in 1084 1094 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 … … 1087 1097 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1088 1098 > 'a1 **) 1089 let rec init_mutable_rect_Type5 h_mk_init_mutable x_ 292 =1099 let rec init_mutable_rect_Type5 h_mk_init_mutable x_32 = 1090 1100 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1091 built0 } = x_ 2921101 built0 } = x_32 1092 1102 in 1093 1103 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 … … 1096 1106 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1097 1107 > 'a1 **) 1098 let rec init_mutable_rect_Type3 h_mk_init_mutable x_ 294 =1108 let rec init_mutable_rect_Type3 h_mk_init_mutable x_34 = 1099 1109 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1100 built0 } = x_ 2941110 built0 } = x_34 1101 1111 in 1102 1112 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 … … 1105 1115 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1106 1116 > 'a1 **) 1107 let rec init_mutable_rect_Type2 h_mk_init_mutable x_ 296 =1117 let rec init_mutable_rect_Type2 h_mk_init_mutable x_36 = 1108 1118 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1109 built0 } = x_ 2961119 built0 } = x_36 1110 1120 in 1111 1121 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 … … 1114 1124 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1115 1125 > 'a1 **) 1116 let rec init_mutable_rect_Type1 h_mk_init_mutable x_ 298 =1126 let rec init_mutable_rect_Type1 h_mk_init_mutable x_38 = 1117 1127 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1118 built0 } = x_ 2981128 built0 } = x_38 1119 1129 in 1120 1130 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0 … … 1123 1133 (Z.z > Z.z > ASM.labelled_instruction List.list > 'a1) > init_mutable 1124 1134 > 'a1 **) 1125 let rec init_mutable_rect_Type0 h_mk_init_mutable x_ 300 =1135 let rec init_mutable_rect_Type0 h_mk_init_mutable x_40 = 1126 1136 let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built = 1127 built0 } = x_ 3001137 built0 } = x_40 1128 1138 in 1129 1139 h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
Note: See TracChangeset
for help on using the changeset viewer.