source: extracted/fetch.mli @ 2960

Last change on this file since 2960 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 1.9 KB
Line 
1open Preamble
2
3open Exp
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open Types
22
23open List
24
25open Util
26
27open FoldStuff
28
29open Bool
30
31open Hints_declaration
32
33open Core_notation
34
35open Pts
36
37open Logic
38
39open Relations
40
41open Nat
42
43open BitVector
44
45open Arithmetic
46
47open BitVectorTrie
48
49open String
50
51open Integers
52
53open AST
54
55open LabelledObjects
56
57open Proper
58
59open PositiveMap
60
61open Deqsets
62
63open ErrorMessages
64
65open PreIdentifiers
66
67open Errors
68
69open Extralib
70
71open Lists
72
73open Positive
74
75open Identifiers
76
77open CostLabel
78
79open ASM
80
81val inefficient_address_of_word_labels_code_mem :
82  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
83
84type label_map = Nat.nat Identifiers.identifier_map
85
86val create_label_cost_map0 :
87  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
88  BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
89
90val create_label_cost_map :
91  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
92  BitVectorTrie.bitVectorTrie) Types.prod
93
94val address_of_word_labels :
95  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
96
97val bitvector_max_nat : Nat.nat -> Nat.nat
98
99val code_memory_size : Nat.nat
100
101val next :
102  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
103  (BitVector.word, BitVector.byte) Types.prod
104
105val load_code_memory0 :
106  ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
107
108val load_code_memory :
109  ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
110
111val prod_inv_rect_Type0 :
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.