chore(library/init/lean/ir): cleanup

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) :=

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)

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

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)

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