refactor: remove optional leading pipe from match, use many1Indent instead of sepBy1
This commit is contained in:
Sebastian Ullrich
parent
d22d639fcb
commit
f9dcbbddc4
16 changed files with 101 additions and 128 deletions
|
|
@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Lean.Elab.Term
|
||||
import Lean.Parser.Term
|
||||
|
||||
namespace Lean.Elab.Term
|
||||
open Meta
|
||||
open Lean.Parser.Term
|
||||
|
||||
/--
|
||||
Given syntax of the forms
|
||||
|
|
@ -350,10 +352,11 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (
|
|||
x s.fvars s.expectedType?
|
||||
|
||||
/- Helper function for `expandEqnsIntoMatch` -/
|
||||
private def getMatchAltNumPatterns (matchAlts : Syntax) : Nat :=
|
||||
let alt0 := matchAlts[1][0]
|
||||
let pats := alt0[0].getSepArgs
|
||||
pats.size
|
||||
private def getMatchAltsNumPatterns : Syntax → Nat
|
||||
| alts => match alts[0][0] with
|
||||
| `(matchAltExpr| | $pats,* => $rhs) =>
|
||||
pats.getElems.size
|
||||
| _ => unreachable!
|
||||
|
||||
private def mkMatch (ref : Syntax) (discrs : Array Syntax) (matchAlts : Syntax) (matchTactic := false) : Syntax :=
|
||||
Syntax.node (if matchTactic then `Lean.Parser.Tactic.match else `Lean.Parser.Term.match)
|
||||
|
|
@ -429,10 +432,10 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (mat
|
|||
```
|
||||
-/
|
||||
def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := false) : MacroM Syntax :=
|
||||
expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltNumPatterns matchAlts) #[]
|
||||
expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltsNumPatterns matchAlts) #[]
|
||||
|
||||
def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
|
||||
expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltNumPatterns matchAlts) #[]
|
||||
expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltsNumPatterns matchAlts) #[]
|
||||
|
||||
/--
|
||||
Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.
|
||||
|
|
@ -477,7 +480,7 @@ def expandMatchAltsWhereDecls (ref : Syntax) (matchAltsWhereDecls : Syntax) : Ma
|
|||
let x ← `(x)
|
||||
let body ← loop n (addDiscr ref discrs x)
|
||||
`(@fun $x => $body)
|
||||
loop (getMatchAltNumPatterns matchAlts) #[]
|
||||
loop (getMatchAltsNumPatterns matchAlts) #[]
|
||||
|
||||
@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match stx with
|
||||
| `(fun $binders* => $body) => do
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ import Lean.Elab.Deriving.Basic
|
|||
import Lean.Elab.Deriving.Util
|
||||
|
||||
namespace Lean.Elab.Deriving.BEq
|
||||
|
||||
open Lean.Parser.Term
|
||||
open Meta
|
||||
|
||||
structure Header where
|
||||
|
|
@ -37,7 +37,7 @@ def mkHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
|
|||
def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) (argNames : Array Name) : TermElabM Syntax := do
|
||||
let discrs ← mkDiscrs
|
||||
let alts ← mkAlts
|
||||
`(match $[$discrs],* with | $[$alts:matchAlt]|*)
|
||||
`(match $[$discrs],* with $alts:matchAlt*)
|
||||
where
|
||||
mkDiscr (varName : Name) : TermElabM Syntax :=
|
||||
`(Parser.Term.matchDiscr| $(mkIdent varName):term)
|
||||
|
|
@ -57,7 +57,7 @@ where
|
|||
patterns := patterns.push (← `(_))
|
||||
patterns := patterns.push (← `(_))
|
||||
let altRhs ← `(false)
|
||||
`(matchAltExpr| $[$patterns:term],* => $altRhs:term)
|
||||
`(matchAltExpr| | $[$patterns:term],* => $altRhs:term)
|
||||
|
||||
mkAlts : TermElabM (Array Syntax) := do
|
||||
let mut alts := #[]
|
||||
|
|
@ -93,7 +93,7 @@ where
|
|||
rhs ← `($rhs && $a:ident == $b:ident)
|
||||
patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1:term*))
|
||||
patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2:term*))
|
||||
`(matchAltExpr| $[$patterns:term],* => $rhs:term)
|
||||
`(matchAltExpr| | $[$patterns:term],* => $rhs:term)
|
||||
alts := alts.push alt
|
||||
alts := alts.push (← mkElseAlt)
|
||||
return alts
|
||||
|
|
|
|||
|
|
@ -12,7 +12,6 @@ open Meta
|
|||
def implicitBinderF := Parser.Term.implicitBinder
|
||||
def instBinderF := Parser.Term.instBinder
|
||||
def explicitBinderF := Parser.Term.explicitBinder
|
||||
def matchAltExpr := Parser.Term.matchAlt
|
||||
|
||||
def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
|
||||
forallTelescopeReducing indVal.type fun xs _ => do
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ import Lean.Elab.Term
|
|||
import Lean.Elab.Binders
|
||||
import Lean.Elab.Match
|
||||
import Lean.Elab.Quotation.Util
|
||||
import Lean.Parser.Do
|
||||
|
||||
namespace Lean.Elab.Term
|
||||
open Meta
|
||||
|
|
@ -1016,15 +1017,12 @@ partial def toTerm : Code → M Syntax
|
|||
| Code.seq stx k => do seqToTerm stx (← toTerm k)
|
||||
| Code.ite ref _ o c t e => do mkIte ref o c (← toTerm t) (← toTerm e)
|
||||
| Code.«match» ref discrs optType alts => do
|
||||
let mut termSepAlts := #[]
|
||||
let mut termAlts := #[]
|
||||
for alt in alts do
|
||||
termSepAlts := termSepAlts.push $ mkAtomFrom alt.ref "|"
|
||||
let rhs ← toTerm alt.rhs
|
||||
let termAlt := mkNode `Lean.Parser.Term.matchAlt #[alt.patterns, mkAtomFrom alt.ref "=>", rhs]
|
||||
termSepAlts := termSepAlts.push termAlt
|
||||
let firstVBar := termSepAlts[0]
|
||||
let termSepAlts := mkNullNode termSepAlts[1:termSepAlts.size]
|
||||
let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode #[firstVBar], termSepAlts]
|
||||
let termAlt := mkNode `Lean.Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", alt.patterns, mkAtomFrom alt.ref "=>", rhs]
|
||||
termAlts := termAlts.push termAlt
|
||||
let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
|
||||
pure $ mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", discrs, optType, mkAtomFrom ref "with", termMatchAlts]
|
||||
|
||||
def run (code : Code) (m : Syntax) (uvars : Array Name := #[]) (kind := Kind.regular) : MacroM Syntax := do
|
||||
|
|
@ -1328,22 +1326,16 @@ def doForToCode (doSeqToCode : List Syntax → M CodeBlock) (doFor : Syntax) (do
|
|||
let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)
|
||||
doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
|
||||
|
||||
/--
|
||||
Generate `CodeBlock` for `doMatch; doElems`
|
||||
```
|
||||
def doMatchAlt := sepBy1 termParser ", " >> darrow >> doSeq
|
||||
def doMatchAlts := parser! optional "| " >> sepBy1 doMatchAlt "|"
|
||||
def doMatch := parser! "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
|
||||
``` -/
|
||||
/-- Generate `CodeBlock` for `doMatch; doElems` -/
|
||||
def doMatchToCode (doSeqToCode : List Syntax → M CodeBlock) (doMatch : Syntax) (doElems: List Syntax) : M CodeBlock := do
|
||||
let ref := doMatch
|
||||
let discrs := doMatch[1]
|
||||
let optType := doMatch[2]
|
||||
let matchAlts := doMatch[4][1].getSepArgs -- Array of `doMatchAlt`
|
||||
let matchAlts := doMatch[4][0].getArgs -- Array of `doMatchAlt`
|
||||
let alts ← matchAlts.mapM fun matchAlt => do
|
||||
let patterns := matchAlt[0]
|
||||
let patterns := matchAlt[1]
|
||||
let vars ← getPatternsVarsEx patterns.getSepArgs
|
||||
let rhs := matchAlt[2]
|
||||
let rhs := matchAlt[3]
|
||||
let rhs ← doSeqToCode (getDoSeqElems rhs)
|
||||
pure { ref := matchAlt, vars := vars, patterns := patterns, rhs := rhs : Alt CodeBlock }
|
||||
let matchCode ← mkMatch ref discrs optType alts
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ import Lean.Meta.Match.MatchPatternAttr
|
|||
import Lean.Meta.Match.Match
|
||||
import Lean.Elab.SyntheticMVars
|
||||
import Lean.Elab.App
|
||||
import Lean.Parser.Term
|
||||
|
||||
namespace Lean.Elab.Term
|
||||
open Meta
|
||||
|
|
@ -14,15 +15,6 @@ open Meta
|
|||
/- This modules assumes "match"-expressions use the following syntax.
|
||||
|
||||
```lean
|
||||
def matchAlt : Parser :=
|
||||
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
|
||||
sepBy1 termParser ", " >> darrow >> termParser
|
||||
|
||||
def matchAlts (optionalFirstBar := true) : Parser :=
|
||||
group $ withPosition $ fun pos =>
|
||||
(if optionalFirstBar then optional "| " else "| ") >>
|
||||
sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
|
||||
|
||||
def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
|
||||
|
||||
def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
|
||||
|
|
@ -34,12 +26,6 @@ structure MatchAltView where
|
|||
patterns : Array Syntax
|
||||
rhs : Syntax
|
||||
|
||||
def mkMatchAltView (ref : Syntax) (matchAlt : Syntax) : MatchAltView := {
|
||||
ref := ref
|
||||
patterns := matchAlt[0].getSepArgs
|
||||
rhs := matchAlt[2]
|
||||
}
|
||||
|
||||
private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
let newStx ← `(let $lhsVar := $discr; $rhs)
|
||||
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
|
||||
|
|
@ -122,28 +108,20 @@ private def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptType : Sy
|
|||
let discrs ← elabDiscrsWitMatchType discrStxs matchType expectedType
|
||||
pure (discrs, matchType, matchAltViews)
|
||||
|
||||
/-
|
||||
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ sepBy1 termParser ", " >> darrow >> termParser
|
||||
-/
|
||||
def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array MatchAltView) := do
|
||||
matchAlts.mapM fun matchAlt => do
|
||||
let patterns ← matchAlt.patterns.mapM expandMacros
|
||||
pure { matchAlt with patterns := patterns }
|
||||
|
||||
/- Given `stx` a match-expression, return its alternatives. -/
|
||||
private def getMatchAlts (stx : Syntax) : Array MatchAltView := do
|
||||
let matchAlts := stx[4]
|
||||
let firstVBar := matchAlts[0]
|
||||
let mut ref := firstVBar
|
||||
let mut result := #[]
|
||||
for arg in matchAlts[1].getArgs do
|
||||
if ref.isNone then
|
||||
ref := arg -- The first vertical bar is optional
|
||||
if arg.getKind == `Lean.Parser.Term.matchAlt then
|
||||
result := result.push (mkMatchAltView ref arg)
|
||||
else
|
||||
ref := arg -- current `arg` is a vertical bar
|
||||
pure result
|
||||
/- Given `stx` a match-expression, return its alternatives. -/
|
||||
private def getMatchAlts : Syntax → Array MatchAltView
|
||||
| `(match $discrs,* $[: $ty?]? with $[| $patternss,* => $rhss]*) =>
|
||||
patternss.zipWith rhss fun patterns rhs => {
|
||||
ref := patterns[0],
|
||||
patterns := patterns,
|
||||
rhs := rhs
|
||||
}
|
||||
| stx => dbgTrace s!"{stx}" fun _ => unreachable!
|
||||
|
||||
/--
|
||||
Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
|
||||
|
|
@ -894,9 +872,7 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
|
|||
-- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
|
||||
@[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? =>
|
||||
match stx with
|
||||
| `(match $discr:term with $y:ident => $rhs:term) => expandSimpleMatch stx discr y rhs expectedType?
|
||||
| `(match $discr:term with | $y:ident => $rhs:term) => expandSimpleMatch stx discr y rhs expectedType?
|
||||
| `(match $discr:term : $type with $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
|
||||
| `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
|
||||
| _ => do
|
||||
match (← expandNonAtomicDiscrs? stx) with
|
||||
|
|
|
|||
|
|
@ -166,10 +166,6 @@ private def expandWhereDeclsAsStructInst (whereDecls : Syntax) : MacroM Syntax :
|
|||
/-
|
||||
Recall that
|
||||
```
|
||||
def matchAlts (optionalFirstBar := true) : Parser :=
|
||||
withPosition $ fun pos =>
|
||||
(if optionalFirstBar then optional "| " else "| ") >>
|
||||
sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
|
||||
def declValSimple := parser! " :=\n" >> termParser >> optional Term.whereDecls
|
||||
def declValEqns := parser! Term.matchAltsWhereDecls
|
||||
def declVal := declValSimple <|> declValEqns <|> Term.whereDecls
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ import Lean.Syntax
|
|||
import Lean.ResolveName
|
||||
import Lean.Elab.Term
|
||||
import Lean.Elab.Quotation.Util
|
||||
import Lean.Parser.Term
|
||||
|
||||
namespace Lean.Elab.Term.Quotation
|
||||
|
||||
|
|
@ -343,7 +344,7 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li
|
|||
|
||||
def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
|
||||
match stx with
|
||||
| `(match $[$discrs:term],* with $[|]? $[$[$patss],* => $rhss]|*) => do
|
||||
| `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
|
||||
-- letBindRhss ...
|
||||
if patss.all (·.all (!·.isQuot)) then
|
||||
-- no quotations => fall back to regular `match`
|
||||
|
|
|
|||
|
|
@ -172,6 +172,7 @@ end Term
|
|||
|
||||
namespace Command
|
||||
open Lean.Syntax
|
||||
open Lean.Parser.Term hiding macroArg
|
||||
open Lean.Parser.Command
|
||||
|
||||
private def getCatSuffix (catName : Name) : String :=
|
||||
|
|
@ -329,54 +330,56 @@ def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
|
|||
Recall that syntax node kinds contain the current namespace.
|
||||
-/
|
||||
def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
let alts ← alts.mapSepElemsM fun alt => do
|
||||
let lhs := alt[0]
|
||||
let pat := lhs[0]
|
||||
let alts ← alts.mapM fun alt => match alt with
|
||||
| `(matchAltExpr| | $pats,* => $rhs) => do
|
||||
let pat := pats.elemsAndSeps[0]
|
||||
if !pat.isQuot then
|
||||
throwUnsupportedSyntax
|
||||
let quoted := getQuotContent pat
|
||||
let k' := quoted.getKind
|
||||
if k' == k then
|
||||
pure alt
|
||||
else if k' == choiceKind then
|
||||
match quoted.getArgs.find? fun quotAlt => quotAlt.getKind == k with
|
||||
| none => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
|
||||
| some quoted =>
|
||||
let pat := pat.setArg 1 quoted
|
||||
let pats := pats.elemsAndSeps.set! 0 pat
|
||||
`(matchAltExpr| | $pats,* => $rhs)
|
||||
else
|
||||
throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
|
||||
| _ => throwUnsupportedSyntax
|
||||
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
|
||||
fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
|
||||
|
||||
def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
|
||||
| `(matchAltExpr| | $pats,* => $rhs) => do
|
||||
let pat := pats.elemsAndSeps[0]
|
||||
if !pat.isQuot then
|
||||
throwUnsupportedSyntax
|
||||
let quot := pat[1]
|
||||
let k' := quot.getKind
|
||||
if k' == k then
|
||||
pure alt
|
||||
else if k' == choiceKind then
|
||||
match quot.getArgs.find? fun quotAlt => quotAlt.getKind == k with
|
||||
| none => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
|
||||
| some quot =>
|
||||
let pat := pat.setArg 1 quot
|
||||
let lhs := lhs.setArg 0 pat
|
||||
pure $ alt.setArg 0 lhs
|
||||
else
|
||||
throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
|
||||
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
|
||||
fun | $(SepArray.mk alts):matchAlt|* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
|
||||
|
||||
def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
|
||||
let lhs := alt[0]
|
||||
let pat := lhs[0]
|
||||
if !pat.isQuot then
|
||||
throwUnsupportedSyntax
|
||||
let quot := pat[1]
|
||||
pure quot.getKind
|
||||
let quoted := getQuotContent pat
|
||||
pure quoted.getKind
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
let k ← inferMacroRulesAltKind (alts.get! 0)
|
||||
let k ← inferMacroRulesAltKind alts[0]
|
||||
if k == choiceKind then
|
||||
throwErrorAt! alts[0]
|
||||
"invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
|
||||
else
|
||||
let altsK ← alts.filterSepElemsM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
|
||||
let altsNotK ← alts.filterSepElemsM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
|
||||
let altsK ← alts.filterM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
|
||||
let altsNotK ← alts.filterM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
|
||||
let defCmd ← elabMacroRulesAux k altsK
|
||||
if altsNotK.isEmpty then
|
||||
pure defCmd
|
||||
else
|
||||
`($defCmd:command macro_rules $(SepArray.mk altsNotK):matchAlt|*)
|
||||
`($defCmd:command macro_rules $altsNotK:matchAlt*)
|
||||
|
||||
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
|
||||
adaptExpander fun stx => match stx with
|
||||
| `(macro_rules $[|]? $alts:matchAlt|*) => elabNoKindMacroRulesAux alts.elemsAndSeps
|
||||
| `(macro_rules [$kind] $[|]? $alts:matchAlt|*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts.elemsAndSeps
|
||||
| _ => throwUnsupportedSyntax
|
||||
| `(macro_rules $alts:matchAlt*) => elabNoKindMacroRulesAux alts
|
||||
| `(macro_rules [$kind] $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
-- TODO: cleanup after we have support for optional syntax at `match_syntax`
|
||||
@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
|
||||
|
|
|
|||
|
|
@ -326,7 +326,9 @@ private def introStep (n : Name) : TacticM Unit :=
|
|||
| `(tactic| intro $h:ident) => introStep h.getId
|
||||
| `(tactic| intro _) => introStep `_
|
||||
| `(tactic| intro $pat:term) => do
|
||||
let stxNew ← `(tactic| intro h; match h with | $pat:term => _; clear h)
|
||||
let m ← `(match h with | $pat:term => _)
|
||||
let m := m.setKind ``Lean.Parser.Tactic.match
|
||||
let stxNew ← `(tactic| intro h; $m; clear h)
|
||||
withMacroExpansion stx stxNew $ evalTactic stxNew
|
||||
| `(tactic| intro $hs:term*) => do
|
||||
let h0 := hs.get! 0
|
||||
|
|
|
|||
|
|
@ -23,13 +23,13 @@ open Meta
|
|||
```
|
||||
-/
|
||||
private def getAltName (alt : Syntax) : Name :=
|
||||
getNameOfIdent' alt[0] |>.eraseMacroScopes
|
||||
getNameOfIdent' alt[1] |>.eraseMacroScopes
|
||||
private def getAltVarNames (alt : Syntax) : Array Name :=
|
||||
alt[1].getArgs.map getNameOfIdent'
|
||||
alt[2].getArgs.map getNameOfIdent'
|
||||
private def getAltRHS (alt : Syntax) : Syntax :=
|
||||
alt[3]
|
||||
alt[4]
|
||||
private def getAltDArrow (alt : Syntax) : Syntax :=
|
||||
alt[2]
|
||||
alt[3]
|
||||
|
||||
-- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
|
||||
def isHoleRHS (rhs : Syntax) : Bool :=
|
||||
|
|
@ -241,7 +241,7 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
|
|||
pure (fvarIds.size, [mvarId'])
|
||||
|
||||
private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
|
||||
inductionAlts[2].getSepArgs
|
||||
inductionAlts[1].getArgs
|
||||
|
||||
private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
|
||||
if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]
|
||||
|
|
|
|||
|
|
@ -16,10 +16,10 @@ structure AuxMatchTermState where
|
|||
|
||||
private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
|
||||
let matchAlts := matchTac[4]
|
||||
let alts := matchAlts[1].getArgs
|
||||
let newAlts ← alts.mapSepElemsM fun alt => do
|
||||
let alts := matchAlts[0].getArgs
|
||||
let newAlts ← alts.mapM fun alt => do
|
||||
let alt := alt.setKind ``Parser.Term.matchAlt
|
||||
let holeOrTacticSeq := alt[2]
|
||||
let holeOrTacticSeq := alt[3]
|
||||
if holeOrTacticSeq.isOfKind ``Parser.Term.syntheticHole then
|
||||
pure alt
|
||||
else if holeOrTacticSeq.isOfKind ``Parser.Term.hole then
|
||||
|
|
@ -28,15 +28,15 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
|
|||
let holeName := mkIdentFrom holeOrTacticSeq tag
|
||||
let newHole ← `(?$holeName:ident)
|
||||
modify fun s => { s with nextIdx := s.nextIdx + 1}
|
||||
pure $ alt.setArg 2 newHole
|
||||
pure $ alt.setArg 3 newHole
|
||||
else withFreshMacroScope do
|
||||
let newHole ← `(?rhs)
|
||||
let newHoleId := newHole[1]
|
||||
let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
|
||||
modify fun s => { s with cases := s.cases.push newCase }
|
||||
pure $ alt.setArg 2 newHole
|
||||
pure $ alt.setArg 3 newHole
|
||||
let result := matchTac.setKind ``Parser.Term.«match»
|
||||
let result := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
|
||||
let result := result.setArg 4 (mkNode ``Parser.Term.matchAlts #[mkNullNode newAlts])
|
||||
pure result
|
||||
|
||||
private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do
|
||||
|
|
|
|||
|
|
@ -112,12 +112,14 @@ def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpa
|
|||
|
||||
def matchAlt (rhsParser : Parser := termParser) : Parser :=
|
||||
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
|
||||
sepBy1 termParser ", " >> darrow >> rhsParser
|
||||
"| " >> ppIndent (sepBy1 termParser ", " >> darrow >> rhsParser)
|
||||
/--
|
||||
Useful for syntax quotations. Note that generic patterns such as `` `(matchAltExpr| | ... => $rhs) `` should also
|
||||
work with other `rhsParser`s (of arity 1). -/
|
||||
def matchAltExpr := matchAlt
|
||||
|
||||
def matchAlts (rhsParser : Parser := termParser) (optionalFirstBar := true) : Parser :=
|
||||
parser! ppDedent $ withPosition $
|
||||
ppLine >> (if optionalFirstBar then optional "| " else group "| ") >>
|
||||
sepBy1 (ppIndent <| matchAlt rhsParser) "|" (ppLine >> checkColGe "alternatives must be indented" >> "| ")
|
||||
def matchAlts (rhsParser : Parser := termParser) : Parser :=
|
||||
parser! ppDedent $ withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
|
||||
|
||||
def matchDiscr := parser! optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
|
||||
|
||||
|
|
@ -129,7 +131,7 @@ def funSimpleBinder := atomic (lookahead (many1 binderIdent >> " : ")) >> simp
|
|||
def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
|
||||
-- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
|
||||
def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
|
||||
@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts (optionalFirstBar := false))
|
||||
@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
|
||||
|
||||
def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
|
||||
@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
|
||||
|
|
@ -144,7 +146,7 @@ def simpleBinderWithoutType := node `Lean.Parser.Term.simpleBinder (many1 binder
|
|||
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
|
||||
def letIdDecl := node `Lean.Parser.Term.letIdDecl $ atomic (letIdLhs >> " := ") >> termParser
|
||||
def letPatDecl := node `Lean.Parser.Term.letPatDecl $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser
|
||||
def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts (optionalFirstBar := false)
|
||||
def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts
|
||||
-- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
|
||||
def letDecl := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
|
||||
@[builtinTermParser] def «let» := parser!:leadPrec withPosition ("let " >> letDecl) >> optSemicolon termParser
|
||||
|
|
@ -163,7 +165,7 @@ def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSym
|
|||
@[runBuiltinParserAttributeHooks]
|
||||
def whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";"))
|
||||
@[runBuiltinParserAttributeHooks]
|
||||
def matchAltsWhereDecls := parser! matchAlts (optionalFirstBar := false) >> optional whereDecls
|
||||
def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
|
||||
|
||||
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser maxPrec
|
||||
@[builtinTermParser] def nativeDecide := parser! "nativeDecide!"
|
||||
|
|
|
|||
|
|
@ -219,9 +219,8 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
|
|||
Syntax.mkApp stx st.moreArgs
|
||||
| _, #[] => failure
|
||||
| _, _ =>
|
||||
let discrs ← st.discrs.mapM fun discr => `(matchDiscr|$discr:term)
|
||||
let pats ← delabPatterns st
|
||||
let stx ← `(match $[$discrs],* with | $[$[$pats],* => $st.rhss]|*)
|
||||
let stx ← `(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
|
||||
Syntax.mkApp stx st.moreArgs
|
||||
|
||||
@[builtinDelab mdata]
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ def f (x : Nat) (g : Nat → Nat) := g x
|
|||
#check f 1 $ fun x => x -- should work
|
||||
|
||||
syntax "foo" term:max term:max : term
|
||||
macro_rules `(foo $x $y) => `(f $x $y)
|
||||
macro_rules | `(foo $x $y) => `(f $x $y)
|
||||
|
||||
#check foo 1 (fun x => x) -- should work
|
||||
#check foo 1 fun x => x -- should work
|
||||
|
|
|
|||
|
|
@ -134,7 +134,7 @@ match n, parity n with
|
|||
| _, _ => none
|
||||
|
||||
-- overapplied matcher
|
||||
#check fun x => (match x with 0 => id | x+1 => id) x
|
||||
#check fun x => (match x with | 0 => id | x+1 => id) x
|
||||
|
||||
#check fun
|
||||
| #[1, 2] => 2
|
||||
|
|
|
|||
|
|
@ -10,16 +10,16 @@
|
|||
4
|
||||
---- inv
|
||||
10
|
||||
match1.lean:82:0: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
|
||||
match1.lean:82:2: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
|
||||
VecPred P Vec.nil
|
||||
expected type
|
||||
VecPred P tail✝
|
||||
[false, true, true]
|
||||
match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found
|
||||
match1.lean:113:2: error: dependent match elimination failed, inaccessible pattern found
|
||||
.(j + j)
|
||||
constructor expected
|
||||
[false, true, true]
|
||||
match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables
|
||||
match1.lean:124:11: error: invalid match-expression, type of pattern variable 'a' contains metavariables
|
||||
?m
|
||||
fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m
|
||||
fun (x : Nat × Nat) =>
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue