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

feat: monad polymorphic withSynthesize

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-20 12:32:05 -08:00
parent 8fa1ecde49
commit bcd8f09672
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Elab/SyntheticMVars.lean
View file

@ -296,11 +296,7 @@ def synthesizeSyntheticMVarsUsingDefault : TermElabM Unit := do
synthesizeSyntheticMVars (mayPostpone := true)
synthesizeUsingDefaultLoop
/--
Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
If `mayPostpone == false`, then all of them must be synthesized.
Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
partial def withSynthesize {α} (k : TermElabM α) (mayPostpone := false) : TermElabM α := do
private partial def withSynthesizeImp {α} (k : TermElabM α) (mayPostpone : Bool) : TermElabM α := do
let s ← get
let syntheticMVarsSaved := s.syntheticMVars
modify fun s => { s with syntheticMVars := [] }
@ -313,6 +309,13 @@ partial def withSynthesize {α} (k : TermElabM α) (mayPostpone := false) : Term
finally
modify fun s => { s with syntheticMVars := s.syntheticMVars ++ syntheticMVarsSaved }
/--
Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
If `mayPostpone == false`, then all of them must be synthesized.
Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
@[inline] def withSynthesize [MonadFunctorT TermElabM m] [Monad m] (k : m α) (mayPostpone := false) : m α :=
monadMap (m := TermElabM) (withSynthesizeImp . mayPostpone) k
/-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
withRef stx do