From 560187914e88790cef9787904874df8517aa157c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Oct 2020 12:42:00 +0100
Subject: 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.
---
 kernel/cClosure.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3


From 786f3b7d2d5cfdf3a5643192e5103863a8a04b1c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 26 Oct 2020 12:49:12 +0100
Subject: Yet another normal / neutral bug in primitive conversion.

By no means a float is a neutral value. When put inside a Zprimitive context
it can trigger computation.
---
 kernel/cClosure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 236ce42628..952237ab99 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -1165,7 +1165,7 @@ module FNativeEntries =
 
     let mkFloat env f =
       check_float env;
-      { mark = mark Norm KnownR; term = FFloat f }
+      { mark = mark Cstr KnownR; term = FFloat f }
 
     let mkBool env b =
       check_bool env;
-- 
cgit v1.2.3