source: extracted/positiveMap.mli @ 2746

Last change on this file since 2746 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: 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
31open Setoids
32
33open Monad
34
35open Option
36
37type 'a positive_map =
38| Pm_leaf
39| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
40
41val positive_map_rect_Type4 :
42  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
43  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
44
45val positive_map_rect_Type3 :
46  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
47  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
48
49val positive_map_rect_Type2 :
50  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
51  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
52
53val positive_map_rect_Type1 :
54  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
55  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
56
57val positive_map_rect_Type0 :
58  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
59  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
60
61val positive_map_inv_rect_Type4 :
62  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
63  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
64
65val positive_map_inv_rect_Type3 :
66  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
67  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
68
69val positive_map_inv_rect_Type2 :
70  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
71  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
72
73val positive_map_inv_rect_Type1 :
74  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
75  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
76
77val positive_map_inv_rect_Type0 :
78  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
79  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
80
81val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __
82
83val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __
84
85val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option
86
87val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1
88
89val pm_set :
90  Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map
91
92val insert : Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map
93
94val update :
95  Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option
96
97val fold0 :
98  (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2
99
100val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map
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.