From b6ef65d8fd0be4f8d33ecb1daaab9d5155255935 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Dec 2021 07:52:25 -0800 Subject: [PATCH] fix: `where` structure instance parser closes #753 --- src/Lean/Elab/MutualDef.lean | 19 +++++++++---------- src/Lean/Parser/Command.lean | 7 ++++++- tests/lean/run/753.lean | 8 ++++++++ 3 files changed, 23 insertions(+), 11 deletions(-) create mode 100644 tests/lean/run/753.lean diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index d9e11f2ada..12e401d213 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -156,13 +156,12 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) ( k fvars loop 0 #[] -private def expandWhereDeclsAsStructInst : Macro - | `(whereDecls|where $[$decls:letRecDecl$[;]?]*) => do +private def expandWhereStructInst : Macro + | `(Parser.Command.whereStructInst|where $[$decls:letDecl$[;]?]*) => do let letIdDecls ← decls.mapM fun stx => match stx with - | `(letRecDecl|$attrs:attributes $decl:letDecl) => Macro.throwErrorAt stx "attributes are 'where' elements are currently not supported here" - | `(letRecDecl|$decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here" - | `(letRecDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl - | `(letRecDecl|$decl:letIdDecl) => pure decl + | `(letDecl|$decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here" + | `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl + | `(letDecl|$decl:letIdDecl) => pure decl | _ => Macro.throwUnsupported let structInstFields ← letIdDecls.mapM fun | stx@`(letIdDecl|$id:ident $[$binders]* $[: $ty?]? := $val) => withRef stx do @@ -184,12 +183,12 @@ def declVal := declValSimple <|> declValEqns <|> Term.whereDecls ``` -/ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal do - if declVal.isOfKind `Lean.Parser.Command.declValSimple then + if declVal.isOfKind ``Lean.Parser.Command.declValSimple then expandWhereDeclsOpt declVal[2] declVal[1] - else if declVal.isOfKind `Lean.Parser.Command.declValEqns then + else if declVal.isOfKind ``Lean.Parser.Command.declValEqns then expandMatchAltsWhereDecls declVal[0] - else if declVal.isOfKind `Lean.Parser.Term.whereDecls then - expandWhereDeclsAsStructInst declVal + else if declVal.isOfKind ``Lean.Parser.Command.whereStructInst then + expandWhereStructInst declVal else if declVal.isMissing then Macro.throwErrorAt declVal "declaration body is missing" else diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 6d993635bc..9f55bcb732 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -54,7 +54,12 @@ def declSig := leading_parser many (ppSpace >> (Term.simpleBinderWithou def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls def declValEqns := leading_parser Term.matchAltsWhereDecls -def declVal := declValSimple <|> declValEqns <|> Term.whereDecls +def whereStructInst := leading_parser "where " >> many1Indent (group (Term.letDecl >> optional ";")) +/- + Remark: we should not use `Term.whereDecls` at `declVal` because `Term.whereDecls` is defined using `Term.letRecDecl` which may contain attributes. + Issue #753 showns an example that fails to be parsed when we used `Term.whereDecls`. +-/ +def declVal := declValSimple <|> declValEqns <|> whereStructInst def «abbrev» := leading_parser "abbrev " >> declId >> optDeclSig >> declVal def optDefDeriving := optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") def «def» := leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving >> terminationSuffix diff --git a/tests/lean/run/753.lean b/tests/lean/run/753.lean new file mode 100644 index 0000000000..50ca97b1e6 --- /dev/null +++ b/tests/lean/run/753.lean @@ -0,0 +1,8 @@ +inductive Val +| mk : Nat -> Val + +instance : Inhabited Val where +default := Val.mk 0 + +@[simp] +theorem true_iff_true : True <-> True := Iff.intro (fun _ => trivial) (fun _ => trivial)