69d8d63d58
This PR improves the error message of generalized field notation if the issue is that the resolved declaration is not visible in the current context.
498 lines
12 KiB
Text
498 lines
12 KiB
Text
module
|
||
|
||
meta import Init.Dynamic
|
||
meta import Init.System.IO
|
||
|
||
public axiom testSorry : α
|
||
|
||
/-! Module docstring -/
|
||
|
||
/-- A definition (not exposed). -/
|
||
public def f := 1
|
||
|
||
/--
|
||
info: def f : Nat :=
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
#print f
|
||
|
||
/-- A definition (exposed) -/
|
||
@[expose] public def fexp := 1
|
||
|
||
/--
|
||
info: @[expose] def fexp : Nat :=
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
#print fexp
|
||
|
||
/-- An abbrev (auto-exposed). -/
|
||
public abbrev fabbrev := 1
|
||
|
||
/--
|
||
info: @[reducible, expose] def fabbrev : Nat :=
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
#print fabbrev
|
||
|
||
/-- A non-exposed function type. -/
|
||
public def Fun := Nat → Nat
|
||
|
||
/-! The compiler should check it has sufficient information about types available. -/
|
||
|
||
/--
|
||
error: Compilation failed, locally inferred compilation type
|
||
(Nat → Nat) → Nat → Nat
|
||
differs from type
|
||
(Nat → Nat) → lcAny
|
||
that would be inferred in other modules. This usually means that a type `def` involved with the mentioned declarations needs to be `@[expose]`d. This is a current compiler limitation for `module`s that may be lifted in the future.
|
||
-/
|
||
#guard_msgs in
|
||
public def Fun.mk (f : Nat → Nat) : Fun := f
|
||
|
||
#guard_msgs(drop warning) in
|
||
/-- A theorem. -/
|
||
public theorem t : f = 1 := testSorry
|
||
|
||
/-- A private definition. -/
|
||
def fpriv := 1
|
||
|
||
public section
|
||
/-- Examples are always private. -/
|
||
example : fpriv = 1 := rfl
|
||
|
||
/--
|
||
error: Unknown identifier `fpriv`
|
||
|
||
Note: A private declaration `fpriv` (from the current module) exists but would need to be public to access here.
|
||
-/
|
||
#guard_msgs in
|
||
/-- ...unless explicitly marked `public`. -/
|
||
public example : fpriv = 1 := rfl
|
||
end
|
||
|
||
/--
|
||
error: Unknown identifier `fpriv`
|
||
|
||
Note: A private declaration `fpriv` (from the current module) exists but would need to be public to access here.
|
||
-/
|
||
#guard_msgs in
|
||
public theorem tpriv : fpriv = 1 := rfl
|
||
|
||
/-! Type inference should not be able to smuggle out private references. -/
|
||
|
||
/--
|
||
error: Unknown constant `_private.Module.Basic.0.fpriv`
|
||
|
||
Note: A private declaration `fpriv` (from the current module) exists but would need to be public to access here.
|
||
-/
|
||
#guard_msgs in
|
||
public def inferredPrivRef := (rfl : fpriv = 1)
|
||
|
||
public class X
|
||
|
||
/-- A local instance of a public class. -/
|
||
instance : X := ⟨⟩
|
||
|
||
|
||
-- Check that the theorem types are checked in exported context, where `f` is not defeq to `1`
|
||
-- (but `fexp` is)
|
||
|
||
/--
|
||
error: Type mismatch
|
||
y
|
||
has type
|
||
Vector Unit 1
|
||
but is expected to have type
|
||
Vector Unit f
|
||
|
||
Note: The following definitions were not unfolded because their definition is not exposed:
|
||
f ↦ 1
|
||
-/
|
||
#guard_msgs in
|
||
public theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry
|
||
|
||
theorem v' (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry
|
||
|
||
theorem v'' (x : Vector Unit fexp) (y : Vector Unit 1) : x = y := testSorry
|
||
|
||
-- Check that rfl theorems are complained about if they aren't rfl in the context of their type
|
||
|
||
/--
|
||
error: Not a definitional equality: the left-hand side
|
||
f
|
||
is not definitionally equal to the right-hand side
|
||
1
|
||
|
||
Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
|
||
-/
|
||
#guard_msgs in
|
||
public theorem trfl : f = 1 := rfl
|
||
/--
|
||
error: Not a definitional equality: the left-hand side
|
||
f
|
||
is not definitionally equal to the right-hand side
|
||
1
|
||
|
||
Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
|
||
-/
|
||
#guard_msgs in
|
||
@[defeq] public theorem trfl' : f = 1 := (rfl)
|
||
|
||
theorem trflprivate : f = 1 := rfl
|
||
def trflprivate' : f = 1 := rfl
|
||
@[defeq] def trflprivate''' : f = 1 := rfl
|
||
theorem trflprivate'''' : f = 1 := (rfl)
|
||
|
||
public theorem fexp_trfl : fexp = 1 := rfl
|
||
@[defeq] public theorem fexp_trfl' : fexp = 1 := rfl
|
||
|
||
public opaque P : Nat → Prop
|
||
public axiom hP1 : P 1
|
||
|
||
/-- error: `dsimp` made no progress -/
|
||
#guard_msgs in
|
||
example : P f := by dsimp only [t]; exact hP1
|
||
example : P f := by simp only [t]; exact hP1
|
||
|
||
/-- error: `dsimp` made no progress -/
|
||
#guard_msgs in
|
||
example : P f := by dsimp only [trfl]; exact hP1
|
||
/-- error: `dsimp` made no progress -/
|
||
#guard_msgs in
|
||
example : P f := by dsimp only [trfl']; exact hP1
|
||
example : P f := by dsimp only [trflprivate]; exact hP1
|
||
example : P f := by dsimp only [trflprivate']; exact hP1
|
||
|
||
|
||
example : P fexp := by dsimp only [fexp_trfl]; exact hP1
|
||
example : P fexp := by dsimp only [fexp_trfl]; exact hP1
|
||
|
||
|
||
-- Check that the error message does not mention the export issue if
|
||
-- it wouldn’t be a rfl otherwise either
|
||
|
||
/--
|
||
error: Not a definitional equality: the left-hand side
|
||
f
|
||
is not definitionally equal to the right-hand side
|
||
2
|
||
-/
|
||
#guard_msgs in
|
||
@[defeq] public theorem not_rfl : f = 2 := testSorry
|
||
|
||
/-- A private definition. -/
|
||
def priv := 2
|
||
|
||
/-! Private decls should not be accessible in exported contexts. -/
|
||
|
||
/--
|
||
error: Unknown identifier `priv`
|
||
|
||
Note: A private declaration `priv` (from the current module) exists but would need to be public to access here.
|
||
-/
|
||
#guard_msgs in
|
||
public abbrev h := priv
|
||
|
||
|
||
/-! Equational theorems tests. -/
|
||
|
||
public def f_struct : Nat → Nat
|
||
| 0 => 0
|
||
| n + 1 => f_struct n
|
||
termination_by structural n => n
|
||
|
||
public def f_wfrec : Nat → Nat → Nat
|
||
| 0, acc => acc
|
||
| n + 1, acc => f_wfrec n (acc + 1)
|
||
termination_by n => n
|
||
|
||
@[expose] public def f_exp_wfrec : Nat → Nat → Nat
|
||
| 0, acc => acc
|
||
| n + 1, acc => f_exp_wfrec n (acc + 1)
|
||
termination_by n => n
|
||
|
||
@[inline] protected def Test.Option.map (f : α → β) : Option α → Option β
|
||
| some x => some (f x)
|
||
| none => none
|
||
|
||
|
||
/-- error: `f.eq_def` is a reserved name -/
|
||
#guard_msgs in
|
||
public def f.eq_def := 1
|
||
|
||
/-- error: `fexp.eq_def` is a reserved name -/
|
||
#guard_msgs in
|
||
public def fexp.eq_def := 1
|
||
|
||
/-- info: @[defeq] private theorem f.eq_def : f = 1 -/
|
||
#guard_msgs in #print sig f.eq_def
|
||
|
||
/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/
|
||
#guard_msgs in #print sig f.eq_unfold
|
||
|
||
/-- info: @[defeq] theorem fexp.eq_def : fexp = 1 -/
|
||
#guard_msgs in #print sig fexp.eq_def
|
||
|
||
/-- info: @[defeq] theorem fexp.eq_unfold : fexp = 1 -/
|
||
#guard_msgs in #print sig fexp.eq_unfold
|
||
|
||
/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
|
||
#guard_msgs in #print sig f_struct.eq_1
|
||
|
||
/--
|
||
info: private theorem f_struct.eq_def : ∀ (x : Nat),
|
||
f_struct x =
|
||
match x with
|
||
| 0 => 0
|
||
| n.succ => f_struct n
|
||
-/
|
||
#guard_msgs in #print sig f_struct.eq_def
|
||
|
||
/--
|
||
info: private theorem f_struct.eq_unfold : f_struct = fun x =>
|
||
match x with
|
||
| 0 => 0
|
||
| n.succ => f_struct n
|
||
-/
|
||
#guard_msgs(pass trace, all) in #print sig f_struct.eq_unfold
|
||
|
||
/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
|
||
#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
|
||
|
||
/--
|
||
info: private theorem f_wfrec.eq_def : ∀ (x x_1 : Nat),
|
||
f_wfrec x x_1 =
|
||
match x, x_1 with
|
||
| 0, acc => acc
|
||
| n.succ, acc => f_wfrec n (acc + 1)
|
||
-/
|
||
#guard_msgs in #print sig f_wfrec.eq_def
|
||
|
||
/--
|
||
info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 =>
|
||
match x, x_1 with
|
||
| 0, acc => acc
|
||
| n.succ, acc => f_wfrec n (acc + 1)
|
||
-/
|
||
#guard_msgs in #print sig f_wfrec.eq_unfold
|
||
|
||
/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
|
||
#guard_msgs in #print sig f_exp_wfrec.eq_1
|
||
|
||
/--
|
||
info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat),
|
||
f_exp_wfrec x x_1 =
|
||
match x, x_1 with
|
||
| 0, acc => acc
|
||
| n.succ, acc => f_exp_wfrec n (acc + 1)
|
||
-/
|
||
#guard_msgs in #print sig f_exp_wfrec.eq_def
|
||
|
||
/--
|
||
info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 =>
|
||
match x, x_1 with
|
||
| 0, acc => acc
|
||
| n.succ, acc => f_exp_wfrec n (acc + 1)
|
||
-/
|
||
#guard_msgs in #print sig f_exp_wfrec.eq_unfold
|
||
|
||
/-! Private fields should force private ctors. -/
|
||
|
||
abbrev Priv := Nat
|
||
|
||
public structure StructWithPrivateField where
|
||
private x : Priv
|
||
|
||
/--
|
||
info: structure StructWithPrivateField : Type
|
||
number of parameters: 0
|
||
fields:
|
||
private StructWithPrivateField.x : Priv
|
||
constructor:
|
||
private StructWithPrivateField.mk (x : Priv) : StructWithPrivateField
|
||
-/
|
||
#guard_msgs in
|
||
#print StructWithPrivateField
|
||
|
||
#check { x := 1 : StructWithPrivateField }
|
||
|
||
/-- error: invalid {...} notation, constructor for `StructWithPrivateField` is marked as private -/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#check { x := 1 : StructWithPrivateField }
|
||
|
||
#check (⟨1⟩ : StructWithPrivateField)
|
||
|
||
/--
|
||
error: Invalid `⟨...⟩` notation: Constructor for `StructWithPrivateField` is marked as private
|
||
-/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#check (⟨1⟩ : StructWithPrivateField)
|
||
|
||
#check StructWithPrivateField.x
|
||
|
||
/-- error: Unknown constant `StructWithPrivateField.x` -/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#check StructWithPrivateField.x
|
||
|
||
/-! Private constructors should be compatible with public fields. -/
|
||
|
||
public structure StructWithPrivateCtor where private mk ::
|
||
x : Nat
|
||
|
||
/--
|
||
info: structure StructWithPrivateCtor : Type
|
||
number of parameters: 0
|
||
fields:
|
||
StructWithPrivateCtor.x : Nat
|
||
constructor:
|
||
private StructWithPrivateCtor.mk (x : Nat) : StructWithPrivateCtor
|
||
-/
|
||
#guard_msgs in
|
||
#print StructWithPrivateCtor
|
||
|
||
/-- error: invalid {...} notation, constructor for `StructWithPrivateCtor` is marked as private -/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#check { x := 1 : StructWithPrivateCtor }
|
||
|
||
#with_exporting
|
||
#check StructWithPrivateCtor.x
|
||
|
||
#check StructWithPrivateCtor.mk
|
||
|
||
/-- error: Unknown constant `StructWithPrivateCtor.mk` -/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#check StructWithPrivateCtor.mk
|
||
|
||
/-! Private duplicate in public section should not panic. -/
|
||
|
||
public section
|
||
|
||
private def foo : Nat := 0
|
||
/-- error: private declaration `foo` has already been declared -/
|
||
#guard_msgs in
|
||
private def foo : Nat := 0
|
||
|
||
end
|
||
|
||
/-! Check visibility of auto params. -/
|
||
|
||
public structure OptParamStruct where
|
||
private pauto : Nat := by exact 0
|
||
auto : Nat := by exact 0
|
||
|
||
/--
|
||
info: structure OptParamStruct : Type
|
||
number of parameters: 0
|
||
fields:
|
||
private OptParamStruct.pauto : Nat := by
|
||
exact 0
|
||
OptParamStruct.auto : Nat := by
|
||
exact 0
|
||
constructor:
|
||
private OptParamStruct.mk (pauto : Nat := by exact 0) (auto : Nat := by exact 0) : OptParamStruct
|
||
-/
|
||
#guard_msgs in
|
||
#print OptParamStruct
|
||
|
||
section
|
||
set_option pp.oneline true
|
||
/--
|
||
info: private meta def OptParamStruct.pauto._autoParam : Lean.Syntax :=
|
||
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq [...]
|
||
-/
|
||
#guard_msgs in
|
||
#print OptParamStruct.pauto._autoParam
|
||
/--
|
||
info: @[expose] meta def OptParamStruct.auto._autoParam : Lean.Syntax :=
|
||
Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq [...]
|
||
-/
|
||
#guard_msgs in
|
||
#print OptParamStruct.auto._autoParam
|
||
end
|
||
|
||
/-! `deriving` should derive `meta` defs on `meta` structures. -/
|
||
meta structure Foo where
|
||
deriving TypeName
|
||
|
||
/--
|
||
info: private meta def instTypeNameFoo : TypeName Foo :=
|
||
inst✝
|
||
-/
|
||
#guard_msgs in
|
||
#print instTypeNameFoo
|
||
|
||
public meta def pubMeta := 1
|
||
|
||
/-! `#eval` should accept `meta` and non-`meta`. -/
|
||
|
||
meta def fmeta := 1
|
||
|
||
/-- info: 2 -/
|
||
#guard_msgs in
|
||
#eval f + fmeta
|
||
|
||
/-! Prop `instance`s should have direct access to the private scope. -/
|
||
|
||
public class PropClass : Prop where
|
||
proof : True
|
||
|
||
theorem privTrue : True := trivial
|
||
public instance : PropClass := ⟨privTrue⟩
|
||
|
||
/-! Meta defs should only be exposed explicitly. -/
|
||
|
||
@[expose] section
|
||
public meta def msec := 1
|
||
@[expose] public meta def msecexp := 1
|
||
end
|
||
|
||
/--
|
||
info: meta def msec : Nat :=
|
||
<not imported>
|
||
-/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#print msec
|
||
|
||
/--
|
||
info: @[expose] meta def msecexp : Nat :=
|
||
1
|
||
-/
|
||
#guard_msgs in
|
||
#with_exporting
|
||
#print msecexp
|
||
|
||
attribute [simp] f_struct
|
||
|
||
/-! `[inherit_doc]` should work independently of visibility. -/
|
||
|
||
@[inherit_doc priv] public def pubInheritDoc := 1
|
||
|
||
/-! `initialize` should be run even if imported IR-only. -/
|
||
|
||
public initialize initialized : Nat ← pure 5
|
||
|
||
/-! Error message on private dot notation access. -/
|
||
|
||
public structure S
|
||
|
||
def S.s := 1
|
||
|
||
/--
|
||
error: Invalid field `s`: The environment does not contain `S.s`
|
||
s
|
||
has type
|
||
S
|
||
|
||
Note: A private declaration `S.s` (from the current module) exists but would need to be public to access here.
|
||
-/
|
||
#guard_msgs in
|
||
@[expose] public def useS (s : S) := s.s
|