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

feat: add expandStructInstExpectedType

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-21 09:36:50 -07:00
parent 959a860bdf
commit f44fe34661
1 changed files with 20 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Init/Lean/Elab/StructInst.lean
View file

@ -762,19 +762,30 @@ 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
-- TODO: expand expected type syntax at structurInst
stxNew? ← expandNonAtomicExplicitSource stx;
stxNew? ← liftMacroM $ expandStructInstExpectedType 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 stx ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
| _, _ => elabStructInstAux stx expectedType? sourceView
| 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 stx ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
| _, _ => elabStructInstAux stx expectedType? sourceView
end StructInst
end Term