From 4239ae69f673d39c1f3beb617e646a20305073de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Aug 2021 17:24:58 -0700 Subject: [PATCH] chore: fix tests --- tests/lean/343.lean | 2 +- tests/lean/423.lean.expected.out | 20 +++---- tests/lean/infoTree.lean.expected.out | 78 ++++++++++++------------- tests/lean/macroStack.lean.expected.out | 2 - tests/lean/typeOf.lean.expected.out | 10 ++-- 5 files changed, 49 insertions(+), 63 deletions(-) diff --git a/tests/lean/343.lean b/tests/lean/343.lean index b90367f30e..eb2b5c8e8f 100644 --- a/tests/lean/343.lean +++ b/tests/lean/343.lean @@ -16,7 +16,7 @@ abbrev Catish : CatIsh := universe m o unif_hint (mvar : CatIsh) where - Catish.{o,m} =?= mvar |- mvar.Obj =?= CatIsh.{m,o} + Catish.{m, o} =?= mvar |- mvar.Obj =?= CatIsh.{m,o} structure CtxSyntaxLayerParamsObj where Ct : CatIsh diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out index 2b08400483..cf53fe9a00 100644 --- a/tests/lean/423.lean.expected.out +++ b/tests/lean/423.lean.expected.out @@ -1,11 +1,9 @@ -423.lean:3:35-3:40: error: application type mismatch - HAdd.hAdd (α := Nat) a -argument - a +423.lean:3:39-3:40: error: type mismatch + 0 has type - T : Sort u -but is expected to have type Nat : Type +but is expected to have type + T : Sort u 423.lean:5:33-5:38: error: application type mismatch Add T argument @@ -22,11 +20,9 @@ has type Sort u : Type u but is expected to have type Type ?u : Type (?u + 1) -423.lean:5:55-5:60: error: application type mismatch - HAdd.hAdd (α := Nat) a -argument - a +423.lean:5:59-5:60: error: type mismatch + 0 has type - T : Sort u -but is expected to have type Nat : Type +but is expected to have type + T : Sort u diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out index 6b9d954e7f..a31980007d 100644 --- a/tests/lean/infoTree.lean.expected.out +++ b/tests/lean/infoTree.lean.expected.out @@ -1,9 +1,9 @@ [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.535} @ ⟨13, 11⟩-⟨13, 14⟩ + [.] `Nat : some Sort.{?_uniq.405} @ ⟨13, 11⟩-⟨13, 14⟩ Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ x : Nat @ ⟨13, 7⟩-⟨13, 8⟩ - Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2258 + Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2315 Macro expansion Nat × Nat ===> @@ -11,10 +11,10 @@ Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩† Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.539} @ ⟨13, 18⟩-⟨13, 21⟩ + [.] `Nat : some Type.{?_uniq.409} @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩ + [.] `Nat : some Type.{?_uniq.408} @ ⟨13, 24⟩-⟨13, 27⟩ Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ let y := (x, x); id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabLetDecl @@ -39,39 +39,33 @@ [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.566} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.436} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ x : Nat @ ⟨17, 9⟩-⟨17, 10⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.568} @ ⟨17, 15⟩-⟨17, 18⟩ + [.] `Nat : some Sort.{?_uniq.438} @ ⟨17, 15⟩-⟨17, 18⟩ Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ y : Nat @ ⟨17, 11⟩-⟨17, 12⟩ Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.571} @ ⟨17, 27⟩-⟨17, 31⟩ + [.] `Bool : some Sort.{?_uniq.441} @ ⟨17, 27⟩-⟨17, 31⟩ Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ b : Bool @ ⟨17, 23⟩-⟨17, 24⟩ - x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9563 + x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9571 Macro expansion x + 0 = x ===> binrel% Eq✝ (x + 0)x x + 0 = x : Prop @ ⟨17, 35⟩†-⟨17, 44⟩ @ Lean.Elab.Term.elabBinRel - x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.5829 + x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.6125 Macro expansion x + 0 ===> binop% HAdd.hAdd✝ x 0 - x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.elabBinOp - Macro expansion - binop% HAdd.hAdd✝ x 0 - ===> - HAdd.hAdd✝ x 0 - x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.elabApp - HAdd.hAdd : {α β γ : Type} → [self : HAdd α β γ] → α → β → γ @ ⟨17, 35⟩†-⟨17, 40⟩† - x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ @ Lean.Elab.Term.elabIdent - x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ - 0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit + x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.BinOp.elabBinOp' + x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ @ Lean.Elab.Term.elabIdent + x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ + 0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ fun x y b => @@ -115,20 +109,20 @@ [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.818} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.591} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ x : Nat @ ⟨21, 10⟩-⟨21, 11⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.820} @ ⟨21, 16⟩-⟨21, 19⟩ + [.] `Nat : some Sort.{?_uniq.593} @ ⟨21, 16⟩-⟨21, 19⟩ Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ y : Nat @ ⟨21, 12⟩-⟨21, 13⟩ Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent - [.] `Bool : some Sort.{?_uniq.823} @ ⟨21, 28⟩-⟨21, 32⟩ + [.] `Bool : some Sort.{?_uniq.596} @ ⟨21, 28⟩-⟨21, 32⟩ Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ b : Bool @ ⟨21, 24⟩-⟨21, 25⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.825} @ ⟨21, 36⟩-⟨21, 39⟩ + [.] `Nat : some Sort.{?_uniq.598} @ ⟨21, 36⟩-⟨21, 39⟩ Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ fun x y b => let x := (x + y, x - y); @@ -170,22 +164,22 @@ Prod.mk✝ (x + y) (x - y) (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩† - x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.5829 + x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.6125 Macro expansion x + y ===> binop% HAdd.hAdd✝ x y - x + y : Nat @ ⟨23, 19⟩†-⟨23, 24⟩ @ Lean.Elab.Term.elabBinOp + x + y : Nat @ ⟨23, 19⟩†-⟨23, 24⟩ @ Lean.Elab.Term.BinOp.elabBinOp' x : Nat @ ⟨23, 19⟩-⟨23, 20⟩ @ Lean.Elab.Term.elabIdent x : Nat @ ⟨23, 19⟩-⟨23, 20⟩ y : Nat @ ⟨23, 23⟩-⟨23, 24⟩ @ Lean.Elab.Term.elabIdent y : Nat @ ⟨23, 23⟩-⟨23, 24⟩ - x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.5925 + x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.6221 Macro expansion x - y ===> binop% HSub.hSub✝ x y - x - y : Nat @ ⟨23, 26⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabBinOp + x - y : Nat @ ⟨23, 26⟩†-⟨23, 31⟩ @ Lean.Elab.Term.BinOp.elabBinOp' x : Nat @ ⟨23, 26⟩-⟨23, 27⟩ @ Lean.Elab.Term.elabIdent x : Nat @ ⟨23, 26⟩-⟨23, 27⟩ y : Nat @ ⟨23, 30⟩-⟨23, 31⟩ @ Lean.Elab.Term.elabIdent @@ -209,29 +203,29 @@ let z1 := z + w; z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl Nat : Type @ ⟨24, 8⟩†-⟨24, 10⟩† @ Lean.Elab.Term.elabHole - z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.5829 + z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.6125 Macro expansion z + w ===> binop% HAdd.hAdd✝ z w - z + w : Nat @ ⟨24, 14⟩†-⟨24, 19⟩ @ Lean.Elab.Term.elabBinOp + z + w : Nat @ ⟨24, 14⟩†-⟨24, 19⟩ @ Lean.Elab.Term.BinOp.elabBinOp' z : Nat @ ⟨24, 14⟩-⟨24, 15⟩ @ Lean.Elab.Term.elabIdent z : Nat @ ⟨24, 14⟩-⟨24, 15⟩ w : Nat @ ⟨24, 18⟩-⟨24, 19⟩ @ Lean.Elab.Term.elabIdent w : Nat @ ⟨24, 18⟩-⟨24, 19⟩ z1 : Nat @ ⟨24, 8⟩-⟨24, 10⟩ - z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.5829 + z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.6125 Macro expansion z + z1 ===> binop% HAdd.hAdd✝ z z1 - z + z1 : Nat @ ⟨25, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabBinOp + z + z1 : Nat @ ⟨25, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.BinOp.elabBinOp' z : Nat @ ⟨25, 4⟩-⟨25, 5⟩ @ Lean.Elab.Term.elabIdent z : Nat @ ⟨25, 4⟩-⟨25, 5⟩ z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabIdent z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩ [Elab.info] command @ ⟨27, 0⟩-⟨28, 17⟩ @ Lean.Elab.Command.elabDeclaration - Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2258 + Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2315 Macro expansion Nat × Array (Array Nat) ===> @@ -239,10 +233,10 @@ Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩† Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.1520} @ ⟨27, 12⟩-⟨27, 15⟩ + [.] `Nat : some Type.{?_uniq.800} @ ⟨27, 12⟩-⟨27, 15⟩ Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.1519} @ ⟨27, 18⟩-⟨27, 23⟩ + [.] `Array : some Type.{?_uniq.799} @ ⟨27, 18⟩-⟨27, 23⟩ Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩ Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen Macro expansion @@ -250,17 +244,17 @@ ===> Array Nat Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Type.{?_uniq.1521} @ ⟨27, 25⟩-⟨27, 30⟩ + [.] `Array : some Type.{?_uniq.801} @ ⟨27, 25⟩-⟨27, 30⟩ Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.1522} @ ⟨27, 31⟩-⟨27, 34⟩ + [.] `Nat : some Type.{?_uniq.802} @ ⟨27, 31⟩-⟨27, 34⟩ Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩ Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp - [.] `Array : some Sort.{?_uniq.1524} @ ⟨27, 39⟩-⟨27, 44⟩ + [.] `Array : some Sort.{?_uniq.804} @ ⟨27, 39⟩-⟨27, 44⟩ Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Type.{?_uniq.1525} @ ⟨27, 45⟩-⟨27, 48⟩ + [.] `Nat : some Type.{?_uniq.805} @ ⟨27, 45⟩-⟨27, 48⟩ Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩ @@ -274,11 +268,11 @@ Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩ [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1568} @ ⟨30, 14⟩-⟨30, 15⟩ + [.] `B : some Sort.{?_uniq.848} @ ⟨30, 14⟩-⟨30, 15⟩ B : Type @ ⟨30, 14⟩-⟨30, 15⟩ arg : B @ ⟨30, 8⟩-⟨30, 11⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1570} @ ⟨30, 19⟩-⟨30, 22⟩ + [.] `Nat : some Sort.{?_uniq.850} @ ⟨30, 19⟩-⟨30, 22⟩ Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp arg : B @ ⟨31, 2⟩-⟨31, 5⟩ @@ -291,11 +285,11 @@ 0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent - [.] `Nat : some Sort.{?_uniq.1592} @ ⟨33, 12⟩-⟨33, 15⟩ + [.] `Nat : some Sort.{?_uniq.872} @ ⟨33, 12⟩-⟨33, 15⟩ Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ x : Nat @ ⟨33, 8⟩-⟨33, 9⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent - [.] `B : some Sort.{?_uniq.1594} @ ⟨33, 19⟩-⟨33, 20⟩ + [.] `B : some Sort.{?_uniq.874} @ ⟨33, 19⟩-⟨33, 20⟩ B : Type @ ⟨33, 19⟩-⟨33, 20⟩ { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out index 16aa45b45b..0676dd24f4 100644 --- a/tests/lean/macroStack.lean.expected.out +++ b/tests/lean/macroStack.lean.expected.out @@ -12,8 +12,6 @@ macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested ins macroStack.lean:17:0-17:6: error: failed to synthesize instance HAdd Nat String ?m with resulting expansion - HAdd.hAdd✝ (x + x✝) x✝¹ -while expanding binop% HAdd.hAdd✝ (x + x✝)x✝¹ while expanding (x + x✝) + x✝¹ diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out index 43e1b4b6d5..eff0a58127 100644 --- a/tests/lean/typeOf.lean.expected.out +++ b/tests/lean/typeOf.lean.expected.out @@ -1,9 +1,7 @@ -typeOf.lean:11:21-11:24: error: type mismatch - x + 1 -has type - Nat : Type -but is expected to have type - Bool : Type +typeOf.lean:11:21-11:24: error: failed to synthesize instance + HAdd Nat Nat Bool +typeOf.lean:12:0-12:5: error: failed to synthesize instance + HAdd Bool Nat Nat typeOf.lean:20:54-20:60: error: invalid reassignment, term has type Bool : Type but is expected to have type