feat(library/init/lean/compiler/ir): add emitutil.lean and emitcpp.lean files

library/init/lean/compiler/ir/emitcpp.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.control.conditional
+import init.lean.name_mangling
+import init.lean.compiler.ir.compilerm
+import init.lean.compiler.ir.emitutil
+
+namespace Lean
+namespace IR
+namespace EmitCpp
+local attribute [instance] monadInhabited
+
+def leanMainFn := "_lean_main"
+
+structure Context :=
+(env        : Environment)
+(localCtx   : LocalContext)
+(modName    : Name)
+(modDeps    : Array Name)
+(mainFn     : FunId)
+(mainParams : Array Param)
+
+abbrev M := ReaderT Context (EState String String)
+
+def getEnv : M Environment := Context.env <$> read
+def getModName : M Name := Context.modName <$> read
+
+@[inline] def emit {α : Type} [HasToString α] (a : α) : M Unit :=
+modify (λ out, out ++ toString a)
+
+@[inline] def emitLn {α : Type} [HasToString α] (a : α) : M Unit :=
+emit a *> emit "\n"
+
+def emitMainFn (d : Decl) : M Unit :=
+match d with
+| Decl.fdecl f xs t b := do
+  unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code"),
+  env ← getEnv,
+  let usesLeanAPI := usesLeanNamespace env d,
+  when usesLeanAPI (emitLn "namespace lean { void initialize(); }"),
+  emitLn "int main(int argc, char ** argv) {",
+  if usesLeanAPI then
+    emitLn "lean::initialize();"
+  else
+    emitLn "lean::initialize_runtime_module();",
+  emitLn "obj * w = lean::io_mk_world();",
+  modName ← getModName,
+  emitLn ("w = initialize_" ++ (modName.mangle "") ++ "(w);"),
+  emitLn "lean::io_mark_end_initialization();",
+  emitLn "if (io_result_is_ok(w)) {\n",
+  emitLn "lean::scoped_task_manager tmanager(lean::hardware_concurrency());",
+  if xs.size == 2 then do {
+    emitLn "obj* in = lean::box(0);",
+    emitLn "int i = argc;\n",
+    emitLn "while (i > 1) {",
+    emitLn " i--;",
+    emitLn " obj* n = lean::alloc_cnstr(1,2,0); lean::cnstr_set(n, 0, lean::mk_string(argv[i])); lean::cnstr_set(n, 1, in);",
+    emitLn " in = n;",
+    emitLn "}",
+    emitLn ("w = " ++ leanMainFn ++ "(in, w);")
+  } else do {
+    emitLn ("w = " ++ leanMainFn ++ "(w);")
+  },
+  emitLn "}",
+  emitLn "if (io_result_is_ok(w)) {",
+  emitLn "  int ret = lean::unbox(io_result_get_value(w));",
+  emitLn "  lean::dec_ref(w);",
+  emitLn "  return ret;",
+  emitLn "} else {",
+  emitLn "  lean::io_result_show_error(w);",
+  emitLn "  lean::dec_ref(w);",
+  emitLn "  return 1;",
+  emitLn "}",
+  emitLn "}"
+| other := throw "function declaration expected"
+
+end EmitCpp
+
+end IR
+end Lean

