Merge tag 'upstream/0.2'

[pkg-cerco/acc-trusted.git] / extracted / fetch.ml

diff --git a/extracted/fetch.ml b/extracted/fetch.ml
index 4ad7b4f6387719f40bf33896e8d6dbb96a6bb894..0932432faba353fe8bf9751015c32cca36d2eaa6 100644 (file)
--- a/extracted/fetch.ml
+++ b/extracted/fetch.ml
@@ -1,5 +1,19 @@
 open Preamble
 
+open Types
+
+open Hints_declaration
+
+open Core_notation
+
+open Pts
+
+open Logic
+
+open Jmeq
+
+open Russell
+
 open Exp
 
 open Setoids
@@ -14,12 +28,6 @@ open Vector
 
 open Div_and_mod
 
-open Jmeq
-
-open Russell
-
-open Types
-
 open List
 
 open Util
@@ -28,14 +36,6 @@ open FoldStuff
 
 open Bool
 
-open Hints_declaration
-
-open Core_notation
-
-open Pts
-
-open Logic
-
 open Relations
 
 open Nat
@@ -78,30 +78,26 @@ open CostLabel
 
 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 _ ->
@@ -134,29 +130,21 @@ let create_label_cost_map0 program =
       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 **)