diff options
| author | Pierre-Marie Pédrot | 2020-10-26 12:42:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-26 12:51:12 +0100 |
| commit | 560187914e88790cef9787904874df8517aa157c (patch) | |
| tree | 73ec1001ef3b5867a59e85aa9566f044d2f8aa80 /kernel/cClosure.ml | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Fix bug in conversion of primitive values.
A partially applied primitive was considered CClosure.Norm, i.e. neutral. But
this is not true, because substituting this term as the head of an application
may trigger further reduction. In this respect, primitive functions behave like
fixpoints.
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index a23ef8fdca..236ce42628 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1328,10 +1328,14 @@ let rec knr info tab m stk = | FFlex(ConstKey (kn,_u as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with | Def v -> kni info tab v stk - | Primitive op when check_native_args op stk -> - let rargs, a, nargs, stk = get_native_args1 op c stk in - kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) - | Undef _ | OpaqueDef _ | Primitive _ -> (set_norm m; (m,stk))) + | Primitive op -> + if check_native_args op stk then + let rargs, a, nargs, stk = get_native_args1 op c stk in + kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) + else + (* Similarly to fix, partially applied primitives are not Norm! *) + (m, stk) + | Undef _ | OpaqueDef _ -> (set_norm m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info tab (VarKey id) with | Def v -> kni info tab v stk |