From 93f3c987800061f5c67e731ef682aff81ce43257 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Jan 2021 18:44:26 -0800
Subject: [PATCH] test: add partial/unsafe tests

---
 tests/lean/run/toExpr.lean                |  2 +-
 tests/lean/sanitychecks.lean              | 29 +++++++++++++++++++++++
 tests/lean/sanitychecks.lean.expected.out | 13 ++++++++++
 3 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/sanitychecks.lean
 create mode 100644 tests/lean/sanitychecks.lean.expected.out

diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean
index eb1133af2c..bc8a66f718 100644
--- a/tests/lean/run/toExpr.lean
+++ b/tests/lean/run/toExpr.lean
@@ -11,7 +11,7 @@ let decl := Declaration.defnDecl {
   value    := toExpr a,
   type     := toTypeExpr α,
   hints    := ReducibilityHints.abbrev,
-  isUnsafe := false
+  safety   := DefinitionSafety.safe
 };
 IO.println (toExpr a);
 (match env.addAndCompile {} decl with
diff --git a/tests/lean/sanitychecks.lean b/tests/lean/sanitychecks.lean
new file mode 100644
index 0000000000..8919ea76c5
--- /dev/null
+++ b/tests/lean/sanitychecks.lean
@@ -0,0 +1,29 @@
+theorem unsound : False := -- Error
+  unsound
+
+partial theorem unsound : False := -- Error
+  unsound
+
+unsafe theorem unsound : False := -- Error
+  unsound
+
+constant unsound : False  -- Error
+
+axiom magic : False -- OK
+
+partial def foo (x : Nat) : Nat := foo x  -- OK
+
+unsafe def unsound2 : False := unsound  -- OK
+
+partial def unsound3 : False := unsound3  -- Error
+
+partial def badcast1 (x : Nat) : Bool :=
+  unsafeCast x -- Error: partial cannot use unsafe constant
+
+partial def badcast2 (x : Nat) : Bool :=
+  if x == 0 then unsafeCast x -- Error: partial cannot use unsafe constant
+  else badcast2 (x + 1)
+
+unsafe def badcast3 (x : Nat) : Bool := -- OK
+  if x == 0 then unsafeCast x
+  else badcast3 (x + 1)
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
new file mode 100644
index 0000000000..40c523a749
--- /dev/null
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -0,0 +1,13 @@
+sanitychecks.lean:1:0: error: fail to show termination for
+  unsound
+with errors
+structural recursion cannot be used
+
+well founded recursion has not been implemented yet
+sanitychecks.lean:4:8: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
+sanitychecks.lean:7:7: error: 'unsafe' theorems are not allowed
+sanitychecks.lean:10:0: error: failed to synthesize instance
+  Inhabited False
+sanitychecks.lean:18:0: error: failed to compile partial definition 'unsound3', failed to show that type is inhabited
+sanitychecks.lean:20:0: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
+sanitychecks.lean:23:0: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'