open Preamble
+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+
open Exp
open Setoids
open Div_and_mod
-open Jmeq
-
-open Russell
-
-open Types
-
open List
open Util
open Bool
-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-
open Relations
open Nat
open ASM
-(** val inefficient_address_of_word_labels_code_mem :
- ASM.labelled_instruction List.list -> ASM.identifier ->
- BitVector.bitVector **)
-let inefficient_address_of_word_labels_code_mem code_mem id =
- Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (LabelledObjects.index_of
- (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
- id) code_mem)
+(** val inefficient_address_of_label :
+ ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **)
+let inefficient_address_of_label instr_list id =
+ LabelledObjects.index_of
+ (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id)
+ instr_list
type label_map = Nat.nat Identifiers.identifier_map
(** val create_label_cost_map0 :
- ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
+ ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+ Types.prod Types.sig0 **)
let create_label_cost_map0 program =
(Types.pi1
(FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
- (let { Types.fst = eta28695; Types.snd = ppc } =
+ (let { Types.fst = eta19; Types.snd = ppc } =
Types.pi1 labels_costs_ppc
in
(fun _ ->
- (let { Types.fst = labels; Types.snd = costs } = eta28695 in
+ (let { Types.fst = labels; Types.snd = costs } = eta19 in
(fun _ ->
(let { Types.fst = label; Types.snd = instr } = x in
(fun _ ->
Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
(** val create_label_cost_map :
- ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
- BitVectorTrie.bitVectorTrie) Types.prod **)
+ ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
+ Types.prod **)
let create_label_cost_map program =
Types.pi1 (create_label_cost_map0 program)
(** val address_of_word_labels :
ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
-let address_of_word_labels code_mem id =
- let labels = (create_label_cost_map code_mem).Types.fst in
+let address_of_word_labels program id =
+ let labels = (create_label_cost_map program).Types.fst in
+ let address_of_label = fun l ->
+ Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O
+ in
Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
- (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
-
-(** val bitvector_max_nat : Nat.nat -> Nat.nat **)
-let bitvector_max_nat length =
- Exp.exp (Nat.S (Nat.S Nat.O)) length
-
-(** val code_memory_size : Nat.nat **)
-let code_memory_size =
- bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
- Nat.O))))))))))))))))
+ Nat.O)))))))))))))))) (address_of_label id)
(** val prod_inv_rect_Type0 :
('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)