diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-01 18:09:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-01 18:32:53 +0200 |
| commit | 5e310fc0456bc5123ab5aef255d61dde6ee8f4d7 (patch) | |
| tree | 2a4600ac5f24ba9bd7a9f8e67828c70c9ece46b9 /kernel/cClosure.ml | |
| parent | 97ee8fbd0bf917c29e47f746c0a28623ebc7da9a (diff) | |
Actually take advantage of the normalization status of kernel closures.
We know that when a fterm is marked as Whnf or Norm, the only thing that can
happen in the reduction machine is administrative reduction pushing the
destructured term on the stack. Thus there is no need to perform any
actual performative reduction.
Furthermore, every head subterm of those terms are recursively Whnf or Norm,
which implies that no update mark is pushed on the stack during the
destructuration. So there is no need to unzip the stack to unset FLOCKED
nodes as well.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 08114abc4..b9d26216b 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1052,7 +1052,12 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k |