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

feat: elaborate StateRefT macro

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-27 12:15:14 -07:00
parent 1e1e7a4ab2
commit f80e2c1db6
2 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/BuiltinNotation.lean
View file

@ -364,4 +364,13 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
mkEqNDRec (← mkMotive expectedAbst) h heq
| _ => throwUnsupportedSyntax
@[builtinTermElab stateRefT] def elabStateRefT : TermElab := fun stx _ => do
let σ ← elabType stx[1]
let m ← elabTerm stx[2] (← mkArrow (mkSort levelOne) (mkSort levelOne))
let ω ← mkFreshExprMVar (mkSort levelOne)
let stWorld ← mkAppM `STWorld #[ω, m]
mkInstMVar stWorld
mkAppM `StateRefT' #[ω, σ, m]
end Lean.Elab.Term

4
src/Lean/Parser/Term.lean
View file

@ -259,8 +259,8 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def dbgTrace := parser!:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
@[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
-- Macro for avoiding exponentially big terms when using due to `STWorld`
@[builtinTermParser] def stateRefT := parser! "StateRefTNew" >> termParser maxPrec >> termParser maxPrec
-- Macro for avoiding exponentially big terms when using `STWorld`
@[builtinTermParser] def stateRefT := parser! "StateRefT" >> termParser maxPrec >> termParser maxPrec
end Term