From e451c4dc78bb17d325f2335a77c5a28f4fa7020e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Sep 2019 16:12:41 -0700
Subject: [PATCH] feat(library/init/lean/compiler): add `@[effectful]`

This attribute is used for low-level primitives like unsafeIO
---
 library/init/lean/compiler/default.lean       |  1 +
 library/init/lean/compiler/effectfulattr.lean | 22 +++++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 library/init/lean/compiler/effectfulattr.lean

diff --git a/library/init/lean/compiler/default.lean b/library/init/lean/compiler/default.lean
index 5b1732fe7f..2365a77636 100644
--- a/library/init/lean/compiler/default.lean
+++ b/library/init/lean/compiler/default.lean
@@ -10,4 +10,5 @@ import init.lean.compiler.constfolding
 import init.lean.compiler.closedtermcache
 import init.lean.compiler.externattr
 import init.lean.compiler.implementedbyattr
+import init.lean.compiler.effectfulattr
 import init.lean.compiler.ir
diff --git a/library/init/lean/compiler/effectfulattr.lean b/library/init/lean/compiler/effectfulattr.lean
new file mode 100644
index 0000000000..fd3206cd4d
--- /dev/null
+++ b/library/init/lean/compiler/effectfulattr.lean
@@ -0,0 +1,22 @@
+/-
+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.lean.environment
+import init.lean.attributes
+
+namespace Lean
+
+def mkEffectfulAttr : IO TagAttribute :=
+registerTagAttribute `effectful "mark that a declaration has implicit effects, and the compiler should avoid optimizations such as common subexpression elimination and closed term extraction"
+
+@[init mkEffectfulAttr]
+constant effectfulAttr : TagAttribute := default _
+
+@[export lean_has_effectful_attribute]
+def hasEffectfulAttribute (env : Environment) (n : Name) : Bool :=
+effectfulAttr.hasTag env n
+
+end Lean