source: extracted/util.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: 5.4 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Jmeq
22
23open Russell
24
25type dAEMONXXX =
26| K1DAEMONXXX
27| K2DAEMONXXX
28
29val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
30
31val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
32
33val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
34
35val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
36
37val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
38
39val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1
40
41val dAEMONXXX_inv_rect_Type4 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
42
43val dAEMONXXX_inv_rect_Type3 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
44
45val dAEMONXXX_inv_rect_Type2 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
46
47val dAEMONXXX_inv_rect_Type1 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
48
49val dAEMONXXX_inv_rect_Type0 : dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
50
51val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __
52
53val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __
54
55val ltb : Nat.nat -> Nat.nat -> Bool.bool
56
57val geb : Nat.nat -> Nat.nat -> Bool.bool
58
59val gtb : Nat.nat -> Nat.nat -> Bool.bool
60
61val eq_nat : Nat.nat -> Nat.nat -> Bool.bool
62
63val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
64
65val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list
66
67val fold_left2 :
68  ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list -> 'a1
69
70val remove_n_first_internal :
71  Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list
72
73val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list
74
75val foldi_from_until_internal :
76  Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
77  List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list
78
79val foldi_from_until :
80  Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) ->
81  'a1 List.list -> 'a1 List.list -> 'a1 List.list
82
83val foldi_from :
84  Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
85  List.list -> 'a1 List.list -> 'a1 List.list
86
87val foldi_until :
88  Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
89  List.list -> 'a1 List.list -> 'a1 List.list
90
91val foldi :
92  (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list -> 'a1
93  List.list -> 'a1 List.list
94
95val hd_safe : 'a1 List.list -> 'a1
96
97val tail_safe : 'a1 List.list -> 'a1 List.list
98
99val safe_split :
100  'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod
101
102val nth_safe : Nat.nat -> 'a1 List.list -> 'a1
103
104val last_safe : 'a1 List.list -> 'a1
105
106val reduce :
107  'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
108  Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
109
110val reduce_strong :
111  'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
112  Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
113  Types.sig0
114
115val map2_opt :
116  ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
117  Types.option
118
119val map2 :
120  ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
121
122val map3 :
123  ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
124  List.list -> 'a4 List.list
125
126val eq_rect_Type0_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2
127
128val safe_nth : Nat.nat -> 'a1 List.list -> 'a1
129
130val nub_by_internal :
131  ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list
132
133val nub_by : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
134
135val member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool
136
137val take : Nat.nat -> 'a1 List.list -> 'a1 List.list
138
139val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list
140
141val list_split :
142  Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod
143
144val mapi_internal :
145  Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
146
147val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list
148
149val zip_pottier :
150  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
151
152val zip_safe :
153  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
154
155val zip :
156  'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
157  Types.option
158
159val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
160
161val rev : 'a1 List.list -> 'a1 List.list
162
163val fold_left_i_aux :
164  (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1
165
166val fold_left_i :
167  (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1
168
169val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2
170
171val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1
172
173val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
174
175val division : Nat.nat -> Nat.nat -> Nat.nat
176
177val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
178
179val modulus : Nat.nat -> Nat.nat -> Nat.nat
180
181val divide_with_remainder :
182  Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod
183
184val less_than_or_equal_b_elim :
185  Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
186
187open Div_and_mod
188
189val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
190
191val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
192
193val eq_rect_Type1_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2
194
195val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
196
197val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2
198
199val eq_sum :
200  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
201  Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool
202
203val eq_prod :
204  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
205  Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool
206
Note: See TracBrowser for help on using the repository browser.