Changeset 2001 for src/ASM/ASMCostsSplit.ma

Timestamp:

May 25, 2012, 1:47:32 PM (8 years ago)

Author:

campbell

Message:

Get the compiler to output more.

File:

• src/ASM/ASMCostsSplit.ma (modified) (1 diff)

src/ASM/ASMCostsSplit.ma

@@ -326 +326 @@
     let code_memory ≝ load_code_memory program in
       traverse_code code_memory cost_labels cost_labels_injective.
+
+definition object_code ≝ list Byte.
+definition costlabel_map ≝ BitVectorTrie costlabel 16.      
+
+definition ASM_cost_map :
+  ∀p.let code_memory ≝ load_code_memory (\fst p) in
+  ? → as_cost_map (ASM_abstract_status code_memory (\snd p)) ≝
+  λp : object_code × costlabel_map.
+  λcost_labels_injective.
+  let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
+  λl_sig.
+  lookup_present … cost_map l_sig ?.
+  cases cost_map
+  #m * #prf #_ cases l_sig cases daemon (*bla bla*)
+  qed.