max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: pattern hover information

Browse source 
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
This commit is contained in:
Leonardo de Moura 2022-04-08 14:38:56 -07:00
parent 4793c7e734
commit 3cf425ba52
17 changed files with 237 additions and 134 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

82
src/Lean/Elab/Match.lean
View file

@ -378,13 +378,6 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.as Pattern.val Pattern.arrayLit AltLHS MatcherResult)
private def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=
Core.transform e fun e =>
if let some e := inaccessible? e then
return TransformStep.visit e
else
return TransformStep.visit e
namespace ToDepElimPattern
private def throwInvalidPattern (e : Expr) : MetaM α :=
@ -438,15 +431,18 @@ private def withMVar (mvarId : MVarId) (x : M α) : M α := do
partial def normalize (e : Expr) : M Expr := do
match inaccessible? e with
| some e => processInaccessible e
| none =>
match patternWithRef? e with
| some (ref, e) => return mkPatternWithRef (← normalize e) ref
| none =>
match e.arrayLit? with
| some (α, lits) => mkArrayLit α (← lits.mapM normalize)
| none =>
if e.isAppOfArity ``_root_.namedPattern 4 then
if let some e := Match.isNamedPattern? e then
let x := e.getArg! 1
let p := e.getArg! 2
let h := e.getArg! 3
unless x.isFVar && h.isFVar do
unless x.consumeMData.isFVar && h.consumeMData.isFVar do
throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
addVar x
let p ← normalize p
@ -485,32 +481,35 @@ partial def normalize (e : Expr) : M Expr := do
return mkAppN e.getAppFn (params ++ fields))
where
addVar (e : Expr) : M Unit := do
let e ← erasePatternRefAnnotations e
unless (← get).patternVars.contains e do
modify fun s => { s with patternVars := s.patternVars.push e }
processVar (e : Expr) : M Expr := do
if (← get).patternVars.contains e then
return mkInaccessible e
let e' ← erasePatternRefAnnotations e
if (← get).patternVars.contains e' then
return mkInaccessible (← eraseInaccessibleAnnotations e)
else
if e.isMVar then
setMVarTag e.mvarId! (← read).userName
modify fun s => { s with patternVars := s.patternVars.push e }
if e'.isMVar then
setMVarTag e'.mvarId! (← read).userName
modify fun s => { s with patternVars := s.patternVars.push e' }
return e
processInaccessible (e : Expr) : M Expr := do
match e with
let e' ← erasePatternRefAnnotations e
match e' with
| Expr.fvar fvarId _ =>
if (← isExplicitPatternVar e) then
if (← isExplicitPatternVar e') then
processVar e
else
return mkInaccessible e
| _ =>
if e.getAppFn.isMVar then
let eNew ← instantiateMVars e
if eNew != e then
withMVar e.getAppFn.mvarId! <| processInaccessible eNew
else if e.isMVar then
withMVar e.mvarId! <| processVar e
if e'.getAppFn.isMVar then
let eNew ← instantiateMVars e'
if eNew != e' then
withMVar e'.getAppFn.mvarId! <| processInaccessible eNew
else if e'.isMVar then
withMVar e'.mvarId! <| processVar e'
else
throwInvalidPattern e
else
@ -542,7 +541,7 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
match e.arrayLit? with
| some (α, lits) => return Pattern.arrayLit α (← lits.mapM toPattern)
| none =>
if e.isAppOfArity ``_root_.namedPattern 4 then
if let some e := Match.isNamedPattern? e then
let p ← toPattern <| e.getArg! 2
match e.getArg! 1, e.getArg! 3 with
| Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
@ -603,6 +602,20 @@ where
modify fun s => { s with result := s.result.push e }
| _ => return ()
/--
Save pattern information in the info tree, and remove `patternWithRef?` annotations.
-/
def savePatternInfo (p : Expr) : TermElabM Expr :=
withReader (fun ctx => { ctx with inPattern := false }) do
let post (e : Expr) : TermElabM TransformStep := do
if let some (stx, e) := patternWithRef? e then
-- TODO: track whether we are inside of an inaccessible, and set `isBinder`
addTermInfo' stx e
return .done e
else
return .done e
transform p (post := post)
/--
Main method for `withDepElimPatterns`.
- `PatternVarDecls`: are the explicit pattern variables provided by the user.
@ -612,21 +625,23 @@ where
- `k` is the continuation that is executed in an updated local context with the all pattern variables (explicit and implicit). Note that, `patternVarDecls` are all
replaced since they may depend on implicit pattern variables (i.e., metavariables) that are converted into new free variables by this method.
-/
def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
partial def main (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
let explicitPatternVars := patternVarDecls.map fun decl => decl.fvarId
let (ps, s) ← ps.mapM normalize |>.run { explicitPatternVars } |>.run {}
let patternVars ← topSort s.patternVars
trace[Elab.match] "patternVars after topSort: {patternVars}"
for explicit in explicitPatternVars do
unless patternVars.any (· == mkFVar explicit) do
withInPattern do
throwError "invalid patterns, `{mkFVar explicit}` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching{indentD (MessageData.joinSep (ps.toList.map (MessageData.ofExpr .)) m!"\n\n")}"
let packed ← pack patternVars ps matchType
trace[Elab.match] "packed: {packed}"
let lctx := explicitPatternVars.foldl (init := (← getLCtx)) fun lctx d => lctx.erase d
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctx }) do
check packed
lambdaTelescope packed fun patternVars packed => do
unpack packed fun patternVars patterns matchType => do
let localDecls ← patternVars.mapM fun x => getLocalDecl x.fvarId!
let (matchType, patterns) := unpackMatchTypePatterns packed
trace[Elab.match] "patternVars: {patternVars}, matchType: {matchType}"
k localDecls (← patterns.mapM fun p => toPattern p) matchType
where
pack (patternVars : Array Expr) (ps : Array Expr) (matchType : Expr) : MetaM Expr := do
@ -642,7 +657,7 @@ where
```
-/
let setMVarsAt (e : Expr) : StateRefT (Array MVarId) MetaM Unit := do
let mvarIds ← setMVarUserNamesAt e patternVars
let mvarIds ← setMVarUserNamesAt (← erasePatternRefAnnotations e) patternVars
modify (· ++ mvarIds)
let go : StateRefT (Array MVarId) MetaM Expr := do
try
@ -653,6 +668,19 @@ where
resetMVarUserNames (← get)
go |>.run' #[]
unpack (packed : Expr) (k : (patternVars : Array Expr) → (patterns : Array Expr) → (matchType : Expr) → TermElabM α) : TermElabM α :=
let rec go (packed : Expr) (patternVars : Array Expr) : TermElabM α := do
match packed with
| .lam n d b _ =>
withLocalDeclD n (← erasePatternRefAnnotations (← eraseInaccessibleAnnotations d)) fun patternVar =>
go (b.instantiate1 patternVar) (patternVars.push patternVar)
| _ =>
let (matchType, patterns) := unpackMatchTypePatterns packed
let matchType ← erasePatternRefAnnotations (← eraseInaccessibleAnnotations matchType)
let patterns ← patterns.mapM (savePatternInfo ·)
k patternVars patterns matchType
go packed #[]
end ToDepElimPattern
def withDepElimPatterns (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do

6
src/Lean/Elab/PreDefinition/Eqns.lean
View file

@ -129,8 +129,10 @@ where
let go (e : Expr) (ω) : ST ω FVarIdSet := do
let ref ← ST.mkRef {}
e.forEach fun e => do
if e.isAppOfArity ``namedPattern 4 && e.appArg!.isFVar then
ST.Prim.Ref.modify ref (·.insert e.appArg!.fvarId!)
if let some e := Match.isNamedPattern? e then
let arg := e.appArg!.consumeMData
if arg.isFVar then
ST.Prim.Ref.modify ref (·.insert arg.fvarId!)
ST.Prim.Ref.get ref
runST (go e)

15
src/Lean/Elab/Term.lean
View file

@ -994,16 +994,21 @@ def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Op
return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType?, isBinder }
def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Expr := do
-- TODO: do not save info when inPattern is true, and store `stx` in `Expr.mdata`
withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
return e
if (← read).inPattern then
return mkPatternWithRef e stx
else
withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
return e
def addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit :=
discard <| addTermInfo stx e expectedType? lctx? elaborator isBinder
def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Sum Info MVarId)) : TermElabM Expr := do
-- TODO: do not save info when inPattern is true, and store `stx` in `Expr.mdata`
Elab.withInfoContext' x mkInfo
if (← read).inPattern then
let e ← x
return mkPatternWithRef e stx
else
Elab.withInfoContext' x mkInfo
/-
Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or

34
src/Lean/Expr.lean
View file

@ -1259,6 +1259,40 @@ def mkInaccessible (e : Expr) : Expr :=
def inaccessible? (e : Expr) : Option Expr :=
annotation? `_inaccessible e
private def patternRefAnnotationKey := `_patWithRef
/--
During elaboration expressions corresponding to pattern matching terms
are annotated with `Syntax` objects. This function returns `some (stx, p')` if
`p` is the pattern `p'` annotated with `stx`
-/
def patternWithRef? (p : Expr) : Option (Syntax × Expr) :=
match p with
| Expr.mdata d b _ =>
match d.find patternRefAnnotationKey with
| some (DataValue.ofSyntax stx) => some (stx, p.mdataExpr!)
| _ => none
| _ => none
/--
Annotate the pattern `p` with `stx`. This is an auxiliary annotation
for producing better hover information.
-/
def mkPatternWithRef (p : Expr) (stx : Syntax) : Expr :=
if patternWithRef? p |>.isSome then
p
else
mkMData (KVMap.empty.insert patternRefAnnotationKey (DataValue.ofSyntax stx)) p
/-- Return `some p` if `e` is an annotated pattern (`inaccessible?` or `patternWithRef?`) -/
def patternAnnotation? (e : Expr) : Option Expr :=
if let some e := inaccessible? e then
some e
else if let some (_, e) := patternWithRef? e then
some e
else
none
/--
Annotate `e` with the LHS annotation. The delaborator displays
expressions of the form `lhs = rhs` as `lhs` when they have this annotation.

6
src/Lean/Meta/ExprDefEq.lean
View file

@ -1381,16 +1381,16 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
-- ⊢ q ((fun x => x + 1) 0)
sorry
```
However, the inaccessible pattern annotation must be consumed.
However, pattern annotations (`inaccessible?` and `patternWithRef?`) must be consumed.
The frontend relies on the fact that is must not be propagated by `isDefEq`.
Thus, we consume it here. This is a bit hackish since it is very adhoc.
We might other annotations in the future that we should not preserve.
Perhaps, we should mark the annotation we do want to preserve ones
(e.g., hints for the pretty printer), and consume all other
-/
if let some t := inaccessible? t then
if let some t := patternAnnotation? t then
isDefEqQuick t s
else if let some s := inaccessible? s then
else if let some s := patternAnnotation? s then
isDefEqQuick t s
else if t == s then
return LBool.true

14
src/Lean/Meta/Match/Basic.lean
View file

@ -9,6 +9,16 @@ import Lean.Meta.Match.CaseArraySizes
namespace Lean.Meta.Match
def mkNamedPattern (x h p : Expr) : MetaM Expr :=
mkAppM ``namedPattern #[x, p, h]
def isNamedPattern? (e : Expr) : Option Expr :=
let e := e.consumeMData
if e.getAppNumArgs == 4 && e.getAppFn.consumeMData.isConstOf ``namedPattern then
some e
else
none
inductive Pattern : Type where
| inaccessible (e : Expr) : Pattern
| var (fvarId : FVarId) : Pattern
@ -44,7 +54,7 @@ where
| as fvarId p hId =>
-- TODO
if annotate then
mkAppM ``namedPattern #[mkFVar fvarId, (← visit p), mkFVar hId]
mkNamedPattern (mkFVar fvarId) (mkFVar hId) (← visit p)
else
visit p
| arrayLit type xs =>
@ -276,7 +286,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
| some (α, lits) =>
return Pattern.arrayLit α (← lits.mapM toPattern)
| none =>
if e.isAppOfArity ``namedPattern 4 then
if let some e := isNamedPattern? e then
let p ← toPattern <| e.getArg! 2
match e.getArg! 1, e.getArg! 3 with
| Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h

8
src/Lean/Meta/Match/MatchEqs.lean
View file

@ -53,10 +53,9 @@ def casesOnStuckLHS? (mvarId : MVarId) : MetaM (Option (Array MVarId)) := do
namespace Match
def unfoldNamedPattern (e : Expr) : MetaM Expr := do
let visit (e : Expr) : MetaM TransformStep := do
if e.isAppOfArity ``namedPattern 4 then
if let some e := isNamedPattern? e then
if let some eNew ← unfoldDefinition? e then
return TransformStep.visit eNew
return TransformStep.visit e
@ -103,7 +102,10 @@ where
isNamedPatternProof (type : Expr) (h : Expr) : Bool :=
Option.isSome <| type.find? fun e =>
e.isAppOfArity ``namedPattern 4 && e.appArg! == h
if let some e := isNamedPattern? e then
e.appArg! == h
else
false
namespace SimpH

6
src/Lean/Meta/Transform.lean
View file

@ -142,5 +142,11 @@ def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
| _ => return TransformStep.visit e
Core.transform e (pre := pre)
def eraseInaccessibleAnnotations (e : Expr) : CoreM Expr :=
Core.transform e (post := fun e => return TransformStep.done <| if let some e := inaccessible? e then e else e)
def erasePatternRefAnnotations (e : Expr) : CoreM Expr :=
Core.transform e (post := fun e => return TransformStep.done <| if let some (_, e) := patternWithRef? e then e else e)
end Meta
end Lean

4
src/Lean/PrettyPrinter/Delaborator/Basic.lean
View file

@ -6,6 +6,7 @@ Authors: Sebastian Ullrich
import Lean.KeyedDeclsAttribute
import Lean.ProjFns
import Lean.Syntax
import Lean.Meta.Transform
import Lean.Meta.Match.Match
import Lean.Elab.Term
import Lean.Elab.AuxDiscr
@ -264,6 +265,9 @@ end Delaborator
open Delaborator (OptionsPerPos topDownAnalyze Pos)
def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Syntax × Std.RBMap Pos Elab.Info compare) := do
/- Using `erasePatternAnnotations` here is a bit hackish, but we do it
`Expr.mdata` affects the delaborator. TODO: should we fix that? -/
let e ← Meta.erasePatternRefAnnotations e
trace[PrettyPrinter.delab.input] "{Std.format e}"
let mut opts ← getOptions
-- default `pp.proofs` to `true` if `e` is a proof

15
src/Lean/Util/Recognizers.lean
View file

@ -81,18 +81,19 @@ def isDIte (e : Expr) :=
partial def listLit? (e : Expr) : Option (Expr × List Expr) :=
let rec loop (e : Expr) (acc : List Expr) :=
if e.isAppOfArity ``List.nil 1 then
some (e.appArg!, acc.reverse)
else if e.isAppOfArity ``List.cons 3 then
loop e.appArg! (e.appFn!.appArg! :: acc)
if e.isAppOfArity' ``List.nil 1 then
some (e.appArg!', acc.reverse)
else if e.isAppOfArity' ``List.cons 3 then
loop e.appArg!' (e.appFn!'.appArg!' :: acc)
else
none
loop e []
def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
match e.app2? ``List.toArray with
| some (_, e) => e.listLit?
| none => none
if e.isAppOfArity' ``List.toArray 2 then
listLit? e.appArg!'
else
none
/-- Recognize `α × β` -/
def prod? (e : Expr) : Option (Expr × Expr) :=

34
tests/lean/1018unknowMVarIssue.lean.expected.out
View file

@ -40,33 +40,23 @@ a : α
[.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
@Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
?α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
Fam2.any : Fam2 ?α ?α @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabApp
[.] `Fam2.any : some Fam2 ([mdata _inaccessible:1 ?_uniq.651]) ([mdata _inaccessible:1 ?_uniq.652]) @ ⟨9, 4⟩-⟨9, 12⟩
@Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabInaccessible
?α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† @ Lean.Elab.Term.elabHole
a : ?α @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
a : ?α @ ⟨8, 2⟩†-⟨10, 19⟩†
[.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.654]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.655]]]) @ ⟨9, 4⟩-⟨9, 12⟩
α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
[.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
[.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabInaccessible
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabSyntheticHole
Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ @ Lean.Elab.Term.elabApp
[.] `Fam2.nat : some Fam2 ([mdata _inaccessible:1 ?_uniq.683]) ([mdata _inaccessible:1 ?_uniq.684]) @ ⟨10, 4⟩-⟨10, 12⟩
Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
n : Nat @ ⟨10, 13⟩-⟨10, 14⟩ @ Lean.Elab.Term.elabIdent
n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† @ Lean.Elab.Term.elabIdent
a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
[.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.686]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.687]]]) @ ⟨10, 4⟩-⟨10, 12⟩
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
n : Nat @ ⟨10, 13⟩-⟨10, 14⟩
Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
a : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
@_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩

12
tests/lean/infoTree.lean.expected.out
View file

@ -213,14 +213,10 @@
@Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
[.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
[.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
(z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩ @ Lean.Elab.Term.elabApp
@Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole
Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩† @ Lean.Elab.Term.elabHole
z : Nat @ ⟨23, 9⟩-⟨23, 10⟩ @ Lean.Elab.Term.elabIdent
z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
w : Nat @ ⟨23, 12⟩-⟨23, 13⟩ @ Lean.Elab.Term.elabIdent
w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
(z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩
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

15
tests/lean/interactive/matchPatternHover.lean Normal file
View file

@ -0,0 +1,15 @@
inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
| nil : HList β []
| cons : β i → HList β is → HList β (i::is)
infix:67 " :: " => HList.cons
inductive Member : α → List α → Type
| head : Member a (a::as)
| tail : Member a bs → Member a (b::bs)
def HList.get : HList β is → Member i is → β i
| a::as, .head => a
--v textDocument/hover
| a::as, .tail h => as.get h
--^ textDocument/hover

10
tests/lean/interactive/matchPatternHover.lean.expected.out Normal file
View file

@ -0,0 +1,10 @@
{"textDocument": {"uri": "file://matchPatternHover.lean"},
"position": {"line": 13, "character": 7}}
{"range":
{"start": {"line": 13, "character": 7}, "end": {"line": 13, "character": 9}},
"contents": {"value": "```lean\nas : HList β is✝\n```", "kind": "markdown"}}
{"textDocument": {"uri": "file://matchPatternHover.lean"},
"position": {"line": 13, "character": 17}}
{"range":
{"start": {"line": 13, "character": 17}, "end": {"line": 13, "character": 18}},
"contents": {"value": "```lean\nh : Member i is✝\n```", "kind": "markdown"}}

92
tests/lean/jason1.lean.expected.out
View file

@ -1,49 +1,3 @@
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
@TySyntaxLayer.arrow G T EG getCtx
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
@ -108,6 +62,52 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
@TySyntaxLayer.arrow G T EG getCtx
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:

3
tests/lean/run/match1.lean
View file

@ -96,7 +96,8 @@ def Vec.mapHead1 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β
def Vec.mapHead2 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
| _, nil, nil, f => none
| _, @cons _ n a as, cons b bs, f => some (f a b)
#eval checkWithMkMatcherInput ``Vec.mapHead2.match_1
set_option pp.match false in
#print Vec.mapHead2 -- reused Vec.mapHead1.match_1
def Vec.mapHead3 {α β δ} : {n : Nat} → Vec α n → Vec β n → (α → β → δ) → Option δ
| _, nil, nil, f => none

15
tests/lean/syntheticHolesAsPatterns.lean.expected.out
View file

@ -11,8 +11,13 @@ context:
α β : Type
a✝ : α
x : Fam2 α β
a : Nat
n : Nat
a n : Nat
⊢ Nat
syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
context:
α β : Type
x : Fam2 α β
n a : Nat
⊢ Nat
syntheticHolesAsPatterns.lean:12:18-12:19: error: don't know how to synthesize placeholder
context:
@ -21,9 +26,3 @@ x : Fam2 α✝ β
α : Type
a : α
⊢ α
syntheticHolesAsPatterns.lean:13:18-13:19: error: don't know how to synthesize placeholder
context:
α β : Type
x : Fam2 α β
n a : Nat
⊢ Nat