diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 62 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 2 |
2 files changed, 64 insertions, 0 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 5c8060996..244f013e3 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -470,6 +470,68 @@ let loc_of_glob_constr = function | GCast (loc,_,_) -> loc (**********************************************************************) +(* Alpha-renaming *) + +let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l +let test_id l id = if collide_id l id then raise Not_found +let test_na l na = name_iter (test_id l) na + +let update_subst na l = + let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in + let l' = name_fold Id.List.remove_assoc na l in + name_fold + (fun id _ -> + if in_range id l' then + let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in + Name id', (id,id')::l + else na,l) + na (na,l) + +let rec rename_glob_vars l = function + | GVar (loc,id) as r -> + (try GVar (loc,Id.List.assoc id l) + with Not_found -> + if List.exists (fun (_,id') -> Id.equal id id') l then raise Not_found + else r) + | GRef (_,VarRef id,_) as r -> + if List.exists (fun (_,id') -> Id.equal id id') l then raise Not_found + else r + | GProd (loc,na,bk,t,c) -> + let na',l' = update_subst na l in + GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLambda (loc,na,bk,t,c) -> + let na',l' = update_subst na l in + GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLetIn (loc,na,b,c) -> + let na',l' = update_subst na l in + GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) + | GCases (loc,ci,po,tomatchl,cls) -> + let test_pred_pat (na,ino) = + test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in + let test_clause idl = List.iter (test_id l) idl in + let po = Option.map (rename_glob_vars l) po in + let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in + let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in + GCases (loc,ci,po,tomatchl,cls) + | GLetTuple (loc,nal,(na,po),c,b) -> + List.iter (test_na l) (na::nal); + GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po), + rename_glob_vars l c,rename_glob_vars l b) + | GIf (loc,c,(na,po),b1,b2) -> + test_na l na; + GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), + rename_glob_vars l b1,rename_glob_vars l b2) + | GRec (loc,k,idl,decls,bs,ts) -> + Array.iter (test_id l) idl; + GRec (loc,k,idl, + Array.map (List.map (fun (na,k,bbd,bty) -> + test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, + Array.map (rename_glob_vars l) bs, + Array.map (rename_glob_vars l) ts) + | r -> map_glob_constr (rename_glob_vars l) r + +(**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) let rec cases_pattern_of_glob_constr na = function diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index c2b27ca6a..dcc6ef88b 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -44,6 +44,8 @@ val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t val glob_visible_short_qualid : glob_constr -> Id.t list +val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr + (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. It is used to |