From f336525f3153e278a75876e1f1d3462302c1f23f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 7 Mar 2024 10:14:06 -0800 Subject: [PATCH] fix: make `delabConstWithSignature` avoid using inaccessible names (#3625) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `delabConstWithSignature` delaborator is responsible for pretty printing constants with a declaration-like signature, with binders, a colon, and a type. This is used by the `#check` command when it is given just an identifier. It used to accumulate binders from pi types indiscriminately, but this led to unfriendly behavior. For example, `#check String.append` would give ``` String.append (a✝ : String) (a✝¹ : String) : String ``` with inaccessible names. These appear because `String.append` is defined using patterns, so it never names these parameters. Now the delaborator stops accumulating binders once it reaches an inaccessible name, and for example `#check String.append` now gives ``` String.append : String → String → String ``` We do not synthesize names for the sake of enabling binder syntax because the binder names are part of the API of a function — one can use `(arg := ...)` syntax to pass arguments by name. The delaborator also now stops accumulating binders once it reaches a parameter with a name already seen before — we then rely on the main delaborator to provide that parameter with a fresh name when pretty printing the pi type. As a special case, instance parameters with inaccessible names are included as binders, pretty printing like `[LT α]`, rather than relegating them (and all the remaining parameters) to after the colon. It would be more accurate to pretty print this as `[inst✝ : LT α]`, but we make the simplifying assumption that such instance parameters are generally used via typeclass inference. Likely `inst✝` would not directly appear in pretty printer output, and even if it appears in a hover, users can likely figure out what is going on. (We may consider making such `inst✝` variables pretty print as `‹LT α›` or `infer_instance` in the future, to make this more consistent.) Something we note here is that we do not do anything to make sure parameters that can be used as named arguments actually appear named after the colon (nor do we assure that the names are the correct names). For example, one sees `foo : String → String → String` rather than `foo : String → (baz : String) → String`. We can investigate this later if it is wanted. We also give `delabConstWithSignature` a `universes` flag to enable turning off pretty printing universe levels parameters. Closes #2846 --- .../PrettyPrinter/Delaborator/Builtins.lean | 100 +++++++++++++----- tests/lean/1377.lean.expected.out | 2 +- tests/lean/714.lean.expected.out | 2 +- tests/lean/974.lean.expected.out | 16 +-- ...toImplicitChainNameIssue.lean.expected.out | 2 +- .../lean/interactive/hover.lean.expected.out | 8 +- tests/lean/levelNGen.lean.expected.out | 6 +- tests/lean/match1.lean.expected.out | 4 +- tests/lean/namePatEqThm.lean.expected.out | 6 +- tests/lean/run/2846.lean | 74 +++++++++++++ tests/lean/run/funind_demo.lean | 2 +- tests/lean/run/funind_mutual_dep.lean | 2 +- tests/lean/run/funind_tests.lean | 24 +++-- tests/lean/sizeof.lean.expected.out | 3 +- .../lean/terminationFailure.lean.expected.out | 2 +- tests/lean/varBinderUpdate.lean.expected.out | 2 +- 16 files changed, 189 insertions(+), 66 deletions(-) create mode 100644 tests/lean/run/2846.lean diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index b34c32b4e4..101c17d4f5 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -1082,41 +1082,85 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) @[implemented_by evalSyntaxConstantUnsafe] private opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw "" -/-- Pretty-prints a constant `c` as `c.{} : `. -/ -partial def delabConstWithSignature : Delab := do +/-- +Pretty-prints a constant `c` as `c.{} : `. + +If `universes` is `false`, then the universe level parameters are omitted. +-/ +partial def delabConstWithSignature (universes : Bool := true) : Delab := do let e ← getExpr -- use virtual expression node of arity 2 to separate name and type info let idStx ← descend e 0 <| - withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <| + withOptions (pp.universes.set · universes |> (pp.fullNames.set · true)) <| delabConst descend (← inferType e) 1 <| - delabParams idStx #[] #[] + delabParams {} idStx #[] where - -- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups - delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do - if let .forallE n d _ i ← getExpr then - let stxN ← annotateCurPos (mkIdent n) - let curIds := curIds.push ⟨stxN⟩ - if ← shouldGroupWithNext then - withBindingBody n <| delabParams idStx groups curIds - else - let delabTy := withOptions (pp.piBinderTypes.set · true) delab - let group ← withBindingDomain do - match i with - | .implicit => `(bracketedBinderF|{$curIds* : $(← delabTy)}) - | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄) - | .instImplicit => `(bracketedBinderF|[$curIds.back : $(← delabTy)]) - | _ => - if d.isOptParam then - `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy))) - else if let some (.const tacticDecl _) := d.getAutoParamTactic? then - let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl - `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax)) - else - `(bracketedBinderF|($curIds* : $(← delabTy))) - withBindingBody n <| delabParams idStx (groups.push group) #[] + /-- + For types in the signature, we want to be sure pi binder types are pretty printed. + -/ + delabTy : DelabM Term := withOptions (pp.piBinderTypes.set · true) delab + /- + Similar to `delabBinders`, but does not uniquify binder names (since for named arguments we want to know the name), + and it always merges binder groups when possible. + Once it reaches a binder with an inaccessible name, or a name that has already been used, + the remaining binders appear in pi types after the `:` of the declaration. + -/ + delabParams (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) := do + let e ← getExpr + if e.isForall && e.binderInfo.isInstImplicit && e.bindingName!.hasMacroScopes then + -- Assumption: this instance can be found by instance search, so it does not need to be named. + -- The oversight here is that this inaccessible name can appear in the pretty printed expression. + -- We could check to see whether the instance appears in the type and avoid omitting the instance name, + -- but this would be the usual case. + let group ← withBindingDomain do `(bracketedBinderF|[$(← delabTy)]) + withBindingBody e.bindingName! <| delabParams bindingNames idStx (groups.push group) + else if e.isForall && !e.bindingName!.hasMacroScopes && !bindingNames.contains e.bindingName! then + delabParamsAux bindingNames idStx groups #[] else - let type ← delab + let type ← delabTy `(declSigWithId| $idStx:ident $groups* : $type) + /-- + Inner loop for `delabParams`, collecting binders. + Invariants: + - The current expression is a forall. + - It has a name that's not inaccessible. + - It has a name that hasn't been used yet. + -/ + delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do + let e@(.forallE n d e' i) ← getExpr | unreachable! + let bindingNames := bindingNames.insert n + let stxN := mkIdent n + let curIds := curIds.push ⟨stxN⟩ + if shouldGroupWithNext bindingNames e e' then + withBindingBody n <| delabParamsAux bindingNames idStx groups curIds + else + let group ← withBindingDomain do + match i with + | .implicit => `(bracketedBinderF|{$curIds* : $(← delabTy)}) + | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄) + | .instImplicit => `(bracketedBinderF|[$stxN : $(← delabTy)]) + | _ => + if d.isOptParam then + `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy))) + else if let some (.const tacticDecl _) := d.getAutoParamTactic? then + let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl + `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax)) + else + `(bracketedBinderF|($curIds* : $(← delabTy))) + withBindingBody n <| delabParams bindingNames idStx (groups.push group) + /- + Given the forall `e` with body `e'`, determines if the binder from `e'` (if it is a forall) should be grouped with `e`'s binder. + -/ + shouldGroupWithNext (bindingNames : NameSet) (e e' : Expr) : Bool := + e'.isForall && + -- At the first sign of an inaccessible name, stop merging binders: + !e'.bindingName!.hasMacroScopes && + -- If it's a name that has already been used, stop merging binders: + !bindingNames.contains e'.bindingName! && + e.binderInfo == e'.binderInfo && + e.bindingDomain! == e'.bindingDomain! && + -- Inst implicits can't be grouped: + e'.binderInfo != BinderInfo.instImplicit end Lean.PrettyPrinter.Delaborator diff --git a/tests/lean/1377.lean.expected.out b/tests/lean/1377.lean.expected.out index b3ffd2cae8..b22940f237 100644 --- a/tests/lean/1377.lean.expected.out +++ b/tests/lean/1377.lean.expected.out @@ -1,2 +1,2 @@ 1377.lean:3:2-3:5: warning: declaration uses 'sorry' -foo.bar (x✝ : Unit) {n : Nat} (a✝ : Fin n) : Fin n +foo.bar : Unit → {n : Nat} → Fin n → Fin n diff --git a/tests/lean/714.lean.expected.out b/tests/lean/714.lean.expected.out index 3b2a4c4368..de9e1ff1be 100644 --- a/tests/lean/714.lean.expected.out +++ b/tests/lean/714.lean.expected.out @@ -1 +1 @@ -test {α : Type} [inst✝ : LT α] : Type +test {α : Type} [LT α] : Type diff --git a/tests/lean/974.lean.expected.out b/tests/lean/974.lean.expected.out index 418dba1e98..afc0622e0a 100644 --- a/tests/lean/974.lean.expected.out +++ b/tests/lean/974.lean.expected.out @@ -1,7 +1,9 @@ -Formula.count_quantifiers._eq_1.{u_1} (x✝ : Nat) (f₁ f₂ : Formula x✝) : - Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂ -Formula.count_quantifiers._eq_2.{u_1} (x✝ : Nat) (f : Formula (x✝ + 1)) : - Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1 -Formula.count_quantifiers._eq_3.{u_1} (x✝ : Nat) (x✝¹ : Formula x✝) - (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = Formula.imp f₁ f₂ → False) - (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = Formula.all f → False) : Formula.count_quantifiers x✝¹ = 0 +Formula.count_quantifiers._eq_1.{u_1} : + ∀ (x : Nat) (f₁ f₂ : Formula x), + Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂ +Formula.count_quantifiers._eq_2.{u_1} : + ∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1 +Formula.count_quantifiers._eq_3.{u_1} : + ∀ (x : Nat) (x_1 : Formula x), + (∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) → + (∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0 diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out index e68366ea75..e6b966055a 100644 --- a/tests/lean/autoImplicitChainNameIssue.lean.expected.out +++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out @@ -3,4 +3,4 @@ case nil α✝ : Type u_1 as : List α✝ ⊢ Palindrome (List.reverse []) -palindrome_reverse.{u_1} {α✝ : Type u_1} {as : List α✝} (h : Palindrome as) : Palindrome (List.reverse as) +palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as) diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 8b6baeb070..5437b2017f 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -120,7 +120,7 @@ {"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}}, "contents": {"value": - "```lean\nNat.add (a✝a✝¹ : Nat) : Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*", + "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 77, "character": 10}} @@ -620,7 +620,7 @@ "end": {"line": 291, "character": 20}}, "contents": {"value": - "```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) (a✝ : List α) : List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*", + "```lean\nList.map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List α → List β\n```\n***\n`O(|l|)`. `map f l` applies `f` to each element of the list.\n* `map f [a, b, c] = [f a, f b, f c]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 294, "character": 26}} @@ -629,7 +629,7 @@ "end": {"line": 294, "character": 29}}, "contents": {"value": - "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", + "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 294, "character": 19}} @@ -638,5 +638,5 @@ "end": {"line": 294, "character": 22}}, "contents": {"value": - "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} (a✝ : List α) (a✝¹ : List β) : List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", + "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\n`O(min |xs| |ys|)`. Combines the two lists into a list of pairs, with one element from each list.\nThe longer list is truncated to match the shorter list.\n* `zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*", "kind": "markdown"}} diff --git a/tests/lean/levelNGen.lean.expected.out b/tests/lean/levelNGen.lean.expected.out index 743e0c5919..927f2ce745 100644 --- a/tests/lean/levelNGen.lean.expected.out +++ b/tests/lean/levelNGen.lean.expected.out @@ -1,5 +1,5 @@ -test1.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1 +test1.{u_1, u_2} {α : Sort u_2} : α → Sort u_1 levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry' -test2.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1 +test2.{u_1, u_2} {α : Sort u_2} : α → Sort u_1 levelNGen.lean:5:33-5:38: warning: declaration uses 'sorry' -test3.{u_1, u_2} {α : Sort u_2} (a✝ : α) : Sort u_1 +test3.{u_1, u_2} {α : Sort u_2} : α → Sort u_1 diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index f7dab2aa43..7e2fbddbb4 100644 --- a/tests/lean/match1.lean.expected.out +++ b/tests/lean/match1.lean.expected.out @@ -46,6 +46,6 @@ fun x => | #[] => 0 | #[3, 4, 5] => 3 | x => 4 : Array Nat → Nat -g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a]) - (h_2 : (x : List α) → motive x) : motive x✝ +g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) : + (x : List α) → ((a : α) → motive [a]) → ((x : List α) → motive x) → motive x fun e => nomatch e : Empty → False diff --git a/tests/lean/namePatEqThm.lean.expected.out b/tests/lean/namePatEqThm.lean.expected.out index 17bd2acfba..73e55b147d 100644 --- a/tests/lean/namePatEqThm.lean.expected.out +++ b/tests/lean/namePatEqThm.lean.expected.out @@ -2,5 +2,7 @@ iota._eq_1 : iota 0 = [] iota._eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n f._eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y]) f._eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs -f._eq_3 (x✝ : List Nat) (x_2 : ∀ (x y : Nat), x✝ = [x, y] → False) - (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: y :: zs → False) : f x✝ = ([], []) +f._eq_3 : + ∀ (x : List Nat), + (∀ (x_1 y : Nat), x = [x_1, y] → False) → + (∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], []) diff --git a/tests/lean/run/2846.lean b/tests/lean/run/2846.lean new file mode 100644 index 0000000000..d519eb3bae --- /dev/null +++ b/tests/lean/run/2846.lean @@ -0,0 +1,74 @@ +/-! +# `delabConstWithSignature` avoids using inaccessible names +-/ + +/-! +Defined without named arguments, prints without named arguments. +-/ +/-- info: String.append : String → String → String -/ +#guard_msgs in #check String.append + +/-! +The List argument is not named, it is not printed as a named argument. +-/ +/-- info: List.length.{u_1} {α : Type u_1} : List α → Nat -/ +#guard_msgs in #check List.length + +/-! +All arguments are named, all are printed as named arguments. +-/ +/-- info: Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n ^ m -/ +#guard_msgs in #check Nat.pos_pow_of_pos + +/-! +The hypothesis is not a named argument, so it's not printed as a named argument. +-/ +def Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m := Nat.pos_pow_of_pos m + +/-- info: Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m -/ +#guard_msgs in #check Nat.pos_pow_of_pos' + +/-! +Repetition of a named argument, only the first is printed as a named argument. +-/ +def foo (n n : Nat) : Fin (n + 1) := 0 + +/-- info: foo (n : Nat) : (n : Nat) → Fin (n + 1) -/ +#guard_msgs in #check foo + +/-! +Repetition of a named argument, only the first is printed as a named argument. +This is checking that shadowing is handled correctly (that's not the responsibility of +`delabConstWithSignature`, but it assumes that the main delaborator will handle this correctly). +-/ +def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0 + +/-- info: foo' (n : Nat) : (n_1 : Nat) → Fin (n + 1) → Fin (n_1 + 1) -/ +#guard_msgs in #check foo' + +/-! +Named argument after inaccesible name, still stays after the colon. +But, it does not print using named pi notation since this is not a dependent type. +-/ +def foo'' : String → (needle : String) → String := fun _ yo => yo + +/-- info: foo'' : String → String → String -/ +#guard_msgs in #check foo'' + +/-! +Named argument after inaccessible name, still stays after the colon. +Here, because it's a dependent type the named pi notation shows the name. +-/ +def bar : String → (n : Nat) → Fin (n+1) := fun _ n => ⟨0, Nat.zero_lt_succ n⟩ + +/-- info: bar : String → (n : Nat) → Fin (n + 1) -/ +#guard_msgs in #check bar + +/-! +Instance argument is an inaccessible name, and we assume that it is a nameless instance, +so it goes before the colon. +-/ +def bar' [LT α] (x : α) : x < x := sorry + +/-- info: bar'.{u_1} {α : Type u_1} [LT α] (x : α) : x < x -/ +#guard_msgs in #check bar' diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean index e7ea42bfb0..6091baa4f4 100644 --- a/tests/lean/run/funind_demo.lean +++ b/tests/lean/run/funind_demo.lean @@ -10,7 +10,7 @@ derive_functional_induction ackermann info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) - (x x : Nat) : motive x x + (x : Nat) : ∀ (x_1 : Nat), motive x x_1 -/ #guard_msgs in #check ackermann.induct diff --git a/tests/lean/run/funind_mutual_dep.lean b/tests/lean/run/funind_mutual_dep.lean index e3a4d6c96c..229c26fa42 100644 --- a/tests/lean/run/funind_mutual_dep.lean +++ b/tests/lean/run/funind_mutual_dep.lean @@ -65,7 +65,7 @@ info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (x : Type) (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → α)), motive2 (Finite.asType (Finite.arr t1 t2) → α) t2 rest) → motive2 α (Finite.arr t1 t2) results) - (x : Type) (x : Finite) (x : List x) : motive2 x x x + (x : Type) : ∀ (x_1 : Finite) (x_2 : List x), motive2 x x_1 x_2 -/ #guard_msgs in #check Finite.functions.induct diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 175cf0069d..1e3cdd5262 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -32,7 +32,7 @@ derive_functional_induction ackermann info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) - (x x : Nat) : motive x x + (x : Nat) : ∀ (x_1 : Nat), motive x x_1 -/ #guard_msgs in #check ackermann.induct @@ -244,7 +244,7 @@ derive_functional_induction with_arg_refining_match1 /-- info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0) (case2 : ∀ (n : Nat), motive 0 (Nat.succ n)) - (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (x x : Nat) : motive x x + (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (x : Nat) : ∀ (x_1 : Nat), motive x x_1 -/ #guard_msgs in #check with_arg_refining_match1.induct @@ -259,7 +259,8 @@ derive_functional_induction with_arg_refining_match2 /-- info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n) (case2 : ∀ (i : Nat), ¬i = 0 → motive i 0) - (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (x x : Nat) : motive x x + (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (x : Nat) : + ∀ (x_1 : Nat), motive x x_1 -/ #guard_msgs in #check with_arg_refining_match2.induct @@ -293,7 +294,8 @@ derive_functional_induction with_mixed_match_tailrec /-- info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (c d x : Nat), motive 0 x c d) - (case2 : ∀ (c d a x : Nat), motive a x (c % 2) (d % 2) → motive (Nat.succ a) x c d) (x x x x : Nat) : motive x x x x + (case2 : ∀ (c d a x : Nat), motive a x (c % 2) (d % 2) → motive (Nat.succ a) x c d) (x : Nat) : + ∀ (x_1 x_2 x_3 : Nat), motive x x_1 x_2 x_3 -/ #guard_msgs in #check with_mixed_match_tailrec.induct @@ -312,8 +314,8 @@ derive_functional_induction with_mixed_match_tailrec2 /-- info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a b c d : Nat), motive 0 a b c d) (case2 : ∀ (c d n x : Nat), motive (Nat.succ n) 0 x c d) - (case3 : ∀ (c d n a x : Nat), motive n a x (c % 2) (d % 2) → motive (Nat.succ n) (Nat.succ a) x c d) - (x x x x x : Nat) : motive x x x x x + (case3 : ∀ (c d n a x : Nat), motive n a x (c % 2) (d % 2) → motive (Nat.succ n) (Nat.succ a) x c d) (x : Nat) : + ∀ (x_1 x_2 x_3 x_4 : Nat), motive x x_1 x_2 x_3 x_4 -/ #guard_msgs in #check with_mixed_match_tailrec2.induct @@ -404,7 +406,7 @@ derive_functional_induction binary /-- info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) - (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) (x x : Nat) : motive x x + (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) (x : Nat) : ∀ (x_1 : Nat), motive x x_1 -/ #guard_msgs in #check binary.induct @@ -543,7 +545,7 @@ termination_by xs => xs derive_functional_induction foo /-- info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive []) - (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (x : List α) : motive x + (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x -/ #guard_msgs in #check foo.induct @@ -559,7 +561,7 @@ termination_by xs => xs derive_functional_induction bar /-- info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive []) - (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (x : List α) : motive x + (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (x : List α), motive x -/ #guard_msgs in #check bar.induct @@ -694,7 +696,7 @@ derive_functional_induction foo /-- info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) - (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (x x : Nat) : motive x x + (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (x : Nat) : ∀ (x_1 : Nat), motive x x_1 -/ #guard_msgs in #check foo.induct @@ -721,7 +723,7 @@ info: Nary.foo.induct (motive : Nat → Nat → (x : Nat) → Fin x → Prop) (case5 : ∀ (n m k : Nat) (x : Fin (k + 2)), motive n m (k + 1) { val := 0, isLt := ⋯ } → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) - (x x x : Nat) (x : Fin x) : motive x x x x + (x : Nat) : ∀ (x_1 x_2 : Nat) (x_3 : Fin x_2), motive x x_1 x_2 x_3 -/ #guard_msgs in #check foo.induct diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out index b732b071d9..52020debae 100644 --- a/tests/lean/sizeof.lean.expected.out +++ b/tests/lean/sizeof.lean.expected.out @@ -7,5 +7,4 @@ 308 310 11 -InfTree.node.sizeOf_spec.{u} {α : Type u} [inst✝ : SizeOf α] (children : Nat → InfTree α) : - sizeOf (InfTree.node children) = 1 +InfTree.node.sizeOf_spec.{u} {α : Type u} [SizeOf α] (children : Nat → InfTree α) : sizeOf (InfTree.node children) = 1 diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out index e2951ec50d..824aff87fe 100644 --- a/tests/lean/terminationFailure.lean.expected.out +++ b/tests/lean/terminationFailure.lean.expected.out @@ -16,7 +16,7 @@ x1 = Please use `termination_by` to specify a decreasing measure. f (x : Nat) : Nat -f.g (a✝ : Nat) : Nat +f.g : Nat → Nat 1 2 terminationFailure.lean:24:9-24:12: error: fail to show termination for diff --git a/tests/lean/varBinderUpdate.lean.expected.out b/tests/lean/varBinderUpdate.lean.expected.out index e789dfabe9..b23fdb0d80 100644 --- a/tests/lean/varBinderUpdate.lean.expected.out +++ b/tests/lean/varBinderUpdate.lean.expected.out @@ -1,6 +1,6 @@ f Nat 5 : Nat g 5 : Nat -Ex1.f (α : Type) [inst✝ : Add α] (a : α) : α +Ex1.f (α : Type) [Add α] (a : α) : α Ex1.g {α : Type} (b : α) : α f Nat 5 : Nat g 5 : Nat