From 2e0629133f6eae42977642e53106f1a3055c99eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 May 2018 18:29:54 -0700 Subject: [PATCH] feat(library/init/lean/ir): add emit_lit --- library/init/lean/ir/extract_cpp.lean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index 7a195f8038..06f6be4a3e 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/library/init/lean/ir/extract_cpp.lean @@ -175,8 +175,19 @@ match op with | unop.unbox := emit_x_op_y x "lean::unbox" y | unop.cast := emit_var x >> emit " := static_cast<" >> emit_type t >> emit ">(" >> emit_var y >> emit ")" +def emit_num_suffix : type → extract_m unit +| type.uint32 := emit "u" +| type.uint64 := emit "ull" +| type.int64 := emit "ll" +| _ := return () + def emit_lit (x : var) (t : type) (l : literal) : extract_m unit := -return () -- TODO +match l with +| literal.bool tt := emit_var x >> emit " := true" +| literal.bool ff := emit_var x >> emit " := false" +| literal.str s := emit_var x >> emit " := lean::mk_string(" >> emit (repr s) >> emit ")" +| literal.float v := emit_var x >> emit " := " >> emit v +| literal.num v := emit_var x >> emit " := " >> emit v >> emit_num_suffix t def emit_instr (ins : instr) : extract_m unit := ins.decorate_error $