From f0da709639044eab19ff7d6155ccf99740f9f89a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 2 Apr 2019 13:59:06 +0200
Subject: Fix pretty-printing of primitive integers

A scope delimiter was missing for primitive integers constants.

Add related regression tests.
---
 interp/constrextern.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 24b1362e6d..68791f85aa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -738,6 +738,14 @@ let extern_optimal extern r r' =
   | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
   | _ -> raise No_match
 
+(* Helper function for safe and optimal printing of primitive tokens  *)
+(* such as those for Int63                                            *)
+let extern_prim_token_delimiter_if_required n key_n scope_n scopes =
+  match availability_of_prim_token n scope_n scopes with
+  | Some None -> CPrim n
+  | None -> CDelimiters(key_n, CAst.make (CPrim n))
+  | Some (Some key) -> CDelimiters(key, CAst.make (CPrim n))
+
 (**********************************************************************)
 (* mapping decl                                                       *)
 
@@ -967,8 +975,11 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
              map_cast_type (extern_typ scopes vars) c')
+
   | GInt i ->
-     CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+     extern_prim_token_delimiter_if_required
+       (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+       "int63" "int63_scope" (snd scopes)
 
   in insert_coercion coercion (CAst.make ?loc c)
 
-- 
cgit v1.2.3