diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-09 21:47:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-28 16:51:21 +0200 |
| commit | d28304f6ba18ad9527a63cd01b39a5ad27526845 (patch) | |
| tree | ddd8c5d10f0d1e52c675e8e027053fac7f05f259 /vernac/auto_ind_decl.ml | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
Efficient fresh name generation relying on sets.
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 59920742d..503508fc0 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -533,7 +533,7 @@ open Namegen let compute_bl_goal ind lnamesparrec nparrec = let eqI, eff = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -578,7 +578,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) in let fresh_id s gl = - let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in + let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in Proofview.Goal.enter begin fun gl -> @@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let eqI, eff = eqI ind lnamesparrec in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and @@ -722,7 +722,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = ( List.map (fun (_,_,_,slb) -> slb) list_id ) in let fresh_id s gl = - let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in + let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in Proofview.Goal.enter begin fun gl -> @@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -870,7 +870,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ( List.map (fun (_,_,_,slb) -> slb) list_id ) in let fresh_id s gl = - let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in + let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in Proofview.Goal.enter begin fun gl -> |