diff options
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 267 | ||||
| -rw-r--r-- | test-suite/complexity/evar_instance.v | 78 |
4 files changed, 258 insertions, 93 deletions
diff --git a/lib/util.ml b/lib/util.ml index ba3d2c6d28..f3b7c99e90 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 f900e9bf71..80f2fda380 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 a33c81b097..3b20b82df1 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 0000000000..97a66c95c2 --- /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)). |