Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid simpleBinder nesting #1296

Merged
merged 2 commits into from
Jul 8, 2022
Merged

Avoid simpleBinder nesting #1296

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
38b179c
refactor: avoid nested sequence in `simpleBinder`
Kha Jul 7, 2022
32d26ad
chore: update stage0
Kha Jul 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 28 additions & 22 deletions src/Lean/Elab/Binders.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,11 +106,9 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=

private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
let k := stx.getKind
if k == ``Lean.Parser.Term.simpleBinder then
-- binderIdent+ >> optType
let ids ← getBinderIds stx[0]
let optType := stx[1]
ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := expandOptType id optType, bi := BinderInfo.default }
if stx.isIdent || k == ``hole then
-- binderIdent
pure #[{ id := (← expandBinderIdent stx), type := mkHole stx, bi := BinderInfo.default }]
else if k == ``Lean.Parser.Term.explicitBinder then
-- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
let ids ← getBinderIds stx[1]
Expand Down Expand Up @@ -191,7 +189,7 @@ def elabBindersEx {α} (binders : Array Syntax) (k : Array (Syntax × Expr) →
elabBindersAux binders k

/--
Elaborate the given binders (i.e., `Syntax` objects for `simpleBinder <|> bracketedBinder`),
Elaborate the given binders (i.e., `Syntax` objects for `bracketedBinder`),
update the local context, set of local instances, reset instance chache (if needed), and then
execute `k` with the updated context.
The local context will only be included inside `k`.
Expand All @@ -206,6 +204,18 @@ def elabBinders (binders : Array Syntax) (k : Array Expr → TermElabM α) : Ter
def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
elabBinders #[binder] fun fvars => x fvars[0]!

def expandSimpleBinderWithType (type : Term) (binder : Syntax) : MacroM Syntax :=
if binder.isOfKind ``hole || binder.isIdent then
`(bracketedBinder| ($binder : $type))
else
Macro.throwErrorAt type "unexpected type ascription"

@[builtinMacro Lean.Parser.Term.forall] def expandForall : Macro
| `(forall $binders* : $ty, $term) => do
let binders ← binders.mapM (expandSimpleBinderWithType ty)
`(forall $binders*, $term)
| _ => Macro.throwUnsupported

@[builtinTermElab «forall»] def elabForall : TermElab := fun stx _ =>
match stx with
| `(forall $binders*, $term) =>
Expand Down Expand Up @@ -286,17 +296,13 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
let (binders, newBody, _) ← loop body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder))
let newBody ← `(match $major:ident with | $pattern => $newBody)
pure (binders, newBody, true)
match binder with
| Syntax.node _ ``Lean.Parser.Term.implicitBinder _ => loop body (i+1) (newBinders.push binder)
| Syntax.node _ ``Lean.Parser.Term.strictImplicitBinder _ => loop body (i+1) (newBinders.push binder)
| Syntax.node _ ``Lean.Parser.Term.instBinder _ => loop body (i+1) (newBinders.push binder)
| Syntax.node _ ``Lean.Parser.Term.explicitBinder _ => loop body (i+1) (newBinders.push binder)
| Syntax.node _ ``Lean.Parser.Term.simpleBinder _ => loop body (i+1) (newBinders.push binder)
| Syntax.node _ ``Lean.Parser.Term.hole _ =>
let ident ← mkFreshIdent binder
let type := binder
loop body (i+1) (newBinders.push <| mkExplicitBinder ident type)
| Syntax.node _ ``Lean.Parser.Term.paren _ =>
match binder.getKind with
| ``Lean.Parser.Term.implicitBinder
| ``Lean.Parser.Term.strictImplicitBinder
| ``Lean.Parser.Term.instBinder
| ``Lean.Parser.Term.explicitBinder
| ``Lean.Parser.Term.hole | `ident => loop body (i+1) (newBinders.push binder)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice. It is great to see new features making our code cleaner :)

