source: extracted/interpret.mli @ 2717

Last change on this file since 2717 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: 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 String
28
29open LabelledObjects
30
31open BitVectorTrie
32
33open Exp
34
35open Arithmetic
36
37open Integers
38
39open AST
40
41open CostLabel
42
43open Proper
44
45open PositiveMap
46
47open ErrorMessages
48
49open PreIdentifiers
50
51open Errors
52
53open Extralib
54
55open Setoids
56
57open Monad
58
59open Option
60
61open Lists
62
63open Positive
64
65open Identifiers
66
67open Extranat
68
69open Vector
70
71open Div_and_mod
72
73open Jmeq
74
75open Russell
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open ASM
84
85open Status
86
87open StatusProofs
88
89open Fetch
90
91open StructuredTraces
92
93open AbstractStatus
94
95val execute_1_preinstruction :
96  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
97  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
98  Status.preStatus
99
100val execute_1_preinstruction_ok' :
101  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
102  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
103  Status.preStatus Types.sig0
104
105val compute_target_of_unconditional_jump :
106  BitVector.word -> ASM.instruction -> BitVector.word
107
108val is_unconditional_jump : ASM.instruction -> Bool.bool
109
110val program_counter_after_other :
111  BitVector.word -> ASM.instruction -> BitVector.word
112
113val addr_of_relative :
114  'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word
115
116val execute_1_0 :
117  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
118  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
119  Status.status Types.sig0
120
121val current_instruction_cost :
122  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat
123
124val execute_1' :
125  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
126  Status.status Types.sig0
127
128val execute_1 :
129  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
130  Status.status
131
132val execute_1_pseudo_instruction0 :
133  (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
134  Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
135  Status.pseudoStatus
136
137val execute_1_pseudo_instruction :
138  (ASM.preamble, ASM.labelled_instruction List.list) Types.prod ->
139  (BitVector.word -> __ -> (Nat.nat, Nat.nat) Types.prod) ->
140  Status.pseudoStatus -> Status.pseudoStatus
141
142val execute :
143  Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
144  Status.status
145
Note: See TracBrowser for help on using the repository browser.