[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Hints_declaration |
---|
| 4 | |
---|
| 5 | open Core_notation |
---|
| 6 | |
---|
| 7 | open Pts |
---|
| 8 | |
---|
| 9 | open Logic |
---|
| 10 | |
---|
| 11 | open Types |
---|
| 12 | |
---|
| 13 | open Bool |
---|
| 14 | |
---|
| 15 | open Relations |
---|
| 16 | |
---|
| 17 | open Nat |
---|
| 18 | |
---|
| 19 | open Positive |
---|
| 20 | |
---|
| 21 | open Div_and_mod |
---|
| 22 | |
---|
| 23 | open Jmeq |
---|
| 24 | |
---|
| 25 | open Russell |
---|
| 26 | |
---|
| 27 | open List |
---|
| 28 | |
---|
| 29 | open Util |
---|
| 30 | |
---|
[2717] | 31 | open Setoids |
---|
| 32 | |
---|
| 33 | open Monad |
---|
| 34 | |
---|
| 35 | open Option |
---|
| 36 | |
---|
[2601] | 37 | type 'a positive_map = |
---|
| 38 | | Pm_leaf |
---|
| 39 | | Pm_node of 'a Types.option * 'a positive_map * 'a positive_map |
---|
| 40 | |
---|
| 41 | (** val positive_map_rect_Type4 : |
---|
| 42 | 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 |
---|
| 43 | -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **) |
---|
| 44 | let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function |
---|
| 45 | | Pm_leaf -> h_pm_leaf |
---|
[2827] | 46 | | Pm_node (x_3287, x_3286, x_3285) -> |
---|
| 47 | h_pm_node x_3287 x_3286 x_3285 |
---|
| 48 | (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3286) |
---|
| 49 | (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3285) |
---|
[2601] | 50 | |
---|
| 51 | (** val positive_map_rect_Type3 : |
---|
| 52 | 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 |
---|
| 53 | -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **) |
---|
| 54 | let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function |
---|
| 55 | | Pm_leaf -> h_pm_leaf |
---|
[2827] | 56 | | Pm_node (x_3299, x_3298, x_3297) -> |
---|
| 57 | h_pm_node x_3299 x_3298 x_3297 |
---|
| 58 | (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3298) |
---|
| 59 | (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3297) |
---|
[2601] | 60 | |
---|
| 61 | (** val positive_map_rect_Type2 : |
---|
| 62 | 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 |
---|
| 63 | -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **) |
---|
| 64 | let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function |
---|
| 65 | | Pm_leaf -> h_pm_leaf |
---|
[2827] | 66 | | Pm_node (x_3305, x_3304, x_3303) -> |
---|
| 67 | h_pm_node x_3305 x_3304 x_3303 |
---|
| 68 | (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3304) |
---|
| 69 | (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3303) |
---|
[2601] | 70 | |
---|
| 71 | (** val positive_map_rect_Type1 : |
---|
| 72 | 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 |
---|
| 73 | -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **) |
---|
| 74 | let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function |
---|
| 75 | | Pm_leaf -> h_pm_leaf |
---|
[2827] | 76 | | Pm_node (x_3311, x_3310, x_3309) -> |
---|
| 77 | h_pm_node x_3311 x_3310 x_3309 |
---|
| 78 | (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3310) |
---|
| 79 | (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3309) |
---|
[2601] | 80 | |
---|
| 81 | (** val positive_map_rect_Type0 : |
---|
| 82 | 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 |
---|
| 83 | -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **) |
---|
| 84 | let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function |
---|
| 85 | | Pm_leaf -> h_pm_leaf |
---|
[2827] | 86 | | Pm_node (x_3317, x_3316, x_3315) -> |
---|
| 87 | h_pm_node x_3317 x_3316 x_3315 |
---|
| 88 | (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3316) |
---|
| 89 | (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3315) |
---|
[2601] | 90 | |
---|
| 91 | (** val positive_map_inv_rect_Type4 : |
---|
| 92 | 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map |
---|
| 93 | -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 94 | let positive_map_inv_rect_Type4 hterm h1 h2 = |
---|
| 95 | let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __ |
---|
| 96 | |
---|
| 97 | (** val positive_map_inv_rect_Type3 : |
---|
| 98 | 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map |
---|
| 99 | -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 100 | let positive_map_inv_rect_Type3 hterm h1 h2 = |
---|
| 101 | let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __ |
---|
| 102 | |
---|
| 103 | (** val positive_map_inv_rect_Type2 : |
---|
| 104 | 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map |
---|
| 105 | -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 106 | let positive_map_inv_rect_Type2 hterm h1 h2 = |
---|
| 107 | let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __ |
---|
| 108 | |
---|
| 109 | (** val positive_map_inv_rect_Type1 : |
---|
| 110 | 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map |
---|
| 111 | -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 112 | let positive_map_inv_rect_Type1 hterm h1 h2 = |
---|
| 113 | let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __ |
---|
| 114 | |
---|
| 115 | (** val positive_map_inv_rect_Type0 : |
---|
| 116 | 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map |
---|
| 117 | -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **) |
---|
| 118 | let positive_map_inv_rect_Type0 hterm h1 h2 = |
---|
| 119 | let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __ |
---|
| 120 | |
---|
| 121 | (** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **) |
---|
| 122 | let positive_map_discr x y = |
---|
| 123 | Logic.eq_rect_Type2 x |
---|
| 124 | (match x with |
---|
| 125 | | Pm_leaf -> Obj.magic (fun _ dH -> dH) |
---|
| 126 | | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 127 | |
---|
| 128 | (** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **) |
---|
| 129 | let positive_map_jmdiscr x y = |
---|
| 130 | Logic.eq_rect_Type2 x |
---|
| 131 | (match x with |
---|
| 132 | | Pm_leaf -> Obj.magic (fun _ dH -> dH) |
---|
| 133 | | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 134 | |
---|
| 135 | (** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **) |
---|
| 136 | let rec lookup_opt b = function |
---|
| 137 | | Pm_leaf -> Types.None |
---|
| 138 | | Pm_node (a, l, r) -> |
---|
| 139 | (match b with |
---|
| 140 | | Positive.One -> a |
---|
| 141 | | Positive.P1 tl -> lookup_opt tl r |
---|
| 142 | | Positive.P0 tl -> lookup_opt tl l) |
---|
| 143 | |
---|
| 144 | (** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **) |
---|
| 145 | let lookup b t x = |
---|
| 146 | match lookup_opt b t with |
---|
| 147 | | Types.None -> x |
---|
| 148 | | Types.Some r -> r |
---|
| 149 | |
---|
| 150 | (** val pm_set : |
---|
| 151 | Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **) |
---|
| 152 | let rec pm_set b a t = |
---|
| 153 | match b with |
---|
| 154 | | Positive.One -> |
---|
| 155 | (match t with |
---|
| 156 | | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf) |
---|
| 157 | | Pm_node (x, l, r) -> Pm_node (a, l, r)) |
---|
| 158 | | Positive.P1 tl -> |
---|
| 159 | (match t with |
---|
| 160 | | Pm_leaf -> Pm_node (Types.None, Pm_leaf, (pm_set tl a Pm_leaf)) |
---|
| 161 | | Pm_node (x, l, r) -> Pm_node (x, l, (pm_set tl a r))) |
---|
| 162 | | Positive.P0 tl -> |
---|
| 163 | (match t with |
---|
| 164 | | Pm_leaf -> Pm_node (Types.None, (pm_set tl a Pm_leaf), Pm_leaf) |
---|
| 165 | | Pm_node (x, l, r) -> Pm_node (x, (pm_set tl a l), r)) |
---|
| 166 | |
---|
| 167 | (** val insert : |
---|
| 168 | Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **) |
---|
| 169 | let insert p a = |
---|
| 170 | pm_set p (Types.Some a) |
---|
| 171 | |
---|
| 172 | (** val update : |
---|
| 173 | Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **) |
---|
| 174 | let rec update b a t = |
---|
| 175 | match b with |
---|
| 176 | | Positive.One -> |
---|
| 177 | (match t with |
---|
| 178 | | Pm_leaf -> Types.None |
---|
| 179 | | Pm_node (x, l, r) -> |
---|
| 180 | Types.option_map (fun x0 -> Pm_node ((Types.Some a), l, r)) x) |
---|
| 181 | | Positive.P1 tl -> |
---|
| 182 | (match t with |
---|
| 183 | | Pm_leaf -> Types.None |
---|
| 184 | | Pm_node (x, l, r) -> |
---|
[2773] | 185 | Types.option_map (fun r0 -> Pm_node (x, l, r0)) (update tl a r)) |
---|
[2601] | 186 | | Positive.P0 tl -> |
---|
| 187 | (match t with |
---|
| 188 | | Pm_leaf -> Types.None |
---|
| 189 | | Pm_node (x, l, r) -> |
---|
| 190 | Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l)) |
---|
| 191 | |
---|
[2773] | 192 | (** val fold : |
---|
[2601] | 193 | (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **) |
---|
[2773] | 194 | let rec fold f t b = |
---|
[2601] | 195 | match t with |
---|
| 196 | | Pm_leaf -> b |
---|
| 197 | | Pm_node (a, l, r) -> |
---|
| 198 | let b0 = |
---|
| 199 | match a with |
---|
| 200 | | Types.None -> b |
---|
| 201 | | Types.Some a0 -> f Positive.One a0 b |
---|
| 202 | in |
---|
[2773] | 203 | let b1 = fold (fun x -> f (Positive.P0 x)) l b0 in |
---|
| 204 | fold (fun x -> f (Positive.P1 x)) r b1 |
---|
[2601] | 205 | |
---|
| 206 | (** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **) |
---|
| 207 | let domain_of_pm t = |
---|
[2773] | 208 | fold (fun p a b -> insert p Types.It b) t Pm_leaf |
---|
[2601] | 209 | |
---|
| 210 | (** val is_none : 'a1 Types.option -> Bool.bool **) |
---|
| 211 | let is_none = function |
---|
| 212 | | Types.None -> Bool.True |
---|
| 213 | | Types.Some x -> Bool.False |
---|
| 214 | |
---|
| 215 | (** val is_pm_leaf : 'a1 positive_map -> Bool.bool **) |
---|
| 216 | let is_pm_leaf = function |
---|
| 217 | | Pm_leaf -> Bool.True |
---|
| 218 | | Pm_node (x, x0, x1) -> Bool.False |
---|
| 219 | |
---|
| 220 | (** val map_opt : |
---|
| 221 | ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map **) |
---|
| 222 | let rec map_opt f = function |
---|
| 223 | | Pm_leaf -> Pm_leaf |
---|
| 224 | | Pm_node (a, l, r) -> |
---|
| 225 | let a' = |
---|
[2773] | 226 | Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x -> |
---|
[2601] | 227 | Obj.magic f x) |
---|
| 228 | in |
---|
| 229 | let l' = map_opt f l in |
---|
| 230 | let r' = map_opt f r in |
---|
| 231 | (match Bool.andb (Bool.andb (is_none (Obj.magic a')) (is_pm_leaf l')) |
---|
| 232 | (is_pm_leaf r') with |
---|
| 233 | | Bool.True -> Pm_leaf |
---|
| 234 | | Bool.False -> Pm_node ((Obj.magic a'), l', r')) |
---|
| 235 | |
---|
[2773] | 236 | (** val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **) |
---|
| 237 | let map f = |
---|
[2601] | 238 | map_opt (fun x -> Types.Some (f x)) |
---|
| 239 | |
---|
| 240 | (** val merge : |
---|
| 241 | ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1 |
---|
| 242 | positive_map -> 'a2 positive_map -> 'a3 positive_map **) |
---|
| 243 | let rec merge choice a b = |
---|
| 244 | match a with |
---|
| 245 | | Pm_leaf -> map_opt (fun x -> choice Types.None (Types.Some x)) b |
---|
| 246 | | Pm_node (o, l, r) -> |
---|
| 247 | (match b with |
---|
| 248 | | Pm_leaf -> map_opt (fun x -> choice (Types.Some x) Types.None) a |
---|
| 249 | | Pm_node (o', l', r') -> |
---|
| 250 | let o'' = choice o o' in |
---|
| 251 | let l'' = merge choice l l' in |
---|
| 252 | let r'' = merge choice r r' in |
---|
| 253 | (match Bool.andb (Bool.andb (is_none o'') (is_pm_leaf l'')) |
---|
| 254 | (is_pm_leaf r'') with |
---|
| 255 | | Bool.True -> Pm_leaf |
---|
| 256 | | Bool.False -> Pm_node (o'', l'', r''))) |
---|
| 257 | |
---|
| 258 | (** val domain_size : 'a1 positive_map -> Nat.nat **) |
---|
| 259 | let rec domain_size = function |
---|
| 260 | | Pm_leaf -> Nat.O |
---|
| 261 | | Pm_node (a, l, r) -> |
---|
| 262 | Nat.plus |
---|
| 263 | (Nat.plus |
---|
| 264 | (match a with |
---|
| 265 | | Types.None -> Nat.O |
---|
| 266 | | Types.Some x -> Nat.S Nat.O) (domain_size l)) (domain_size r) |
---|
| 267 | |
---|
| 268 | (** val pm_all_aux : |
---|
| 269 | 'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) -> |
---|
| 270 | (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **) |
---|
| 271 | let rec pm_all_aux m t pre x = |
---|
| 272 | (match t with |
---|
| 273 | | Pm_leaf -> (fun _ x0 -> Bool.True) |
---|
| 274 | | Pm_node (a, l, r) -> |
---|
| 275 | (fun _ f -> |
---|
| 276 | Bool.andb |
---|
| 277 | (Bool.andb (pm_all_aux m l (fun x0 -> pre (Positive.P0 x0)) f) |
---|
| 278 | ((match a with |
---|
| 279 | | Types.None -> (fun _ -> Bool.True) |
---|
| 280 | | Types.Some a' -> (fun _ -> f (pre Positive.One) a' __)) __)) |
---|
| 281 | (pm_all_aux m r (fun x0 -> pre (Positive.P1 x0)) f))) __ x |
---|
| 282 | |
---|
| 283 | (** val pm_all : |
---|
| 284 | 'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **) |
---|
| 285 | let pm_all m f = |
---|
| 286 | pm_all_aux m m (fun x -> x) f |
---|
| 287 | |
---|
| 288 | (** val pm_choose : |
---|
| 289 | 'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map) |
---|
| 290 | Types.prod Types.option **) |
---|
| 291 | let rec pm_choose = function |
---|
| 292 | | Pm_leaf -> Types.None |
---|
| 293 | | Pm_node (a, l, r) -> |
---|
| 294 | (match pm_choose l with |
---|
| 295 | | Types.None -> |
---|
| 296 | (match pm_choose r with |
---|
| 297 | | Types.None -> |
---|
| 298 | (match a with |
---|
| 299 | | Types.None -> Types.None |
---|
| 300 | | Types.Some a0 -> |
---|
| 301 | Types.Some { Types.fst = { Types.fst = Positive.One; Types.snd = |
---|
| 302 | a0 }; Types.snd = Pm_leaf }) |
---|
| 303 | | Types.Some x -> |
---|
| 304 | Types.Some { Types.fst = { Types.fst = (Positive.P1 |
---|
| 305 | x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd }; |
---|
| 306 | Types.snd = (Pm_node (a, l, x.Types.snd)) }) |
---|
| 307 | | Types.Some x -> |
---|
| 308 | Types.Some { Types.fst = { Types.fst = (Positive.P0 |
---|
| 309 | x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd }; |
---|
| 310 | Types.snd = (Pm_node (a, x.Types.snd, r)) }) |
---|
| 311 | |
---|
| 312 | (** val pm_try_remove : |
---|
| 313 | Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod |
---|
| 314 | Types.option **) |
---|
| 315 | let rec pm_try_remove b t = |
---|
| 316 | match b with |
---|
| 317 | | Positive.One -> |
---|
| 318 | (match t with |
---|
| 319 | | Pm_leaf -> Types.None |
---|
| 320 | | Pm_node (x, l, r) -> |
---|
| 321 | Types.option_map (fun x0 -> { Types.fst = x0; Types.snd = (Pm_node |
---|
| 322 | (Types.None, l, r)) }) x) |
---|
| 323 | | Positive.P1 tl -> |
---|
| 324 | (match t with |
---|
| 325 | | Pm_leaf -> Types.None |
---|
| 326 | | Pm_node (x, l, r) -> |
---|
| 327 | Types.option_map (fun xr -> { Types.fst = xr.Types.fst; Types.snd = |
---|
| 328 | (Pm_node (x, l, xr.Types.snd)) }) (pm_try_remove tl r)) |
---|
| 329 | | Positive.P0 tl -> |
---|
| 330 | (match t with |
---|
| 331 | | Pm_leaf -> Types.None |
---|
| 332 | | Pm_node (x, l, r) -> |
---|
| 333 | Types.option_map (fun xl -> { Types.fst = xl.Types.fst; Types.snd = |
---|
| 334 | (Pm_node (x, xl.Types.snd, r)) }) (pm_try_remove tl l)) |
---|
| 335 | |
---|
| 336 | (** val pm_fold_inf_aux : |
---|
| 337 | 'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1 |
---|
| 338 | positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2 **) |
---|
| 339 | let rec pm_fold_inf_aux t f t' pre b = |
---|
| 340 | (match t' with |
---|
| 341 | | Pm_leaf -> (fun _ -> b) |
---|
| 342 | | Pm_node (a, l, r) -> |
---|
| 343 | (fun _ -> |
---|
| 344 | let b0 = |
---|
| 345 | (match a with |
---|
| 346 | | Types.None -> (fun _ -> b) |
---|
| 347 | | Types.Some a0 -> (fun _ -> f (pre Positive.One) a0 __ b)) __ |
---|
| 348 | in |
---|
| 349 | let b1 = pm_fold_inf_aux t f l (fun x -> pre (Positive.P0 x)) b0 in |
---|
| 350 | pm_fold_inf_aux t f r (fun x -> pre (Positive.P1 x)) b1)) __ |
---|
| 351 | |
---|
| 352 | (** val pm_fold_inf : |
---|
| 353 | 'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> |
---|
| 354 | 'a2 **) |
---|
| 355 | let pm_fold_inf t f b = |
---|
| 356 | pm_fold_inf_aux t f t (fun x -> x) b |
---|
| 357 | |
---|
| 358 | (** val pm_find_aux : |
---|
| 359 | (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos -> |
---|
| 360 | 'a1 -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option **) |
---|
| 361 | let rec pm_find_aux pre t p = |
---|
| 362 | match t with |
---|
| 363 | | Pm_leaf -> Types.None |
---|
| 364 | | Pm_node (a, l, r) -> |
---|
| 365 | let x = |
---|
| 366 | match a with |
---|
| 367 | | Types.None -> Types.None |
---|
| 368 | | Types.Some a0 -> |
---|
| 369 | (match p (pre Positive.One) a0 with |
---|
| 370 | | Bool.True -> |
---|
| 371 | Types.Some { Types.fst = (pre Positive.One); Types.snd = a0 } |
---|
| 372 | | Bool.False -> Types.None) |
---|
| 373 | in |
---|
| 374 | (match x with |
---|
| 375 | | Types.None -> |
---|
| 376 | (match pm_find_aux (fun x0 -> pre (Positive.P0 x0)) l p with |
---|
| 377 | | Types.None -> pm_find_aux (fun x0 -> pre (Positive.P1 x0)) r p |
---|
| 378 | | Types.Some y -> Types.Some y) |
---|
| 379 | | Types.Some x0 -> Types.Some x0) |
---|
| 380 | |
---|
| 381 | (** val pm_find : |
---|
| 382 | 'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos, |
---|
| 383 | 'a1) Types.prod Types.option **) |
---|
| 384 | let pm_find x x0 = |
---|
| 385 | pm_find_aux (fun x1 -> x1) x x0 |
---|
| 386 | |
---|