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

feat: elaborate Term.binderTactic at structure declarations

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-27 14:49:23 -07:00
parent 3b5e762882
commit 0ccd110eb4
1 changed files with 30 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/Lean/Elab/Structure.lean
View file

@ -12,6 +12,7 @@ import Lean.Elab.DeclModifiers
import Lean.Elab.DeclUtil
import Lean.Elab.Inductive
import Lean.Elab.DeclarationRange
import Lean.Elab.Binders
namespace Lean.Elab.Command
@ -142,10 +143,10 @@ def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
/-
```
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) >> ")"
def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault)
def structFields := leading_parser many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
```
-/
@ -169,20 +170,39 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
if fieldModifiers.isProtected && structModifiers.isPrivate then
throwError "invalid 'protected' field in a 'private' structure"
let inferMod := !fieldBinder[3].isNone
let (binders, type?) :=
let (binders, type?) ←
if binfo == BinderInfo.default then
expandOptDeclSig fieldBinder[4]
let (binders, type?) := expandOptDeclSig fieldBinder[4]
let optBinderTacticDefault := fieldBinder[5]
if optBinderTacticDefault.isNone then
pure (binders, type?)
else if optBinderTacticDefault[0].getKind != ``Parser.Term.binderTactic then
pure (binders, type?)
else
let binderTactic := optBinderTacticDefault[0]
match type? with
| none => throwErrorAt binderTactic "invalid field declaration, type must be provided when auto-param (tactic) is used"
| some type =>
let tac := binderTactic[2]
let name ← Term.declareTacticSyntax tac
let type ← `(autoParam $type $(mkIdentFrom tac name))
pure (binders, some type)
else
let (binders, type) := expandDeclSig fieldBinder[4]
(binders, some type)
let value? :=
if binfo != BinderInfo.default then none
pure (binders, some type)
let value? ←
if binfo != BinderInfo.default then
pure none
else
let optBinderDefault := fieldBinder[5]
if optBinderDefault.isNone then none
let optBinderTacticDefault := fieldBinder[5]
-- trace[Elab.struct] ">>> {optBinderTacticDefault}"
if optBinderTacticDefault.isNone then
pure none
else if optBinderTacticDefault[0].getKind == ``Parser.Term.binderTactic then
pure none
else
-- binderDefault := leading_parser " := " >> termParser
some optBinderDefault[0][1]
pure (some optBinderTacticDefault[0][1])
let idents := fieldBinder[2].getArgs
idents.foldlM (init := views) fun (views : Array StructFieldView) ident => withRef ident do
let name := ident.getId