source: extracted/integers.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: 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 Exp
38
39open Arithmetic
40
41type comparison =
42| Ceq
43| Cne
44| Clt
45| Cle
46| Cgt
47| Cge
48
49val comparison_rect_Type4 :
50  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
51
52val comparison_rect_Type5 :
53  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
54
55val comparison_rect_Type3 :
56  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
57
58val comparison_rect_Type2 :
59  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
60
61val comparison_rect_Type1 :
62  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
63
64val comparison_rect_Type0 :
65  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> comparison -> 'a1
66
67val comparison_inv_rect_Type4 :
68  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
69  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
70
71val comparison_inv_rect_Type3 :
72  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
73  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
74
75val comparison_inv_rect_Type2 :
76  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
77  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
78
79val comparison_inv_rect_Type1 :
80  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
81  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
82
83val comparison_inv_rect_Type0 :
84  comparison -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
85  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
86
87val comparison_discr : comparison -> comparison -> __
88
89val comparison_jmdiscr : comparison -> comparison -> __
90
91val negate_comparison : comparison -> comparison
92
93val swap_comparison : comparison -> comparison
94
95val wordsize : Nat.nat
96
97type int = BitVector.bitVector
98
99val repr : Nat.nat -> int
100
101val zero0 : int
102
103val one : int
104
105val mone : BitVector.bitVector
106
107val iwordsize : int
108
109val eq_dec : int -> int -> (__, __) Types.sum
110
111val eq : int -> int -> Bool.bool
112
113val lt : int -> int -> Bool.bool
114
115val ltu : int -> int -> Bool.bool
116
117val neg : int -> int
118
119val mul :
120  BitVector.bitVector -> BitVector.bitVector -> Bool.bool Vector.vector
121
122val zero_ext_n :
123  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
124
125val zero_ext0 : Nat.nat -> int -> int
126
127val sign_ext_n :
128  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
129
130val sign_ext0 : Nat.nat -> int -> int
131
132val i_and : int -> int -> int
133
134val or0 : int -> int -> int
135
136val xor : int -> int -> int
137
138val not : int -> int
139
140val shl : int -> int -> int
141
142val shru : int -> int -> int
143
144val shr : int -> int -> int
145
146val shrx : int -> int -> int
147
148val shr_carry : int -> int -> BitVector.bitVector
149
150val rol : int -> int -> int
151
152val ror : int -> int -> int
153
154val rolm : int -> int -> int -> int
155
156val cmp : comparison -> int -> int -> Bool.bool
157
158val cmpu : comparison -> int -> int -> Bool.bool
159
160val notbool : int -> int
161
Note: See TracBrowser for help on using the repository browser.