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

feat: listLit and arrayLit as macros

Browse source 
Motivation: avoid special support at `Match.lean`.
This commit is contained in:
Leonardo de Moura 2020-08-11 13:03:36 -07:00
parent d0e07d5608
commit c66cb01a4b
1 changed files with 7 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Elab/Term.lean
View file

@ -1117,23 +1117,20 @@ fun stx expectedType? =>
withMacroExpansion stx pairs (elabTerm pairs expectedType?)
| _ => throwError stx "unexpected parentheses notation"
@[builtinTermElab «listLit»] def elabListLit : TermElab :=
fun stx expectedType? => do
@[builtinMacro Lean.Parser.Term.listLit] def expandListLit : Macro :=
fun stx =>
let openBkt := stx.getArg 0;
let args := stx.getArg 1;
let closeBkt := stx.getArg 2;
let consId := mkTermIdFrom openBkt `List.cons;
let nilId := mkTermIdFrom closeBkt `List.nil;
let newStx := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId;
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
pure $ args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId
@[builtinTermElab «arrayLit»] def elabArrayLit : TermElab :=
fun stx expectedType? => do
@[builtinMacro Lean.Parser.Term.arrayLit] def expandArrayLit : Macro :=
fun stx =>
match_syntax stx with
| `(#[$args*]) => do
newStx ← `(List.toArray [$args*]);
withMacroExpansion stx newStx (elabTerm newStx expectedType?)
| _ => throwError stx "unexpected array literal syntax"
| `(#[$args*]) => `(List.toArray [$args*])
| _ => throw $ Macro.Exception.error stx "unexpected array literal syntax"
private partial def resolveLocalNameAux (lctx : LocalContext) : Name → List String → Option (Expr × List String)
| n, projs =>