From e1fa9c131cbca5cc244f6e5012d6bc043ac7043d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Mar 2022 16:50:21 -0800 Subject: [PATCH] feat: inferring namespace from expected type a la Swift Now that `PatternVars.lean` has been redesigned, it is feasible to implement issue #944. closes #944 --- RELEASES.md | 25 +++++++++++++++++++++++++ src/Lean/Elab/App.lean | 20 +++++++++++++++++++- src/Lean/Elab/PatternVar.lean | 12 +++++++++++- tests/lean/run/944.lean | 35 +++++++++++++++++++++++++++++++++++ 4 files changed, 90 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/944.lean diff --git a/RELEASES.md b/RELEASES.md index 2b9bc95821..a0ea3c48b2 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -188,3 +188,28 @@ def head2 (x : Vector α (n+1)) : α := match x with | a :: as => a -- `::` is `Vector.cons` here ``` + +* New notation `.` based on Swift. The namespace is inferred from the expected type. Examples: +```lean +def f (x : Nat) : Except String Nat := + if x > 0 then + .ok x + else + .error "x is zero" + +namespace Lean.Elab +open Lsp + +def identOf : Info → Option (RefIdent × Bool) + | .ofTermInfo ti => match ti.expr with + | .const n .. => some (.const n, ti.isBinder) + | .fvar id .. => some (.fvar id, ti.isBinder) + | _ => none + | .ofFieldInfo fi => some (.const fi.projName, false) + | _ => none + +def isImplicit (bi : BinderInfo) : Bool := + bi matches .implicit + +end Lean.Elab +``` diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index d25823d627..ee731c3577 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -820,7 +820,7 @@ where | field::fields, false => LVal.fieldName field field.getId.toString none fIdent :: toLVals fields false private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg) - (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : TermElabM (Array (TermElabResult Expr)) := + (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : TermElabM (Array (TermElabResult Expr)) := do if f.getKind == choiceKind then -- Set `errToSorry` to `false` when processing choice nodes. See comment above about the interaction between `errToSorry` and `observing`. withReader (fun ctx => { ctx with errToSorry := false }) do @@ -853,6 +853,23 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc | `(@$t) => throwUnsupportedSyntax -- invalid occurrence of `@` | `(_) => throwError "placeholders '_' cannot be used where a function is expected" + | `(.$id:ident) => + tryPostponeIfNoneOrMVar expectedType? + match expectedType? with + | none => throwError "invalid dotted identifier notation, expected type must be known" + | some expectedType => + if let Expr.const declName .. := (← instantiateMVars expectedType).getAppFn then + let idNew := declName ++ id.getId.eraseMacroScopes + unless (← getEnv).contains idNew do + throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}" + let fConst ← mkConst idNew + addTermInfo f fConst + let s ← observing do + let e ← elabAppLVals fConst lvals namedArgs args expectedType? explicit ellipsis + if overloaded then ensureHasType expectedType? e else pure e + return acc.push s + else + throwError "invalid dotted identifier notation, expected type is not of the form (C ...) where C is a constant{indentExpr expectedType}" | _ => do let catchPostpone := !overloaded /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms. @@ -954,6 +971,7 @@ private def elabAtom : TermElab := fun stx expectedType? => @[builtinTermElab ident] def elabIdent : TermElab := elabAtom /-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/ @[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom +@[builtinTermElab dotIdent] def elabDotIdent : TermElab := elabAtom /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/ @[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom /-- `e |>.x` is a shorthand for `(e).x`. It is especially useful for avoiding parentheses with repeated applications. -/ diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 2c6296a242..2aa5b7cf61 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -142,6 +142,8 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc else if k == ``Lean.Parser.Term.anonymousCtor then let elems ← stx[1].getArgs.mapSepElemsM collect return stx.setArg 1 <| mkNullNode elems + else if k == ``Lean.Parser.Term.dotIdent then + return stx else if k == ``Lean.Parser.Term.structInst then /- ``` @@ -243,7 +245,15 @@ where processCtorApp (stx : Syntax) : M Syntax := do let (f, namedArgs, args, ellipsis) ← expandApp stx true - processCtorAppCore f namedArgs args ellipsis + if f.getKind == ``Parser.Term.dotIdent then + unless namedArgs.isEmpty do + throwError "invalid dotted notation in a pattern, named arguments are not supported yet" + let mut argsNew ← args.mapM fun | Arg.stx arg => collect arg | _ => unreachable! + if ellipsis then + argsNew := argsNew.push (mkNode ``Parser.Term.ellipsis #[mkAtomFrom stx ".."]) + return Syntax.mkApp f argsNew + else + processCtorAppCore f namedArgs args ellipsis processCtor (stx : Syntax) : M Syntax := do processCtorAppCore stx #[] #[] false diff --git a/tests/lean/run/944.lean b/tests/lean/run/944.lean new file mode 100644 index 0000000000..3b133a7472 --- /dev/null +++ b/tests/lean/run/944.lean @@ -0,0 +1,35 @@ +import Lean + +def f1 (x : Nat) : Except String Nat := + if x > 0 then + .ok x + else + .error "argument is zero" + +namespace Lean.Elab +open Lsp + +def identOf : Info → Option (RefIdent × Bool) + | .ofTermInfo ti => match ti.expr with + | .const n .. => some (.const n, ti.isBinder) + | .fvar id .. => some (.fvar id, ti.isBinder) + | _ => none + | .ofFieldInfo fi => some (.const fi.projName, false) + | _ => none + +def isConst (e : Expr) : Bool := + e matches .const .. + +def isImplicit (bi : BinderInfo) : Bool := + bi matches .implicit + +end Lean.Elab + +def f2 (xs : List Nat) : List Nat := + .map (. + 1) xs + +def f3 : Nat := + .zero + +def f4 (x : Nat) : Nat := + .succ x