source: extracted/integers.mli @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 2.9 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Types
18
19open Extranat
20
21open Vector
22
23open Div_and_mod
24
25open Jmeq
26
27open Russell
28
29open List
30
31open Util
32
33open FoldStuff
34
35open BitVector
36
37open Arithmetic
38
39type comparison =
40| Ceq
41| Cne
42| Clt
43| Cle
44| Cgt
45| Cge
46
47val comparison_rect_Type4 :
48  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
49
50val comparison_rect_Type5 :
51  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
52
53val comparison_rect_Type3 :
54  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
55
56val comparison_rect_Type2 :
57  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
58
59val comparison_rect_Type1 :
60  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
61
62val comparison_rect_Type0 :
63  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
64
65val comparison_inv_rect_Type4 :
66  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
67  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
68
69val comparison_inv_rect_Type3 :
70  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
71  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
72
73val comparison_inv_rect_Type2 :
74  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
75  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
76
77val comparison_inv_rect_Type1 :
78  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
79  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
80
81val comparison_inv_rect_Type0 :
82  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
83  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
84
85val comparison_discr : comparison -> comparison -> __
86
87val comparison_jmdiscr : comparison -> comparison -> __
88
89val negate_comparison : comparison -> comparison
90
91val swap_comparison : comparison -> comparison
92
93val wordsize : Nat.nat
94
95type int = BitVector.bitVector
96
97val repr : Nat.nat -> int
98
99val zero0 : int
100
101val one : int
102
103val mone : BitVector.bitVector
104
105val iwordsize : int
106
107val eq_dec : int -> int -> (__, __) Types.sum
108
109val eq : int -> int -> Bool.bool
110
111val lt : int -> int -> Bool.bool
112
113val ltu : int -> int -> Bool.bool
114
115val neg : int -> int
116
117val mul :
118  BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector
119
120val zero_ext_n :
121  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
122
123val zero_ext0 : Nat.nat -> int -> int
124
125val sign_ext_n :
126  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
127
128val sign_ext0 : Nat.nat -> int -> int
129
130val i_and : int -> int -> int
131
132val or0 : int -> int -> int
133
134val xor : int -> int -> int
135
136val not : int -> int
137
138val shl : int -> int -> int
139
140val shru : int -> int -> int
141
142val shr : int -> int -> int
143
144val shrx : int -> int -> int
145
146val shr_carry : int -> int -> BitVector.bitVector
147
148val rol : int -> int -> int
149
150val ror : int -> int -> int
151
152val rolm : int -> int -> int -> int
153
154val cmp : comparison -> int -> int -> Bool.bool
155
156val cmpu : comparison -> int -> int -> Bool.bool
157
158val notbool : int -> int
159
Note: See TracBrowser for help on using the repository browser.