source: extracted/interpret.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: 2.4 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Sets
6
7open Bool
8
9open Relations
10
11open Nat
12
13open Hints_declaration
14
15open Core_notation
16
17open Pts
18
19open Logic
20
21open Types
22
23open List
24
25open Listb
26
27open BitVectorTrie
28
29open LabelledObjects
30
31open Coqlib
32
33open Floats
34
35open Arithmetic
36
37open Integers
38
39open AST
40
41open CostLabel
42
43open Proper
44
45open PositiveMap
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Lists
60
61open Positive
62
63open Identifiers
64
65open Char
66
67open String
68
69open Extranat
70
71open Vector
72
73open Div_and_mod
74
75open Jmeq
76
77open Russell
78
79open Util
80
81open FoldStuff
82
83open BitVector
84
85open ASM
86
87open Status
88
89open StatusProofs
90
91open Fetch
92
93open StructuredTraces
94
95open AbstractStatus
96
97val execute_1_preinstruction :
98  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
99  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
100  Status.preStatus
101
102val execute_1_preinstruction_ok' :
103  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
104  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
105  Status.preStatus Types.sig0
106
107val compute_target_of_unconditional_jump :
108  BitVector.word -> ASM.instruction -> BitVector.word
109
110val is_unconditional_jump : ASM.instruction -> Bool.bool
111
112val program_counter_after_other :
113  BitVector.word -> ASM.instruction -> BitVector.word
114
115val addr_of_relative :
116  'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word
117
118val execute_1_0 :
119  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
120  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
121  Status.status Types.sig0
122
123val current_instruction_cost :
124  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat
125
126val execute_1' :
127  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
128  Status.status Types.sig0
129
130val execute_1 :
131  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
132  Status.status
133
134val execute_1_pseudo_instruction0 :
135  (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
136  Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
137  Status.pseudoStatus
138
139val execute_1_pseudo_instruction :
140  (ASM.preamble, ASM.labelled_instruction List.list) Types.prod ->
141  (BitVector.word -> __ -> (Nat.nat, Nat.nat) Types.prod) ->
142  Status.pseudoStatus -> Status.pseudoStatus
143
144val execute :
145  Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
146  Status.status
147
Note: See TracBrowser for help on using the repository browser.