source: extracted/fetch.mli @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 1.9 KB
Line 
1open Preamble
2
3open Extranat
4
5open Vector
6
7open Div_and_mod
8
9open Jmeq
10
11open Russell
12
13open List
14
15open Util
16
17open FoldStuff
18
19open Bool
20
21open Relations
22
23open Nat
24
25open BitVector
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open BitVectorTrie
38
39open Arithmetic
40
41open String
42
43open LabelledObjects
44
45open Integers
46
47open AST
48
49open CostLabel
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
64
65open Setoids
66
67open Monad
68
69open Option
70
71open Lists
72
73open Positive
74
75open Identifiers
76
77open ASM
78
79val inefficient_address_of_word_labels_code_mem :
80  ASM.labelled_instruction List.list -> ASM.identifier0 ->
81  BitVector.bitVector
82
83type label_map = Nat.nat Identifiers.identifier_map
84
85val create_label_cost_map0 :
86  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
87  BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
88
89val create_label_cost_map :
90  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
91  BitVectorTrie.bitVectorTrie) Types.prod
92
93val address_of_word_labels :
94  ASM.labelled_instruction List.list -> ASM.identifier0 -> BitVector.word
95
96val bitvector_max_nat : Nat.nat -> Nat.nat
97
98val code_memory_size : Nat.nat
99
100val next :
101  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
102  (BitVector.word, BitVector.byte) Types.prod
103
104val load_code_memory0 :
105  BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
106  Types.sig0
107
108val load_code_memory :
109  BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
110
111val prod_inv_rect_Type5 :
112  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
113
114val fetch0 :
115  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
116  BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
117  Types.prod
118
119val fetch :
120  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
121  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
122
Note: See TracBrowser for help on using the repository browser.