source: extracted/simplifyCasts.mli @ 2960

Last change on this file since 2960 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
RevLine 
[2601]1open Preamble
2
3open CostLabel
4
[2649]5open Coqlib
6
[2601]7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
[2717]27open Exp
28
[2601]29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
[2773]35open Util
36
37open FoldStuff
38
39open BitVector
40
[2601]41open Jmeq
42
43open Russell
44
45open List
46
[2773]47open Setoids
[2601]48
[2773]49open Monad
[2601]50
[2773]51open Option
[2601]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
[2773]177val related_globals_rect_Type4 :
[2601]178  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
179  -> __ -> 'a2) -> 'a2
180
[2773]181val related_globals_rect_Type5 :
[2601]182  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
183  -> __ -> 'a2) -> 'a2
184
[2773]185val related_globals_rect_Type3 :
[2601]186  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
187  -> __ -> 'a2) -> 'a2
188
[2773]189val related_globals_rect_Type2 :
[2601]190  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
191  -> __ -> 'a2) -> 'a2
192
[2773]193val related_globals_rect_Type1 :
[2601]194  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
195  -> __ -> 'a2) -> 'a2
196
[2773]197val related_globals_rect_Type0 :
[2601]198  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
199  -> __ -> 'a2) -> 'a2
200
[2773]201val related_globals_inv_rect_Type4 :
[2601]202  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
203  -> __ -> __ -> 'a2) -> 'a2
204
[2773]205val related_globals_inv_rect_Type3 :
[2601]206  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
207  -> __ -> __ -> 'a2) -> 'a2
208
[2773]209val related_globals_inv_rect_Type2 :
[2601]210  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
211  -> __ -> __ -> 'a2) -> 'a2
212
[2773]213val related_globals_inv_rect_Type1 :
[2601]214  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
215  -> __ -> __ -> 'a2) -> 'a2
216
[2773]217val related_globals_inv_rect_Type0 :
[2601]218  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ -> __
219  -> __ -> __ -> 'a2) -> 'a2
220
[2773]221val related_globals_discr :
[2601]222  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
223
[2773]224val related_globals_jmdiscr :
[2601]225  ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __
226
Note: See TracBrowser for help on using the repository browser.