source: extracted/positiveMap.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: 4.0 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
19open Positive
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open List
28
29open Util
30
31type 'a positive_map =
32| Pm_leaf
33| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
34
35val positive_map_rect_Type4 :
36  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
37  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
38
39val positive_map_rect_Type3 :
40  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
41  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
42
43val positive_map_rect_Type2 :
44  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
45  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
46
47val positive_map_rect_Type1 :
48  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
49  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
50
51val positive_map_rect_Type0 :
52  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
53  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
54
55val positive_map_inv_rect_Type4 :
56  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
57  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
58
59val positive_map_inv_rect_Type3 :
60  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
61  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
62
63val positive_map_inv_rect_Type2 :
64  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
65  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
66
67val positive_map_inv_rect_Type1 :
68  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
69  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
70
71val positive_map_inv_rect_Type0 :
72  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
73  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
74
75val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __
76
77val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __
78
79val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option
80
81val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1
82
83val pm_set :
84  Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map
85
86val insert : Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map
87
88val update :
89  Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option
90
91val fold0 :
92  (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2
93
94val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map
95
96open Setoids
97
98open Monad
99
100open Option
101
102val is_none : 'a1 Types.option -> Bool.bool
103
104val is_pm_leaf : 'a1 positive_map -> Bool.bool
105
106val map_opt :
107  ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map
108
109val map0 : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map
110
111val merge :
112  ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
113  positive_map -> 'a2 positive_map -> 'a3 positive_map
114
115val domain_size : 'a1 positive_map -> Nat.nat
116
117val pm_all_aux :
118  'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
119  (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool
120
121val pm_all :
122  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool
123
124val pm_choose :
125  'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
126  Types.prod Types.option
127
128val pm_try_remove :
129  Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
130  Types.option
131
132val pm_fold_inf_aux :
133  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
134  positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2
135
136val pm_fold_inf :
137  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
138
139val pm_find_aux :
140  (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos -> 'a1
141  -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option
142
143val pm_find :
144  'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
145  'a1) Types.prod Types.option
146
Note: See TracBrowser for help on using the repository browser.