test: add partial/unsafe tests

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

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)

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'