aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r--kernel/nativelambda.ml17
1 files changed, 15 insertions, 2 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 29b3e59da..dfe9d025e 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -83,9 +83,9 @@ let get_const_prefix env c =
(* A generic map function *)
-let map_lam_with_binders g f n lam =
+let rec map_lam_with_binders g f n lam =
match lam with
- | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
+ | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _
| Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam
| Lprod(dom,codom) ->
let dom' = f n dom in
@@ -134,6 +134,19 @@ let map_lam_with_binders g f n lam =
| Lmakeblock(prefix,cn,tag,args) ->
let args' = Array.smartmap (f n) args in
if args == args' then lam else Lmakeblock(prefix,cn,tag,args')
+ | Luint u ->
+ let u' = map_uint g f n u in
+ if u == u' then lam else Luint u'
+
+and map_uint g f n u =
+ match u with
+ | UintVal _ -> u
+ | UintDigits(prefix,c,args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then u else UintDigits(prefix,c,args')
+ | UintDecomp(prefix,c,a) ->
+ let a' = f n a in
+ if a == a' then u else UintDecomp(prefix,c,a')
(*s Lift and substitution *)