source: extracted/fetch.mli @ 2999

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

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File size: 1.6 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 prod_inv_rect_Type0 :
102  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
103
104val fetch0 :
105  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
106  BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
107  Types.prod
108
109val fetch :
110  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
111  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
112
Note: See TracBrowser for help on using the repository browser.