source: extracted/list.mli @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 3.8 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19type 'a list =
20| Nil
21| Cons of 'a * 'a list
22
23val list_rect_Type4 :
24  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
25
26val list_rect_Type3 :
27  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
28
29val list_rect_Type2 :
30  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
31
32val list_rect_Type1 :
33  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
34
35val list_rect_Type0 :
36  'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2
37
38val list_inv_rect_Type4 :
39  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
40  'a2
41
42val list_inv_rect_Type3 :
43  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
44  'a2
45
46val list_inv_rect_Type2 :
47  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
48  'a2
49
50val list_inv_rect_Type1 :
51  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
52  'a2
53
54val list_inv_rect_Type0 :
55  'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2) ->
56  'a2
57
58val list_discr : 'a1 list -> 'a1 list -> __
59
60val append : 'a1 list -> 'a1 list -> 'a1 list
61
62val hd : 'a1 list -> 'a1 -> 'a1
63
64val tail : 'a1 list -> 'a1 list
65
66val option_hd : 'a1 list -> 'a1 Types.option
67
68val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
69
70val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2
71
72val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list
73
74val compose0 : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list
75
76val rev_append : 'a1 list -> 'a1 list -> 'a1 list
77
78val reverse : 'a1 list -> 'a1 list
79
80val length : 'a1 list -> Nat.nat
81
82type mem = __
83
84val split_rev :
85  'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
86
87val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod
88
89val flatten : 'a1 list list -> 'a1 list
90
91val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1
92
93val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option
94
95type all = __
96
97type allr = __
98
99type exists = __
100
101val fold :
102  ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
103  list -> 'a2
104
105type 'a aop =
106  'a -> 'a -> 'a
107  (* singleton inductive, whose constructor was mk_Aop *)
108
109val aop_rect_Type4 :
110  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
111
112val aop_rect_Type5 :
113  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
114
115val aop_rect_Type3 :
116  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
117
118val aop_rect_Type2 :
119  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
120
121val aop_rect_Type1 :
122  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
123
124val aop_rect_Type0 :
125  'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2
126
127val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1
128
129val aop_inv_rect_Type4 :
130  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
131  'a2
132
133val aop_inv_rect_Type3 :
134  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
135  'a2
136
137val aop_inv_rect_Type2 :
138  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
139  'a2
140
141val aop_inv_rect_Type1 :
142  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
143  'a2
144
145val aop_inv_rect_Type0 :
146  'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
147  'a2
148
149val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __
150
151val dpi1__o__op : 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1
152
153val lhd : 'a1 list -> Nat.nat -> 'a1 list
154
155val ltl : 'a1 list -> Nat.nat -> 'a1 list
156
157val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option
158
159val position_of_aux :
160  ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option
161
162val position_of : ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option
163
164val make_list : 'a1 -> Nat.nat -> 'a1 list
165
Note: See TracBrowser for help on using the repository browser.