max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/ir/extract_cpp): add support for bignum literals

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-14 11:12:49 -07:00
parent 095d100a38
commit 31ce1a23e7
2 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/lean/ir/extract_cpp.lean
View file

@ -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"

4
tests/lean/run/lirc1.lean
View file

@ -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;