Changeset 1557 for src/ASM/ASMCosts.ma

Timestamp:

Nov 24, 2011, 6:09:13 PM (8 years ago)

Author:

sacerdot

Message:

Byte => costlabel

File:

• src/ASM/ASMCosts.ma (modified) (8 diffs)

src/ASM/ASMCosts.ma

@@ -158 +158 @@
 
 let rec block_cost'
-  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
+  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     (program_counter: Word) (program_size: nat) (cost_so_far: nat)
       on program_size ≝
@@ -191 +191 @@
 definition block_cost ≝
   λmem: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie Byte 16.
+  λcost_labels: BitVectorTrie costlabel 16.
   λprogram_counter: Word.
   λprogram_size: nat.
@@ -198 +198 @@
 let rec traverse_code_internal
   (program: list Byte) (mem: BitVectorTrie Byte 16)
-    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
-      on program: BitVectorTrie nat 8 ≝
+    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
+      on program: identifier_map CostTag nat ≝
   match instruction_info mem pc with
   [ dp info proof ⇒
     let newpc ≝ \snd (\fst (\fst info)) in
     match program with
-    [ nil ⇒ Stub …
+    [ nil ⇒ empty_map …
     | cons hd tl ⇒
       match lookup_opt … pc cost_labels with
@@ -211 +211 @@
         let cost ≝ block_cost mem cost_labels pc program_size in
         let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
-          insert … lbl cost cost_mapping
+          add … cost_mapping lbl cost
       ]
     ]
@@ -224 +224 @@
 
 let rec first_cost_label_internal
-  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
+  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     (program_size: nat) (oldpc: Word)
-      on program_size: (Byte × nat) ≝
+      on program_size: (costlabel × nat) ≝
   match program_size with
   [ O ⇒ ⊥ (* XXX: ummm ... ? *)
@@ -255 +255 @@
 definition first_cost_label ≝
   λmem: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie Byte 16.
+  λcost_labels: BitVectorTrie costlabel 16.
   λprogram_size: nat.
     first_cost_label_internal mem cost_labels program_size (zero …).
@@ -261 +261 @@
 definition initialize_costs ≝
   λmem: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie Byte 16.
-  λcost_mapping: BitVectorTrie nat 8.
+  λcost_labels: BitVectorTrie costlabel 16.
+  λcost_mapping: identifier_map CostTag nat.
   λprogram_size: nat.
   let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
   let old_cost ≝
-    match lookup_opt … lbl cost_mapping with
+    match lookup ?? cost_mapping lbl with
     [ None ⇒ 0
     | Some cost ⇒ cost
@@ -272 +272 @@
   in
   let new_cost ≝ old_cost + cost in
-    insert … lbl new_cost cost_mapping.
+    add … cost_mapping lbl new_cost.
 
 definition compute_costs ≝
   λprogram: list Byte.
-  λcost_labels: BitVectorTrie Byte 16.
+  λcost_labels: BitVectorTrie costlabel 16.
   λhas_main: bool.
   let program_size ≝ |program| in