aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction/sat_checker.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/extraction/sat_checker.ml')
-rw-r--r--src/extraction/sat_checker.ml2726
1 files changed, 2414 insertions, 312 deletions
diff --git a/src/extraction/sat_checker.ml b/src/extraction/sat_checker.ml
index 839f95b..9d881f4 100644
--- a/src/extraction/sat_checker.ml
+++ b/src/extraction/sat_checker.ml
@@ -1,14 +1,6 @@
-(**************************************************************************)
-(* *)
-(* SMTCoq *)
-(* Copyright (C) 2011 - 2022 *)
-(* *)
-(* See file "AUTHORS" for the list of authors *)
-(* *)
-(* This file is distributed under the terms of the CeCILL-C licence *)
-(* *)
-(**************************************************************************)
+type __ = Obj.t
+let __ = let rec f _ = Obj.repr f in Obj.repr f
(** val negb : bool -> bool **)
@@ -16,232 +8,2400 @@ let negb = function
| true -> false
| false -> true
+type nat =
+| O
+| S of nat
+
+type 'a option =
+| Some of 'a
+| None
+
+(** val fst : ('a1 * 'a2) -> 'a1 **)
+
+let fst = function
+| (x, _) -> x
+
+(** val snd : ('a1 * 'a2) -> 'a2 **)
+
+let snd = function
+| (_, y) -> y
+
type 'a list =
| Nil
| Cons of 'a * 'a list
-(** val existsb : ('a1 -> bool) -> 'a1 list -> bool **)
+(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
+
+let rec app l m =
+ match l with
+ | Nil -> m
+ | Cons (a, l1) -> Cons (a, (app l1 m))
+
+(** val compOpp : int -> int **)
+
+let compOpp = function
+| 0 -> 0
+| (-1) -> 1
+| 1 -> (-1)
+
+type sumbool =
+| Left
+| Right
+
+(** val add : nat -> nat -> nat **)
+
+let rec add n m =
+ match n with
+ | O -> m
+ | S p -> S (add p m)
+
+type positive =
+| XI of positive
+| XO of positive
+| XH
+
+type z =
+| Z0
+| Zpos of positive
+| Zneg of positive
+
+module type EqLtLe =
+ sig
+ type t
+ end
+
+module MakeOrderTac =
+ functor (O:EqLtLe) ->
+ functor (P:sig
+ end) ->
+ struct
+ end
+
+module Pos =
+ struct
+ (** val succ : positive -> positive **)
+
+ let rec succ = function
+ | XI p -> XO (succ p)
+ | XO p -> XI p
+ | XH -> XO XH
+
+ (** val add : positive -> positive -> positive **)
+
+ let rec add x y =
+ match x with
+ | XI p ->
+ (match y with
+ | XI q -> XO (add_carry p q)
+ | XO q -> XI (add p q)
+ | XH -> XO (succ p))
+ | XO p ->
+ (match y with
+ | XI q -> XI (add p q)
+ | XO q -> XO (add p q)
+ | XH -> XI p)
+ | XH -> (match y with
+ | XI q -> XO (succ q)
+ | XO q -> XI q
+ | XH -> XO XH)
+
+ (** val add_carry : positive -> positive -> positive **)
+
+ and add_carry x y =
+ match x with
+ | XI p ->
+ (match y with
+ | XI q -> XI (add_carry p q)
+ | XO q -> XO (add_carry p q)
+ | XH -> XI (succ p))
+ | XO p ->
+ (match y with
+ | XI q -> XO (add_carry p q)
+ | XO q -> XI (add p q)
+ | XH -> XO (succ p))
+ | XH ->
+ (match y with
+ | XI q -> XI (succ q)
+ | XO q -> XO (succ q)
+ | XH -> XI XH)
+
+ (** val pred_double : positive -> positive **)
+
+ let rec pred_double = function
+ | XI p -> XI (XO p)
+ | XO p -> XI (pred_double p)
+ | XH -> XH
+
+ (** val mul : positive -> positive -> positive **)
+
+ let rec mul x y =
+ match x with
+ | XI p -> add y (XO (mul p y))
+ | XO p -> XO (mul p y)
+ | XH -> y
+
+ (** val compare_cont : int -> positive -> positive -> int **)
+
+ let rec compare_cont r x y =
+ match x with
+ | XI p ->
+ (match y with
+ | XI q -> compare_cont r p q
+ | XO q -> compare_cont 1 p q
+ | XH -> 1)
+ | XO p ->
+ (match y with
+ | XI q -> compare_cont (-1) p q
+ | XO q -> compare_cont r p q
+ | XH -> 1)
+ | XH -> (match y with
+ | XH -> r
+ | _ -> (-1))
+
+ (** val compare : positive -> positive -> int **)
+
+ let compare =
+ compare_cont 0
+
+ (** val eqb : positive -> positive -> bool **)
+
+ let rec eqb p q =
+ match p with
+ | XI p0 -> (match q with
+ | XI q0 -> eqb p0 q0
+ | _ -> false)
+ | XO p0 -> (match q with
+ | XO q0 -> eqb p0 q0
+ | _ -> false)
+ | XH -> (match q with
+ | XH -> true
+ | _ -> false)
+
+ (** val eq_dec : positive -> positive -> sumbool **)
+
+ let rec eq_dec p x0 =
+ match p with
+ | XI p0 -> (match x0 with
+ | XI p1 -> eq_dec p0 p1
+ | _ -> Right)
+ | XO p0 -> (match x0 with
+ | XO p1 -> eq_dec p0 p1
+ | _ -> Right)
+ | XH -> (match x0 with
+ | XH -> Left
+ | _ -> Right)
+ end
+
+module Z =
+ struct
+ (** val double : z -> z **)
+
+ let double = function
+ | Z0 -> Z0
+ | Zpos p -> Zpos (XO p)
+ | Zneg p -> Zneg (XO p)
+
+ (** val succ_double : z -> z **)
+
+ let succ_double = function
+ | Z0 -> Zpos XH
+ | Zpos p -> Zpos (XI p)
+ | Zneg p -> Zneg (Pos.pred_double p)
+
+ (** val pred_double : z -> z **)
+
+ let pred_double = function
+ | Z0 -> Zneg XH
+ | Zpos p -> Zpos (Pos.pred_double p)
+ | Zneg p -> Zneg (XI p)
+
+ (** val pos_sub : positive -> positive -> z **)
+
+ let rec pos_sub x y =
+ match x with
+ | XI p ->
+ (match y with
+ | XI q -> double (pos_sub p q)
+ | XO q -> succ_double (pos_sub p q)
+ | XH -> Zpos (XO p))
+ | XO p ->
+ (match y with
+ | XI q -> pred_double (pos_sub p q)
+ | XO q -> double (pos_sub p q)
+ | XH -> Zpos (Pos.pred_double p))
+ | XH ->
+ (match y with
+ | XI q -> Zneg (XO q)
+ | XO q -> Zneg (Pos.pred_double q)
+ | XH -> Z0)
+
+ (** val add : z -> z -> z **)
+
+ let add x y =
+ match x with
+ | Z0 -> y
+ | Zpos x' ->
+ (match y with
+ | Z0 -> x
+ | Zpos y' -> Zpos (Pos.add x' y')
+ | Zneg y' -> pos_sub x' y')
+ | Zneg x' ->
+ (match y with
+ | Z0 -> x
+ | Zpos y' -> pos_sub y' x'
+ | Zneg y' -> Zneg (Pos.add x' y'))
+
+ (** val opp : z -> z **)
+
+ let opp = function
+ | Z0 -> Z0
+ | Zpos x0 -> Zneg x0
+ | Zneg x0 -> Zpos x0
+
+ (** val sub : z -> z -> z **)
+
+ let sub m n =
+ add m (opp n)
+
+ (** val mul : z -> z -> z **)
+
+ let mul x y =
+ match x with
+ | Z0 -> Z0
+ | Zpos x' ->
+ (match y with
+ | Z0 -> Z0
+ | Zpos y' -> Zpos (Pos.mul x' y')
+ | Zneg y' -> Zneg (Pos.mul x' y'))
+ | Zneg x' ->
+ (match y with
+ | Z0 -> Z0
+ | Zpos y' -> Zneg (Pos.mul x' y')
+ | Zneg y' -> Zpos (Pos.mul x' y'))
+
+ (** val compare : z -> z -> int **)
+
+ let compare x y =
+ match x with
+ | Z0 -> (match y with
+ | Z0 -> 0
+ | Zpos _ -> (-1)
+ | Zneg _ -> 1)
+ | Zpos x' -> (match y with
+ | Zpos y' -> Pos.compare x' y'
+ | _ -> 1)
+ | Zneg x' ->
+ (match y with
+ | Zneg y' -> compOpp (Pos.compare x' y')
+ | _ -> (-1))
+
+ (** val leb : z -> z -> bool **)
+
+ let leb x y =
+ match compare x y with
+ | 1 -> false
+ | _ -> true
+
+ (** val ltb : z -> z -> bool **)
+
+ let ltb x y =
+ match compare x y with
+ | (-1) -> true
+ | _ -> false
+
+ (** val eqb : z -> z -> bool **)
+
+ let eqb x y =
+ match x with
+ | Z0 -> (match y with
+ | Z0 -> true
+ | _ -> false)
+ | Zpos p -> (match y with
+ | Zpos q -> Pos.eqb p q
+ | _ -> false)
+ | Zneg p -> (match y with
+ | Zneg q -> Pos.eqb p q
+ | _ -> false)
-let rec existsb f = function
-| Nil -> false
-| Cons (a, l0) -> if f a then true else existsb f l0
+ (** val max : z -> z -> z **)
-type int = ExtrNative.uint
+ let max n m =
+ match compare n m with
+ | (-1) -> m
+ | _ -> n
-(** val lsl0 : int -> int -> int **)
+ (** val eq_dec : z -> z -> sumbool **)
-let lsl0 = ExtrNative.l_sl
+ let eq_dec x y =
+ match x with
+ | Z0 -> (match y with
+ | Z0 -> Left
+ | _ -> Right)
+ | Zpos x0 -> (match y with
+ | Zpos p0 -> Pos.eq_dec x0 p0
+ | _ -> Right)
+ | Zneg x0 -> (match y with
+ | Zneg p0 -> Pos.eq_dec x0 p0
+ | _ -> Right)
+ end
+
+(** val rev : 'a1 list -> 'a1 list **)
+
+let rec rev = function
+| Nil -> Nil
+| Cons (x, l') -> app (rev l') (Cons (x, Nil))
+
+(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)
+
+let rec fold_left f l a0 =
+ match l with
+ | Nil -> a0
+ | Cons (b, t0) -> fold_left f t0 (f a0 b)
+
+(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)
+
+let rec fold_right f a0 = function
+| Nil -> a0
+| Cons (b, t0) -> f b (fold_right f a0 t0)
+
+(** val size : nat **)
-(** val lsr0 : int -> int -> int **)
+let size =
+ S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S
+ (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S
+ (S (S (S (S (S (S (S (S (S (S (S (S (S (S
+ O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-let lsr0 = ExtrNative.l_sr
+(** val lsl0 : Uint63.t -> Uint63.t -> Uint63.t **)
-(** val land0 : int -> int -> int **)
+let lsl0 = Uint63.l_sl
-let land0 = ExtrNative.l_and
+(** val lsr0 : Uint63.t -> Uint63.t -> Uint63.t **)
-(** val lxor0 : int -> int -> int **)
+let lsr0 = Uint63.l_sr
-let lxor0 = ExtrNative.l_xor
+(** val lxor0 : Uint63.t -> Uint63.t -> Uint63.t **)
-(** val sub : int -> int -> int **)
+let lxor0 = Uint63.l_xor
-let sub = ExtrNative.sub
+(** val add0 : Uint63.t -> Uint63.t -> Uint63.t **)
-(** val eqb : int -> int -> bool **)
+let add0 = Uint63.add
-let eqb = fun i j -> ExtrNative.compare i j = ExtrNative.Eq
+(** val sub0 : Uint63.t -> Uint63.t -> Uint63.t **)
-(** val foldi_cont :
- (int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1
- -> 'a2 **)
+let sub0 = Uint63.sub
-let foldi_cont = ExtrNative.foldi_cont
+(** val eqb0 : Uint63.t -> Uint63.t -> bool **)
-(** val foldi_down_cont :
- (int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1
- -> 'a2 **)
+let eqb0 = Uint63.equal
-let foldi_down_cont = ExtrNative.foldi_down_cont
+(** val ltb0 : Uint63.t -> Uint63.t -> bool **)
-(** val is_zero : int -> bool **)
+let ltb0 = Uint63.lt
+
+(** val leb0 : Uint63.t -> Uint63.t -> bool **)
+
+let leb0 = Uint63.le
+
+(** val digits : Uint63.t **)
+
+let digits =
+ (Uint63.of_int (63))
+
+(** val is_zero : Uint63.t -> bool **)
let is_zero i =
- eqb i (ExtrNative.of_uint(0))
+ eqb0 i (Uint63.of_int (0))
-(** val is_even : int -> bool **)
+(** val bit : Uint63.t -> Uint63.t -> bool **)
-let is_even i =
- is_zero (land0 i (ExtrNative.of_uint(1)))
+let bit i n =
+ negb (is_zero (lsl0 (lsr0 i n) (sub0 digits (Uint63.of_int (1)))))
-(** val compare : int -> int -> ExtrNative.comparison **)
+(** val compare0 : Uint63.t -> Uint63.t -> int **)
-let compare = ExtrNative.compare
+let compare0 = Uint63.compare
-(** val foldi : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1 **)
+type 'x compare1 =
+| LT
+| EQ
+| GT
-let foldi f from to0 =
- foldi_cont (fun i cont a -> cont (f i a)) from to0 (fun a -> a)
+module type OrderedType =
+ sig
+ type t
-(** val foldi_down : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1 **)
+ val compare : t -> t -> t compare1
-let foldi_down f from downto0 =
- foldi_down_cont (fun i cont a -> cont (f i a)) from downto0 (fun a -> a)
+ val eq_dec : t -> t -> sumbool
+ end
-type 'a array = 'a ExtrNative.parray
+module OrderedTypeFacts =
+ functor (O:OrderedType) ->
+ struct
+ module TO =
+ struct
+ type t = O.t
+ end
-(** val make : int -> 'a1 -> 'a1 array **)
+ module IsTO =
+ struct
+ end
-let make = ExtrNative.parray_make
+ module OrderTac = MakeOrderTac(TO)(IsTO)
-module Coq__1 = struct
- (** val get : 'a1 array -> int -> 'a1 **)
-
- let get = ExtrNative.parray_get
-end
-let get = Coq__1.get
+ (** val eq_dec : O.t -> O.t -> sumbool **)
-(** val set : 'a1 array -> int -> 'a1 -> 'a1 array **)
+ let eq_dec =
+ O.eq_dec
-let set = ExtrNative.parray_set
+ (** val lt_dec : O.t -> O.t -> sumbool **)
-(** val length : 'a1 array -> int **)
+ let lt_dec x y =
+ match O.compare x y with
+ | LT -> Left
+ | _ -> Right
-let length = ExtrNative.parray_length
+ (** val eqb : O.t -> O.t -> bool **)
-(** val to_list : 'a1 array -> 'a1 list **)
+ let eqb x y =
+ match eq_dec x y with
+ | Left -> true
+ | Right -> false
+ end
-let to_list t0 =
- let len = length t0 in
- if eqb (ExtrNative.of_uint(0)) len
- then Nil
- else foldi_down (fun i l -> Cons ((get t0 i), l))
- (sub len (ExtrNative.of_uint(1))) (ExtrNative.of_uint(0)) Nil
+module KeyOrderedType =
+ functor (O:OrderedType) ->
+ struct
+ module MO = OrderedTypeFacts(O)
+ end
-(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 array -> 'a1 **)
+module Raw =
+ functor (X:OrderedType) ->
+ struct
+ module MX = OrderedTypeFacts(X)
-let fold_left f a t0 =
- let len = length t0 in
- if eqb (ExtrNative.of_uint(0)) len
- then a
- else foldi (fun i a0 -> f a0 (get t0 i)) (ExtrNative.of_uint(0))
- (sub (length t0) (ExtrNative.of_uint(1))) a
-
-(** val foldi_right :
- (int -> 'a1 -> 'a2 -> 'a2) -> 'a1 array -> 'a2 -> 'a2 **)
-
-let foldi_right f t0 b =
- let len = length t0 in
- if eqb (ExtrNative.of_uint(0)) len
- then b
- else foldi_down (fun i b0 -> f i (get t0 i) b0)
- (sub len (ExtrNative.of_uint(1))) (ExtrNative.of_uint(0)) b
-
-module Valuation =
- struct
- type t = int -> bool
+ module PX = KeyOrderedType(X)
+
+ type key = X.t
+
+ type 'elt t = (X.t * 'elt) list
+
+ (** val empty : 'a1 t **)
+
+ let empty =
+ Nil
+
+ (** val is_empty : 'a1 t -> bool **)
+
+ let is_empty = function
+ | Nil -> true
+ | Cons (_, _) -> false
+
+ (** val mem : key -> 'a1 t -> bool **)
+
+ let rec mem k = function
+ | Nil -> false
+ | Cons (p, l) ->
+ let (k', _) = p in
+ (match X.compare k k' with
+ | LT -> false
+ | EQ -> true
+ | GT -> mem k l)
+
+ type 'elt coq_R_mem =
+ | R_mem_0 of 'elt t
+ | R_mem_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_mem_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_mem_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * bool * 'elt coq_R_mem
+
+ (** val coq_R_mem_rect :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2) -> 'a1 t ->
+ bool -> 'a1 coq_R_mem -> 'a2 **)
+
+ let rec coq_R_mem_rect k f f0 f1 f2 _ _ = function
+ | R_mem_0 s -> f s __
+ | R_mem_1 (s, k', _x, l) -> f0 s k' _x l __ __ __
+ | R_mem_2 (s, k', _x, l) -> f1 s k' _x l __ __ __
+ | R_mem_3 (s, k', _x, l, _res, r0) ->
+ f2 s k' _x l __ __ __ _res r0 (coq_R_mem_rect k f f0 f1 f2 l _res r0)
+
+ (** val coq_R_mem_rec :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2) -> 'a1 t ->
+ bool -> 'a1 coq_R_mem -> 'a2 **)
+
+ let rec coq_R_mem_rec k f f0 f1 f2 _ _ = function
+ | R_mem_0 s -> f s __
+ | R_mem_1 (s, k', _x, l) -> f0 s k' _x l __ __ __
+ | R_mem_2 (s, k', _x, l) -> f1 s k' _x l __ __ __
+ | R_mem_3 (s, k', _x, l, _res, r0) ->
+ f2 s k' _x l __ __ __ _res r0 (coq_R_mem_rec k f f0 f1 f2 l _res r0)
+
+ (** val mem_rect :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let rec mem_rect k f2 f1 f0 f s =
+ let f3 = f2 s in
+ let f4 = f1 s in
+ let f5 = f0 s in
+ let f6 = f s in
+ (match s with
+ | Nil -> f3 __
+ | Cons (p, l) ->
+ let (t0, e) = p in
+ let f7 = f6 t0 e l __ in
+ let f8 = fun _ _ -> let hrec = mem_rect k f2 f1 f0 f l in f7 __ __ hrec
+ in
+ let f9 = f5 t0 e l __ in
+ let f10 = f4 t0 e l __ in
+ (match X.compare k t0 with
+ | LT -> f10 __ __
+ | EQ -> f9 __ __
+ | GT -> f8 __ __))
+
+ (** val mem_rec :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let mem_rec =
+ mem_rect
+
+ (** val coq_R_mem_correct : key -> 'a1 t -> bool -> 'a1 coq_R_mem **)
+
+ let coq_R_mem_correct k s _res =
+ Obj.magic mem_rect k (fun y _ _ _ -> R_mem_0 y)
+ (fun y y0 y1 y2 _ _ _ _ _ -> R_mem_1 (y, y0, y1, y2))
+ (fun y y0 y1 y2 _ _ _ _ _ -> R_mem_2 (y, y0, y1, y2))
+ (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_mem_3 (y, y0, y1, y2, (mem k y2),
+ (y6 (mem k y2) __))) s _res __
+
+ (** val find : key -> 'a1 t -> 'a1 option **)
+
+ let rec find k = function
+ | Nil -> None
+ | Cons (p, s') ->
+ let (k', x) = p in
+ (match X.compare k k' with
+ | LT -> None
+ | EQ -> Some x
+ | GT -> find k s')
+
+ type 'elt coq_R_find =
+ | R_find_0 of 'elt t
+ | R_find_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_find_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_find_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt option
+ * 'elt coq_R_find
+
+ (** val coq_R_find_rect :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find -> 'a2 -> 'a2) -> 'a1
+ t -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+ let rec coq_R_find_rect k f f0 f1 f2 _ _ = function
+ | R_find_0 s -> f s __
+ | R_find_1 (s, k', x, s') -> f0 s k' x s' __ __ __
+ | R_find_2 (s, k', x, s') -> f1 s k' x s' __ __ __
+ | R_find_3 (s, k', x, s', _res, r0) ->
+ f2 s k' x s' __ __ __ _res r0 (coq_R_find_rect k f f0 f1 f2 s' _res r0)
+
+ (** val coq_R_find_rec :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find -> 'a2 -> 'a2) -> 'a1
+ t -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+ let rec coq_R_find_rec k f f0 f1 f2 _ _ = function
+ | R_find_0 s -> f s __
+ | R_find_1 (s, k', x, s') -> f0 s k' x s' __ __ __
+ | R_find_2 (s, k', x, s') -> f1 s k' x s' __ __ __
+ | R_find_3 (s, k', x, s', _res, r0) ->
+ f2 s k' x s' __ __ __ _res r0 (coq_R_find_rec k f f0 f1 f2 s' _res r0)
+
+ (** val find_rect :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let rec find_rect k f2 f1 f0 f s =
+ let f3 = f2 s in
+ let f4 = f1 s in
+ let f5 = f0 s in
+ let f6 = f s in
+ (match s with
+ | Nil -> f3 __
+ | Cons (p, l) ->
+ let (t0, e) = p in
+ let f7 = f6 t0 e l __ in
+ let f8 = fun _ _ ->
+ let hrec = find_rect k f2 f1 f0 f l in f7 __ __ hrec
+ in
+ let f9 = f5 t0 e l __ in
+ let f10 = f4 t0 e l __ in
+ (match X.compare k t0 with
+ | LT -> f10 __ __
+ | EQ -> f9 __ __
+ | GT -> f8 __ __))
+
+ (** val find_rec :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let find_rec =
+ find_rect
+
+ (** val coq_R_find_correct :
+ key -> 'a1 t -> 'a1 option -> 'a1 coq_R_find **)
+
+ let coq_R_find_correct k s _res =
+ Obj.magic find_rect k (fun y _ _ _ -> R_find_0 y)
+ (fun y y0 y1 y2 _ _ _ _ _ -> R_find_1 (y, y0, y1, y2))
+ (fun y y0 y1 y2 _ _ _ _ _ -> R_find_2 (y, y0, y1, y2))
+ (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_find_3 (y, y0, y1, y2, (find k y2),
+ (y6 (find k y2) __))) s _res __
+
+ (** val add : key -> 'a1 -> 'a1 t -> 'a1 t **)
+
+ let rec add k x s = match s with
+ | Nil -> Cons ((k, x), Nil)
+ | Cons (p, l) ->
+ let (k', y) = p in
+ (match X.compare k k' with
+ | LT -> Cons ((k, x), s)
+ | EQ -> Cons ((k, x), l)
+ | GT -> Cons ((k', y), (add k x l)))
+
+ type 'elt coq_R_add =
+ | R_add_0 of 'elt t
+ | R_add_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_add_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_add_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt t
+ * 'elt coq_R_add
+
+ (** val coq_R_add_rect :
+ key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_add -> 'a2 ->
+ 'a2) -> 'a1 t -> 'a1 t -> 'a1 coq_R_add -> 'a2 **)
+
+ let rec coq_R_add_rect k x f f0 f1 f2 _ _ = function
+ | R_add_0 s -> f s __
+ | R_add_1 (s, k', y, l) -> f0 s k' y l __ __ __
+ | R_add_2 (s, k', y, l) -> f1 s k' y l __ __ __
+ | R_add_3 (s, k', y, l, _res, r0) ->
+ f2 s k' y l __ __ __ _res r0 (coq_R_add_rect k x f f0 f1 f2 l _res r0)
+
+ (** val coq_R_add_rec :
+ key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_add -> 'a2 ->
+ 'a2) -> 'a1 t -> 'a1 t -> 'a1 coq_R_add -> 'a2 **)
+
+ let rec coq_R_add_rec k x f f0 f1 f2 _ _ = function
+ | R_add_0 s -> f s __
+ | R_add_1 (s, k', y, l) -> f0 s k' y l __ __ __
+ | R_add_2 (s, k', y, l) -> f1 s k' y l __ __ __
+ | R_add_3 (s, k', y, l, _res, r0) ->
+ f2 s k' y l __ __ __ _res r0 (coq_R_add_rec k x f f0 f1 f2 l _res r0)
+
+ (** val add_rect :
+ key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let rec add_rect k x f2 f1 f0 f s =
+ let f3 = f2 s in
+ let f4 = f1 s in
+ let f5 = f0 s in
+ let f6 = f s in
+ (match s with
+ | Nil -> f3 __
+ | Cons (p, l) ->
+ let (t0, e) = p in
+ let f7 = f6 t0 e l __ in
+ let f8 = fun _ _ ->
+ let hrec = add_rect k x f2 f1 f0 f l in f7 __ __ hrec
+ in
+ let f9 = f5 t0 e l __ in
+ let f10 = f4 t0 e l __ in
+ (match X.compare k t0 with
+ | LT -> f10 __ __
+ | EQ -> f9 __ __
+ | GT -> f8 __ __))
+
+ (** val add_rec :
+ key -> 'a1 -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let add_rec =
+ add_rect
+
+ (** val coq_R_add_correct :
+ key -> 'a1 -> 'a1 t -> 'a1 t -> 'a1 coq_R_add **)
+
+ let coq_R_add_correct k x s _res =
+ add_rect k x (fun y _ _ _ -> R_add_0 y) (fun y y0 y1 y2 _ _ _ _ _ ->
+ R_add_1 (y, y0, y1, y2)) (fun y y0 y1 y2 _ _ _ _ _ -> R_add_2 (y, y0,
+ y1, y2)) (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_add_3 (y, y0, y1, y2,
+ (add k x y2), (y6 (add k x y2) __))) s _res __
+
+ (** val remove : key -> 'a1 t -> 'a1 t **)
+
+ let rec remove k s = match s with
+ | Nil -> Nil
+ | Cons (p, l) ->
+ let (k', x) = p in
+ (match X.compare k k' with
+ | LT -> s
+ | EQ -> l
+ | GT -> Cons ((k', x), (remove k l)))
+
+ type 'elt coq_R_remove =
+ | R_remove_0 of 'elt t
+ | R_remove_1 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_remove_2 of 'elt t * X.t * 'elt * (X.t * 'elt) list
+ | R_remove_3 of 'elt t * X.t * 'elt * (X.t * 'elt) list * 'elt t
+ * 'elt coq_R_remove
+
+ (** val coq_R_remove_rect :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 -> 'a2) -> 'a1 t
+ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 **)
+
+ let rec coq_R_remove_rect k f f0 f1 f2 _ _ = function
+ | R_remove_0 s -> f s __
+ | R_remove_1 (s, k', x, l) -> f0 s k' x l __ __ __
+ | R_remove_2 (s, k', x, l) -> f1 s k' x l __ __ __
+ | R_remove_3 (s, k', x, l, _res, r0) ->
+ f2 s k' x l __ __ __ _res r0 (coq_R_remove_rect k f f0 f1 f2 l _res r0)
+
+ (** val coq_R_remove_rec :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 -> 'a2) -> 'a1 t
+ -> 'a1 t -> 'a1 coq_R_remove -> 'a2 **)
+
+ let rec coq_R_remove_rec k f f0 f1 f2 _ _ = function
+ | R_remove_0 s -> f s __
+ | R_remove_1 (s, k', x, l) -> f0 s k' x l __ __ __
+ | R_remove_2 (s, k', x, l) -> f1 s k' x l __ __ __
+ | R_remove_3 (s, k', x, l, _res, r0) ->
+ f2 s k' x l __ __ __ _res r0 (coq_R_remove_rec k f f0 f1 f2 l _res r0)
+
+ (** val remove_rect :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let rec remove_rect k f2 f1 f0 f s =
+ let f3 = f2 s in
+ let f4 = f1 s in
+ let f5 = f0 s in
+ let f6 = f s in
+ (match s with
+ | Nil -> f3 __
+ | Cons (p, l) ->
+ let (t0, e) = p in
+ let f7 = f6 t0 e l __ in
+ let f8 = fun _ _ ->
+ let hrec = remove_rect k f2 f1 f0 f l in f7 __ __ hrec
+ in
+ let f9 = f5 t0 e l __ in
+ let f10 = f4 t0 e l __ in
+ (match X.compare k t0 with
+ | LT -> f10 __ __
+ | EQ -> f9 __ __
+ | GT -> f8 __ __))
+
+ (** val remove_rec :
+ key -> ('a1 t -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2) -> ('a1 t -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> __ -> __ -> 'a2 -> 'a2) -> 'a1 t -> 'a2 **)
+
+ let remove_rec =
+ remove_rect
+
+ (** val coq_R_remove_correct : key -> 'a1 t -> 'a1 t -> 'a1 coq_R_remove **)
+
+ let coq_R_remove_correct k s _res =
+ Obj.magic remove_rect k (fun y _ _ _ -> R_remove_0 y)
+ (fun y y0 y1 y2 _ _ _ _ _ -> R_remove_1 (y, y0, y1, y2))
+ (fun y y0 y1 y2 _ _ _ _ _ -> R_remove_2 (y, y0, y1, y2))
+ (fun y y0 y1 y2 _ _ _ y6 _ _ -> R_remove_3 (y, y0, y1, y2,
+ (remove k y2), (y6 (remove k y2) __))) s _res __
+
+ (** val elements : 'a1 t -> 'a1 t **)
+
+ let elements m =
+ m
+
+ (** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 **)
+
+ let rec fold f m acc =
+ match m with
+ | Nil -> acc
+ | Cons (p, m') -> let (k, e) = p in fold f m' (f k e acc)
+
+ type ('elt, 'a) coq_R_fold =
+ | R_fold_0 of 'elt t * 'a
+ | R_fold_1 of 'elt t * 'a * X.t * 'elt * (X.t * 'elt) list * 'a
+ * ('elt, 'a) coq_R_fold
+
+ (** val coq_R_fold_rect :
+ (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+ 'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a2 -> ('a1, 'a2)
+ coq_R_fold -> 'a3 -> 'a3) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
+ coq_R_fold -> 'a3 **)
+
+ let rec coq_R_fold_rect f f0 f1 _ _ _ = function
+ | R_fold_0 (m, acc) -> f0 m acc __
+ | R_fold_1 (m, acc, k, e, m', _res, r0) ->
+ f1 m acc k e m' __ _res r0
+ (coq_R_fold_rect f f0 f1 m' (f k e acc) _res r0)
+
+ (** val coq_R_fold_rec :
+ (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+ 'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a2 -> ('a1, 'a2)
+ coq_R_fold -> 'a3 -> 'a3) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
+ coq_R_fold -> 'a3 **)
+
+ let rec coq_R_fold_rec f f0 f1 _ _ _ = function
+ | R_fold_0 (m, acc) -> f0 m acc __
+ | R_fold_1 (m, acc, k, e, m', _res, r0) ->
+ f1 m acc k e m' __ _res r0 (coq_R_fold_rec f f0 f1 m' (f k e acc) _res r0)
+
+ (** val fold_rect :
+ (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+ 'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a3 -> 'a3) -> 'a1 t ->
+ 'a2 -> 'a3 **)
+
+ let rec fold_rect f1 f0 f m acc =
+ let f2 = f0 m acc in
+ let f3 = f m acc in
+ (match m with
+ | Nil -> f2 __
+ | Cons (p, l) ->
+ let (t0, e) = p in
+ let f4 = f3 t0 e l __ in
+ let hrec = fold_rect f1 f0 f l (f1 t0 e acc) in f4 hrec)
+
+ (** val fold_rec :
+ (key -> 'a1 -> 'a2 -> 'a2) -> ('a1 t -> 'a2 -> __ -> 'a3) -> ('a1 t ->
+ 'a2 -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> 'a3 -> 'a3) -> 'a1 t ->
+ 'a2 -> 'a3 **)
+
+ let fold_rec =
+ fold_rect
+
+ (** val coq_R_fold_correct :
+ (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 -> ('a1, 'a2)
+ coq_R_fold **)
+
+ let coq_R_fold_correct f m acc _res =
+ fold_rect f (fun y y0 _ _ _ -> R_fold_0 (y, y0))
+ (fun y y0 y1 y2 y3 _ y5 _ _ -> R_fold_1 (y, y0, y1, y2, y3,
+ (fold f y3 (f y1 y2 y0)), (y5 (fold f y3 (f y1 y2 y0)) __))) m acc _res
+ __
+
+ (** val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool **)
+
+ let rec equal cmp m m' =
+ match m with
+ | Nil -> (match m' with
+ | Nil -> true
+ | Cons (_, _) -> false)
+ | Cons (p, l) ->
+ let (x, e) = p in
+ (match m' with
+ | Nil -> false
+ | Cons (p0, l') ->
+ let (x', e') = p0 in
+ (match X.compare x x' with
+ | EQ -> if cmp e e' then equal cmp l l' else false
+ | _ -> false))
+
+ type 'elt coq_R_equal =
+ | R_equal_0 of 'elt t * 'elt t
+ | R_equal_1 of 'elt t * 'elt t * X.t * 'elt * (X.t * 'elt) list * X.t
+ * 'elt * (X.t * 'elt) list * bool * 'elt coq_R_equal
+ | R_equal_2 of 'elt t * 'elt t * X.t * 'elt * (X.t * 'elt) list * X.t
+ * 'elt * (X.t * 'elt) list * X.t compare1
+ | R_equal_3 of 'elt t * 'elt t * 'elt t * 'elt t
+
+ (** val coq_R_equal_rect :
+ ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+ -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> bool -> 'a1 coq_R_equal -> 'a2 ->
+ 'a2) -> ('a1 t -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t
+ -> 'a1 -> (X.t * 'a1) list -> __ -> X.t compare1 -> __ -> __ -> 'a2) ->
+ ('a1 t -> 'a1 t -> 'a1 t -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t ->
+ 'a1 t -> bool -> 'a1 coq_R_equal -> 'a2 **)
+
+ let rec coq_R_equal_rect cmp f f0 f1 f2 _ _ _ = function
+ | R_equal_0 (m, m') -> f m m' __ __
+ | R_equal_1 (m, m', x, e, l, x', e', l', _res, r0) ->
+ f0 m m' x e l __ x' e' l' __ __ __ _res r0
+ (coq_R_equal_rect cmp f f0 f1 f2 l l' _res r0)
+ | R_equal_2 (m, m', x, e, l, x', e', l', _x) ->
+ f1 m m' x e l __ x' e' l' __ _x __ __
+ | R_equal_3 (m, m', _x, _x0) -> f2 m m' _x __ _x0 __ __
+
+ (** val coq_R_equal_rec :
+ ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+ -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> bool -> 'a1 coq_R_equal -> 'a2 ->
+ 'a2) -> ('a1 t -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t
+ -> 'a1 -> (X.t * 'a1) list -> __ -> X.t compare1 -> __ -> __ -> 'a2) ->
+ ('a1 t -> 'a1 t -> 'a1 t -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t ->
+ 'a1 t -> bool -> 'a1 coq_R_equal -> 'a2 **)
+
+ let rec coq_R_equal_rec cmp f f0 f1 f2 _ _ _ = function
+ | R_equal_0 (m, m') -> f m m' __ __
+ | R_equal_1 (m, m', x, e, l, x', e', l', _res, r0) ->
+ f0 m m' x e l __ x' e' l' __ __ __ _res r0
+ (coq_R_equal_rec cmp f f0 f1 f2 l l' _res r0)
+ | R_equal_2 (m, m', x, e, l, x', e', l', _x) ->
+ f1 m m' x e l __ x' e' l' __ _x __ __
+ | R_equal_3 (m, m', _x, _x0) -> f2 m m' _x __ _x0 __ __
+
+ (** val equal_rect :
+ ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+ -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> ('a1 t -> 'a1 t ->
+ X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> X.t compare1 -> __ -> __ -> 'a2) -> ('a1 t -> 'a1 t -> 'a1 t
+ -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t -> 'a1 t -> 'a2 **)
+
+ let rec equal_rect cmp f2 f1 f0 f m m' =
+ let f3 = f2 m m' in
+ let f4 = f1 m m' in
+ let f5 = f0 m m' in
+ let f6 = f m m' in
+ let f7 = f6 m __ in
+ let f8 = f7 m' __ in
+ (match m with
+ | Nil ->
+ let f9 = f3 __ in (match m' with
+ | Nil -> f9 __
+ | Cons (_, _) -> f8 __)
+ | Cons (p, l) ->
+ let (t0, e) = p in
+ let f9 = f5 t0 e l __ in
+ let f10 = f4 t0 e l __ in
+ (match m' with
+ | Nil -> f8 __
+ | Cons (p0, l0) ->
+ let (t1, e0) = p0 in
+ let f11 = f9 t1 e0 l0 __ in
+ let f12 = let _x = X.compare t0 t1 in f11 _x __ in
+ let f13 = f10 t1 e0 l0 __ in
+ let f14 = fun _ _ ->
+ let hrec = equal_rect cmp f2 f1 f0 f l l0 in f13 __ __ hrec
+ in
+ (match X.compare t0 t1 with
+ | EQ -> f14 __ __
+ | _ -> f12 __)))
+
+ (** val equal_rec :
+ ('a1 -> 'a1 -> bool) -> ('a1 t -> 'a1 t -> __ -> __ -> 'a2) -> ('a1 t
+ -> 'a1 t -> X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 ->
+ (X.t * 'a1) list -> __ -> __ -> __ -> 'a2 -> 'a2) -> ('a1 t -> 'a1 t ->
+ X.t -> 'a1 -> (X.t * 'a1) list -> __ -> X.t -> 'a1 -> (X.t * 'a1) list
+ -> __ -> X.t compare1 -> __ -> __ -> 'a2) -> ('a1 t -> 'a1 t -> 'a1 t
+ -> __ -> 'a1 t -> __ -> __ -> 'a2) -> 'a1 t -> 'a1 t -> 'a2 **)
+
+ let equal_rec =
+ equal_rect
+
+ (** val coq_R_equal_correct :
+ ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool -> 'a1 coq_R_equal **)
+
+ let coq_R_equal_correct cmp m m' _res =
+ equal_rect cmp (fun y y0 _ _ _ _ -> R_equal_0 (y, y0))
+ (fun y y0 y1 y2 y3 _ y5 y6 y7 _ _ _ y11 _ _ -> R_equal_1 (y, y0, y1,
+ y2, y3, y5, y6, y7, (equal cmp y3 y7), (y11 (equal cmp y3 y7) __)))
+ (fun y y0 y1 y2 y3 _ y5 y6 y7 _ y9 _ _ _ _ -> R_equal_2 (y, y0, y1, y2,
+ y3, y5, y6, y7, y9)) (fun y y0 y1 _ y3 _ _ _ _ -> R_equal_3 (y, y0, y1,
+ y3)) m m' _res __
+
+ (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+ let rec map f = function
+ | Nil -> Nil
+ | Cons (p, m') -> let (k, e) = p in Cons ((k, (f e)), (map f m'))
+
+ (** val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+ let rec mapi f = function
+ | Nil -> Nil
+ | Cons (p, m') -> let (k, e) = p in Cons ((k, (f k e)), (mapi f m'))
+
+ (** val option_cons :
+ key -> 'a1 option -> (key * 'a1) list -> (key * 'a1) list **)
+
+ let option_cons k o l =
+ match o with
+ | Some e -> Cons ((k, e), l)
+ | None -> l
+
+ (** val map2_l :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a3 t **)
+
+ let rec map2_l f = function
+ | Nil -> Nil
+ | Cons (p, l) ->
+ let (k, e) = p in option_cons k (f (Some e) None) (map2_l f l)
+
+ (** val map2_r :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a2 t -> 'a3 t **)
+
+ let rec map2_r f = function
+ | Nil -> Nil
+ | Cons (p, l') ->
+ let (k, e') = p in option_cons k (f None (Some e')) (map2_r f l')
+
+ (** val map2 :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t **)
+
+ let rec map2 f m = match m with
+ | Nil -> map2_r f
+ | Cons (p, l) ->
+ let (k, e) = p in
+ let rec map2_aux m' = match m' with
+ | Nil -> map2_l f m
+ | Cons (p0, l') ->
+ let (k', e') = p0 in
+ (match X.compare k k' with
+ | LT -> option_cons k (f (Some e) None) (map2 f l m')
+ | EQ -> option_cons k (f (Some e) (Some e')) (map2 f l l')
+ | GT -> option_cons k' (f None (Some e')) (map2_aux l'))
+ in map2_aux
+
+ (** val combine : 'a1 t -> 'a2 t -> ('a1 option * 'a2 option) t **)
+
+ let rec combine m = match m with
+ | Nil -> map (fun e' -> (None, (Some e')))
+ | Cons (p, l) ->
+ let (k, e) = p in
+ let rec combine_aux m' = match m' with
+ | Nil -> map (fun e0 -> ((Some e0), None)) m
+ | Cons (p0, l') ->
+ let (k', e') = p0 in
+ (match X.compare k k' with
+ | LT -> Cons ((k, ((Some e), None)), (combine l m'))
+ | EQ -> Cons ((k, ((Some e), (Some e'))), (combine l l'))
+ | GT -> Cons ((k', (None, (Some e'))), (combine_aux l')))
+ in combine_aux
+
+ (** val fold_right_pair :
+ ('a1 -> 'a2 -> 'a3 -> 'a3) -> ('a1 * 'a2) list -> 'a3 -> 'a3 **)
+
+ let fold_right_pair f l i =
+ fold_right (fun p -> f (fst p) (snd p)) i l
+
+ (** val map2_alt :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t ->
+ (key * 'a3) list **)
+
+ let map2_alt f m m' =
+ let m0 = combine m m' in
+ let m1 = map (fun p -> f (fst p) (snd p)) m0 in
+ fold_right_pair option_cons m1 Nil
+
+ (** val at_least_one :
+ 'a1 option -> 'a2 option -> ('a1 option * 'a2 option) option **)
+
+ let at_least_one o o' =
+ match o with
+ | Some _ -> Some (o, o')
+ | None -> (match o' with
+ | Some _ -> Some (o, o')
+ | None -> None)
+
+ (** val at_least_one_then_f :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 option -> 'a2 option ->
+ 'a3 option **)
+
+ let at_least_one_then_f f o o' =
+ match o with
+ | Some _ -> f o o'
+ | None -> (match o' with
+ | Some _ -> f o o'
+ | None -> None)
end
-module Var =
- struct
- (** val _true : int **)
-
- let _true =
- (ExtrNative.of_uint(0))
-
- (** val _false : int **)
-
- let _false =
- (ExtrNative.of_uint(1))
-
- (** val interp : Valuation.t -> int -> bool **)
-
- let interp rho x =
- rho x
+module type Int =
+ sig
+ type t
+
+ val i2z : t -> z
+
+ val _0 : t
+
+ val _1 : t
+
+ val _2 : t
+
+ val _3 : t
+
+ val add : t -> t -> t
+
+ val opp : t -> t
+
+ val sub : t -> t -> t
+
+ val mul : t -> t -> t
+
+ val max : t -> t -> t
+
+ val eqb : t -> t -> bool
+
+ val ltb : t -> t -> bool
+
+ val leb : t -> t -> bool
+
+ val gt_le_dec : t -> t -> sumbool
+
+ val ge_lt_dec : t -> t -> sumbool
+
+ val eq_dec : t -> t -> sumbool
end
-module Lit =
- struct
- (** val is_pos : int -> bool **)
-
- let is_pos l =
- is_even l
-
- (** val blit : int -> int **)
-
- let blit l =
- lsr0 l (ExtrNative.of_uint(1))
-
- (** val lit : int -> int **)
-
- let lit x =
- lsl0 x (ExtrNative.of_uint(1))
-
- (** val neg : int -> int **)
-
- let neg l =
- lxor0 l (ExtrNative.of_uint(1))
-
- (** val nlit : int -> int **)
-
- let nlit x =
- neg (lit x)
-
- (** val _true : int **)
-
+module Z_as_Int =
+ struct
+ type t = z
+
+ (** val _0 : z **)
+
+ let _0 =
+ Z0
+
+ (** val _1 : z **)
+
+ let _1 =
+ Zpos XH
+
+ (** val _2 : z **)
+
+ let _2 =
+ Zpos (XO XH)
+
+ (** val _3 : z **)
+
+ let _3 =
+ Zpos (XI XH)
+
+ (** val add : z -> z -> z **)
+
+ let add =
+ Z.add
+
+ (** val opp : z -> z **)
+
+ let opp =
+ Z.opp
+
+ (** val sub : z -> z -> z **)
+
+ let sub =
+ Z.sub
+
+ (** val mul : z -> z -> z **)
+
+ let mul =
+ Z.mul
+
+ (** val max : z -> z -> z **)
+
+ let max =
+ Z.max
+
+ (** val eqb : z -> z -> bool **)
+
+ let eqb =
+ Z.eqb
+
+ (** val ltb : z -> z -> bool **)
+
+ let ltb =
+ Z.ltb
+
+ (** val leb : z -> z -> bool **)
+
+ let leb =
+ Z.leb
+
+ (** val eq_dec : z -> z -> sumbool **)
+
+ let eq_dec =
+ Z.eq_dec
+
+ (** val gt_le_dec : z -> z -> sumbool **)
+
+ let gt_le_dec i j =
+ let b = Z.ltb j i in if b then Left else Right
+
+ (** val ge_lt_dec : z -> z -> sumbool **)
+
+ let ge_lt_dec i j =
+ let b = Z.ltb i j in if b then Right else Left
+
+ (** val i2z : t -> z **)
+
+ let i2z n =
+ n
+ end
+
+module Coq_Raw =
+ functor (I:Int) ->
+ functor (X:OrderedType) ->
+ struct
+ type key = X.t
+
+ type 'elt tree =
+ | Leaf
+ | Node of 'elt tree * key * 'elt * 'elt tree * I.t
+
+ (** val tree_rect :
+ 'a2 -> ('a1 tree -> 'a2 -> key -> 'a1 -> 'a1 tree -> 'a2 -> I.t -> 'a2)
+ -> 'a1 tree -> 'a2 **)
+
+ let rec tree_rect f f0 = function
+ | Leaf -> f
+ | Node (t1, k, y, t2, t3) ->
+ f0 t1 (tree_rect f f0 t1) k y t2 (tree_rect f f0 t2) t3
+
+ (** val tree_rec :
+ 'a2 -> ('a1 tree -> 'a2 -> key -> 'a1 -> 'a1 tree -> 'a2 -> I.t -> 'a2)
+ -> 'a1 tree -> 'a2 **)
+
+ let rec tree_rec f f0 = function
+ | Leaf -> f
+ | Node (t1, k, y, t2, t3) ->
+ f0 t1 (tree_rec f f0 t1) k y t2 (tree_rec f f0 t2) t3
+
+ (** val height : 'a1 tree -> I.t **)
+
+ let height = function
+ | Leaf -> I._0
+ | Node (_, _, _, _, h) -> h
+
+ (** val cardinal : 'a1 tree -> nat **)
+
+ let rec cardinal = function
+ | Leaf -> O
+ | Node (l, _, _, r, _) -> S (add (cardinal l) (cardinal r))
+
+ (** val empty : 'a1 tree **)
+
+ let empty =
+ Leaf
+
+ (** val is_empty : 'a1 tree -> bool **)
+
+ let is_empty = function
+ | Leaf -> true
+ | Node (_, _, _, _, _) -> false
+
+ (** val mem : X.t -> 'a1 tree -> bool **)
+
+ let rec mem x = function
+ | Leaf -> false
+ | Node (l, y, _, r, _) ->
+ (match X.compare x y with
+ | LT -> mem x l
+ | EQ -> true
+ | GT -> mem x r)
+
+ (** val find : X.t -> 'a1 tree -> 'a1 option **)
+
+ let rec find x = function
+ | Leaf -> None
+ | Node (l, y, d, r, _) ->
+ (match X.compare x y with
+ | LT -> find x l
+ | EQ -> Some d
+ | GT -> find x r)
+
+ (** val create : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+ let create l x e r =
+ Node (l, x, e, r, (I.add (I.max (height l) (height r)) I._1))
+
+ (** val assert_false : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+ let assert_false =
+ create
+
+ (** val bal : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+ let bal l x d r =
+ let hl = height l in
+ let hr = height r in
+ (match I.gt_le_dec hl (I.add hr I._2) with
+ | Left ->
+ (match l with
+ | Leaf -> assert_false l x d r
+ | Node (ll, lx, ld, lr, _) ->
+ (match I.ge_lt_dec (height ll) (height lr) with
+ | Left -> create ll lx ld (create lr x d r)
+ | Right ->
+ (match lr with
+ | Leaf -> assert_false l x d r
+ | Node (lrl, lrx, lrd, lrr, _) ->
+ create (create ll lx ld lrl) lrx lrd (create lrr x d r))))
+ | Right ->
+ (match I.gt_le_dec hr (I.add hl I._2) with
+ | Left ->
+ (match r with
+ | Leaf -> assert_false l x d r
+ | Node (rl, rx, rd, rr, _) ->
+ (match I.ge_lt_dec (height rr) (height rl) with
+ | Left -> create (create l x d rl) rx rd rr
+ | Right ->
+ (match rl with
+ | Leaf -> assert_false l x d r
+ | Node (rll, rlx, rld, rlr, _) ->
+ create (create l x d rll) rlx rld (create rlr rx rd rr))))
+ | Right -> create l x d r))
+
+ (** val add : key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+ let rec add x d = function
+ | Leaf -> Node (Leaf, x, d, Leaf, I._1)
+ | Node (l, y, d', r, h) ->
+ (match X.compare x y with
+ | LT -> bal (add x d l) y d' r
+ | EQ -> Node (l, y, d, r, h)
+ | GT -> bal l y d' (add x d r))
+
+ (** val remove_min :
+ 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree * (key * 'a1) **)
+
+ let rec remove_min l x d r =
+ match l with
+ | Leaf -> (r, (x, d))
+ | Node (ll, lx, ld, lr, _) ->
+ let (l', m) = remove_min ll lx ld lr in ((bal l' x d r), m)
+
+ (** val merge : 'a1 tree -> 'a1 tree -> 'a1 tree **)
+
+ let merge s1 s2 =
+ match s1 with
+ | Leaf -> s2
+ | Node (_, _, _, _, _) ->
+ (match s2 with
+ | Leaf -> s1
+ | Node (l2, x2, d2, r2, _) ->
+ let (s2', p) = remove_min l2 x2 d2 r2 in
+ let (x, d) = p in bal s1 x d s2')
+
+ (** val remove : X.t -> 'a1 tree -> 'a1 tree **)
+
+ let rec remove x = function
+ | Leaf -> Leaf
+ | Node (l, y, d, r, _) ->
+ (match X.compare x y with
+ | LT -> bal (remove x l) y d r
+ | EQ -> merge l r
+ | GT -> bal l y d (remove x r))
+
+ (** val join : 'a1 tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree **)
+
+ let rec join l = match l with
+ | Leaf -> add
+ | Node (ll, lx, ld, lr, lh) ->
+ (fun x d ->
+ let rec join_aux r = match r with
+ | Leaf -> add x d l
+ | Node (rl, rx, rd, rr, rh) ->
+ (match I.gt_le_dec lh (I.add rh I._2) with
+ | Left -> bal ll lx ld (join lr x d r)
+ | Right ->
+ (match I.gt_le_dec rh (I.add lh I._2) with
+ | Left -> bal (join_aux rl) rx rd rr
+ | Right -> create l x d r))
+ in join_aux)
+
+ type 'elt triple = { t_left : 'elt tree; t_opt : 'elt option;
+ t_right : 'elt tree }
+
+ (** val t_left : 'a1 triple -> 'a1 tree **)
+
+ let t_left t0 =
+ t0.t_left
+
+ (** val t_opt : 'a1 triple -> 'a1 option **)
+
+ let t_opt t0 =
+ t0.t_opt
+
+ (** val t_right : 'a1 triple -> 'a1 tree **)
+
+ let t_right t0 =
+ t0.t_right
+
+ (** val split : X.t -> 'a1 tree -> 'a1 triple **)
+
+ let rec split x = function
+ | Leaf -> { t_left = Leaf; t_opt = None; t_right = Leaf }
+ | Node (l, y, d, r, _) ->
+ (match X.compare x y with
+ | LT ->
+ let { t_left = ll; t_opt = o; t_right = rl } = split x l in
+ { t_left = ll; t_opt = o; t_right = (join rl y d r) }
+ | EQ -> { t_left = l; t_opt = (Some d); t_right = r }
+ | GT ->
+ let { t_left = rl; t_opt = o; t_right = rr } = split x r in
+ { t_left = (join l y d rl); t_opt = o; t_right = rr })
+
+ (** val concat : 'a1 tree -> 'a1 tree -> 'a1 tree **)
+
+ let concat m1 m2 =
+ match m1 with
+ | Leaf -> m2
+ | Node (_, _, _, _, _) ->
+ (match m2 with
+ | Leaf -> m1
+ | Node (l2, x2, d2, r2, _) ->
+ let (m2', xd) = remove_min l2 x2 d2 r2 in
+ join m1 (fst xd) (snd xd) m2')
+
+ (** val elements_aux : (key * 'a1) list -> 'a1 tree -> (key * 'a1) list **)
+
+ let rec elements_aux acc = function
+ | Leaf -> acc
+ | Node (l, x, d, r, _) ->
+ elements_aux (Cons ((x, d), (elements_aux acc r))) l
+
+ (** val elements : 'a1 tree -> (key * 'a1) list **)
+
+ let elements m =
+ elements_aux Nil m
+
+ (** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 tree -> 'a2 -> 'a2 **)
+
+ let rec fold f m a =
+ match m with
+ | Leaf -> a
+ | Node (l, x, d, r, _) -> fold f r (f x d (fold f l a))
+
+ type 'elt enumeration =
+ | End
+ | More of key * 'elt * 'elt tree * 'elt enumeration
+
+ (** val enumeration_rect :
+ 'a2 -> (key -> 'a1 -> 'a1 tree -> 'a1 enumeration -> 'a2 -> 'a2) -> 'a1
+ enumeration -> 'a2 **)
+
+ let rec enumeration_rect f f0 = function
+ | End -> f
+ | More (k, e0, t0, e1) -> f0 k e0 t0 e1 (enumeration_rect f f0 e1)
+
+ (** val enumeration_rec :
+ 'a2 -> (key -> 'a1 -> 'a1 tree -> 'a1 enumeration -> 'a2 -> 'a2) -> 'a1
+ enumeration -> 'a2 **)
+
+ let rec enumeration_rec f f0 = function
+ | End -> f
+ | More (k, e0, t0, e1) -> f0 k e0 t0 e1 (enumeration_rec f f0 e1)
+
+ (** val cons : 'a1 tree -> 'a1 enumeration -> 'a1 enumeration **)
+
+ let rec cons m e =
+ match m with
+ | Leaf -> e
+ | Node (l, x, d, r, _) -> cons l (More (x, d, r, e))
+
+ (** val equal_more :
+ ('a1 -> 'a1 -> bool) -> X.t -> 'a1 -> ('a1 enumeration -> bool) -> 'a1
+ enumeration -> bool **)
+
+ let equal_more cmp x1 d1 cont = function
+ | End -> false
+ | More (x2, d2, r2, e3) ->
+ (match X.compare x1 x2 with
+ | EQ -> if cmp d1 d2 then cont (cons r2 e3) else false
+ | _ -> false)
+
+ (** val equal_cont :
+ ('a1 -> 'a1 -> bool) -> 'a1 tree -> ('a1 enumeration -> bool) -> 'a1
+ enumeration -> bool **)
+
+ let rec equal_cont cmp m1 cont e2 =
+ match m1 with
+ | Leaf -> cont e2
+ | Node (l1, x1, d1, r1, _) ->
+ equal_cont cmp l1 (equal_more cmp x1 d1 (equal_cont cmp r1 cont)) e2
+
+ (** val equal_end : 'a1 enumeration -> bool **)
+
+ let equal_end = function
+ | End -> true
+ | More (_, _, _, _) -> false
+
+ (** val equal : ('a1 -> 'a1 -> bool) -> 'a1 tree -> 'a1 tree -> bool **)
+
+ let equal cmp m1 m2 =
+ equal_cont cmp m1 equal_end (cons m2 End)
+
+ (** val map : ('a1 -> 'a2) -> 'a1 tree -> 'a2 tree **)
+
+ let rec map f = function
+ | Leaf -> Leaf
+ | Node (l, x, d, r, h) -> Node ((map f l), x, (f d), (map f r), h)
+
+ (** val mapi : (key -> 'a1 -> 'a2) -> 'a1 tree -> 'a2 tree **)
+
+ let rec mapi f = function
+ | Leaf -> Leaf
+ | Node (l, x, d, r, h) -> Node ((mapi f l), x, (f x d), (mapi f r), h)
+
+ (** val map_option : (key -> 'a1 -> 'a2 option) -> 'a1 tree -> 'a2 tree **)
+
+ let rec map_option f = function
+ | Leaf -> Leaf
+ | Node (l, x, d, r, _) ->
+ (match f x d with
+ | Some d' -> join (map_option f l) x d' (map_option f r)
+ | None -> concat (map_option f l) (map_option f r))
+
+ (** val map2_opt :
+ (key -> 'a1 -> 'a2 option -> 'a3 option) -> ('a1 tree -> 'a3 tree) ->
+ ('a2 tree -> 'a3 tree) -> 'a1 tree -> 'a2 tree -> 'a3 tree **)
+
+ let rec map2_opt f mapl mapr m1 m2 =
+ match m1 with
+ | Leaf -> mapr m2
+ | Node (l1, x1, d1, r1, _) ->
+ (match m2 with
+ | Leaf -> mapl m1
+ | Node (_, _, _, _, _) ->
+ let { t_left = l2'; t_opt = o2; t_right = r2' } = split x1 m2 in
+ (match f x1 d1 o2 with
+ | Some e ->
+ join (map2_opt f mapl mapr l1 l2') x1 e
+ (map2_opt f mapl mapr r1 r2')
+ | None ->
+ concat (map2_opt f mapl mapr l1 l2') (map2_opt f mapl mapr r1 r2')))
+
+ (** val map2 :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 tree -> 'a2 tree -> 'a3
+ tree **)
+
+ let map2 f =
+ map2_opt (fun _ d o -> f (Some d) o)
+ (map_option (fun _ d -> f (Some d) None))
+ (map_option (fun _ d' -> f None (Some d')))
+
+ module Proofs =
+ struct
+ module MX = OrderedTypeFacts(X)
+
+ module PX = KeyOrderedType(X)
+
+ module L = Raw(X)
+
+ type 'elt coq_R_mem =
+ | R_mem_0 of 'elt tree
+ | R_mem_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t *
+ bool * 'elt coq_R_mem
+ | R_mem_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ | R_mem_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t *
+ bool * 'elt coq_R_mem
+
+ (** val coq_R_mem_rect :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2
+ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+ __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1
+ tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2)
+ -> 'a1 tree -> bool -> 'a1 coq_R_mem -> 'a2 **)
+
+ let rec coq_R_mem_rect x f f0 f1 f2 _ _ = function
+ | R_mem_0 m -> f m __
+ | R_mem_1 (m, l, y, _x, r0, _x0, _res, r1) ->
+ f0 m l y _x r0 _x0 __ __ __ _res r1
+ (coq_R_mem_rect x f f0 f1 f2 l _res r1)
+ | R_mem_2 (m, l, y, _x, r0, _x0) -> f1 m l y _x r0 _x0 __ __ __
+ | R_mem_3 (m, l, y, _x, r0, _x0, _res, r1) ->
+ f2 m l y _x r0 _x0 __ __ __ _res r1
+ (coq_R_mem_rect x f f0 f1 f2 r0 _res r1)
+
+ (** val coq_R_mem_rec :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2
+ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+ __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1
+ tree -> I.t -> __ -> __ -> __ -> bool -> 'a1 coq_R_mem -> 'a2 -> 'a2)
+ -> 'a1 tree -> bool -> 'a1 coq_R_mem -> 'a2 **)
+
+ let rec coq_R_mem_rec x f f0 f1 f2 _ _ = function
+ | R_mem_0 m -> f m __
+ | R_mem_1 (m, l, y, _x, r0, _x0, _res, r1) ->
+ f0 m l y _x r0 _x0 __ __ __ _res r1
+ (coq_R_mem_rec x f f0 f1 f2 l _res r1)
+ | R_mem_2 (m, l, y, _x, r0, _x0) -> f1 m l y _x r0 _x0 __ __ __
+ | R_mem_3 (m, l, y, _x, r0, _x0, _res, r1) ->
+ f2 m l y _x r0 _x0 __ __ __ _res r1
+ (coq_R_mem_rec x f f0 f1 f2 r0 _res r1)
+
+ type 'elt coq_R_find =
+ | R_find_0 of 'elt tree
+ | R_find_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt option * 'elt coq_R_find
+ | R_find_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ | R_find_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt option * 'elt coq_R_find
+
+ (** val coq_R_find_rect :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+ -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+ I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+ -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+ let rec coq_R_find_rect x f f0 f1 f2 _ _ = function
+ | R_find_0 m -> f m __
+ | R_find_1 (m, l, y, d, r0, _x, _res, r1) ->
+ f0 m l y d r0 _x __ __ __ _res r1
+ (coq_R_find_rect x f f0 f1 f2 l _res r1)
+ | R_find_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+ | R_find_3 (m, l, y, d, r0, _x, _res, r1) ->
+ f2 m l y d r0 _x __ __ __ _res r1
+ (coq_R_find_rect x f f0 f1 f2 r0 _res r1)
+
+ (** val coq_R_find_rec :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+ -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+ I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 option -> 'a1 coq_R_find
+ -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 option -> 'a1 coq_R_find -> 'a2 **)
+
+ let rec coq_R_find_rec x f f0 f1 f2 _ _ = function
+ | R_find_0 m -> f m __
+ | R_find_1 (m, l, y, d, r0, _x, _res, r1) ->
+ f0 m l y d r0 _x __ __ __ _res r1
+ (coq_R_find_rec x f f0 f1 f2 l _res r1)
+ | R_find_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+ | R_find_3 (m, l, y, d, r0, _x, _res, r1) ->
+ f2 m l y d r0 _x __ __ __ _res r1
+ (coq_R_find_rec x f f0 f1 f2 r0 _res r1)
+
+ type 'elt coq_R_bal =
+ | R_bal_0 of 'elt tree * key * 'elt * 'elt tree
+ | R_bal_1 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key *
+ 'elt * 'elt tree * I.t
+ | R_bal_2 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key *
+ 'elt * 'elt tree * I.t
+ | R_bal_3 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key *
+ 'elt * 'elt tree * I.t * 'elt tree * key * 'elt * 'elt tree *
+ I.t
+ | R_bal_4 of 'elt tree * key * 'elt * 'elt tree
+ | R_bal_5 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key *
+ 'elt * 'elt tree * I.t
+ | R_bal_6 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key *
+ 'elt * 'elt tree * I.t
+ | R_bal_7 of 'elt tree * key * 'elt * 'elt tree * 'elt tree * key *
+ 'elt * 'elt tree * I.t * 'elt tree * key * 'elt * 'elt tree *
+ I.t
+ | R_bal_8 of 'elt tree * key * 'elt * 'elt tree
+
+ (** val coq_R_bal_rect :
+ ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> 'a2) -> ('a1
+ tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key ->
+ 'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+ I.t -> __ -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1
+ tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ ->
+ 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __
+ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+ __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+ __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __
+ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+ __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+ __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2) -> ('a1
+ tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> 'a2) -> 'a1
+ tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_bal -> 'a2 **)
+
+ let coq_R_bal_rect f f0 f1 f2 f3 f4 f5 f6 f7 _ _ _ _ _ = function
+ | R_bal_0 (x, x0, x1, x2) -> f x x0 x1 x2 __ __ __
+ | R_bal_1 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f0 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __
+ | R_bal_2 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f1 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ __
+ | R_bal_3 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+ f2 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+ | R_bal_4 (x, x0, x1, x2) -> f3 x x0 x1 x2 __ __ __ __ __
+ | R_bal_5 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f4 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __
+ | R_bal_6 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f5 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ __
+ | R_bal_7 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+ f6 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+ | R_bal_8 (x, x0, x1, x2) -> f7 x x0 x1 x2 __ __ __ __
+
+ (** val coq_R_bal_rec :
+ ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> 'a2) -> ('a1
+ tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key ->
+ 'a1 -> 'a1 tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+ I.t -> __ -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1
+ tree -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ ->
+ 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __
+ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+ __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+ __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __
+ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+ -> __ -> 'a2) -> ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> __ ->
+ __ -> __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ ->
+ __ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2) -> ('a1
+ tree -> key -> 'a1 -> 'a1 tree -> __ -> __ -> __ -> __ -> 'a2) -> 'a1
+ tree -> key -> 'a1 -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_bal -> 'a2 **)
+
+ let coq_R_bal_rec f f0 f1 f2 f3 f4 f5 f6 f7 _ _ _ _ _ = function
+ | R_bal_0 (x, x0, x1, x2) -> f x x0 x1 x2 __ __ __
+ | R_bal_1 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f0 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __
+ | R_bal_2 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f1 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ __
+ | R_bal_3 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+ f2 x x0 x1 x2 __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+ | R_bal_4 (x, x0, x1, x2) -> f3 x x0 x1 x2 __ __ __ __ __
+ | R_bal_5 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f4 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __
+ | R_bal_6 (x, x0, x1, x2, x3, x4, x5, x6, x7) ->
+ f5 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ __
+ | R_bal_7 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+ f6 x x0 x1 x2 __ __ __ __ x3 x4 x5 x6 x7 __ __ __ x8 x9 x10 x11 x12 __
+ | R_bal_8 (x, x0, x1, x2) -> f7 x x0 x1 x2 __ __ __ __
+
+ type 'elt coq_R_add =
+ | R_add_0 of 'elt tree
+ | R_add_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt tree * 'elt coq_R_add
+ | R_add_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ | R_add_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt tree * 'elt coq_R_add
+
+ (** val coq_R_add_rect :
+ key -> 'a1 -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key
+ -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+ coq_R_add -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 ->
+ 'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree ->
+ key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+ coq_R_add -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_add ->
+ 'a2 **)
+
+ let rec coq_R_add_rect x d f f0 f1 f2 _ _ = function
+ | R_add_0 m -> f m __
+ | R_add_1 (m, l, y, d', r0, h, _res, r1) ->
+ f0 m l y d' r0 h __ __ __ _res r1
+ (coq_R_add_rect x d f f0 f1 f2 l _res r1)
+ | R_add_2 (m, l, y, d', r0, h) -> f1 m l y d' r0 h __ __ __
+ | R_add_3 (m, l, y, d', r0, h, _res, r1) ->
+ f2 m l y d' r0 h __ __ __ _res r1
+ (coq_R_add_rect x d f f0 f1 f2 r0 _res r1)
+
+ (** val coq_R_add_rec :
+ key -> 'a1 -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key
+ -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+ coq_R_add -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 ->
+ 'a1 tree -> I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree ->
+ key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1
+ coq_R_add -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_add ->
+ 'a2 **)
+
+ let rec coq_R_add_rec x d f f0 f1 f2 _ _ = function
+ | R_add_0 m -> f m __
+ | R_add_1 (m, l, y, d', r0, h, _res, r1) ->
+ f0 m l y d' r0 h __ __ __ _res r1
+ (coq_R_add_rec x d f f0 f1 f2 l _res r1)
+ | R_add_2 (m, l, y, d', r0, h) -> f1 m l y d' r0 h __ __ __
+ | R_add_3 (m, l, y, d', r0, h, _res, r1) ->
+ f2 m l y d' r0 h __ __ __ _res r1
+ (coq_R_add_rec x d f f0 f1 f2 r0 _res r1)
+
+ type 'elt coq_R_remove_min =
+ | R_remove_min_0 of 'elt tree * key * 'elt * 'elt tree
+ | R_remove_min_1 of 'elt tree * key * 'elt * 'elt tree * 'elt tree *
+ key * 'elt * 'elt tree * I.t * ('elt tree * (key * 'elt))
+ * 'elt coq_R_remove_min * 'elt tree * (key * 'elt)
+
+ (** val coq_R_remove_min_rect :
+ ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> key
+ -> 'a1 -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 -> 'a1
+ tree -> (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> key -> 'a1 -> 'a1
+ tree -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 **)
+
+ let rec coq_R_remove_min_rect f f0 _ _ _ _ _ = function
+ | R_remove_min_0 (l, x, d, r0) -> f l x d r0 __
+ | R_remove_min_1 (l, x, d, r0, ll, lx, ld, lr, _x, _res, r1, l', m) ->
+ f0 l x d r0 ll lx ld lr _x __ _res r1
+ (coq_R_remove_min_rect f f0 ll lx ld lr _res r1) l' m __
+
+ (** val coq_R_remove_min_rec :
+ ('a1 tree -> key -> 'a1 -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> key
+ -> 'a1 -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 -> 'a1
+ tree -> (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> key -> 'a1 -> 'a1
+ tree -> ('a1 tree * (key * 'a1)) -> 'a1 coq_R_remove_min -> 'a2 **)
+
+ let rec coq_R_remove_min_rec f f0 _ _ _ _ _ = function
+ | R_remove_min_0 (l, x, d, r0) -> f l x d r0 __
+ | R_remove_min_1 (l, x, d, r0, ll, lx, ld, lr, _x, _res, r1, l', m) ->
+ f0 l x d r0 ll lx ld lr _x __ _res r1
+ (coq_R_remove_min_rec f f0 ll lx ld lr _res r1) l' m __
+
+ type 'elt coq_R_merge =
+ | R_merge_0 of 'elt tree * 'elt tree
+ | R_merge_1 of 'elt tree * 'elt tree * 'elt tree * key * 'elt * 'elt tree
+ * I.t
+ | R_merge_2 of 'elt tree * 'elt tree * 'elt tree * key * 'elt * 'elt tree
+ * I.t * 'elt tree * key * 'elt * 'elt tree * I.t * 'elt tree
+ * (key * 'elt) * key * 'elt
+
+ (** val coq_R_merge_rect :
+ ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+ tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+ tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+ (key * 'a1) -> __ -> key -> 'a1 -> __ -> 'a2) -> 'a1 tree -> 'a1 tree
+ -> 'a1 tree -> 'a1 coq_R_merge -> 'a2 **)
+
+ let coq_R_merge_rect f f0 f1 _ _ _ = function
+ | R_merge_0 (x, x0) -> f x x0 __
+ | R_merge_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+ | R_merge_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12,
+ x13, x14) ->
+ f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __ x13 x14 __
+
+ (** val coq_R_merge_rec :
+ ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+ tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+ tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+ (key * 'a1) -> __ -> key -> 'a1 -> __ -> 'a2) -> 'a1 tree -> 'a1 tree
+ -> 'a1 tree -> 'a1 coq_R_merge -> 'a2 **)
+
+ let coq_R_merge_rec f f0 f1 _ _ _ = function
+ | R_merge_0 (x, x0) -> f x x0 __
+ | R_merge_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+ | R_merge_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12,
+ x13, x14) ->
+ f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __ x13 x14 __
+
+ type 'elt coq_R_remove =
+ | R_remove_0 of 'elt tree
+ | R_remove_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree *
+ I.t * 'elt tree * 'elt coq_R_remove
+ | R_remove_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ | R_remove_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree *
+ I.t * 'elt tree * 'elt coq_R_remove
+
+ (** val coq_R_remove_rect :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+ -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+ I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+ -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_remove -> 'a2 **)
+
+ let rec coq_R_remove_rect x f f0 f1 f2 _ _ = function
+ | R_remove_0 m -> f m __
+ | R_remove_1 (m, l, y, d, r0, _x, _res, r1) ->
+ f0 m l y d r0 _x __ __ __ _res r1
+ (coq_R_remove_rect x f f0 f1 f2 l _res r1)
+ | R_remove_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+ | R_remove_3 (m, l, y, d, r0, _x, _res, r1) ->
+ f2 m l y d r0 _x __ __ __ _res r1
+ (coq_R_remove_rect x f f0 f1 f2 r0 _res r1)
+
+ (** val coq_R_remove_rec :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+ -> 'a2 -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree ->
+ I.t -> __ -> __ -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 tree -> 'a1 coq_R_remove
+ -> 'a2 -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 coq_R_remove -> 'a2 **)
+
+ let rec coq_R_remove_rec x f f0 f1 f2 _ _ = function
+ | R_remove_0 m -> f m __
+ | R_remove_1 (m, l, y, d, r0, _x, _res, r1) ->
+ f0 m l y d r0 _x __ __ __ _res r1
+ (coq_R_remove_rec x f f0 f1 f2 l _res r1)
+ | R_remove_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+ | R_remove_3 (m, l, y, d, r0, _x, _res, r1) ->
+ f2 m l y d r0 _x __ __ __ _res r1
+ (coq_R_remove_rec x f f0 f1 f2 r0 _res r1)
+
+ type 'elt coq_R_concat =
+ | R_concat_0 of 'elt tree * 'elt tree
+ | R_concat_1 of 'elt tree * 'elt tree * 'elt tree * key * 'elt
+ * 'elt tree * I.t
+ | R_concat_2 of 'elt tree * 'elt tree * 'elt tree * key * 'elt
+ * 'elt tree * I.t * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt tree * (key * 'elt)
+
+ (** val coq_R_concat_rect :
+ ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+ tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+ tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+ (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 tree -> 'a1
+ coq_R_concat -> 'a2 **)
+
+ let coq_R_concat_rect f f0 f1 _ _ _ = function
+ | R_concat_0 (x, x0) -> f x x0 __
+ | R_concat_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+ | R_concat_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+ f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __
+
+ (** val coq_R_concat_rec :
+ ('a1 tree -> 'a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> 'a1
+ tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2) -> ('a1
+ tree -> 'a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a1 tree ->
+ (key * 'a1) -> __ -> 'a2) -> 'a1 tree -> 'a1 tree -> 'a1 tree -> 'a1
+ coq_R_concat -> 'a2 **)
+
+ let coq_R_concat_rec f f0 f1 _ _ _ = function
+ | R_concat_0 (x, x0) -> f x x0 __
+ | R_concat_1 (x, x0, x1, x2, x3, x4, x5) -> f0 x x0 x1 x2 x3 x4 x5 __ __
+ | R_concat_2 (x, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) ->
+ f1 x x0 x1 x2 x3 x4 x5 __ x6 x7 x8 x9 x10 __ x11 x12 __
+
+ type 'elt coq_R_split =
+ | R_split_0 of 'elt tree
+ | R_split_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt triple * 'elt coq_R_split * 'elt tree * 'elt option * 'elt tree
+ | R_split_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ | R_split_3 of 'elt tree * 'elt tree * key * 'elt * 'elt tree * I.t
+ * 'elt triple * 'elt coq_R_split * 'elt tree * 'elt option * 'elt tree
+
+ (** val coq_R_split_rect :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split
+ -> 'a2 -> 'a1 tree -> 'a1 option -> 'a1 tree -> __ -> 'a2) -> ('a1
+ tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+ __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split -> 'a2 -> 'a1 tree ->
+ 'a1 option -> 'a1 tree -> __ -> 'a2) -> 'a1 tree -> 'a1 triple -> 'a1
+ coq_R_split -> 'a2 **)
+
+ let rec coq_R_split_rect x f f0 f1 f2 _ _ = function
+ | R_split_0 m -> f m __
+ | R_split_1 (m, l, y, d, r0, _x, _res, r1, ll, o, rl) ->
+ f0 m l y d r0 _x __ __ __ _res r1
+ (coq_R_split_rect x f f0 f1 f2 l _res r1) ll o rl __
+ | R_split_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+ | R_split_3 (m, l, y, d, r0, _x, _res, r1, rl, o, rr) ->
+ f2 m l y d r0 _x __ __ __ _res r1
+ (coq_R_split_rect x f f0 f1 f2 r0 _res r1) rl o rr __
+
+ (** val coq_R_split_rec :
+ X.t -> ('a1 tree -> __ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1
+ -> 'a1 tree -> I.t -> __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split
+ -> 'a2 -> 'a1 tree -> 'a1 option -> 'a1 tree -> __ -> 'a2) -> ('a1
+ tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> __ -> __
+ -> 'a2) -> ('a1 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t ->
+ __ -> __ -> __ -> 'a1 triple -> 'a1 coq_R_split -> 'a2 -> 'a1 tree ->
+ 'a1 option -> 'a1 tree -> __ -> 'a2) -> 'a1 tree -> 'a1 triple -> 'a1
+ coq_R_split -> 'a2 **)
+
+ let rec coq_R_split_rec x f f0 f1 f2 _ _ = function
+ | R_split_0 m -> f m __
+ | R_split_1 (m, l, y, d, r0, _x, _res, r1, ll, o, rl) ->
+ f0 m l y d r0 _x __ __ __ _res r1
+ (coq_R_split_rec x f f0 f1 f2 l _res r1) ll o rl __
+ | R_split_2 (m, l, y, d, r0, _x) -> f1 m l y d r0 _x __ __ __
+ | R_split_3 (m, l, y, d, r0, _x, _res, r1, rl, o, rr) ->
+ f2 m l y d r0 _x __ __ __ _res r1
+ (coq_R_split_rec x f f0 f1 f2 r0 _res r1) rl o rr __
+
+ type ('elt, 'x) coq_R_map_option =
+ | R_map_option_0 of 'elt tree
+ | R_map_option_1 of 'elt tree * 'elt tree * key * 'elt * 'elt tree *
+ I.t * 'x * 'x tree * ('elt, 'x) coq_R_map_option * 'x tree
+ * ('elt, 'x) coq_R_map_option
+ | R_map_option_2 of 'elt tree * 'elt tree * key * 'elt * 'elt tree *
+ I.t * 'x tree * ('elt, 'x) coq_R_map_option * 'x tree
+ * ('elt, 'x) coq_R_map_option
+
+ (** val coq_R_map_option_rect :
+ (key -> 'a1 -> 'a2 option) -> ('a1 tree -> __ -> 'a3) -> ('a1 tree ->
+ 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 -> __ -> 'a2
+ tree -> ('a1, 'a2) coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2)
+ coq_R_map_option -> 'a3 -> 'a3) -> ('a1 tree -> 'a1 tree -> key ->
+ 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2 tree -> ('a1, 'a2)
+ coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+ 'a3 -> 'a3) -> 'a1 tree -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+ 'a3 **)
+
+ let rec coq_R_map_option_rect f f0 f1 f2 _ _ = function
+ | R_map_option_0 m -> f0 m __
+ | R_map_option_1 (m, l, x, d, r0, _x, d', _res0, r1, _res, r2) ->
+ f1 m l x d r0 _x __ d' __ _res0 r1
+ (coq_R_map_option_rect f f0 f1 f2 l _res0 r1) _res r2
+ (coq_R_map_option_rect f f0 f1 f2 r0 _res r2)
+ | R_map_option_2 (m, l, x, d, r0, _x, _res0, r1, _res, r2) ->
+ f2 m l x d r0 _x __ __ _res0 r1
+ (coq_R_map_option_rect f f0 f1 f2 l _res0 r1) _res r2
+ (coq_R_map_option_rect f f0 f1 f2 r0 _res r2)
+
+ (** val coq_R_map_option_rec :
+ (key -> 'a1 -> 'a2 option) -> ('a1 tree -> __ -> 'a3) -> ('a1 tree ->
+ 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 -> __ -> 'a2
+ tree -> ('a1, 'a2) coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2)
+ coq_R_map_option -> 'a3 -> 'a3) -> ('a1 tree -> 'a1 tree -> key ->
+ 'a1 -> 'a1 tree -> I.t -> __ -> __ -> 'a2 tree -> ('a1, 'a2)
+ coq_R_map_option -> 'a3 -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+ 'a3 -> 'a3) -> 'a1 tree -> 'a2 tree -> ('a1, 'a2) coq_R_map_option ->
+ 'a3 **)
+
+ let rec coq_R_map_option_rec f f0 f1 f2 _ _ = function
+ | R_map_option_0 m -> f0 m __
+ | R_map_option_1 (m, l, x, d, r0, _x, d', _res0, r1, _res, r2) ->
+ f1 m l x d r0 _x __ d' __ _res0 r1
+ (coq_R_map_option_rec f f0 f1 f2 l _res0 r1) _res r2
+ (coq_R_map_option_rec f f0 f1 f2 r0 _res r2)
+ | R_map_option_2 (m, l, x, d, r0, _x, _res0, r1, _res, r2) ->
+ f2 m l x d r0 _x __ __ _res0 r1
+ (coq_R_map_option_rec f f0 f1 f2 l _res0 r1) _res r2
+ (coq_R_map_option_rec f f0 f1 f2 r0 _res r2)
+
+ type ('elt, 'x0, 'x) coq_R_map2_opt =
+ | R_map2_opt_0 of 'elt tree * 'x0 tree
+ | R_map2_opt_1 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt
+ * 'elt tree * I.t
+ | R_map2_opt_2 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt
+ * 'elt tree * I.t * 'x0 tree * key * 'x0 * 'x0 tree * I.t * 'x0 tree
+ * 'x0 option * 'x0 tree * 'x * 'x tree
+ * ('elt, 'x0, 'x) coq_R_map2_opt * 'x tree
+ * ('elt, 'x0, 'x) coq_R_map2_opt
+ | R_map2_opt_3 of 'elt tree * 'x0 tree * 'elt tree * key * 'elt
+ * 'elt tree * I.t * 'x0 tree * key * 'x0 * 'x0 tree * I.t * 'x0 tree
+ * 'x0 option * 'x0 tree * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt
+ * 'x tree * ('elt, 'x0, 'x) coq_R_map2_opt
+
+ (** val coq_R_map2_opt_rect :
+ (key -> 'a1 -> 'a2 option -> 'a3 option) -> ('a1 tree -> 'a3 tree) ->
+ ('a2 tree -> 'a3 tree) -> ('a1 tree -> 'a2 tree -> __ -> 'a4) -> ('a1
+ tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> __ -> 'a4) -> ('a1 tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 ->
+ 'a1 tree -> I.t -> __ -> 'a2 tree -> key -> 'a2 -> 'a2 tree -> I.t ->
+ __ -> 'a2 tree -> 'a2 option -> 'a2 tree -> __ -> 'a3 -> __ -> 'a3
+ tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3 tree -> ('a1,
+ 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> ('a1 tree -> 'a2 tree ->
+ 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 tree -> key ->
+ 'a2 -> 'a2 tree -> I.t -> __ -> 'a2 tree -> 'a2 option -> 'a2 tree ->
+ __ -> __ -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3
+ tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> 'a1 tree ->
+ 'a2 tree -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 **)
+
+ let rec coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 _ _ _ = function
+ | R_map2_opt_0 (m1, m2) -> f0 m1 m2 __
+ | R_map2_opt_1 (m1, m2, l1, x1, d1, r1, _x) ->
+ f1 m1 m2 l1 x1 d1 r1 _x __ __
+ | R_map2_opt_2 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+ o2, r2', e, _res0, r0, _res, r2) ->
+ f2 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ e __
+ _res0 r0
+ (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0) _res r2
+ (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+ | R_map2_opt_3 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+ o2, r2', _res0, r0, _res, r2) ->
+ f3 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ __
+ _res0 r0
+ (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0) _res r2
+ (coq_R_map2_opt_rect f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+
+ (** val coq_R_map2_opt_rec :
+ (key -> 'a1 -> 'a2 option -> 'a3 option) -> ('a1 tree -> 'a3 tree) ->
+ ('a2 tree -> 'a3 tree) -> ('a1 tree -> 'a2 tree -> __ -> 'a4) -> ('a1
+ tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __
+ -> __ -> 'a4) -> ('a1 tree -> 'a2 tree -> 'a1 tree -> key -> 'a1 ->
+ 'a1 tree -> I.t -> __ -> 'a2 tree -> key -> 'a2 -> 'a2 tree -> I.t ->
+ __ -> 'a2 tree -> 'a2 option -> 'a2 tree -> __ -> 'a3 -> __ -> 'a3
+ tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3 tree -> ('a1,
+ 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> ('a1 tree -> 'a2 tree ->
+ 'a1 tree -> key -> 'a1 -> 'a1 tree -> I.t -> __ -> 'a2 tree -> key ->
+ 'a2 -> 'a2 tree -> I.t -> __ -> 'a2 tree -> 'a2 option -> 'a2 tree ->
+ __ -> __ -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a3
+ tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 -> 'a4) -> 'a1 tree ->
+ 'a2 tree -> 'a3 tree -> ('a1, 'a2, 'a3) coq_R_map2_opt -> 'a4 **)
+
+ let rec coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 _ _ _ = function
+ | R_map2_opt_0 (m1, m2) -> f0 m1 m2 __
+ | R_map2_opt_1 (m1, m2, l1, x1, d1, r1, _x) ->
+ f1 m1 m2 l1 x1 d1 r1 _x __ __
+ | R_map2_opt_2 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+ o2, r2', e, _res0, r0, _res, r2) ->
+ f2 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ e __
+ _res0 r0 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0)
+ _res r2 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+ | R_map2_opt_3 (m1, m2, l1, x1, d1, r1, _x, _x0, _x1, _x2, _x3, _x4, l2',
+ o2, r2', _res0, r0, _res, r2) ->
+ f3 m1 m2 l1 x1 d1 r1 _x __ _x0 _x1 _x2 _x3 _x4 __ l2' o2 r2' __ __
+ _res0 r0 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 l1 l2' _res0 r0)
+ _res r2 (coq_R_map2_opt_rec f mapl mapr f0 f1 f2 f3 r1 r2' _res r2)
+
+ (** val fold' : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 tree -> 'a2 -> 'a2 **)
+
+ let fold' f s =
+ L.fold f (elements s)
+
+ (** val flatten_e : 'a1 enumeration -> (key * 'a1) list **)
+
+ let rec flatten_e = function
+ | End -> Nil
+ | More (x, e0, t0, r) -> Cons ((x, e0), (app (elements t0) (flatten_e r)))
+ end
+ end
+
+module IntMake =
+ functor (I:Int) ->
+ functor (X:OrderedType) ->
+ struct
+ module E = X
+
+ module Raw = Coq_Raw(I)(X)
+
+ type 'elt bst =
+ 'elt Raw.tree
+ (* singleton inductive, whose constructor was Bst *)
+
+ (** val this : 'a1 bst -> 'a1 Raw.tree **)
+
+ let this b =
+ b
+
+ type 'elt t = 'elt bst
+
+ type key = E.t
+
+ (** val empty : 'a1 t **)
+
+ let empty =
+ Raw.empty
+
+ (** val is_empty : 'a1 t -> bool **)
+
+ let is_empty m =
+ Raw.is_empty (this m)
+
+ (** val add : key -> 'a1 -> 'a1 t -> 'a1 t **)
+
+ let add x e m =
+ Raw.add x e (this m)
+
+ (** val remove : key -> 'a1 t -> 'a1 t **)
+
+ let remove x m =
+ Raw.remove x (this m)
+
+ (** val mem : key -> 'a1 t -> bool **)
+
+ let mem x m =
+ Raw.mem x (this m)
+
+ (** val find : key -> 'a1 t -> 'a1 option **)
+
+ let find x m =
+ Raw.find x (this m)
+
+ (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+ let map f m =
+ Raw.map f (this m)
+
+ (** val mapi : (key -> 'a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+ let mapi f m =
+ Raw.mapi f (this m)
+
+ (** val map2 :
+ ('a1 option -> 'a2 option -> 'a3 option) -> 'a1 t -> 'a2 t -> 'a3 t **)
+
+ let map2 f m m' =
+ Raw.map2 f (this m) (this m')
+
+ (** val elements : 'a1 t -> (key * 'a1) list **)
+
+ let elements m =
+ Raw.elements (this m)
+
+ (** val cardinal : 'a1 t -> nat **)
+
+ let cardinal m =
+ Raw.cardinal (this m)
+
+ (** val fold : (key -> 'a1 -> 'a2 -> 'a2) -> 'a1 t -> 'a2 -> 'a2 **)
+
+ let fold f m i =
+ Raw.fold f (this m) i
+
+ (** val equal : ('a1 -> 'a1 -> bool) -> 'a1 t -> 'a1 t -> bool **)
+
+ let equal cmp m m' =
+ Raw.equal cmp (this m) (this m')
+ end
+
+module Make =
+ functor (X:OrderedType) ->
+ IntMake(Z_as_Int)(X)
+
+module IntOrderedType =
+ struct
+ type t = Uint63.t
+
+ (** val compare : Uint63.t -> Uint63.t -> Uint63.t compare1 **)
+
+ let compare x y =
+ if ltb0 x y then LT else if eqb0 x y then EQ else GT
+
+ (** val eq_dec : Uint63.t -> Uint63.t -> sumbool **)
+
+ let eq_dec x y =
+ if eqb0 x y then Left else Right
+ end
+
+module Map = Make(IntOrderedType)
+
+type 'a array = ('a Map.t * 'a) * Uint63.t
+
+(** val make : Uint63.t -> 'a1 -> 'a1 array **)
+
+let make l d =
+ ((Map.empty, d), l)
+
+module Coq__1 = struct
+ (** val get : 'a1 array -> Uint63.t -> 'a1 **)
+ let get t0 i =
+ let (td, l) = t0 in
+ let (t1, d) = td in
+ if ltb0 i l then (match Map.find i t1 with
+ | Some x -> x
+ | None -> d) else d
+end
+include Coq__1
+
+(** val set : 'a1 array -> Uint63.t -> 'a1 -> 'a1 array **)
+
+let set t0 i a =
+ let (td, l) = t0 in
+ if leb0 l i then t0 else let (t1, d) = td in (((Map.add i a t1), d), l)
+
+(** val length : 'a1 array -> Uint63.t **)
+
+let length = function
+| (_, l) -> l
+
+(** val iter_int63_aux : nat -> Uint63.t -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
+
+let rec iter_int63_aux n i f =
+ match n with
+ | O -> (fun x -> x)
+ | S n0 ->
+ if eqb0 i (Uint63.of_int (0))
+ then (fun x -> x)
+ else let g = iter_int63_aux n0 (lsr0 i (Uint63.of_int (1))) f in
+ (fun x -> if bit i (Uint63.of_int (0)) then f (g (g x)) else g (g x))
+
+(** val iter_int63 : Uint63.t -> ('a1 -> 'a1) -> 'a1 -> 'a1 **)
+
+let iter_int63 i f x =
+ iter_int63_aux size i f x
+
+(** val foldi :
+ (Uint63.t -> 'a1 -> 'a1) -> Uint63.t -> Uint63.t -> 'a1 -> 'a1 **)
+
+let foldi f from to0 a =
+ if leb0 to0 from
+ then a
+ else let (_, r) =
+ iter_int63 (sub0 to0 from) (fun jy ->
+ let (j, y) = jy in ((add0 j (Uint63.of_int (1))), (f j y))) (from,
+ a)
+ in
+ r
+
+(** val to_list : 'a1 array -> 'a1 list **)
+
+let to_list t0 =
+ rev
+ (foldi (fun i l -> Cons ((get t0 i), l)) (Uint63.of_int (0)) (length t0)
+ Nil)
+
+module Lit =
+ struct
+ (** val _true : Uint63.t **)
+
let _true =
- (ExtrNative.of_uint(0))
-
- (** val _false : int **)
-
- let _false =
- (ExtrNative.of_uint(2))
-
- (** val eqb : int -> int -> bool **)
-
- let eqb l l' =
- eqb l l'
-
- (** val interp : Valuation.t -> int -> bool **)
-
- let interp rho l =
- if is_pos l
- then Var.interp rho (blit l)
- else negb (Var.interp rho (blit l))
+ (Uint63.of_int (0))
end
-module C =
- struct
- type t = int list
-
- (** val interp : Valuation.t -> t -> bool **)
-
- let interp rho l =
- existsb (Lit.interp rho) l
-
+module C =
+ struct
+ type t = Uint63.t list
+
(** val _true : t **)
-
+
let _true =
Cons (Lit._true, Nil)
-
+
(** val is_false : t -> bool **)
-
+
let is_false = function
| Nil -> true
- | Cons (i, l) -> false
-
- (** val or_aux : (t -> t -> t) -> int -> t -> t -> int list **)
-
+ | Cons (_, _) -> false
+
+ (** val or_aux : (t -> t -> t) -> Uint63.t -> t -> t -> Uint63.t list **)
+
let rec or_aux or0 l1 c1 c2 = match c2 with
| Nil -> Cons (l1, c1)
| Cons (l2, c2') ->
- (match compare l1 l2 with
- | ExtrNative.Eq -> Cons (l1, (or0 c1 c2'))
- | ExtrNative.Lt -> Cons (l1, (or0 c1 c2))
- | ExtrNative.Gt -> Cons (l2, (or_aux or0 l1 c1 c2')))
-
+ (match compare0 l1 l2 with
+ | 0 -> Cons (l1, (or0 c1 c2'))
+ | (-1) -> Cons (l1, (or0 c1 c2))
+ | 1 -> Cons (l2, (or_aux or0 l1 c1 c2')))
+
(** val coq_or : t -> t -> t **)
-
+
let rec coq_or c1 c2 =
match c1 with
| Nil -> c2
@@ -249,29 +2409,29 @@ module C =
(match c2 with
| Nil -> c1
| Cons (l2, c2') ->
- (match compare l1 l2 with
- | ExtrNative.Eq -> Cons (l1, (coq_or c3 c2'))
- | ExtrNative.Lt -> Cons (l1, (coq_or c3 c2))
- | ExtrNative.Gt -> Cons (l2, (or_aux coq_or l1 c3 c2'))))
-
- (** val resolve_aux : (t -> t -> t) -> int -> t -> t -> t **)
-
+ (match compare0 l1 l2 with
+ | 0 -> Cons (l1, (coq_or c3 c2'))
+ | (-1) -> Cons (l1, (coq_or c3 c2))
+ | 1 -> Cons (l2, (or_aux coq_or l1 c3 c2'))))
+
+ (** val resolve_aux : (t -> t -> t) -> Uint63.t -> t -> t -> t **)
+
let rec resolve_aux resolve0 l1 c1 c2 = match c2 with
| Nil -> _true
| Cons (l2, c2') ->
- (match compare l1 l2 with
- | ExtrNative.Eq -> Cons (l1, (resolve0 c1 c2'))
- | ExtrNative.Lt ->
- if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+ (match compare0 l1 l2 with
+ | 0 -> Cons (l1, (resolve0 c1 c2'))
+ | (-1) ->
+ if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
then coq_or c1 c2'
else Cons (l1, (resolve0 c1 c2))
- | ExtrNative.Gt ->
- if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+ | 1 ->
+ if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
then coq_or c1 c2'
else Cons (l2, (resolve_aux resolve0 l1 c1 c2')))
-
+
(** val resolve : t -> t -> t **)
-
+
let rec resolve c1 c2 =
match c1 with
| Nil -> _true
@@ -279,165 +2439,107 @@ module C =
(match c2 with
| Nil -> _true
| Cons (l2, c2') ->
- (match compare l1 l2 with
- | ExtrNative.Eq -> Cons (l1, (resolve c3 c2'))
- | ExtrNative.Lt ->
- if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+ (match compare0 l1 l2 with
+ | 0 -> Cons (l1, (resolve c3 c2'))
+ | (-1) ->
+ if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
then coq_or c3 c2'
else Cons (l1, (resolve c3 c2))
- | ExtrNative.Gt ->
- if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+ | 1 ->
+ if eqb0 (lxor0 l1 l2) (Uint63.of_int (1))
then coq_or c3 c2'
else Cons (l2, (resolve_aux resolve l1 c3 c2'))))
end
-module S =
- struct
+module S =
+ struct
type t = C.t array
-
- (** val get : t -> int -> C.t **)
-
- let get s cid =
- get s cid
-
- (** val internal_set : t -> int -> C.t -> t **)
-
- let internal_set s cid c =
- set s cid c
-
- (** val make : int -> t **)
-
+
+ (** val get : t -> Uint63.t -> C.t **)
+
+ let get =
+ get
+
+ (** val internal_set : t -> Uint63.t -> C.t -> t **)
+
+ let internal_set =
+ set
+
+ (** val make : Uint63.t -> t **)
+
let make nclauses =
make nclauses C._true
-
- (** val insert : int -> int list -> int list **)
-
- let rec insert l1 c = match c with
+
+ (** val insert_no_simpl : Uint63.t -> Uint63.t list -> Uint63.t list **)
+
+ let rec insert_no_simpl l1 c = match c with
| Nil -> Cons (l1, Nil)
| Cons (l2, c') ->
- (match compare l1 l2 with
- | ExtrNative.Eq -> c
- | ExtrNative.Lt ->
- if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
- then C._true
- else Cons (l1, c)
- | ExtrNative.Gt ->
- if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
- then C._true
- else Cons (l2, (insert l1 c')))
-
- (** val sort_uniq : int list -> int list **)
-
- let rec sort_uniq = function
+ (match compare0 l1 l2 with
+ | 0 -> c
+ | (-1) -> Cons (l1, c)
+ | 1 -> Cons (l2, (insert_no_simpl l1 c')))
+
+ (** val sort : Uint63.t list -> Uint63.t list **)
+
+ let rec sort = function
| Nil -> Nil
- | Cons (l1, c0) -> insert l1 (sort_uniq c0)
-
- (** val set_clause : t -> int -> C.t -> t **)
-
+ | Cons (l1, c0) -> insert_no_simpl l1 (sort c0)
+
+ (** val set_clause : t -> Uint63.t -> C.t -> t **)
+
let set_clause s pos c =
- set s pos (sort_uniq c)
-
- (** val set_resolve : t -> int -> int array -> t **)
-
+ set s pos (sort c)
+
+ (** val set_resolve : t -> Uint63.t -> Uint63.t array -> t **)
+
let set_resolve s pos r =
let len = length r in
- if eqb len (ExtrNative.of_uint(0))
+ if eqb0 len (Uint63.of_int (0))
then s
else let c =
- foldi (fun i c -> C.resolve (get s (Coq__1.get r i)) c)
- (ExtrNative.of_uint(1)) (sub len (ExtrNative.of_uint(1)))
- (get s (Coq__1.get r (ExtrNative.of_uint(0))))
+ foldi (fun i c' -> C.resolve (get s (Coq__1.get r i)) c')
+ (Uint63.of_int (1)) len
+ (get s (Coq__1.get r (Uint63.of_int (0))))
in
internal_set s pos c
end
-(** val afold_left :
- 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a1) -> 'a2 array -> 'a1 **)
-
-let afold_left default oP f v =
- let n = length v in
- if eqb n (ExtrNative.of_uint(0))
- then default
- else foldi (fun i a -> oP a (f (get v i))) (ExtrNative.of_uint(1))
- (sub n (ExtrNative.of_uint(1))) (f (get v (ExtrNative.of_uint(0))))
-
-type 'step _trace_ = 'step array array
+type 'step _trace_ = 'step list * 'step
(** val _checker_ :
- (S.t -> 'a1 -> S.t) -> (C.t -> bool) -> S.t -> 'a1 _trace_ -> int -> bool **)
+ (S.t -> 'a1 -> S.t) -> (C.t -> bool) -> S.t -> 'a1 _trace_ -> Uint63.t ->
+ bool **)
let _checker_ check_step is_false0 s t0 confl =
- let s' = fold_left (fun s0 a -> fold_left check_step s0 a) s t0 in
- is_false0 (S.get s' confl)
+ let s' = fold_left check_step (fst t0) s in is_false0 (S.get s' confl)
-module Sat_Checker =
- struct
+module Sat_Checker =
+ struct
type step =
- | Res of int * int array
-
- (** val step_rect : (int -> int array -> 'a1) -> step -> 'a1 **)
-
- let step_rect f = function
- | Res (x, x0) -> f x x0
-
- (** val step_rec : (int -> int array -> 'a1) -> step -> 'a1 **)
-
- let step_rec f = function
- | Res (x, x0) -> f x x0
-
+ | Res of Uint63.t * Uint63.t array
+
(** val resolution_checker :
- (C.t -> bool) -> S.t -> step _trace_ -> int -> bool **)
-
+ (C.t -> bool) -> S.t -> step _trace_ -> Uint63.t -> bool **)
+
let resolution_checker s t0 =
_checker_ (fun s0 st -> let Res (pos, r) = st in S.set_resolve s0 pos r)
s t0
-
- type dimacs = int array array
-
- (** val coq_C_interp_or : Valuation.t -> int array -> bool **)
-
- let coq_C_interp_or rho c =
- afold_left false (fun b1 b2 -> if b1 then true else b2) (Lit.interp rho)
- c
-
- (** val valid : Valuation.t -> dimacs -> bool **)
-
- let valid rho d =
- afold_left true (fun b1 b2 -> if b1 then b2 else false)
- (coq_C_interp_or rho) d
-
+
+ type dimacs = Uint63.t array array
+
type certif =
- | Certif of int * step _trace_ * int
-
- (** val certif_rect :
- (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1 **)
-
- let certif_rect f = function
- | Certif (x, x0, x1) -> f x x0 x1
-
- (** val certif_rec :
- (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1 **)
-
- let certif_rec f = function
- | Certif (x, x0, x1) -> f x x0 x1
-
+ | Certif of Uint63.t * step _trace_ * Uint63.t
+
(** val add_roots : S.t -> dimacs -> S.t **)
-
+
let add_roots s d =
- foldi_right (fun i c s0 -> S.set_clause s0 i (to_list c)) d s
-
+ foldi (fun i s0 -> S.set_clause s0 i (to_list (get d i)))
+ (Uint63.of_int (0)) (length d) s
+
(** val checker : dimacs -> certif -> bool **)
-
+
let checker d = function
| Certif (nclauses, t0, confl_id) ->
resolution_checker C.is_false (add_roots (S.make nclauses) d) t0 confl_id
-
- (** val interp_var : (int -> bool) -> int -> bool **)
-
- let interp_var rho x =
- match compare x (ExtrNative.of_uint(1)) with
- | ExtrNative.Eq -> false
- | ExtrNative.Lt -> true
- | ExtrNative.Gt -> rho (sub x (ExtrNative.of_uint(1)))
end
-
generated by cgit (git 2.34.1) at 2024-05-09 04:50:28 +0000