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

feat: as patterns in syntax match

Browse source 
@leodemoura no problem using the new architecture :)
This commit is contained in:
Sebastian Ullrich 2020-12-19 21:57:44 +01:00
parent 5b06e1011f
commit efc2b79aba
3 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Elab/Quotation.lean
View file

@ -204,7 +204,7 @@ private def noOpMatchAdaptPats : HeadCheck → Alt → Alt
private def adaptRhs (fn : Syntax → TermElabM Syntax) : Alt → TermElabM Alt
| (pats, rhs) => do (pats, ← fn rhs)
private def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
let pat := alt.fst.head!
let unconditionally (rhsFn) := pure {
check := unconditional,
@ -317,8 +317,13 @@ private def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
`(ite (Eq $cond true) $(← yes newDiscrs) $(← no))
}
else match pat with
| `(_) => unconditionally pure
| `($id:ident) => unconditionally (`(let $id := discr; $(·)))
| `(_) => unconditionally pure
| `($id:ident) => unconditionally (`(let $id := discr; $(·)))
| `($id:ident@$pat) => do
let info ← getHeadInfo (pat::alt.1.tail!, alt.2)
{ info with onMatch := fun taken => match info.onMatch taken with
| covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := discr; $(·)))) exh
| r => r }
| _ => throwErrorAt! pat "match_syntax: unexpected pattern kind {pat}"
private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
@ -378,7 +383,9 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
match stx with
| `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
-- letBindRhss ...
if patss.all (·.all (!·.isQuot)) then
if !patss.any (·.any (fun
| `($id@$pat) => pat.isQuot
| pat => pat.isQuot)) then
-- no quotations => fall back to regular `match`
throwUnsupportedSyntax
let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList

1
tests/lean/StxQuot.lean
View file

@ -24,6 +24,7 @@ end Lean.Syntax
#eval run $ do let a ← `(Nat.one); `(f $(id a))
#eval run $ do let a ← `(Nat.one); `($(a).b)
#eval run $ do let a ← `(1 + 2); match a with | `($a + $b) => `($b + $a) | _ => pure Syntax.missing
#eval run $ do let a ← `(1 + 2); match a with | stx@`($a + $b) => `($stx + $a) | _ => pure Syntax.missing
#eval run $ do let a ← `(def foo := 1); match a with | `($f:command) => pure f | _ => pure Syntax.missing
#eval run $ do let a ← `(def foo := 1 def bar := 2); match a with | `($f:command $g:command) => `($g:command $f:command) | _ => pure Syntax.missing

3
tests/lean/StxQuot.lean.expected.out
View file

@ -15,6 +15,7 @@
"(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1])"
"(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
"(term_+_ (numLit \"2\") \"+\" (numLit \"1\"))"
"(term_+_ (term_+_ (numLit \"1\") \"+\" (numLit \"2\")) \"+\" (numLit \"1\"))"
"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\") [])))"
"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"2\") [])))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\") [])))]"
"0"
@ -34,4 +35,4 @@
"(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
"(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
"#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]"
StxQuot.lean:70:33: error: expected parser to return exactly one syntax object
StxQuot.lean:71:33: error: expected parser to return exactly one syntax object