source: extracted/util.mli @ 2716

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 5.5 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 exponential : Nat.nat -> Nat.nat -> Nat.nat
185
186val less_than_or_equal_b_elim :
187  Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
188
189open Div_and_mod
190
191type even_p = __
192
193type odd_p = __
194
195val if_then_else_safe : Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
196
197val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
198
199val eq_rect_Type1_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2
200
201val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
202
203val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2
204
205val eq_sum :
206  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
207  Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool
208
209val eq_prod :
210  ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
211  Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool
212
Note: See TracBrowser for help on using the repository browser.