From 0b0106206f9f1678989e2c605018350a5818d6ae Mon Sep 17 00:00:00 2001 From: Parth Shastri <31370288+cppio@users.noreply.github.com> Date: Fri, 10 Jan 2025 15:06:54 -0500 Subject: [PATCH 1/2] fix: allow dot idents to resolve to local names --- src/Lean/Elab/App.lean | 13 ++++++++----- tests/lean/6601.lean | 26 ++++++++++++++++++++++++++ tests/lean/6601.lean.expected.out | 0 3 files changed, 34 insertions(+), 5 deletions(-) create mode 100644 tests/lean/6601.lean create mode 100644 tests/lean/6601.lean.expected.out diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 23a744a9ff11..566fec4d63af 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1474,7 +1474,7 @@ where | field::fields, false => .fieldName field field.getId.getString! none fIdent :: toLVals fields false /-- Resolve `(.$id:ident)` using the expected type to infer namespace. -/ -private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Name := do +private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do tryPostponeIfNoneOrMVar expectedType? let some expectedType := expectedType? | throwError "invalid dotted identifier notation, expected type must be known" @@ -1489,7 +1489,7 @@ where withForallBody body k else k body - go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Name := do + go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Expr := do let resultType ← instantiateMVars resultType let resultTypeFn := resultType.cleanupAnnotations.getAppFn try @@ -1497,9 +1497,12 @@ where let .const declName .. := resultTypeFn.cleanupAnnotations | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}" let idNew := declName ++ id.getId.eraseMacroScopes - unless (← getEnv).contains idNew do + if (← getEnv).contains idNew then + mkConst idNew + else if let some (fvar, []) ← resolveLocalName idNew then + return fvar + else throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}" - return idNew catch | ex@(.error ..) => match (← unfoldDefinition? resultType) with @@ -1548,7 +1551,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra | `(_) => throwError "placeholders '_' cannot be used where a function is expected" | `(.$id:ident) => addCompletionInfo <| CompletionInfo.dotId f id.getId (← getLCtx) expectedType? - let fConst ← mkConst (← resolveDotName id expectedType?) + let fConst ← resolveDotName id expectedType? let s ← observing do -- Use (force := true) because we want to record the result of .ident resolution even in patterns let fConst ← addTermInfo f fConst expectedType? (force := true) diff --git a/tests/lean/6601.lean b/tests/lean/6601.lean new file mode 100644 index 000000000000..4121d4fd5876 --- /dev/null +++ b/tests/lean/6601.lean @@ -0,0 +1,26 @@ +/-! Dot ident notation should resolve mutual definitions -/ + +mutual + +inductive Even + | zero + | succ (n : Odd) + deriving Inhabited + +inductive Odd + | succ (n : Even) + deriving Inhabited + +end + +mutual + +def Even.ofNat : Nat → Even + | 0 => .zero + | n + 1 => .succ (.ofNat n) + +def Odd.ofNat : Nat → Odd + | 0 => panic! "invalid input" + | n + 1 => .succ (.ofNat n) + +end diff --git a/tests/lean/6601.lean.expected.out b/tests/lean/6601.lean.expected.out new file mode 100644 index 000000000000..e69de29bb2d1 From 918c34d8fde843df7b4d1d4f0ba3dd19cd0d667b Mon Sep 17 00:00:00 2001 From: Parth Shastri <31370288+cppio@users.noreply.github.com> Date: Sun, 12 Jan 2025 11:23:59 -0500 Subject: [PATCH 2/2] chore: adaptation for leanprover/lean4#6602 --- src/Lean/Parser/Basic.lean | 4 ++-- src/Lean/Server/Requests.lean | 2 +- src/Std/Time/Date/Unit/Month.lean | 2 +- src/Std/Time/Date/Unit/Year.lean | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 7649171e922b..857b47f40396 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1583,8 +1583,8 @@ namespace TokenMap def insert (map : TokenMap α) (k : Name) (v : α) : TokenMap α := match map.find? k with - | none => .insert map k [v] - | some vs => .insert map k (v::vs) + | none => RBMap.insert map k [v] + | some vs => RBMap.insert map k (v::vs) instance : Inhabited (TokenMap α) where default := RBMap.empty diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index e57fd94ce477..ea5f62f0b645 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -97,7 +97,7 @@ abbrev RequestT m := ReaderT RequestContext <| ExceptT RequestError m /-- Workers execute request handlers in this monad. -/ abbrev RequestM := ReaderT RequestContext <| EIO RequestError -abbrev RequestTask.pure (a : α) : RequestTask α := .pure (.ok a) +abbrev RequestTask.pure (a : α) : RequestTask α := Task.pure (.ok a) instance : MonadLift IO RequestM where monadLift x := do diff --git a/src/Std/Time/Date/Unit/Month.lean b/src/Std/Time/Date/Unit/Month.lean index d26210080621..16d27d8d69a1 100644 --- a/src/Std/Time/Date/Unit/Month.lean +++ b/src/Std/Time/Date/Unit/Month.lean @@ -67,7 +67,7 @@ Creates an `Offset` from a natural number. -/ @[inline] def ofNat (data : Nat) : Offset := - .ofNat data + Int.ofNat data /-- Creates an `Offset` from an integer. diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean index 94ac4d67ea49..eef7c2010ca2 100644 --- a/src/Std/Time/Date/Unit/Year.lean +++ b/src/Std/Time/Date/Unit/Year.lean @@ -56,7 +56,7 @@ Creates an `Offset` from a natural number. -/ @[inline] def ofNat (data : Nat) : Offset := - .ofNat data + Int.ofNat data /-- Creates an `Offset` from an integer.