source: driver/extracted/values.mli @ 3106

Last change on this file since 3106 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: 3.3 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Coqlib
30
31open ErrorMessages
32
33open Option
34
35open Setoids
36
37open Monad
38
39open Positive
40
41open PreIdentifiers
42
43open Errors
44
45open Proper
46
47open PositiveMap
48
49open Deqsets
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Extranat
68
69open Vector
70
71open FoldStuff
72
73open BitVector
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81type val0 =
82| Vundef
83| Vint of AST.intsize * AST.bvint
84| Vnull
85| Vptr of Pointers.pointer
86
87val val_rect_Type4 :
88  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
89  'a1) -> val0 -> 'a1
90
91val val_rect_Type5 :
92  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
93  'a1) -> val0 -> 'a1
94
95val val_rect_Type3 :
96  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
97  'a1) -> val0 -> 'a1
98
99val val_rect_Type2 :
100  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
101  'a1) -> val0 -> 'a1
102
103val val_rect_Type1 :
104  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
105  'a1) -> val0 -> 'a1
106
107val val_rect_Type0 :
108  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
109  'a1) -> val0 -> 'a1
110
111val val_inv_rect_Type4 :
112  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
113  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
114
115val val_inv_rect_Type3 :
116  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
117  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
118
119val val_inv_rect_Type2 :
120  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
121  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
122
123val val_inv_rect_Type1 :
124  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
125  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
126
127val val_inv_rect_Type0 :
128  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
129  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
130
131val val_discr : val0 -> val0 -> __
132
133val val_jmdiscr : val0 -> val0 -> __
134
135val vzero : AST.intsize -> val0
136
137val vone : AST.intsize -> val0
138
139val mone : AST.intsize -> BitVector.bitVector
140
141val vmone : AST.intsize -> val0
142
143val vtrue : val0
144
145val vfalse : val0
146
147val of_bool : Bool.bool -> val0
148
149val eval_bool_of_val : val0 -> Bool.bool Errors.res
150
151val neg : val0 -> val0
152
153val notint : val0 -> val0
154
155val notbool : val0 -> val0
156
157val zero_ext : AST.intsize -> val0 -> val0
158
159val sign_ext : AST.intsize -> val0 -> val0
160
161val add : val0 -> val0 -> val0
162
163val sub : val0 -> val0 -> val0
164
165val mul : val0 -> val0 -> val0
166
167val v_and : val0 -> val0 -> val0
168
169val or0 : val0 -> val0 -> val0
170
171val xor : val0 -> val0 -> val0
172
173val cmp_match : Integers.comparison -> val0
174
175val cmp_mismatch : Integers.comparison -> val0
176
177val cmp_offset :
178  Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool
179
180val cmp_int :
181  Nat.nat -> Integers.comparison -> BitVector.bitVector ->
182  BitVector.bitVector -> Bool.bool
183
184val cmpu_int :
185  Nat.nat -> Integers.comparison -> BitVector.bitVector ->
186  BitVector.bitVector -> Bool.bool
187
188val cmp : Integers.comparison -> val0 -> val0 -> val0
189
190val cmpu : Integers.comparison -> val0 -> val0 -> val0
191
192val load_result : AST.typ -> val0 -> val0
193
Note: See TracBrowser for help on using the repository browser.