From 31ce1a23e798d45e5475aa33f3906e36f7d7cedc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 May 2018 11:12:49 -0700
Subject: [PATCH] fix(library/init/lean/ir/extract_cpp): add support for bignum
 literals

---
 library/init/lean/ir/extract_cpp.lean | 12 ++++++++++--
 tests/lean/run/lirc1.lean             |  4 +++-
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index 89cbaee0bb..c6de321a7c 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -11,7 +11,8 @@ namespace lean
 namespace ir
 namespace cpp
 def file_header :=
-"#include <lean_obj.h>
+"#include <util/lean_obj.h>
+#include <util/apply.h>
 typedef lean::lean_obj obj;"
 
 structure extract_env :=
@@ -215,7 +216,14 @@ match l with
 | literal.bool ff := emit_var x >> emit " = false"
 | literal.str s   := emit_var x >> emit " = lean::mk_string" >> paren(emit (repr s))
 | literal.float v := emit_var x >> emit " = " >> emit v
-| literal.num v   := emit_var x >> emit " = " >> emit v >> emit_num_suffix t
+| literal.num v   :=
+  match t with
+  | type.object := do
+    emit_var x >> emit " = lean::alloc_mpz(lean::mpz(",
+    if v < uint32_sz then emit v >> emit "u"
+    else emit "\"" >> emit v >> emit "\"",
+    emit "))"
+  | _           := emit_var x >> emit " = " >> emit v >> emit_num_suffix t
 
 def unins2cpp : unins → string
 | unins.inc            := "lean::inc_ref"
diff --git a/tests/lean/run/lirc1.lean b/tests/lean/run/lirc1.lean
index b8c7d534aa..629851840a 100644
--- a/tests/lean/run/lirc1.lean
+++ b/tests/lean/run/lirc1.lean
@@ -8,7 +8,7 @@ match lirc s with
 | except.error e := io.print "Error: " >> io.print e
 
 def PRG1 := "
-[lean::mk_pair] external foo (a : object) (b : object) : object
+[make_my_pair] external foo (a : object) (b : object) : object
 
 def bla (g : object) (a : object) (z : uint32) : object :=
 main:
@@ -22,6 +22,8 @@ main:
   z' : uint32 := add z one;
   h := closure foo a;
   h' := closure f a a a;
+  n : object := 1000;
+  n' : object := 10000000000000000000;
   set r 0 a';
   set r 1 d;
   ret r;