From 0f2a8f09c208f4b435feb4d31bd8ce082a6b0284 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 May 2018 12:09:04 -0700
Subject: [PATCH] chore(library/init/lean/ir): cleanup

---
 library/init/lean/ir/extract_cpp.lean |  2 +-
 library/init/lean/ir/ir.lean          |  3 +++
 library/init/lean/ir/lirc.lean        | 14 +++++++++-----
 tests/ir/lirc.lean                    |  2 +-
 tests/lean/run/parser_ir1.lean        |  2 +-
 5 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index 43b45c4142..eeb6b68e42 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -27,7 +27,7 @@ structure extract_cpp_config :=
 (runtime_dir : string := "runtime")
 (env : environment := λ _, none)
 (external_names : fnid → option string := λ _, none)
-(main_proc : option fnid := some (mk_simple_name "main"))
+(main_proc : option fnid := none)
 
 namespace cpp
 def file_header (runtime_dir : string) :=
diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean
index 1811f236d6..2aaceed68e 100644
--- a/library/init/lean/ir/ir.lean
+++ b/library/init/lean/ir/ir.lean
@@ -126,6 +126,9 @@ def var     := name
 def fnid    := name
 def blockid := name
 
+instance : has_coe string fnid :=
+⟨mk_simple_name⟩
+
 -- TODO: move collection declarations to another file
 instance var_has_lt : has_lt var := (name.has_lt_quick : has_lt name)
 instance blockid_has_lt : has_lt blockid := (name.has_lt_quick : has_lt name)
diff --git a/library/init/lean/ir/lirc.lean b/library/init/lean/ir/lirc.lean
index f93c07c35d..639af8a572 100644
--- a/library/init/lean/ir/lirc.lean
+++ b/library/init/lean/ir/lirc.lean
@@ -37,15 +37,19 @@ d.valid_ssa >> check_blockids d >> type_check d env >> return ()
 
 local attribute [instance] name.has_lt_quick
 
-def mk_env (ds : list decl) : environment :=
+def update_env (ds : list decl) (env : environment) : environment :=
 let m := ds.foldl (λ m d, rbmap.insert m d.name d) (mk_rbmap name decl (<)) in
-λ n, m.find n
+λ n, m.find n <|> env n
 
-def lirc (s : string) (unit_name := "main") (unit_deps : list string := []) : except format string :=
+def update_external_names (m : fnid2string) (external_names : fnid → option string) : fnid → option string :=
+λ n, m.find n <|> external_names n
+
+def lirc (s : string) (cfg : extract_cpp_config) : except format string :=
 do (ds, m) ← parse_input s,
-   let env := mk_env ds,
+   let env := update_env ds cfg.env,
+   let ext := update_external_names m cfg.external_names,
    ds.mfor (check env),
-   extract_cpp ds { env := env, external_names := m.find, unit_name := unit_name, unit_deps := unit_deps }
+   extract_cpp ds { env := env, external_names := ext, ..cfg }
 
 end ir
 end lean
diff --git a/tests/ir/lirc.lean b/tests/ir/lirc.lean
index 1428b0435c..199791b367 100644
--- a/tests/ir/lirc.lean
+++ b/tests/ir/lirc.lean
@@ -8,6 +8,6 @@ do args ← io.cmdline_args,
      io.fail "Error: incorrect number of arguments, expected `lirc file.lean`",
    let fname := args.head,
    input ← fs.read_file fname,
-   match lirc input with
+   match lirc input {main_proc := some "main"} with
    | except.ok r    := fs.write_file (fname ++ ".cpp") r
    | except.error e := io.fail (to_string e)
diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean
index 37579b630f..f8e4f6817e 100644
--- a/tests/lean/run/parser_ir1.lean
+++ b/tests/lean/run/parser_ir1.lean
@@ -67,7 +67,7 @@ main:
 def tst_extract_cpp (s : string) : io unit :=
 do (except.ok d) ← return $ parse (whitespace >> parse_def) s,
    check_decl d,
-   match extract_cpp [elim_phi d] {main_proc := none} with
+   match extract_cpp [elim_phi d] with
    | except.ok code := io.print_ln code
    | except.error s := io.print_ln s