From 5e310fc0456bc5123ab5aef255d61dde6ee8f4d7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 May 2018 18:09:57 +0200 Subject: 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. --- kernel/cClosure.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'kernel/cClosure.ml') 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 -- cgit v1.2.3