| ``Lean.Parser.Term.paren =>
-- `(` (termParser >> parenSpecial)? `)`
-- parenSpecial := (tupleTail <|> typeAscription)?
let binderBody := binder[1]
Expand Down Expand Up @@ -327,9 +333,6 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
match (← getFunBinderIds? term) with
| some idents => loop body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type))
| none => processAsPattern ()
| Syntax.ident .. =>
let type := mkHole binder
loop body (i+1) (newBinders.push <| mkExplicitBinder binder type)
| _ => processAsPattern ()
else
pure (newBinders, body, false)
Expand Down Expand Up @@ -541,7 +544,10 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
loop (getMatchAltsNumPatterns matchAlts) #[]

@[builtinMacro Lean.Parser.Term.fun] partial def expandFun : Macro
| `(fun $binders* => $body) => do
| `(fun $binders* : $ty => $body) => do
let binders ← binders.mapM (expandSimpleBinderWithType ty)
`(fun $binders* => $body)
| `(fun $binders* => $body) => do -- if there is a type ascription, we assume all binders are already simple
let (binders, body, expandedPattern) ← expandFunBinders binders body
if expandedPattern then
`(fun $binders* => $body)
Expand All @@ -552,7 +558,7 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=

open Lean.Elab.Term.Quotation in
@[builtinQuotPrecheck Lean.Parser.Term.fun] def precheckFun : Precheck
| `(fun $binders* => $body) => do
| `(fun $binders* $[: $ty?]? => $body) => do
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we use _ty to avoid the warning from the unused variable linter?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, not sure why I didn't see the warning. Will fix when I'm home.

let (binders, body, _) ← liftMacroM <| expandFunBinders binders body
let mut ids := #[]
for b in binders do
Expand Down
4 changes: 2 additions & 2 deletions src/Lean/Elab/Do.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool :=
else if k == ``Lean.Parser.Term.letEqnsDecl then
true
else if k == ``Lean.Parser.Term.letIdDecl then
-- letIdLhs := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
-- letIdLhs := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType
let binders := letDeclArg[1]
binders.getNumArgs > 0
else
Expand Down Expand Up @@ -615,7 +615,7 @@ def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
let arg := doHave[1][0]
if arg.getKind == ``Lean.Parser.Term.haveIdDecl then
-- haveIdDecl := leading_parser atomic (haveIdLhs >> " := ") >> termParser
-- haveIdLhs := optional (ident >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder))) >> optType
-- haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType
return #[← getHaveIdLhsVar arg[0]]
else if arg.getKind == ``Lean.Parser.Term.letPatDecl then
getLetPatDeclVars arg
Expand Down
4 changes: 2 additions & 2 deletions src/Lean/Elab/MutualDef.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ private def isMultiConstant? (views : Array DefView) : Option (List Name) :=
if views.size == 1 &&
views[0]!.kind == DefKind.opaque &&
views[0]!.binders.getArgs.size > 0 &&
views[0]!.binders.getArgs.all (·.getKind == ``Parser.Term.simpleBinder) then
some <| (views[0]!.binders.getArgs.toList.map (fun stx => stx[0].getArgs.toList.map (·.getId))).join
views[0]!.binders.getArgs.all (·.isIdent) then
some (views[0]!.binders.getArgs.toList.map (·.getId))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice.

else
none

Expand Down
4 changes: 2 additions & 2 deletions src/Lean/Parser/Command.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ def «partial» := leading_parser "partial "
def «nonrec» := leading_parser "nonrec "
def declModifiers (inline : Bool) := leading_parser optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional («partial» <|> «nonrec»)
def declId := leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
def declSig := leading_parser many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := leading_parser many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
def declValSimple := leading_parser " :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
def declValEqns := leading_parser Term.matchAltsWhereDecls
def whereStructField := leading_parser Term.letDecl
Expand Down
16 changes: 5 additions & 11 deletions src/Lean/Parser/Term.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,9 +131,8 @@ Note that we did not add a `explicitShortBinder` parser since `(α) → α →
-/
@[builtinTermParser] def depArrow := leading_parser:25 bracketedBinder true >> unicodeSymbol " → " " -> " >> termParser

