diff options
| author | Hugo Herbelin | 2020-05-23 20:41:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 18:08:10 +0100 |
| commit | 05cf3fca1d0800e4cefaed3cb1825a8420ce9f2c (patch) | |
| tree | 90707bc38824c67364a73fa46aa969a9481c0624 /kernel | |
| parent | af96434d2991b9f01f6cd3963ed114b57e40792f (diff) | |
Adding heterogeneous map on named contexts.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/context.ml | 9 | ||||
| -rw-r--r-- | kernel/context.mli | 3 |
2 files changed, 12 insertions, 0 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 6a99f201f3..ab66898b59 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -365,6 +365,15 @@ struct let ty' = f ty in if v == v' && ty == ty' then decl else LocalDef (id, v', ty') + let map_constr_het f = function + | LocalAssum (id, ty) -> + let ty' = f ty in + LocalAssum (id, ty') + | LocalDef (id, v, ty) -> + let v' = f v in + let ty' = f ty in + LocalDef (id, v', ty') + (** Perform a given action on all terms in a given declaration. *) let iter_constr f = function | LocalAssum (_, ty) -> f ty diff --git a/kernel/context.mli b/kernel/context.mli index 76c4461760..29309daf34 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -231,6 +231,9 @@ sig (** Map all terms in a given declaration. *) val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt + (** Map all terms, with an heterogeneous function. *) + val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt + (** Perform a given action on all terms in a given declaration. *) val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit |