Changeset 2977
- Timestamp:
- Mar 27, 2013, 4:09:56 PM (8 years ago)
- Location:
- extracted
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/backEndOps.ml
r2951 r2977 402 402 -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte -> 403 403 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **) 404 let rec eval_rect_Type4 h_mk_Eval x_1 6349=405 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 6349in404 let rec eval_rect_Type4 h_mk_Eval x_185 = 405 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_185 in 406 406 h_mk_Eval opaccs0 op4 op5 407 407 … … 411 411 -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte -> 412 412 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **) 413 let rec eval_rect_Type5 h_mk_Eval x_1 6351=414 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 6351in413 let rec eval_rect_Type5 h_mk_Eval x_187 = 414 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_187 in 415 415 h_mk_Eval opaccs0 op4 op5 416 416 … … 420 420 -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte -> 421 421 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **) 422 let rec eval_rect_Type3 h_mk_Eval x_1 6353=423 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 6353in422 let rec eval_rect_Type3 h_mk_Eval x_189 = 423 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_189 in 424 424 h_mk_Eval opaccs0 op4 op5 425 425 … … 429 429 -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte -> 430 430 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **) 431 let rec eval_rect_Type2 h_mk_Eval x_1 6355=432 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 6355in431 let rec eval_rect_Type2 h_mk_Eval x_191 = 432 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_191 in 433 433 h_mk_Eval opaccs0 op4 op5 434 434 … … 438 438 -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte -> 439 439 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **) 440 let rec eval_rect_Type1 h_mk_Eval x_1 6357=441 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 6357in440 let rec eval_rect_Type1 h_mk_Eval x_193 = 441 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_193 in 442 442 h_mk_Eval opaccs0 op4 op5 443 443 … … 447 447 -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte -> 448 448 (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **) 449 let rec eval_rect_Type0 h_mk_Eval x_1 6359=450 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_1 6359in449 let rec eval_rect_Type0 h_mk_Eval x_195 = 450 let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_195 in 451 451 h_mk_Eval opaccs0 op4 op5 452 452 … … 705 705 in 706 706 let { Types.fst = rslt; Types.snd = carry0 } = 707 eval0.op3 Bool.False op b2 o1o0.Types.snd707 eval0.op3 Bool.False op o1o0.Types.snd b2 708 708 in 709 709 let p0 = Nat.O in -
extracted/lINToASM.ml
r2963 r2977 134 134 label_map : ASM.identifier Identifiers.identifier_map 135 135 Identifiers.identifier_map; 136 address_map : BitVector.word Identifiers.identifier_map; 137 fresh_cost_label : Positive.pos } 136 address_map : BitVector.word Identifiers.identifier_map } 138 137 139 138 (** val aSM_universe_rect_Type4 : … … 141 140 ASM.identifier Identifiers.identifier_map -> ASM.identifier 142 141 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 143 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 144 -> 'a1 **) 142 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 145 143 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_3 = 146 144 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 147 ident_map0; label_map = label_map0; address_map = address_map0; 148 fresh_cost_label = fresh_cost_label0 } = x_3 145 ident_map0; label_map = label_map0; address_map = address_map0 } = x_3 149 146 in 150 147 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 151 address_map0 __ fresh_cost_label0148 address_map0 __ 152 149 153 150 (** val aSM_universe_rect_Type5 : … … 155 152 ASM.identifier Identifiers.identifier_map -> ASM.identifier 156 153 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 157 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 158 -> 'a1 **) 154 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 159 155 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5 = 160 156 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 161 ident_map0; label_map = label_map0; address_map = address_map0; 162 fresh_cost_label = fresh_cost_label0 } = x_5 157 ident_map0; label_map = label_map0; address_map = address_map0 } = x_5 163 158 in 164 159 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 165 address_map0 __ fresh_cost_label0160 address_map0 __ 166 161 167 162 (** val aSM_universe_rect_Type3 : … … 169 164 ASM.identifier Identifiers.identifier_map -> ASM.identifier 170 165 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 171 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 172 -> 'a1 **) 166 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 173 167 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_7 = 174 168 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 175 ident_map0; label_map = label_map0; address_map = address_map0; 176 fresh_cost_label = fresh_cost_label0 } = x_7 169 ident_map0; label_map = label_map0; address_map = address_map0 } = x_7 177 170 in 178 171 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 179 address_map0 __ fresh_cost_label0172 address_map0 __ 180 173 181 174 (** val aSM_universe_rect_Type2 : … … 183 176 ASM.identifier Identifiers.identifier_map -> ASM.identifier 184 177 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 185 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 186 -> 'a1 **) 178 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 187 179 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_9 = 188 180 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 189 ident_map0; label_map = label_map0; address_map = address_map0; 190 fresh_cost_label = fresh_cost_label0 } = x_9 181 ident_map0; label_map = label_map0; address_map = address_map0 } = x_9 191 182 in 192 183 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 193 address_map0 __ fresh_cost_label0184 address_map0 __ 194 185 195 186 (** val aSM_universe_rect_Type1 : … … 197 188 ASM.identifier Identifiers.identifier_map -> ASM.identifier 198 189 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 199 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 200 -> 'a1 **) 190 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 201 191 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_11 = 202 192 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 203 ident_map0; label_map = label_map0; address_map = address_map0; 204 fresh_cost_label = fresh_cost_label0 } = x_11 193 ident_map0; label_map = label_map0; address_map = address_map0 } = x_11 205 194 in 206 195 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 207 address_map0 __ fresh_cost_label0196 address_map0 __ 208 197 209 198 (** val aSM_universe_rect_Type0 : … … 211 200 ASM.identifier Identifiers.identifier_map -> ASM.identifier 212 201 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 213 Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe 214 -> 'a1 **) 202 Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **) 215 203 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_13 = 216 204 let { id_univ = id_univ0; current_funct = current_funct0; ident_map = 217 ident_map0; label_map = label_map0; address_map = address_map0; 218 fresh_cost_label = fresh_cost_label0 } = x_13 205 ident_map0; label_map = label_map0; address_map = address_map0 } = x_13 219 206 in 220 207 h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 221 address_map0 __ fresh_cost_label0208 address_map0 __ 222 209 223 210 (** val id_univ : … … 248 235 xxx.address_map 249 236 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_label254 255 237 (** val aSM_universe_inv_rect_Type4 : 256 238 AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident 257 239 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 258 240 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 259 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1 **)241 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **) 260 242 let aSM_universe_inv_rect_Type4 x1 hterm h1 = 261 243 let hcut = aSM_universe_rect_Type4 x1 h1 hterm in hcut __ … … 265 247 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 266 248 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 267 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1 **)249 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **) 268 250 let aSM_universe_inv_rect_Type3 x1 hterm h1 = 269 251 let hcut = aSM_universe_rect_Type3 x1 h1 hterm in hcut __ … … 273 255 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 274 256 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 275 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1 **)257 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **) 276 258 let aSM_universe_inv_rect_Type2 x1 hterm h1 = 277 259 let hcut = aSM_universe_rect_Type2 x1 h1 hterm in hcut __ … … 281 263 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 282 264 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 283 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1 **)265 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **) 284 266 let aSM_universe_inv_rect_Type1 x1 hterm h1 = 285 267 let hcut = aSM_universe_rect_Type1 x1 h1 hterm in hcut __ … … 289 271 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 290 272 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 291 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1 **)273 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **) 292 274 let aSM_universe_inv_rect_Type0 x1 hterm h1 = 293 275 let hcut = aSM_universe_rect_Type0 x1 h1 hterm in hcut __ … … 298 280 Logic.eq_rect_Type2 x 299 281 (let { id_univ = a0; current_funct = a10; ident_map = a2; label_map = a3; 300 address_map = a4 ; fresh_cost_label = a6} = x282 address_map = a4 } = x 301 283 in 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 })) 284 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y 317 285 318 286 (** val new_ASM_universe : Joint.joint_program -> aSM_universe **) … … 340 308 (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map = 341 309 (Identifiers.empty_map PreIdentifiers.SymbolTag); address_map = 342 addresses.Types.fst ; fresh_cost_label = Positive.One}310 addresses.Types.fst } 343 311 344 312 (** val identifier_of_label : … … 368 336 u.ident_map; label_map = 369 337 (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0); 370 address_map = u.address_map; fresh_cost_label = u.fresh_cost_label }; 371 Types.snd = id }) 338 address_map = u.address_map }; Types.snd = id }) 372 339 373 340 (** val identifier_of_ident : … … 391 358 let { Types.fst = id; Types.snd = univ } = eta8 in 392 359 { Types.fst = { id_univ = univ; current_funct = u.current_funct; 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 })360 ident_map = imap0; label_map = u.label_map; address_map = 361 u.address_map }; Types.snd = id }) 395 362 396 363 (** val start_funct_translation : … … 400 367 Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct = 401 368 id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map; 402 address_map = u.address_map; fresh_cost_label = u.fresh_cost_label }; 403 Types.snd = Types.It }) 369 address_map = u.address_map }; Types.snd = Types.It }) 404 370 405 371 (** val address_of_ident : … … 419 385 { Types.fst = { id_univ = univ; current_funct = u.current_funct; 420 386 ident_map = u.ident_map; label_map = u.label_map; address_map = 421 u.address_map ; fresh_cost_label = u.fresh_cost_label}; Types.snd = id })387 u.address_map }; Types.snd = id }) 422 388 423 389 (** val register_address : I8051.register -> ASM.subaddressing_mode **) … … 693 659 (match instr with 694 660 | Joint.COST_LABEL 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)) 661 Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl) 698 662 | Joint.CALL (f, x0, x1) -> 699 663 (match f with … … 1172 1136 (List.append (do_store_init_data globals u nxt_dptr data0) acc) } 1173 1137 in 1174 (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd 1138 List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV 1139 (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd = 1140 (ASM.DATA16 1141 (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1142 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 1143 Nat.O)))))))))))))))) start_dptr)) }))))) }, 1144 (List.foldr f { Types.fst = start_dptr; Types.snd = List.Nil } data).Types.snd) 1175 1145 1176 1146 (** val translate_initialization : … … 1276 1246 Monad.m_bind0 (Monad.smax_def State.state_monad) 1277 1247 (translate_initialization p) (fun init -> 1278 Monad.m_bind0 (Monad.smax_def State.state_monad) 1279 State.state_get (fun u -> 1280 Monad.m_return0 (Monad.smax_def State.state_monad) 1281 (let code0 = 1282 List.append init (List.Cons ({ Types.fst = Types.None; 1283 Types.snd = (ASM.Call main) }, (List.Cons 1284 ({ Types.fst = (Types.Some exit_label); Types.snd = 1285 (ASM.Cost u.fresh_cost_label) }, (List.Cons 1286 ({ Types.fst = Types.None; Types.snd = (ASM.Jmp 1287 exit_label) }, code)))))) 1288 in 1289 Monad.m_bind0 (Monad.max_def Option.option) 1290 (Obj.magic (ASM.code_size_opt code0)) (fun _ -> 1291 Monad.m_return0 (Monad.max_def Option.option) 1292 { ASM.preamble = List.Nil; ASM.code = code0; 1293 ASM.renamed_symbols = symboltable; ASM.final_label = 1294 exit_label }))))))))) 1295 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 -
extracted/lINToASM.mli
r2963 r2977 134 134 label_map : ASM.identifier Identifiers.identifier_map 135 135 Identifiers.identifier_map; 136 address_map : BitVector.word Identifiers.identifier_map; 137 fresh_cost_label : Positive.pos } 136 address_map : BitVector.word Identifiers.identifier_map } 138 137 139 138 val aSM_universe_rect_Type4 : … … 141 140 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 142 141 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 143 __ -> Positive.pos ->'a1) -> aSM_universe -> 'a1142 __ -> 'a1) -> aSM_universe -> 'a1 144 143 145 144 val aSM_universe_rect_Type5 : … … 147 146 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 148 147 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 149 __ -> Positive.pos ->'a1) -> aSM_universe -> 'a1148 __ -> 'a1) -> aSM_universe -> 'a1 150 149 151 150 val aSM_universe_rect_Type3 : … … 153 152 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 154 153 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 155 __ -> Positive.pos ->'a1) -> aSM_universe -> 'a1154 __ -> 'a1) -> aSM_universe -> 'a1 156 155 157 156 val aSM_universe_rect_Type2 : … … 159 158 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 160 159 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 161 __ -> Positive.pos ->'a1) -> aSM_universe -> 'a1160 __ -> 'a1) -> aSM_universe -> 'a1 162 161 163 162 val aSM_universe_rect_Type1 : … … 165 164 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 166 165 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 167 __ -> Positive.pos ->'a1) -> aSM_universe -> 'a1166 __ -> 'a1) -> aSM_universe -> 'a1 168 167 169 168 val aSM_universe_rect_Type0 : … … 171 170 Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map 172 171 Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map -> 173 __ -> Positive.pos ->'a1) -> aSM_universe -> 'a1172 __ -> 'a1) -> aSM_universe -> 'a1 174 173 175 174 val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe … … 189 188 Identifiers.identifier_map 190 189 191 val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos192 193 190 val aSM_universe_inv_rect_Type4 : 194 191 AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident 195 192 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 196 193 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 197 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1194 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 198 195 199 196 val aSM_universe_inv_rect_Type3 : … … 201 198 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 202 199 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 203 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1200 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 204 201 205 202 val aSM_universe_inv_rect_Type2 : … … 207 204 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 208 205 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 209 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1206 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 210 207 211 208 val aSM_universe_inv_rect_Type1 : … … 213 210 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 214 211 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 215 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1212 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 216 213 217 214 val aSM_universe_inv_rect_Type0 : … … 219 216 -> ASM.identifier Identifiers.identifier_map -> ASM.identifier 220 217 Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word 221 Identifiers.identifier_map -> __ -> Positive.pos ->__ -> 'a1) -> 'a1218 Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 222 219 223 220 val aSM_universe_jmdiscr : 224 221 AST.ident List.list -> aSM_universe -> aSM_universe -> __ 225 226 val report_cost :227 AST.ident List.list -> CostLabel.costlabel -> Types.unit0228 Monad.smax_def__o__monad229 222 230 223 val new_ASM_universe : Joint.joint_program -> aSM_universe -
extracted/rTL.ml
r2961 r2977 125 125 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **) 126 126 let rec rtl_seq_rect_Type4 h_rtl_stack_address = function 127 | Rtl_stack_address (x_ 7, x_6) -> h_rtl_stack_address x_7 x_6127 | Rtl_stack_address (x_1495, x_1494) -> h_rtl_stack_address x_1495 x_1494 128 128 129 129 (** val rtl_seq_rect_Type5 : 130 130 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **) 131 131 let rec rtl_seq_rect_Type5 h_rtl_stack_address = function 132 | Rtl_stack_address (x_1 1, x_10) -> h_rtl_stack_address x_11 x_10132 | Rtl_stack_address (x_1499, x_1498) -> h_rtl_stack_address x_1499 x_1498 133 133 134 134 (** val rtl_seq_rect_Type3 : 135 135 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **) 136 136 let rec rtl_seq_rect_Type3 h_rtl_stack_address = function 137 | Rtl_stack_address (x_15 , x_14) -> h_rtl_stack_address x_15 x_14137 | Rtl_stack_address (x_1503, x_1502) -> h_rtl_stack_address x_1503 x_1502 138 138 139 139 (** val rtl_seq_rect_Type2 : 140 140 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **) 141 141 let rec rtl_seq_rect_Type2 h_rtl_stack_address = function 142 | Rtl_stack_address (x_1 9, x_18) -> h_rtl_stack_address x_19 x_18142 | Rtl_stack_address (x_1507, x_1506) -> h_rtl_stack_address x_1507 x_1506 143 143 144 144 (** val rtl_seq_rect_Type1 : 145 145 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **) 146 146 let rec rtl_seq_rect_Type1 h_rtl_stack_address = function 147 | Rtl_stack_address (x_ 23, x_22) -> h_rtl_stack_address x_23 x_22147 | Rtl_stack_address (x_1511, x_1510) -> h_rtl_stack_address x_1511 x_1510 148 148 149 149 (** val rtl_seq_rect_Type0 : 150 150 (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **) 151 151 let rec rtl_seq_rect_Type0 h_rtl_stack_address = function 152 | Rtl_stack_address (x_ 27, x_26) -> h_rtl_stack_address x_27 x_26152 | Rtl_stack_address (x_1515, x_1514) -> h_rtl_stack_address x_1515 x_1514 153 153 154 154 (** val rtl_seq_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.