Changeset 2979
- Timestamp:
- Mar 27, 2013, 4:34:35 PM (8 years ago)
- Location:
- extracted
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/lINToASM.ml
r2977 r2979 134 134 label_map : ASM.identifier Identifiers.identifier_map 135 135 Identifiers.identifier_map; 136 address_map : BitVector.word Identifiers.identifier_map } 136 address_map : BitVector.word Identifiers.identifier_map; 137 fresh_cost_label : Positive.pos } 137 138 138 139 (** val aSM_universe_rect_Type4 : … … 140 141 ASM.identifier Identifiers.identifier_map -> ASM.identifier 141 142 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 142 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 143 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 144 -> 'a1 **) 143 145 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 = 144 146 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 145 ident_map0; label_map = label_map0; address_map = address_map0 } = x_3 147 ident_map0; label_map = label_map0; address_map = address_map0; 148 fresh_cost_label = fresh_cost_label0 } = x_3 146 149 in 147 150 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 148 address_map0 __ 151 address_map0 __ fresh_cost_label0 149 152 150 153 (** val aSM_universe_rect_Type5 : … … 152 155 ASM.identifier Identifiers.identifier_map -> ASM.identifier 153 156 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 154 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 157 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 158 -> 'a1 **) 155 159 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 = 156 160 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 157 ident_map0; label_map = label_map0; address_map = address_map0 } = x_5 161 ident_map0; label_map = label_map0; address_map = address_map0; 162 fresh_cost_label = fresh_cost_label0 } = x_5 158 163 in 159 164 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 160 address_map0 __ 165 address_map0 __ fresh_cost_label0 161 166 162 167 (** val aSM_universe_rect_Type3 : … … 164 169 ASM.identifier Identifiers.identifier_map -> ASM.identifier 165 170 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 166 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 171 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 172 -> 'a1 **) 167 173 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 = 168 174 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 169 ident_map0; label_map = label_map0; address_map = address_map0 } = x_7 175 ident_map0; label_map = label_map0; address_map = address_map0; 176 fresh_cost_label = fresh_cost_label0 } = x_7 170 177 in 171 178 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 172 address_map0 __ 179 address_map0 __ fresh_cost_label0 173 180 174 181 (** val aSM_universe_rect_Type2 : … … 176 183 ASM.identifier Identifiers.identifier_map -> ASM.identifier 177 184 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 178 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 185 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 186 -> 'a1 **) 179 187 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 = 180 188 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 181 ident_map0; label_map = label_map0; address_map = address_map0 } = x_9 189 ident_map0; label_map = label_map0; address_map = address_map0; 190 fresh_cost_label = fresh_cost_label0 } = x_9 182 191 in 183 192 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 184 address_map0 __ 193 address_map0 __ fresh_cost_label0 185 194 186 195 (** val aSM_universe_rect_Type1 : … … 188 197 ASM.identifier Identifiers.identifier_map -> ASM.identifier 189 198 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 190 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 199 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 200 -> 'a1 **) 191 201 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 = 192 202 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 193 ident_map0; label_map = label_map0; address_map = address_map0 } = x_11 203 ident_map0; label_map = label_map0; address_map = address_map0; 204 fresh_cost_label = fresh_cost_label0 } = x_11 194 205 in 195 206 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 196 address_map0 __ 207 address_map0 __ fresh_cost_label0 197 208 198 209 (** val aSM_universe_rect_Type0 : … … 200 211 ASM.identifier Identifiers.identifier_map -> ASM.identifier 201 212 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 202 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 213 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 214 -> 'a1 **) 203 215 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 = 204 216 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 205 ident_map0; label_map = label_map0; address_map = address_map0 } = x_13 217 ident_map0; label_map = label_map0; address_map = address_map0; 218 fresh_cost_label = fresh_cost_label0 } = x_13 206 219 in 207 220 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 208 address_map0 __ 221 address_map0 __ fresh_cost_label0 209 222 210 223 (** val id_univ : … … 235 248 xxx.address_map 236 249 250 (** val fresh_cost_label : 251 AST.ident List.list -> aSM_universe -> Positive.pos **) 252 let rec fresh_cost_label globals xxx = 253 xxx.fresh_cost_label 254 237 255 (** val aSM_universe_inv_rect_Type4 : 238 256 AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident 239 257 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 240 258 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 241 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)259 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) 242 260 let aSM_universe_inv_rect_Type4 x1 hterm h1 = 243 261 let hcut = aSM_universe_rect_Type4 x1 h1 hterm in hcut __ … … 247 265 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 248 266 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 249 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)267 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) 250 268 let aSM_universe_inv_rect_Type3 x1 hterm h1 = 251 269 let hcut = aSM_universe_rect_Type3 x1 h1 hterm in hcut __ … … 255 273 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 256 274 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 257 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)275 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) 258 276 let aSM_universe_inv_rect_Type2 x1 hterm h1 = 259 277 let hcut = aSM_universe_rect_Type2 x1 h1 hterm in hcut __ … … 263 281 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 264 282 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 265 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)283 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) 266 284 let aSM_universe_inv_rect_Type1 x1 hterm h1 = 267 285 let hcut = aSM_universe_rect_Type1 x1 h1 hterm in hcut __ … … 271 289 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 272 290 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 273 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)291 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 **) 274 292 let aSM_universe_inv_rect_Type0 x1 hterm h1 = 275 293 let hcut = aSM_universe_rect_Type0 x1 h1 hterm in hcut __ … … 280 298 Logic.eq_rect_Type2 x 281 299 (let { id_univ = a0; current_funct = a10; ident_map = a2; label_map = a3; 282 address_map = a4 } = x300 address_map = a4; fresh_cost_label = a6 } = x 283 301 in 284 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y 302 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y 303 304 (** val report_cost : 305 AST.ident List.list -> CostLabel.costlabel -> Types.unit0 306 Monad.smax_def__o__monad **) 307 let report_cost globals cl = 308 Obj.magic (fun u -> 309 let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in 310 (match Positive.leb u.fresh_cost_label clw with 311 | Bool.True -> 312 { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct; 313 ident_map = u.ident_map; label_map = u.label_map; address_map = 314 u.address_map; fresh_cost_label = (Positive.succ clw) }; Types.snd = 315 Types.It } 316 | Bool.False -> { Types.fst = u; Types.snd = Types.It })) 285 317 286 318 (** val new_ASM_universe : Joint.joint_program -> aSM_universe **) … … 308 340 (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map = 309 341 (Identifiers.empty_map PreIdentifiers.SymbolTag); address_map = 310 addresses.Types.fst }342 addresses.Types.fst; fresh_cost_label = Positive.One } 311 343 312 344 (** val identifier_of_label : … … 336 368 u.ident_map; label_map = 337 369 (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0); 338 address_map = u.address_map }; Types.snd = id }) 370 address_map = u.address_map; fresh_cost_label = u.fresh_cost_label }; 371 Types.snd = id }) 339 372 340 373 (** val identifier_of_ident : … … 358 391 let { Types.fst = id; Types.snd = univ } = eta8 in 359 392 { Types.fst = { id_univ = univ; current_funct = u.current_funct; 360 ident_map = imap0; label_map = u.label_map; address_map = 361 u.address_map}; Types.snd = id })393 ident_map = imap0; label_map = u.label_map; address_map = u.address_map; 394 fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) 362 395 363 396 (** val start_funct_translation : … … 367 400 Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct = 368 401 id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map; 369 address_map = u.address_map }; Types.snd = Types.It }) 402 address_map = u.address_map; fresh_cost_label = u.fresh_cost_label }; 403 Types.snd = Types.It }) 370 404 371 405 (** val address_of_ident : … … 385 419 { Types.fst = { id_univ = univ; current_funct = u.current_funct; 386 420 ident_map = u.ident_map; label_map = u.label_map; address_map = 387 u.address_map }; Types.snd = id })421 u.address_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) 388 422 389 423 (** val register_address : I8051.register -> ASM.subaddressing_mode **) … … 659 693 (match instr with 660 694 | Joint.COST_LABEL lbl -> 661 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl) 695 Monad.m_bind0 (Monad.smax_def State.state_monad) 696 (report_cost globals lbl) (fun x0 -> 697 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl)) 662 698 | Joint.CALL (f, x0, x1) -> 663 699 (match f with … … 1246 1282 Monad.m_bind0 (Monad.smax_def State.state_monad) 1247 1283 (translate_initialization p) (fun init -> 1248 Monad.m_return0 (Monad.smax_def State.state_monad) 1249 (let code0 = 1250 List.append init (List.Cons ({ Types.fst = Types.None; 1251 Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst = 1252 (Types.Some exit_label); Types.snd = (ASM.Jmp 1253 exit_label) }, code)))) 1254 in 1255 Monad.m_bind0 (Monad.max_def Option.option) 1256 (Obj.magic (ASM.code_size_opt code0)) (fun _ -> 1257 Monad.m_return0 (Monad.max_def Option.option) 1258 { ASM.preamble = List.Nil; ASM.code = code0; 1259 ASM.renamed_symbols = symboltable; ASM.final_label = 1260 exit_label })))))))) 1261 1284 Monad.m_bind0 (Monad.smax_def State.state_monad) 1285 State.state_get (fun u -> 1286 Monad.m_return0 (Monad.smax_def State.state_monad) 1287 (let code0 = 1288 List.append init (List.Cons ({ Types.fst = Types.None; 1289 Types.snd = (ASM.Call main) }, (List.Cons 1290 ({ Types.fst = (Types.Some exit_label); Types.snd = 1291 (ASM.Cost u.fresh_cost_label) }, (List.Cons 1292 ({ Types.fst = Types.None; Types.snd = (ASM.Jmp 1293 exit_label) }, code)))))) 1294 in 1295 Monad.m_bind0 (Monad.max_def Option.option) 1296 (Obj.magic (ASM.code_size_opt code0)) (fun _ -> 1297 Monad.m_return0 (Monad.max_def Option.option) 1298 { ASM.preamble = List.Nil; ASM.code = code0; 1299 ASM.renamed_symbols = symboltable; ASM.final_label = 1300 exit_label }))))))))) 1301 -
extracted/lINToASM.mli
r2977 r2979 134 134 label_map : ASM.identifier Identifiers.identifier_map 135 135 Identifiers.identifier_map; 136 address_map : BitVector.word Identifiers.identifier_map } 136 address_map : BitVector.word Identifiers.identifier_map; 137 fresh_cost_label : Positive.pos } 137 138 138 139 val aSM_universe_rect_Type4 : … … 140 141 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 141 142 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 142 __ -> 'a1) -> aSM_universe -> 'a1143 __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 143 144 144 145 val aSM_universe_rect_Type5 : … … 146 147 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 147 148 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 148 __ -> 'a1) -> aSM_universe -> 'a1149 __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 149 150 150 151 val aSM_universe_rect_Type3 : … … 152 153 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 153 154 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 154 __ -> 'a1) -> aSM_universe -> 'a1155 __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 155 156 156 157 val aSM_universe_rect_Type2 : … … 158 159 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 159 160 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 160 __ -> 'a1) -> aSM_universe -> 'a1161 __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 161 162 162 163 val aSM_universe_rect_Type1 : … … 164 165 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 165 166 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 166 __ -> 'a1) -> aSM_universe -> 'a1167 __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 167 168 168 169 val aSM_universe_rect_Type0 : … … 170 171 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 171 172 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 172 __ -> 'a1) -> aSM_universe -> 'a1173 __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 173 174 174 175 val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe … … 188 189 Identifiers.identifier_map 189 190 191 val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos 192 190 193 val aSM_universe_inv_rect_Type4 : 191 194 AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident 192 195 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 193 196 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 194 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1197 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 195 198 196 199 val aSM_universe_inv_rect_Type3 : … … 198 201 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 199 202 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 200 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1203 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 201 204 202 205 val aSM_universe_inv_rect_Type2 : … … 204 207 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 205 208 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 206 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1209 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 207 210 208 211 val aSM_universe_inv_rect_Type1 : … … 210 213 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 211 214 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 212 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1215 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 213 216 214 217 val aSM_universe_inv_rect_Type0 : … … 216 219 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 217 220 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 218 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1221 Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1 219 222 220 223 val aSM_universe_jmdiscr : 221 224 AST.ident List.list -> aSM_universe -> aSM_universe -> __ 225 226 val report_cost : 227 AST.ident List.list -> CostLabel.costlabel -> Types.unit0 228 Monad.smax_def__o__monad 222 229 223 230 val new_ASM_universe : Joint.joint_program -> aSM_universe -
extracted/translateUtils.ml
r2974 r2979 640 640 let prologue = data0.added_prologue in 641 641 let { Types.fst = init0; Types.snd = entry' } = 642 Obj.magic adds_graph_p re dst_g_pars globals (fun x i -> i)prologue642 Obj.magic adds_graph_post dst_g_pars globals prologue 643 643 (Obj.magic entry) init 644 644 in
Note: See TracChangeset
for help on using the changeset viewer.