source: extracted/vector.mli @ 2746

Last change on this file since 2746 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.0 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 Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29open Extranat
30
31type 'a vector =
32| VEmpty
33| VCons of Nat.nat * 'a * 'a vector
34
35val vector_rect_Type4 :
36  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
37  vector -> 'a2
38
39val vector_rect_Type3 :
40  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
41  vector -> 'a2
42
43val vector_rect_Type2 :
44  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
45  vector -> 'a2
46
47val vector_rect_Type1 :
48  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
49  vector -> 'a2
50
51val vector_rect_Type0 :
52  'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
53  vector -> 'a2
54
55val vector_inv_rect_Type4 :
56  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
57  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
58
59val vector_inv_rect_Type3 :
60  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
61  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
62
63val vector_inv_rect_Type2 :
64  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
65  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
66
67val vector_inv_rect_Type1 :
68  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
69  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
70
71val vector_inv_rect_Type0 :
72  Nat.nat -> 'a1 vector -> (__ -> __ -> 'a2) -> (Nat.nat -> 'a1 -> 'a1 vector
73  -> (__ -> __ -> 'a2) -> __ -> __ -> 'a2) -> 'a2
74
75val vector_discr : Nat.nat -> 'a1 vector -> 'a1 vector -> __
76
77val vector_jmdiscr : Nat.nat -> 'a1 vector -> 'a1 vector -> __
78
79val get_index_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1
80
81val get_index' : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1
82
83val get_index_weak_v : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 Types.option
84
85val set_index : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector
86
87val set_index_weak :
88  Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 -> 'a1 vector Types.option
89
90val drop0 : Nat.nat -> 'a1 vector -> Nat.nat -> 'a1 vector Types.option
91
92val head' : Nat.nat -> 'a1 vector -> 'a1
93
94val tail0 : Nat.nat -> 'a1 vector -> 'a1 vector
95
96val vsplit' :
97  Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod
98
99val vsplit :
100  Nat.nat -> Nat.nat -> 'a1 vector -> ('a1 vector, 'a1 vector) Types.prod
101
102val head : Nat.nat -> 'a1 vector -> ('a1, 'a1 vector) Types.prod
103
104val from_singl : 'a1 vector -> 'a1
105
106val fold_right : Nat.nat -> ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2
107
108val fold_right_i :
109  Nat.nat -> (Nat.nat -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 vector -> 'a2
110
111val fold_right2_i :
112  (Nat.nat -> 'a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> Nat.nat -> 'a1 vector ->
113  'a2 vector -> 'a3
114
115val fold_left : Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1
116
117val map0 : Nat.nat -> ('a1 -> 'a2) -> 'a1 vector -> 'a2 vector
118
119val zip_with :
120  Nat.nat -> ('a1 -> 'a2 -> 'a3) -> 'a1 vector -> 'a2 vector -> 'a3 vector
121
122val zip0 :
123  Nat.nat -> 'a1 vector -> 'a2 vector -> ('a1, 'a2) Types.prod vector
124
125val replicate : Nat.nat -> 'a1 -> 'a1 vector
126
127val append0 : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector
128
129val scan_left :
130  Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 vector -> 'a1 vector
131
132val scan_right :
133  Nat.nat -> ('a1 -> 'a2 -> 'a1) -> 'a2 -> 'a1 vector -> 'a1 List.list
134
135val revapp : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector -> 'a1 vector
136
137val reverse0 : Nat.nat -> 'a1 vector -> 'a1 vector
138
139val pad_vector : 'a1 -> Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
140
141val list_of_vector : Nat.nat -> 'a1 vector -> 'a1 List.list
142
143val vector_of_list : 'a1 List.list -> 'a1 vector
144
145val rotate_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
146
147val rotate_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
148
149val shift_left_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
150
151val switch_bv_plus : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector
152
153val shift_right_1 : Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
154
155val shift_left : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
156
157val shift_right : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 -> 'a1 vector
158
159val eq_v :
160  Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector ->
161  Bool.bool
162
163val vector_inv_n : Nat.nat -> 'a1 vector -> __
164
165val eq_v_elim :
166  ('a2 -> 'a2 -> Bool.bool) -> (__ -> 'a2 -> 'a2 -> (__ -> __) -> (__ -> __)
167  -> __) -> Nat.nat -> 'a2 vector -> 'a2 vector -> (__ -> 'a1) -> (__ -> 'a1)
168  -> 'a1
169
170val mem0 :
171  ('a1 -> 'a1 -> Bool.bool) -> Nat.nat -> 'a1 vector -> 'a1 -> Bool.bool
172
173val subvector_with :
174  Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
175  -> Bool.bool
176
177val vprefix :
178  Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
179  -> Bool.bool
180
181val vsuffix :
182  Nat.nat -> Nat.nat -> ('a1 -> 'a1 -> Bool.bool) -> 'a1 vector -> 'a1 vector
183  -> Bool.bool
184
185val rvsplit : Nat.nat -> Nat.nat -> 'a1 vector -> 'a1 vector vector
186
187val vflatten : Nat.nat -> Nat.nat -> 'a1 vector vector -> 'a1 vector
188
Note: See TracBrowser for help on using the repository browser.