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

chore: factor out nested macro at structInst elaborator

Browse source 
@Kha The new macro is another example where it would be super nice to
have better support for `optional` at `match_syntax`.
This commit is contained in:
Leonardo de Moura 2020-09-19 11:55:57 -07:00
parent dc928d7b05
commit 065a845bfd
1 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -18,8 +18,20 @@ open Meta
/- parser! "{" >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}" -/
@[builtinMacro Lean.Parser.Term.structInst] def expandStructInstExpectedType : Macro :=
fun stx =>
let expectedArg := stx.getArg 4;
if expectedArg.isNone
then Macro.throwUnsupported
else
let expected := expectedArg.getArg 1;
let stxNew := stx.setArg 4 mkNullNode;
`(($stxNew : $expected))
/-
If `stx` is of the form `{ s with ... }` and `s` is not a local variable, expand into `let src := s; { src with ... }`.
Note that this one is not a `Macro` because we need to access the local context.
-/
private def expandNonAtomicExplicitSource (stx : Syntax) : TermElabM (Option Syntax) :=
withFreshMacroScope $
@ -782,30 +794,18 @@ match mkStructView stx structName source with
DefaultFields.propagate struct;
pure r
private def expandStructInstExpectedType (stx : Syntax) : MacroM (Option Syntax) :=
let expectedArg := stx.getArg 4;
if expectedArg.isNone then pure none
else
let expected := expectedArg.getArg 1;
let stxNew := stx.setArg 4 mkNullNode;
`(($stxNew : $expected))
@[builtinTermElab structInst] def elabStructInst : TermElab :=
fun stx expectedType? => do
stxNew? ← liftMacroM $ expandStructInstExpectedType stx;
stxNew? ← expandNonAtomicExplicitSource stx;
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
| none => do
stxNew? ← expandNonAtomicExplicitSource stx;
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
| none => do
sourceView ← getStructSource stx;
modifyOp? ← isModifyOp? stx;
match modifyOp?, sourceView with
| some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
| some _, _ => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
| _, _ => elabStructInstAux stx expectedType? sourceView
| none => do
sourceView ← getStructSource stx;
modifyOp? ← isModifyOp? stx;
match modifyOp?, sourceView with
| some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
| some _, _ => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
| _, _ => elabStructInstAux stx expectedType? sourceView
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.struct;