← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to plugins/funind/rawtermops.ml

  • Committer: herbelin
  • Date: 2009-11-09 18:05:13 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12485
A bit of cleaning around name generation + creation of dedicated file namegen.ml

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/funind/rawtermops.ml
202
202
    | PatVar(loc,Name id) ->
203
203
        if List.mem id excluded
204
204
        then
205
 
          let new_id = Nameops.next_ident_away id excluded in
 
205
          let new_id = Namegen.next_ident_away id excluded in
206
206
          PatVar(loc,Name new_id),(new_id::excluded),
207
207
        (Idmap.add id new_id Idmap.empty)
208
208
        else pat,excluded,Idmap.empty
210
210
        let new_na,new_excluded,map =
211
211
          match na with
212
212
            | Name id when List.mem id excluded ->
213
 
                let new_id = Nameops.next_ident_away id excluded in
 
213
                let new_id = Namegen.next_ident_away id excluded in
214
214
                Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
215
215
            | _ -> na,excluded,Idmap.empty
216
216
        in
264
264
    match rt with
265
265
      | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
266
266
      | RLambda(loc,Anonymous,k,t,b) ->
267
 
          let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
 
267
          let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in
268
268
          let new_excluded = new_id :: excluded in
269
269
          let new_t = alpha_rt new_excluded t in
270
270
          let new_b = alpha_rt new_excluded b in
278
278
        let new_b = alpha_rt excluded b in
279
279
        RLetIn(loc,Anonymous,new_t,new_b)
280
280
    | RLambda(loc,Name id,k,t,b) ->
281
 
        let new_id = Nameops.next_ident_away id excluded in
 
281
        let new_id = Namegen.next_ident_away id excluded in
282
282
        let t,b =
283
283
          if new_id = id
284
284
          then t,b
291
291
        let new_b = alpha_rt new_excluded b in
292
292
        RLambda(loc,Name new_id,k,new_t,new_b)
293
293
    | RProd(loc,Name id,k,t,b) ->
294
 
        let new_id = Nameops.next_ident_away id excluded in
 
294
        let new_id = Namegen.next_ident_away id excluded in
295
295
        let new_excluded = new_id::excluded in
296
296
        let t,b =
297
297
          if new_id = id
304
304
        let new_b = alpha_rt new_excluded b in
305
305
        RProd(loc,Name new_id,k,new_t,new_b)
306
306
    | RLetIn(loc,Name id,t,b) ->
307
 
        let new_id = Nameops.next_ident_away id excluded in
 
307
        let new_id = Namegen.next_ident_away id excluded in
308
308
        let t,b =
309
309
          if new_id = id
310
310
          then t,b
325
325
               match na with
326
326
                 | Anonymous -> (na::nal,excluded,mapping)
327
327
                 | Name id ->
328
 
                     let new_id = Nameops.next_ident_away id excluded in
 
328
                     let new_id = Namegen.next_ident_away id excluded in
329
329
                     if new_id = id
330
330
                     then
331
331
                       na::nal,id::excluded,mapping