source: extracted/fetch.mli @ 2968

Last change on this file since 2968 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
RevLine 
[2601]1open Preamble
2
[2773]3open Exp
4
5open Setoids
6
7open Monad
8
9open Option
10
[2601]11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
[2773]21open Types
22
[2601]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
[2773]39open Relations
[2601]40
[2773]41open Nat
[2601]42
[2773]43open BitVector
[2717]44
[2601]45open Arithmetic
46
[2773]47open BitVectorTrie
48
[2649]49open String
50
[2601]51open Integers
52
53open AST
54
[2773]55open LabelledObjects
[2601]56
57open Proper
58
59open PositiveMap
60
61open Deqsets
62
[2649]63open ErrorMessages
64
[2601]65open PreIdentifiers
66
67open Errors
68
69open Extralib
70
71open Lists
72
73open Positive
74
75open Identifiers
76
[2773]77open CostLabel
78
[2601]79open ASM
80
81val inefficient_address_of_word_labels_code_mem :
[2773]82  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
[2601]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 :
[2773]95  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
[2601]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 :
[2773]106  ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0
[2601]107
108val load_code_memory :
[2773]109  ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie
[2601]110
[2773]111val prod_inv_rect_Type0 :
[2601]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.