diff options
author | 2018-02-24 09:33:03 +0100 | |
---|---|---|
committer | 2018-02-24 09:33:03 +0100 | |
commit | bd41af496fd09d6ecd965190cad2873f1cd6b029 (patch) | |
tree | 029c44d509cdaba200db07dfed61adb55b237f9e /kernel/nativelambda.ml | |
parent | c4aeaa7aedb04bf156a4946b05bad8f66d5eec69 (diff) | |
parent | 557c5a2938f16c0601f5a0323c66b78d2da01ee9 (diff) |
Merge PR #6784: New IR in VM: Clambda
Diffstat (limited to 'kernel/nativelambda.ml')
-rw-r--r-- | kernel/nativelambda.ml | 17 |
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 *) |