library/init/lean/compiler/ir/emitutil.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.control.conditional
+import init.lean.compiler.ir.compilerm
+
+/- Helper functions for backend code generators -/
+
+namespace Lean
+namespace IR
+local attribute [instance] monadInhabited
+
+namespace UsesLeanNamespace
+
+abbrev M := ReaderT Environment (State NameSet)
+
+def leanNameSpacePrefix := `Lean
+
+partial def visitFnBody : FnBody → M Bool
+| (FnBody.vdecl _ _ v b) :=
+  let checkFn (f : FunId) : M Bool :=
+     if leanNameSpacePrefix.isPrefixOf f then pure true
+     else do {
+       s ← get,
+       if s.contains f then
+         visitFnBody b
+       else do
+         modify (λ s, s.insert f),
+         env ← read,
+         match findEnvDecl env f with
+         | some (Decl.fdecl _ _ _ fbody) := visitFnBody fbody <||> visitFnBody b
+         | other                         := visitFnBody b
+    } in
+  match v with
+  | Expr.fap f _ := checkFn f
+  | Expr.pap f _ := checkFn f
+  | other        := visitFnBody b
+| (FnBody.jdecl _ _ v b) := visitFnBody v <||> visitFnBody b
+| (FnBody.case _ _ alts) := alts.anyM $ λ alt, visitFnBody alt.body
+| e :=
+  if e.isTerminal then pure false
+  else visitFnBody e.body
+
+end UsesLeanNamespace
+
+def usesLeanNamespace (env : Environment) : Decl → Bool
+| (Decl.fdecl _ _ _ b) := (UsesLeanNamespace.visitFnBody b env).run' {}
+| _                    := false
+
+
+
+end IR
+end Lean

library/init/lean/name.lean

@@ -105,6 +105,11 @@ def replacePrefix : Name → Name → Name → Name
   else
     mkNumeral (p.replacePrefix queryP newP) s
 
+def isPrefixOf : Name → Name → Bool
+| p anonymous          := p == anonymous
+| p n@(mkNumeral p' _) := p == n || isPrefixOf p p'
+| p n@(mkString p' _)  := p == n || isPrefixOf p p'
+
 def quickLtCore : Name → Name → Bool
 | anonymous        anonymous          := false
 | anonymous        _                  := true

library/init/lean/name_mangling.lean

@@ -37,24 +37,6 @@ private def String.mangleAux : Nat → String.Iterator → String → String
 def String.mangle (s : String) : String :=
 String.mangleAux s.length s.mkIterator ""
 
-private def parseMangledStringAux : Nat → String → Parsec' String
-| 0     r := pure r
-| (i+1) r :=
-     (eoi *> pure r)
- <|> (do c ← alpha, parseMangledStringAux i (r.push c))
- <|> (do c ← digit, parseMangledStringAux i (r.push c))
- <|> (do str "__", parseMangledStringAux i (r.push '_'))
- <|> (do str "_x", d₂ ← parseHexDigit, d₁ ← parseHexDigit,
-         parseMangledStringAux i (r.push (Char.ofNat (d₂ * 16 + d₁))))
- <|> (do str "_u", d₄ ← parseHexDigit, d₃ ← parseHexDigit, d₂ ← parseHexDigit, d₁ ← parseHexDigit,
-         parseMangledStringAux i (r.push (Char.ofNat (d₄ * 4096 + d₃ * 256 + d₂ * 16 + d₁))))
-
-private def parseMangledString : Parsec' String :=
-do r ← remaining, parseMangledStringAux r ""
-
-def String.demangle (s : String) : Option String :=
-(Parsec.parse parseMangledString s).toOption
-
 private def Name.mangleAux (pre : String) : Name → String
 | Name.anonymous       := pre
 | (Name.mkString p s) :=
@@ -68,20 +50,4 @@ private def Name.mangleAux (pre : String) : Name → String
 def Name.mangle (n : Name) (pre : String := "_l") : String :=
 Name.mangleAux pre n
 
-private def parseMangledNameAux : Nat → Name → Parsec' Name
-| 0 r     := pure r
-| (i+1) r :=
-      (eoi *> pure r)
-  <|> (do str "_s", n ← num, ch '_',
-          (some s) ← String.demangle <$> take n,
-          parseMangledNameAux i (r.mkString s))
-  <|> (do ch '_', n ← num, ch '_',
-          parseMangledNameAux i (r.mkNumeral n))
-
-private def parseMangledName (pre : String) : Parsec' Name :=
-do str pre, r ← remaining, parseMangledNameAux r Name.anonymous
-
-def Name.demangle (s : String) (pre : String := "_l") : Option Name :=
-(Parsec.parse (parseMangledName pre) s).toOption
-
 end Lean