diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean index 6fb31132a8..76f8f877fb 100644 --- a/library/init/lean/ir/extract_cpp.lean +++ b/library/init/lean/ir/extract_cpp.lean @@ -130,7 +130,7 @@ emit op >> paren (emit_var x) /-- Emit `x := y op z` -/ def emit_infix (x y z : var) (op : string) : extract_m unit := -emit_var x >> emit " := " >> emit_var y >> emit op >> emit_var z +emit_var x >> emit " := " >> emit_var y >> emit " " >> emit op >> emit " " >> emit_var z /- Emit `x := big_op(y, z)` -/ def emit_big_binop (x y z : var) (big_op : string) : extract_m unit := @@ -259,7 +259,7 @@ def emit_header (h : header) : extract_m unit := emit_return h.return >> emit " " >> emit_fnid h.n >> paren(emit_arg_list h.args) def decl_local (x : var) (ty : type) : extract_m unit := -emit_var x >> emit_type ty >> emit_eos +emit_type ty >> emit " " >> emit_var x >> emit_eos def decl_locals (args : list arg) : extract_m unit := do env ← read, @@ -278,7 +278,7 @@ do ctx ← monad_lift $ infer_types d env, end cpp def extract_cpp (env : environment) (cpp_names : fnid → option string) (ds : list decl) : except format string := -let out := cpp.file_header in +let out := cpp.file_header ++ "\n" in run (ds.mfor (cpp.emit_decl env cpp_names) >> get) out end ir diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean index 95ed17968b..fd5ac3d9c6 100644 --- a/tests/lean/run/parser_ir1.lean +++ b/tests/lean/run/parser_ir1.lean @@ -1,6 +1,7 @@ import system.io import init.lean.ir.parser init.lean.ir.format import init.lean.ir.elim_phi init.lean.ir.type_check +import init.lean.ir.extract_cpp open lean.parser open lean.ir @@ -62,3 +63,28 @@ main: ret o; " #eval show_result (whitespace >> parse_def) IR3 + +def tst_extract_cpp (s : string) : io unit := +do (except.ok d) ← return $ parse (whitespace >> parse_def) s, + check_decl d, + (except.ok code) ← return $ extract_cpp (λ _, none) (λ _, none) [elim_phi d], + io.print_ln code + +#eval tst_extract_cpp IR3 +#eval tst_extract_cpp IR2 + +def IR4 := " +def swap (d1 : object) (d2 : object) : object object := +main: + r1 := cnstr 0 2 []; + r2 := cnstr 0 2 []; + set r1 0 d1; + set r1 1 d2; + inc d1; + inc d2; + set r2 0 d2; + set r2 1 d1; + ret r1 r2; +" + +#eval tst_extract_cpp IR4