update line numbers in test after rebase

src/Lean/Elab/BuiltinNotation.lean

@@ -1,12 +1,14 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Gabriel Ebner
 -/
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
+import Lean.Meta.Closure
 import Lean.Meta.MatchUtil
 import Lean.Elab.SyntheticMVars
+import Lean.Compiler.ImplementedByAttr
 
 namespace Lean.Elab.Term
 open Meta
@@ -425,4 +427,33 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
   let e ← elabTerm stx[1] expectedType?
   return DiscrTree.mkNoindexAnnotation e
 
+-- TODO: investigate whether we need this function
+private def mkAuxNameForElabUnsafe (hint : Name) : TermElabM Name :=
+  withFreshMacroScope do
+    let name := (← getDeclName?).getD Name.anonymous ++ hint
+    return addMacroScope (← getMainModule) name (← getCurrMacroScope)
+
+@[builtin_term_elab «unsafe»]
+def elabUnsafe : TermElab := fun stx expectedType? =>
+  match stx with
+  | `(unsafe $t) => do
+    let t ← elabTermAndSynthesize t expectedType?
+    if (← logUnassignedUsingErrorInfos (← getMVars t)) then
+      throwAbortTerm
+    let t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
+    let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
+    let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
+    let implName ← mkAuxNameForElabUnsafe `impl
+    addDecl <| Declaration.defnDecl {
+      name        := implName
+      type        := unsafeDefn.type
+      levelParams := unsafeDefn.levelParams
+      value       := (← mkOfNonempty unsafeDefn.type)
+      hints       := .opaque
+      safety      := .safe
+    }
+    setImplementedBy implName unsafeFn
+    return mkAppN (Lean.mkConst implName unsafeLvls) t.getAppArgs
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term

src/Lean/Parser/Term.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
+Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
 -/
 import Lean.Parser.Attr
 import Lean.Parser.Level
@@ -601,6 +601,19 @@ def matchAltsWhereDecls := leading_parser
 @[builtin_term_parser] def noindex := leading_parser
   "no_index " >> termParser maxPrec
 
+/--
+`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
+body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
+wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
+but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
+the compiler is unable to guarantee the safety of the operation.
+
+For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
+you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
+particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
+-/
+@[builtin_term_parser] def «unsafe» := leading_parser:leadPrec "unsafe " >> termParser
+
 /-- `binrel% r a b` elaborates `r a b` as a binary relation using the type propogation protocol in `Lean.Elab.Extra`. -/
 @[builtin_term_parser] def binrel := leading_parser
   "binrel% " >> ident >> ppSpace >> termParser maxPrec >> ppSpace >> termParser maxPrec

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
-some { range := { pos := { line := 189, column := 42 },
+some { range := { pos := { line := 191, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 195, column := 31 },
+             endPos := { line := 197, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 189, column := 46 },
+  selectionRange := { pos := { line := 191, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 189, column := 58 },
+                      endPos := { line := 191, column := 58 },
                       endCharUtf16 := 58 } }

tests/lean/run/sharecommon.lean

@@ -2,7 +2,7 @@ import Lean.Util.ShareCommon
 
 open Lean.ShareCommon
 def check (b : Bool) : ShareCommonT IO Unit := do
-unless b do throw $ IO.userError "check failed"
+  unless b do throw $ IO.userError "check failed"
 
 unsafe def tst1 : ShareCommonT IO Unit := do
 let x := [1]

tests/lean/run/unsafeTerm.lean

@@ -0,0 +1,3 @@
+def cool :=
+  unsafe (unsafeCast () : Nat)
+#eval cool