From ff74b9f44aa545c9c4bc39b065dede0dd0356d18 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 May 2019 09:25:16 -0700 Subject: [PATCH] feat(library/init/lean/compiler/ir): add `emitutil.lean` and `emitcpp.lean` files --- library/init/lean/compiler/ir/emitcpp.lean | 84 +++++++++++++++++++++ library/init/lean/compiler/ir/emitutil.lean | 56 ++++++++++++++ library/init/lean/name.lean | 5 ++ library/init/lean/name_mangling.lean | 34 --------- 4 files changed, 145 insertions(+), 34 deletions(-) create mode 100644 library/init/lean/compiler/ir/emitcpp.lean create mode 100644 library/init/lean/compiler/ir/emitutil.lean diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean new file mode 100644 index 0000000000..6f070f8c95 --- /dev/null +++ b/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 diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean new file mode 100644 index 0000000000..ca07d8b0da --- /dev/null +++ b/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 diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index 2849620b5e..eb913c2e62 100644 --- a/library/init/lean/name.lean +++ b/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 diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean index b2e4ef7206..e74c9b809c 100644 --- a/library/init/lean/name_mangling.lean +++ b/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