def simpleBinder := leading_parser many1 binderIdent >> optType
@[builtinTermParser]
def «forall» := leading_parser:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
def «forall» := leading_parser:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >> optType >> ", " >> termParser

def matchAlt (rhsParser : Parser := termParser) : Parser :=
leading_parser (withAnonymousAntiquot := false)
Expand Down Expand Up @@ -162,10 +161,9 @@ def motive := leading_parser atomic ("(" >> nonReservedSymbol "motive" >> " := "

def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <| atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
def funStrictImplicitBinder := atomic (lookahead (strictImplicitLeftBracket >> many1 binderIdent >> (symbol " : " <|> strictImplicitRightBracket))) >> strictImplicitBinder
def funSimpleBinder := withAntiquot (mkAntiquot "simpleBinder" ``simpleBinder) <| atomic (lookahead (many1 binderIdent >> " : ")) >> simpleBinder
def funBinder : Parser := withAntiquot (mkAntiquot "funBinder" `Lean.Parser.Term.funBinder (isPseudoKind := true)) (funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec)
def funBinder : Parser := withAntiquot (mkAntiquot "funBinder" `Lean.Parser.Term.funBinder (isPseudoKind := true)) (funStrictImplicitBinder <|> funImplicitBinder <|> instBinder <|> termParser maxPrec)
-- NOTE: we disable anonymous antiquotations to ensure that `fun $b => ...` remains a `term` antiquotation
def basicFun : Parser := leading_parser (withAnonymousAntiquot := false) ppGroup (many1 (ppSpace >> funBinder) >> " =>") >> ppSpace >> termParser
def basicFun : Parser := leading_parser (withAnonymousAntiquot := false) ppGroup (many1 (ppSpace >> funBinder) >> optType >> " =>") >> ppSpace >> termParser
@[builtinTermParser] def «fun» := leading_parser:maxPrec ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)

def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
Expand All @@ -179,11 +177,7 @@ def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "wi
-- note that we cannot use ```"``"``` as a new token either because it would break `precheckedQuot`
@[builtinTermParser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident

-- same shape and (antiquotation) kind as `simpleBinder`
def simpleBinderWithoutType := nodeWithAntiquot "simpleBinder" ``simpleBinder (anonymous := true)
(many1 binderIdent >> pushNone)

def letIdBinder := withAntiquot (mkAntiquot "letIdBinder" `Lean.Parser.Term.letIdBinder (isPseudoKind := true)) (simpleBinderWithoutType <|> bracketedBinder)
def letIdBinder := withAntiquot (mkAntiquot "letIdBinder" `Lean.Parser.Term.letIdBinder (isPseudoKind := true)) (binderIdent <|> bracketedBinder)
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
def letIdLhs : Parser := ident >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >> many (ppSpace >> letIdBinder) >> optType
def letIdDecl := leading_parser (withAnonymousAntiquot := false) atomic (letIdLhs >> " := ") >> termParser
Expand All @@ -210,7 +204,7 @@ def letDecl := leading_parser (withAnonymousAntiquot := false) notFollowedBy
@[builtinTermParser] def «let_tmp» := leading_parser:leadPrec withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser

instance : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) where
coe stx := ⟨stx⟩ -- `simpleBinderWithoutType` prevents using a proper quotation for this
coe stx := ⟨stx⟩

-- like `let_fun` but with optional name
def haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType
Expand Down
2 changes: 1 addition & 1 deletion src/lake
Open in desktop
Submodule lake updated 2 files
+1 −5 Lake/DSL/DeclUtil.lean
+7 −7 Lake/DSL/Script.lean
50 changes: 28 additions & 22 deletions stage0/src/Lean/Elab/Binders.lean
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions stage0/src/Lean/Elab/Do.lean
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions stage0/src/Lean/Elab/MutualDef.lean
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading