Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).

Reasoning modulo variable aliases induced an extra lookup in the
environment at each inversion of the components of the evar instances:
precomputing the aliases map allowed to gain a factor n.
Moreover, solve_evar_evar_l2r was recomputing the evar substitution
from the evar instance n more times than needed.
Function solve_evar_evar_l2r is still on O(n^2) but it does not seem
to be used so often actually. The trivial case has been optimized
(linear time) but the general case could probably be also cut down to
O(n*log(n)) if needed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 258 insertions, 93 deletions

diff --git a/lib/util.ml b/lib/util.ml
index ba3d2c6d2..f3b7c99e9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1109,6 +1109,11 @@ let array_union_map f a acc =
     acc
     a
 
+let array_rev_to_list a =
+  let rec tolist i res =
+    if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
+  tolist 0 []
+
 (* Matrices *)
 
 let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index f900e9bf7..80f2fda38 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -253,6 +253,7 @@ val array_fold_map2' :
   ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
 val array_distinct : 'a array -> bool
 val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
+val array_rev_to_list : 'a array -> 'a list
 
 (*s Matrices *)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a33c81b09..3b20b82df 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -182,6 +182,79 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter insta
   let evd = evar_declare sign newevk typ ~src:src ?filter evd in
   (evd,mkEvar (newevk,Array.of_list instance))
 
+(* Expand rels and vars that are bound to other rels or vars so that
+   dependencies in variables are canonically associated to the most ancient
+   variable in its family of aliased variables *)
+
+let compute_aliases sign =
+  List.fold_right (fun (id,b,c) aliases ->
+    match b with
+    | Some t ->
+	(match kind_of_term t with
+	| Var id' ->
+	    let id'' = try Idmap.find id' aliases with Not_found -> id' in
+	    Idmap.add id id'' aliases
+	| _ -> aliases)
+    | None -> aliases) sign Idmap.empty
+
+let alias_of_var id aliases = try Idmap.find id aliases with Not_found -> id
+
+let make_alias_map env =
+  let var_aliases = compute_aliases (named_context env) in
+  let rels = rel_context env in
+  let rel_aliases = 
+    snd (List.fold_right (fun (_,b,t) (n,aliases) ->
+      (n-1,
+      match b with
+	| Some t when isRel t or isVar t -> Intmap.add n (lift n t) aliases
+	| _ -> aliases)) rels (List.length rels,Intmap.empty)) in
+  (var_aliases,rel_aliases)
+
+let expand_var_once aliases x = match kind_of_term x with
+  | Rel n -> Intmap.find n (snd aliases)
+  | Var id -> mkVar (Idmap.find id (fst aliases))
+  | _ -> raise Not_found
+
+let rec expand_var_at_least_once aliases x =
+  let t = expand_var_once aliases x in
+  try expand_var_at_least_once aliases t
+  with Not_found -> t
+
+let expand_var aliases x =
+  try expand_var_at_least_once aliases x with Not_found -> x
+
+let expand_var_opt aliases x =
+  try Some (expand_var_at_least_once aliases x) with Not_found -> None
+
+let extend_alias (_,b,_) (var_aliases,rel_aliases) =
+  let rel_aliases =
+    Intmap.fold (fun n c -> Intmap.add (n+1) (lift 1 c))
+      rel_aliases Intmap.empty in
+  let rel_aliases =
+    match b with
+    | Some t when isRel t or isVar t -> Intmap.add 1 (lift 1 t) rel_aliases
+    | _ -> rel_aliases in
+  (var_aliases, rel_aliases)
+
+let rec expand_vars_in_term_using aliases t = match kind_of_term t with
+  | Rel _ | Var _ ->
+      expand_var aliases t
+  | _ ->
+      map_constr_with_full_binders
+	extend_alias expand_vars_in_term_using aliases t
+
+let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
+
+let rec expansions_of_var aliases x =
+  try
+    let t = expand_var_once aliases x in
+    t :: expansions_of_var aliases t
+  with Not_found ->
+    [x]
+
+let expand_full_opt aliases y =
+  try Some (expand_var aliases y) with Not_found -> None
+
 (* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
  * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
  * If a variable and an alias of it are bound to the same instance, we skip
@@ -192,20 +265,28 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter insta
  * useful to ensure the uniqueness of a projection.
 *)
 
-let make_projectable_subst sigma evi args =
+let make_projectable_subst aliases sigma evi args =
   let sign = evar_filtered_context evi in
-  let rec alias_of_var id =
-    match pi2 (Sign.lookup_named id sign) with
-    | Some t when isVar t -> alias_of_var (destVar t)
-    | _ -> id in
+  let evar_aliases = compute_aliases sign in
   snd (List.fold_right
     (fun (id,b,c) (args,l) ->
       match b,args with
-	| Some c, a::rest when
-	    isVar c & (try eq_constr a (snd (List.assoc (destVar c) l)) with Not_found -> false) -> (rest,l)
-	| _, a::rest -> (rest, (id, (alias_of_var id,whd_evar sigma a))::l)
+	| None, a::rest ->
+	    let a = whd_evar sigma a in
+	    (rest,Idmap.add id [a,expand_full_opt aliases a,id] l)
+	| Some c, a::rest ->
+	    let a = whd_evar sigma a in
+	    (match kind_of_term c with
+	    | Var id ->
+		let idc = alias_of_var id evar_aliases in
+		let sub = try Idmap.find idc l with Not_found -> [] in
+		if List.exists (fun (c,_,_) -> eq_constr a c) sub then (rest,l)
+		else
+		  (rest,Idmap.add idc ((a,expand_full_opt aliases c,id)::sub) l)
+	    | _ ->
+		(rest,Idmap.add id [a,expand_full_opt aliases a,id] l))
 	| _ -> anomaly "Instance does not match its signature")
-    sign (List.rev (Array.to_list args),[]))
+    sign (array_rev_to_list args,Idmap.empty))
 
 let make_pure_subst evi args =
   snd (List.fold_right
@@ -213,7 +294,7 @@ let make_pure_subst evi args =
       match args with
 	| a::rest -> (rest, (id,a)::l)
 	| _ -> anomaly "Instance does not match its signature")
-    (evar_filtered_context evi) (List.rev (Array.to_list args),[]))
+    (evar_filtered_context evi) (array_rev_to_list args,[]))
 
 (* [push_rel_context_to_named_context] builds the defining context and the
  * initial instance of an evar. If the evar is to be used in context
@@ -235,9 +316,10 @@ let make_pure_subst evi args =
  * Remark 2: If some of the ai or xj are definitions, we keep them in the
  *   instance. This is necessary so that no unfolding of local definitions
  *   happens when inferring implicit arguments (consider e.g. the problem
- *   "x:nat; x':=x; f:forall x, x=x -> Prop |- f _ (refl_equal x')"
- *   we want the hole to be instantiated by x', not by x (which would have the
- *   case in [invert_instance] if x' had disappear of the instance).
+ *   "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
+ *   produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
+ *   the hole to be instantiated by x', not by x (which would have been
+ *   the case in [invert_definition] if x' had disappeared from the instance).
  *   Note that at any time, if, in some context env, the instance of
  *   declaration x:A is t and the instance of definition x':=phi(x) is u, then
  *   we have the property that u and phi(t) are convertible in env.
@@ -490,46 +572,6 @@ let clear_hyps_in_evi evdref hyps concl ids =
   (nhyps,nconcl)
 
 
-(* Expand rels and vars that are bound to other rels or vars so that
-   dependencies in variables are canonically associated to the most ancient
-   variable in its family of aliased variables *)
-
-let expand_var_once env x = match kind_of_term x with
-  | Rel n ->
-      begin match pi2 (lookup_rel n env) with
-      | Some t when isRel t or isVar t -> lift n t
-      | _ -> raise Not_found
-      end
-  | Var id ->
-      begin match pi2 (lookup_named id env) with
-      | Some t when isVar t -> t
-      | _ -> raise Not_found
-      end
-  | _ ->
-      raise Not_found
-
-let rec expand_var_at_least_once env x =
-  let t = expand_var_once env x in
-  try expand_var_at_least_once env t
-  with Not_found -> t
-
-let expand_var env x =
-  try expand_var_at_least_once env x with Not_found -> x
-
-let expand_var_opt env x =
-  try Some (expand_var_at_least_once env x) with Not_found -> None
-
-let rec expand_vars_in_term env t = match kind_of_term t with
-  | Rel _ | Var _ -> expand_var env t
-  | _ -> map_constr_with_full_binders push_rel expand_vars_in_term env t
-
-let rec expansions_of_var env x =
-  try
-    let t = expand_var_once env x in
-    t :: expansions_of_var env t
-  with Not_found ->
-    [x]
-
 (* [find_projectable_vars env sigma y subst] finds all vars of [subst]
  * that project on [y]. It is able to find solutions to the following
  * two kinds of problems:
@@ -569,24 +611,38 @@ type evar_projection =
 | ProjectVar
 | ProjectEvar of existential * evar_info * identifier * evar_projection
 
-let rec find_projectable_vars with_evars env sigma y subst =
-  let is_projectable (id,(idc,y')) =
-    let y' = whd_evar sigma y' in
-    if y = y' or expand_var env y = expand_var env y'
-    then (idc,(y'=y,(id,ProjectVar)))
-    else if with_evars & isEvar y' then
-      let (evk,argsv as t) = destEvar y' in
-      let evi = Evd.find sigma evk in
-      let subst = make_projectable_subst sigma evi argsv in
-      let l = find_projectable_vars with_evars env sigma y subst in
-      match l with
-      | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p))))
-      | _ -> failwith ""
-    else failwith "" in
-  let l = map_succeed is_projectable subst in
-  let l = list_partition_by (fun (idc,_) (idc',_) -> idc = idc') l in
-  let l = List.map (List.map snd) l in
-  List.map (fun l -> try List.assoc true l with Not_found -> snd (List.hd l)) l
+let rec assoc_up_to_alias y yc = function
+  | (c,_,id)::l when y = c -> id
+  | (c,Some cc,id)::l when yc = cc -> id
+  | _::l -> assoc_up_to_alias y yc l
+  | [] -> raise Not_found
+
+let rec find_projectable_vars with_evars aliases sigma y subst =
+  let yc = expand_var aliases y in
+  let is_projectable idc idcl subst' =
+    (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
+    try let id = assoc_up_to_alias y yc idcl in (id,ProjectVar)::subst'
+    with Not_found ->
+    (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
+    (* projectable on [y] *)
+      if with_evars then
+	let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+	match idcl' with
+	| [c,_,id] ->
+	  begin
+	    let (evk,argsv as t) = destEvar c in
+	    let evi = Evd.find sigma evk in
+	    let subst = make_projectable_subst aliases sigma evi argsv in
+	    let l = find_projectable_vars with_evars aliases sigma y subst in
+	    match l with
+	    | [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst'
+	    | _ -> subst'
+	  end
+	| [] -> subst'
+	| _ -> anomaly "More than one non var in aliases class of evar instance"
+      else
+	subst' in
+  Idmap.fold is_projectable subst []
 
 (* [filter_solution] checks if one and only one possible projection exists
  * among a set of solutions to a projection problem *)
@@ -596,8 +652,9 @@ let filter_solution = function
   | (id,p)::_::_ -> raise NotUnique
   | [id,p] -> (mkVar id, p)
 
-let project_with_effects env sigma effects t subst =
-  let c, p = filter_solution (find_projectable_vars false env sigma t subst) in
+let project_with_effects aliases sigma effects t subst =
+  let c, p =
+    filter_solution (find_projectable_vars false aliases sigma t subst) in
   effects := p :: !effects;
   c
 
@@ -636,7 +693,7 @@ let rec do_projection_effects define_fun env ty evd = function
       else
 	evd
 
-(* Assuming Σ; Γ, y1..yk |- c, [invert_subst Γ k Σ [x1:=u1;...;xn:=un] c]
+(* Assuming Σ; Γ, y1..yk |- c, [invert_arg_from_subst Γ k Σ [x1:=u1..xn:=un] c]
  * tries to return φ(x1..xn) such that equation φ(u1..un) = c is valid.
  * The strategy is to imitate the structure of c and then to invert
  * the variables of c (i.e. rels or vars of Γ) using the algorithm
@@ -650,10 +707,10 @@ let rec do_projection_effects define_fun env ty evd = function
  *
  * The effects correspond to evars instantiated while trying to project.
  *
- * [invert_subst] is used on instances of evars. Since the evars are flexible,
- * these instances are potentially erasable. This is why we don't investigate
- * whether evars in the instances of evars are unifiable, to the contrary of
- * [invert_definition].
+ * [invert_arg_from_subst] is used on instances of evars. Since the
+ * evars are flexible, these instances are potentially erasable. This
+ * is why we don't investigate whether evars in the instances of evars
+ * are unifiable, to the contrary of [invert_definition].
  *)
 
 type projectibility_kind =
@@ -664,15 +721,15 @@ type projectibility_status =
   | CannotInvert
   | Invertible of projectibility_kind
 
-let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders =
+let invert_arg_from_subst aliases k sigma subst_in_env c_in_env_extended_with_k_binders =
   let effects = ref [] in
   let rec aux k t =
     let t = whd_evar sigma t in
     match kind_of_term t with
     | Rel i when i>k ->
-	project_with_effects env sigma effects (mkRel (i-k)) subst_in_env
+	project_with_effects aliases sigma effects (mkRel (i-k)) subst_in_env
     | Var id ->
-	project_with_effects env sigma effects t subst_in_env
+	project_with_effects aliases sigma effects t subst_in_env
     | _ ->
 	map_constr_with_binders succ aux k t in
   try
@@ -682,9 +739,8 @@ let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_bind
     | Not_found -> CannotInvert
     | NotUnique -> Invertible NoUniqueProjection
 
-let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
-  let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
-  let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
+let invert_arg aliases k sigma evk subst_in_env c_in_env_extended_with_k_binders =
+  let res = invert_arg_from_subst aliases k sigma subst_in_env c_in_env_extended_with_k_binders in
   match res with
   | Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
   | _ -> res
@@ -798,10 +854,33 @@ let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) =
  * Note: argument f is the function used to instantiate evars.
  *)
 
+let are_canonical_instances args1 args2 env =
+  let n1 = Array.length args1 in
+  let n2 = Array.length args2 in
+  let rec aux n = function
+    | (id,_,c)::sign
+	when n < n1 && args1.(n) = mkVar id && args1.(n) = args2.(n) ->
+	aux (n+1) sign
+    | [] ->
+	let rec aux2 n =
+	  n = n1 ||
+	  (args1.(n) = mkRel (n1-n) && args2.(n) = mkRel (n1-n) && aux2 (n+1))
+	in aux2 n
+    | _ -> false in
+  n1 = n2 & aux 0 (named_context env)
+
 exception CannotProject of projectibility_status list
 
-let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,_ as ev2) =
-  let proj1 = array_map_to_list (invert_arg env 0 evd ev2) args1 in
+let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,args2 as ev2) =
+  let aliases = make_alias_map env in
+  let subst = make_projectable_subst aliases evd (Evd.find evd evk2) args2 in
+  if are_canonical_instances args1 args2 env then
+    (* If instances are canonical, we solve the problem in linear time *)
+    let sign = evar_filtered_context (Evd.find evd evk2) in
+    let subst = List.map (fun (id,_,_) -> mkVar id) sign in
+    Evd.define evk2 (mkEvar(evk1,Array.of_list subst)) evd
+  else
+  let proj1 = array_map_to_list (invert_arg aliases 0 evd evk2 subst) args1 in
   try
     (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *)
     let proj1' = effective_projections proj1 in
@@ -846,16 +925,17 @@ exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress
 
 let rec invert_definition choose env evd (evk,argsv as ev) rhs =
+  let aliases = make_alias_map env in
   let evdref = ref evd in
   let progress = ref false in
   let evi = Evd.find evd evk in
-  let subst = make_projectable_subst evd evi argsv in
+  let subst = make_projectable_subst aliases evd evi argsv in
 
   (* Projection *)
   let project_variable t =
     (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
     try
-      let sols = find_projectable_vars true env !evdref t subst in
+      let sols = find_projectable_vars true aliases !evdref t subst in
       let c, p = match sols with
 	| [] -> raise Not_found
 	| [id,p] -> (mkVar id, p)
@@ -872,7 +952,7 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
       | NotUniqueInType ty ->
 	  if not !progress then raise NotEnoughInformationToProgress;
 	  (* No unique projection but still restrict to where it is possible *)
-	  let ts = expansions_of_var env t in
+	  let ts = expansions_of_var aliases t in
 	  let test c = isEvar c or List.mem c ts in
 	  let filter = array_map_to_list test argsv in
 	  let args' = filter_along (fun x -> x) filter argsv in
@@ -893,7 +973,7 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs =
 	(* Evar/Evar problem (but left evar is virtual) *)
 	let projs' =
 	  array_map_to_list
-	    (invert_arg_from_subst env k !evdref subst) args'
+	    (invert_arg_from_subst aliases k !evdref subst) args'
 	in
 	(try
 	  (* Try to project (a restriction of) the right evar *)
@@ -1033,8 +1113,9 @@ let rec expand_and_check_vars env = function
 let is_unification_pattern_evar env (_,args) l t =
   List.for_all (fun x -> isRel x || isVar x) l (* common failure case *)
   &&
+    let aliases = make_alias_map env in
     let l' = Array.to_list args @ l in
-    let l'' = try Some (expand_and_check_vars env l') with Exit -> None in
+    let l'' = try Some (expand_and_check_vars aliases l') with Exit -> None in
     match l'' with
     | Some l ->
 	let deps =
@@ -1043,7 +1124,7 @@ let is_unification_pattern_evar env (_,args) l t =
 	    l
 	  else
 	    (* Probably strong restrictions coming from t being evar-closed *)
-	    let t = expand_vars_in_term env t in
+	    let t = expand_vars_in_term_using aliases t in
 	    let fv_rels = free_rels t in
 	    let fv_ids = global_vars env t in
 	    List.filter (fun c ->
@@ -1071,7 +1152,7 @@ let is_unification_pattern (env,nb) f l t =
    dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
    return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
 let solve_pattern_eqn env l1 c =
-  let l1 = List.map (expand_var env) l1 in
+  let l1 = List.map (expand_var (make_alias_map env)) l1 in
   let c' = List.fold_right (fun a c ->
     let c' = subst_term (lift 1 a) (lift 1 c) in
     match kind_of_term a with
diff --git a/test-suite/complexity/evar_instance.v b/test-suite/complexity/evar_instance.v
new file mode 100644
index 000000000..97a66c95c
--- /dev/null
+++ b/test-suite/complexity/evar_instance.v
@@ -0,0 +1,78 @@
+(* Checks behavior of unification with respect to the size of evar instances *)
+(* Expected time < 2.00s *)
+
+(* Note that the exact example chosen is not important as soon as it
+   involves a few of each part of the unification algorithme (and especially
+   evar-evar unification and evar-term instantiation) *)
+
+(* In 8.2, the example was in O(n^3) in the number of section variables; 
+   From current commit it is in O(n^2) *)
+
+(* For the record: with coqtop.byte on a Dual Core 2:
+
+   Nb of extra           T  i  m  e
+    variables     8.1    8.2    8.3beta   current
+       800       1.6s   188s    185s      1.6s
+       400       0.5s    24s     24s      0.43s
+       200       0.17s    3s      3.2s    0.12s
+       100       0.06s    0.5s    0.48s   0.04s
+        50       0.02s    0.08s   0.08s   0.016s
+         n      12*a*n^2  a*n^3   a*n^3   8*a*n^2
+*)
+
+Set Implicit Arguments.
+Parameter t:Set->Set.
+Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'.
+Parameter avl: forall elt : Set, t elt -> Prop.
+Parameter bst: forall elt : Set, t elt -> Prop.
+Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   avl m -> avl (map f m).
+Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   bst m -> bst (map f m).
+Record bbst (elt:Set) : Set :=
+  Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}.
+Definition t' := bbst.
+Section B.
+
+Variables
+ a b c d e f g h i j k m n o p q r s u v w x y z
+ a0 b0 c0 d0 e0 f0 g0 h0 i0 j0 k0 m0 n0 o0 p0 q0 r0 s0 u0 v0 w0 x0 y0 z0
+ a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 k1 m1 n1 o1 p1 q1 r1 s1 u1 v1 w1 x1 y1 z1
+ a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 k2 m2 n2 o2 p2 q2 r2 s2 u2 v2 w2 x2 y2 z2
+ a3 b3 c3 d3 e3 f3 g3 h3 i3 j3 k3 m3 n3 o3 p3 q3 r3 s3 u3 v3 w3 x3 y3 z3
+ a4 b4 c4 d4 e4 f4 g4 h4 i4 j4 k4 m4 n4 o4 p4 q4 r4 s4 u4 v4 w4 x4 y4 z4
+ a5 b5 c5 d5 e5 f5 g5 h5 i5 j5 k5 m5 n5 o5 p5 q5 r5 s5 u5 v5 w5 x5 y5 z5
+ a6 b6 c6 d6 e6 f6 g6 h6 i6 j6 k6 m6 n6 o6 p6 q6 r6 s6 u6 v6 w6 x6 y6 z6
+
+ a7 b7 c7 d7 e7 f7 g7 h7 i7 j7 k7 m7 n7 o7 p7 q7 r7 s7 u7 v7 w7 x7 y7 z7
+ a8 b8 c8 d8 e8 f8 g8 h8 i8 j8 k8 m8 n8 o8 p8 q8 r8 s8 u8 v8 w8 x8 y8 z8
+ a9 b9 c9 d9 e9 f9 g9 h9 i9 j9 k9 m9 n9 o9 p9 q9 r9 s9 u9 v9 w9 x9 y9 z9
+ aA bA cA dA eA fA gA hA iA jA kA mA nA oA pA qA rA sA uA vA wA xA yA zA
+ aB bB cB dB eB fB gB hB iB jB kB mB nB oB pB qB rB sB uB vB wB xB yB zB
+ aC bC cC dC eC fC gC hC iC jC kC mC nC oC pC qC rC sC uC vC wC xC yC zC
+ aD bD cD dD eD fD gD hD iD jD kD mD nD oD pD qD rD sD uD vD wD xD yD zD
+ aE bE cE dE eE fE gE hE iE jE kE mE nE oE pE qE rE sE uE vE wE xE yE zE
+
+ aF bF cF dF eF fF gF hF iF jF kF mF nF oF pF qF rF sF uF vF wF xF yF zF
+ aG bG cG dG eG fG gG hG iG jG kG mG nG oG pG qG rG sG uG vG wG xG yG zG
+ aH bH cH dH eH fH gH hH iH jH kH mH nH oH pH qH rH sH uH vH wH xH yH zH
+ aI bI cI dI eI fI gI hI iI jI kI mI nI oI pI qI rI sI uI vI wI xI yI zI
+ aJ bJ cJ dJ eJ fJ gJ hJ iJ jJ kJ mJ nJ oJ pJ qJ rJ sJ uJ vJ wJ xJ yJ zJ
+ aK bK cK dK eK fK gK hK iK jK kK mK nK oK pK qK rK sK uK vK wK xK yK zK
+ aL bL cL dL eL fL gL hL iL jL kL mL nL oL pL qL rL sL uL vL wL xL yL zL
+ aM bM cM dM eM fM gM hM iM jM kM mM nM oM pM qM rM sM uM vM wM xM yM zM
+
+ aN bN cN dN eN fN gN hN iN jN kN mN nN oN pN qN rN sN uN vN wN xN yN zN
+ aO bO cO dO eO fO gO hO iO jO kO mO nO oO pO qO rO sO uO vO wO xO yO zO
+ aP bP cP dP eP fP gP hP iP jP kP mP nP oP pP qP rP sP uP vP wP xP yP zP
+ aQ bQ cQ dQ eQ fQ gQ hQ iQ jQ kQ mQ nQ oQ pQ qQ rQ sQ uQ vQ wQ xQ yQ zQ
+ aR bR cR dR eR fR gR hR iR jR kR mR nR oR pR qR rR sR uR vR wR xR yR zR
+ aS bS cS dS eS fS gS hS iS jS kS mS nS oS pS qS rS sS uS vS wS xS yS zS
+ aT bT cT dT eT fT gT hT iT jT kT mT nT oT pT qT rT sT uT vT wT xT yT zT
+ aU bU cU dU eU fU gU hU iU jU kU mU nU oU pU qU rU sU uU vU wU xU yU zU
+
+ : nat .
+
+Variables elt elt': Set.
+Timeout 5 Time Definition map' f (m:t' elt) : t' elt' :=
+  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).