source: extracted/simplifyCasts.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: 4.0 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open TypeComparison
80
81open ClassifyOp
82
83open Smallstep
84
85open Extra_bool
86
87open FrontEndVal
88
89open Hide
90
91open ByteValues
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
99open Csem
100
101open SmallstepExec
102
103open Division
104
105open Z
106
107open BitVectorZ
108
109open Pointers
110
111open Values
112
113open Events
114
115open IOMonad
116
117open IO
118
119open Cexec
120
121open Casts
122
123open CexecInd
124
125open CexecSound
126
127open Sets
128
129open Listb
130
131open Star
132
133open Frontend_misc
134
135val reduce_bits :
136  Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
137  BitVector.bitVector Types.option
138
139val pred_bitsize_of_intsize : AST.intsize -> Nat.nat
140
141val signed : AST.signedness -> Bool.bool
142
143val simplify_int :
144  AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness -> AST.bvint
145  -> AST.bvint Types.option
146
147val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum
148
149val size_not_lt_to_ge : AST.intsize -> AST.intsize -> (__, __) Types.sum
150
151val sign_eq_dect : AST.signedness -> AST.signedness -> (__, __) Types.sum
152
153val necessary_conditions :
154  AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> Bool.bool
155
156val assert_int_value :
157  Values.val0 Types.option -> AST.intsize -> BitVector.bitVector Types.option
158
159val binop_simplifiable : Csyntax.binary_operation -> Bool.bool
160
161val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0
162
163val simplify_expr :
164  Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool, Csyntax.expr)
165  Types.prod Types.sig0
166
167val simplify_e : Csyntax.expr -> Csyntax.expr
168
169val simplify_ls : Csyntax.labeled_statements -> Csyntax.labeled_statements
170
171val simplify_statement : Csyntax.statement -> Csyntax.statement
172
173val simplify_function : Csyntax.function0 -> Csyntax.function0
174
175val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef
176
177val simplify_program : Csyntax.clight_program -> Csyntax.clight_program
178
179val related_globals_rect_Type6 :
180  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
181  -> __ -> 'a2) -> 'a2
182
183val related_globals_rect_Type7 :
184  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
185  -> __ -> 'a2) -> 'a2
186
187val related_globals_rect_Type8 :
188  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
189  -> __ -> 'a2) -> 'a2
190
191val related_globals_rect_Type9 :
192  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
193  -> __ -> 'a2) -> 'a2
194
195val related_globals_rect_Type10 :
196  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
197  -> __ -> 'a2) -> 'a2
198
199val related_globals_rect_Type11 :
200  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
201  -> __ -> 'a2) -> 'a2
202
203val related_globals_inv_rect_Type5 :
204  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
205  -> __ -> __ -> 'a2) -> 'a2
206
207val related_globals_inv_rect_Type6 :
208  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
209  -> __ -> __ -> 'a2) -> 'a2
210
211val related_globals_inv_rect_Type7 :
212  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
213  -> __ -> __ -> 'a2) -> 'a2
214
215val related_globals_inv_rect_Type8 :
216  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
217  -> __ -> __ -> 'a2) -> 'a2
218
219val related_globals_inv_rect_Type9 :
220  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
221  -> __ -> __ -> 'a2) -> 'a2
222
223val related_globals_discr0 :
224  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
225
226val related_globals_jmdiscr0 :
227  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
228
Note: See TracBrowser for help on using the repository browser.