source: extracted/simplifyCasts.mli @ 3015

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