]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blob - extracted/fetch.mli
Control and copyright added.
[pkg-cerco/acc-trusted.git] / extracted / fetch.mli
1 open Preamble
2
3 open Types
4
5 open Hints_declaration
6
7 open Core_notation
8
9 open Pts
10
11 open Logic
12
13 open Jmeq
14
15 open Russell
16
17 open Exp
18
19 open Setoids
20
21 open Monad
22
23 open Option
24
25 open Extranat
26
27 open Vector
28
29 open Div_and_mod
30
31 open List
32
33 open Util
34
35 open FoldStuff
36
37 open Bool
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_label :
82   ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
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, ASM.costlabel_map)
88   Types.prod Types.sig0
89
90 val create_label_cost_map :
91   ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
92   Types.prod
93
94 val address_of_word_labels :
95   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
96
97 val prod_inv_rect_Type0 :
98   ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
99
100 val fetch0 :
101   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
102   BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
103   Types.prod
104
105 val fetch :
106   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
107   ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
108