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): minor fixes

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-10 10:49:51 -07:00
parent 3ce96ae323
commit aba3d08372
2 changed files with 29 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

26
tests/lean/run/parser_ir1.lean
View file

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