source: extracted/fetch.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 1.9 KB
Line 
1open Preamble
2
3open Char
4
5open String
6
7open Extranat
8
9open Vector
10
11open Div_and_mod
12
13open Jmeq
14
15open Russell
16
17open List
18
19open Util
20
21open FoldStuff
22
23open Bool
24
25open Relations
26
27open Nat
28
29open BitVector
30
31open Hints_declaration
32
33open Core_notation
34
35open Pts
36
37open Logic
38
39open Types
40
41open BitVectorTrie
42
43open Arithmetic
44
45open LabelledObjects
46
47open Coqlib
48
49open Floats
50
51open Integers
52
53open AST
54
55open CostLabel
56
57open Proper
58
59open PositiveMap
60
61open Deqsets
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Lists
76
77open Positive
78
79open Identifiers
80
81open ASM
82
83val inefficient_address_of_word_labels_code_mem :
84  ASM.labelled_instruction List.list -> ASM.identifier0 ->
85  BitVector.bitVector
86
87type label_map = Nat.nat Identifiers.identifier_map
88
89val create_label_cost_map0 :
90  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
91  BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
92
93val create_label_cost_map :
94  ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
95  BitVectorTrie.bitVectorTrie) Types.prod
96
97val address_of_word_labels :
98  ASM.labelled_instruction List.list -> ASM.identifier0 -> BitVector.word
99
100val bitvector_max_nat : Nat.nat -> Nat.nat
101
102val code_memory_size : Nat.nat
103
104val next :
105  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
106  (BitVector.word, BitVector.byte) Types.prod
107
108val load_code_memory0 :
109  BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
110  Types.sig0
111
112val load_code_memory :
113  BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
114
115val prod_inv_rect_Type5 :
116  ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
117
118val fetch0 :
119  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
120  BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
121  Types.prod
122
123val fetch :
124  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
125  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
126
Note: See TracBrowser for help on using the repository browser.