source: extracted/assembly.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: 3.7 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open BitVectorTrie
8
9open Exp
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81open Fetch
82
83open Status
84
85type jump_length =
86| Short_jump
87| Absolute_jump
88| Long_jump
89
90val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
91
92val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
93
94val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
95
96val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
97
98val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
99
100val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1
101
102val jump_length_inv_rect_Type4 :
103  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
104
105val jump_length_inv_rect_Type3 :
106  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
107
108val jump_length_inv_rect_Type2 :
109  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
110
111val jump_length_inv_rect_Type1 :
112  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
113
114val jump_length_inv_rect_Type0 :
115  jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
116
117val jump_length_discr : jump_length -> jump_length -> __
118
119val jump_length_jmdiscr : jump_length -> jump_length -> __
120
121val short_jump_cond :
122  BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
123  Types.prod
124
125val absolute_jump_cond :
126  BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
127  Types.prod
128
129val assembly_preinstruction :
130  ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
131  Vector.vector List.list
132
133val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list
134
135val expand_relative_jump_internal :
136  (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
137  -> (BitVector.word -> Bool.bool) -> ASM.identifier0 -> BitVector.word ->
138  (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
139  ASM.instruction List.list
140
141val expand_relative_jump :
142  (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
143  -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier0
144  ASM.preinstruction -> ASM.instruction List.list
145
146val expand_pseudo_instruction :
147  (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
148  -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier0 ->
149  BitVector.word) -> ASM.pseudo_instruction -> ASM.instruction List.list
150
151val assembly_1_pseudoinstruction :
152  (ASM.identifier0 -> BitVector.word) -> (BitVector.word -> BitVector.word)
153  -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier0 ->
154  BitVector.word) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool
155  Vector.vector List.list) Types.prod
156
157val instruction_size :
158  (ASM.identifier0 -> BitVector.word) -> (ASM.identifier0 -> BitVector.word)
159  -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
160  BitVector.word -> ASM.pseudo_instruction -> Nat.nat
161
162val assembly :
163  ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
164  (BitVector.word -> Bool.bool) -> (BitVector.byte List.list,
165  CostLabel.costlabel BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
166
167val assembly_unlabelled_program :
168  ASM.assembly_program -> (BitVector.byte List.list, ASM.identifier0
169  BitVectorTrie.bitVectorTrie) Types.prod Types.option
170
Note: See TracBrowser for help on using the repository browser.