Changeset 2717 for extracted/fetch.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/fetch.ml
r2649 r2717 36 36 37 37 open BitVectorTrie 38 39 open Exp 38 40 39 41 open Arithmetic … … 96 98 (Types.pi1 97 99 (FoldStuff.foldl_strong program0 (fun prefix0 x tl _ labels_costs_ppc > 98 (let { Types.fst = eta2 4561; Types.snd = ppc } =100 (let { Types.fst = eta28757; Types.snd = ppc } = 99 101 Types.pi1 labels_costs_ppc 100 102 in 101 103 (fun _ > 102 (let { Types.fst = labels; Types.snd = costs } = eta2 4561in104 (let { Types.fst = labels; Types.snd = costs } = eta28757 in 103 105 (fun _ > 104 106 (let { Types.fst = label; Types.snd = instr } = x in … … 121 123 (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) cost costs 122 124  ASM.Jmp x0 > costs 125  ASM.Jnz (x0, x1, x2) > costs 126  ASM.MovSuccessor (x0, x1, x2) > costs 123 127  ASM.Call x0 > costs 124 128  ASM.Mov (x0, x1) > costs … … 148 152 (** val bitvector_max_nat : Nat.nat > Nat.nat **) 149 153 let bitvector_max_nat length0 = 150 Util.exponential(Nat.S (Nat.S Nat.O)) length0154 Exp.exp (Nat.S (Nat.S Nat.O)) length0 151 155 152 156 (** val code_memory_size : Nat.nat **) … … 1012 1016 (match b6 with 1013 1017  Bool.True > 1014 { Types.fst = { Types.fst = (ASM. JMP1015 ASM.INDIRECT_DPTR); Types.snd = pc }; Types.snd =1016 (Nat.S (Nat.S Nat.O)) }1018 { Types.fst = { Types.fst = (ASM.RealInstruction 1019 (ASM.JMP ASM.INDIRECT_DPTR)); Types.snd = pc }; 1020 Types.snd = (Nat.S (Nat.S Nat.O)) } 1017 1021  Bool.False > 1018 1022 prod_inv_rect_Type5 (next pmem pc)
Note: See TracChangeset
for help on using the changeset viewer.