source: extracted/fetch.mli @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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 Exp
40
41open Arithmetic
42
43open String
44
45open LabelledObjects
46
47open Integers
48
49open AST
50
51open CostLabel
52
53open Proper
54
55open PositiveMap
56
57open Deqsets
58
59open ErrorMessages
60
61open PreIdentifiers
62
63open Errors
64
65open Extralib
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Lists
74
75open Positive
76
77open Identifiers
78
79open ASM
80
81val inefficient_address_of_word_labels_code_mem :
82  ASM.labelled_instruction List.list -> ASM.identifier0 ->
83  BitVector.bitVector
84
85type label_map = Nat.nat Identifiers.identifier_map
86
87val create_label_cost_map0 :
88  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
89  BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
90
91val create_label_cost_map :
92  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
93  BitVectorTrie.bitVectorTrie) Types.prod
94
95val address_of_word_labels :
96  ASM.labelled_instruction List.list -> ASM.identifier0 -> BitVector.word
97
98val bitvector_max_nat : Nat.nat -> Nat.nat
99
100val code_memory_size : Nat.nat
101
102val next :
103  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
104  (BitVector.word, BitVector.byte) Types.prod
105
106val load_code_memory0 :
107  BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
108  Types.sig0
109
110val load_code_memory :
111  BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
112
113val prod_inv_rect_Type5 :
114  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
115
116val fetch0 :
117  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
118  BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
119  Types.prod
120
121val fetch :
122  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
123  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
124
Note: See TracBrowser for help on using the repository browser.