]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/fetch.mli
Imported Upstream version 0.1
[pkg-cerco/acc-trusted.git] / extracted / fetch.mli
1 open Preamble
2
3 open Exp
4
5 open Setoids
6
7 open Monad
8
9 open Option
10
11 open Extranat
12
13 open Vector
14
15 open Div_and_mod
16
17 open Jmeq
18
19 open Russell
20
21 open Types
22
23 open List
24
25 open Util
26
27 open FoldStuff
28
29 open Bool
30
31 open Hints_declaration
32
33 open Core_notation
34
35 open Pts
36
37 open Logic
38
39 open Relations
40
41 open Nat
42
43 open BitVector
44
45 open Arithmetic
46
47 open BitVectorTrie
48
49 open String
50
51 open Integers
52
53 open AST
54
55 open LabelledObjects
56
57 open Proper
58
59 open PositiveMap
60
61 open Deqsets
62
63 open ErrorMessages
64
65 open PreIdentifiers
66
67 open Errors
68
69 open Extralib
70
71 open Lists
72
73 open Positive
74
75 open Identifiers
76
77 open CostLabel
78
79 open ASM
80
81 val inefficient_address_of_word_labels_code_mem :
82   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
83
84 type label_map = Nat.nat Identifiers.identifier_map
85
86 val create_label_cost_map0 :
87   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
88   BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
89
90 val create_label_cost_map :
91   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
92   BitVectorTrie.bitVectorTrie) Types.prod
93
94 val address_of_word_labels :
95   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
96
97 val bitvector_max_nat : Nat.nat -> Nat.nat
98
99 val code_memory_size : Nat.nat
100
101 val prod_inv_rect_Type0 :
102   ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
103
104 val fetch0 :
105   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
106   BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
107   Types.prod
108
109 val fetch :
110   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
111   ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
112