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

feat: add autoUnfold to Simp.Config

Browse source 
Add macros for conveniently setting `arith` and `autoUnfold`.
This commit is contained in:
Leonardo de Moura 2022-04-18 15:59:30 -07:00
parent 470d0077ca
commit 18832ad91c
1 changed files with 32 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/Init/Meta.lean
View file

@ -1012,20 +1012,23 @@ structure Config where
proj : Bool := true
decide : Bool := true
arith : Bool := false
autoUnfold : Bool := false
deriving Inhabited, BEq, Repr
-- Configuration object for `simp_all`
structure ConfigCtx extends Config where
contextual := true
def neutralConfig : Simp.Config :=
{ zeta := false
beta := false
eta := false
iota := false
proj := false
decide := false
arith := false }
def neutralConfig : Simp.Config := {
zeta := false
beta := false
eta := false
iota := false
proj := false
decide := false
arith := false
autoUnfold := false
}
end Simp
@ -1044,29 +1047,29 @@ namespace Parser.Tactic
macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
`(rw (config := { transparency := Lean.Meta.TransparencyMode.default }) $s:rwRuleSeq $[$loc:location]?)
/-- Similar to `simp` but with `arith := true` -/
syntax (name := simpArith) "simp_arith " (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
macro "declare_simp_like_tactic" opt:(("(" &"all " " := " &"true" ")")?) tacName:ident tacToken:str updateCfg:term : command => do
let (kind, tkn, stx) ←
if opt.isNone then
pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
else
pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
`($stx:command
@[macro $tacName:ident] def expandSimp : Macro := fun s => do
let c ← match s[1][0] with
| `(config| (config := $$c:term)) => `(config| (config := $updateCfg:term $$c))
| _ => `(config| (config := $updateCfg:term {}))
let s := s.setKind $kind:term
let s := s.setArg 0 (mkAtomFrom s[0] $tkn:term)
let r := s.setArg 1 (mkNullNode #[c])
return r)
@[macro simpArith] def expandSimpArith : Macro := fun s => do
let c ← match s[1][0] with
| `(config| (config := $c:term)) => `(config| (config := { ($c : Lean.Meta.Simp.Config) with arith := true }))
| _ => `(config| (config := { arith := true }))
let s := s.setKind ``simp
let s := s.setArg 0 (mkAtomFrom s[0] "simp")
let r := s.setArg 1 (mkNullNode #[c])
return r
declare_simp_like_tactic simpAutoUnfold "simp! " fun (c : Lean.Meta.Simp.Config) => { c with autoUnfold := true }
declare_simp_like_tactic simpArith "simp_arith " fun (c : Lean.Meta.Simp.Config) => { c with arith := true }
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, autoUnfold := true }
/-- Similar to `simp_all` but with `arith := true` -/
syntax (name := simpAllArith) "simp_all_arith " (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
@[macro simpAllArith] def expandSimpAllArith : Macro := fun s => do
let c ← match s[1][0] with
| `(config| (config := $c:term)) => `(config| (config := { ($c : Lean.Meta.Simp.ConfigCtx) with arith := true }))
| _ => `(config| (config := { arith := true }))
let s := s.setKind ``simpAll
let s := s.setArg 0 (mkAtomFrom s[0] "simp_all")
let r := s.setArg 1 (mkNullNode #[c])
return r
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with autoUnfold := true }
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true }
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, autoUnfold := true }
end Parser.Tactic