source: driver/extracted/fetch.mli @ 3106

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

New extraction.

File size: 1.5 KB
Line 
1open Preamble
2
3open Types
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Jmeq
14
15open Russell
16
17open Exp
18
19open Setoids
20
21open Monad
22
23open Option
24
25open Extranat
26
27open Vector
28
29open Div_and_mod
30
31open List
32
33open Util
34
35open FoldStuff
36
37open Bool
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_label :
82  ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
83
84type label_map = Nat.nat Identifiers.identifier_map
85
86val create_label_cost_map0 :
87  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
88  Types.prod Types.sig0
89
90val create_label_cost_map :
91  ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
92  Types.prod
93
94val address_of_word_labels :
95  ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
96
97val prod_inv_rect_Type0 :
98  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
99
100val fetch0 :
101  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
102  BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
103  Types.prod
104
105val fetch :
106  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
107  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
108
Note: See TracBrowser for help on using the repository browser.