From 175a6ab6068f8726d36c58d8f0e681c3ea42e4c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Oct 2023 09:36:46 -0700 Subject: [PATCH] refactor: add `Init/MetaTypes` to workaround bootstrapping issues Motivation: we could not set `simp` configuration options at `WFTactics.lean` --- src/Init.lean | 1 + src/Init/Meta.lean | 105 +----------------------------------- src/Init/MetaTypes.lean | 117 ++++++++++++++++++++++++++++++++++++++++ src/Init/WFTactics.lean | 3 +- 4 files changed, 122 insertions(+), 104 deletions(-) create mode 100644 src/Init/MetaTypes.lean diff --git a/src/Init.lean b/src/Init.lean index 40dcc8541c..aea7d2ca94 100644 --- a/src/Init.lean +++ b/src/Init.lean @@ -17,6 +17,7 @@ import Init.System import Init.Util import Init.Dynamic import Init.ShareCommon +import Init.MetaTypes import Init.Meta import Init.NotationExtra import Init.SimpLemmas diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index b57bac9325..2f775a6c05 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura and Sebastian Ullrich Additional goodies for writing macros -/ prelude +import Init.MetaTypes import Init.Data.Array.Basic import Init.Data.Option.BasicAux @@ -217,11 +218,6 @@ instance : DecidableEq Name := end Name -structure NameGenerator where - namePrefix : Name := `_uniq - idx : Nat := 1 - deriving Inhabited - namespace NameGenerator @[inline] def curr (g : NameGenerator) : Name := @@ -452,11 +448,6 @@ end Syntax | none => x | some ref => withRef ref x -/-- Syntax objects for a Lean module. -/ -structure Module where - header : Syntax - commands : Array Syntax - /-- Expand macros in the given syntax. A node with kind `k` is visited only if `p k` is true. @@ -1203,99 +1194,7 @@ end TSyntax namespace Meta -inductive TransparencyMode where - | all | default | reducible | instances - deriving Inhabited, BEq, Repr - -inductive EtaStructMode where - /-- Enable eta for structure and classes. -/ - | all - /-- Enable eta only for structures that are not classes. -/ - | notClasses - /-- Disable eta for structures and classes. -/ - | none - deriving Inhabited, BEq, Repr - -namespace DSimp - -structure Config where - zeta : Bool := true - beta : Bool := true - eta : Bool := true - etaStruct : EtaStructMode := .all - iota : Bool := true - proj : Bool := true - decide : Bool := false - autoUnfold : Bool := false - /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all` - will fail if they do not make progress. -/ - failIfUnchanged : Bool := true - /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all` - will unfold even partial applications of `f` when we request `f` to be unfolded. -/ - unfoldPartialApp : Bool := false - deriving Inhabited, BEq, Repr - -end DSimp - -namespace Simp - -def defaultMaxSteps := 100000 - -structure Config where - maxSteps : Nat := defaultMaxSteps - maxDischargeDepth : Nat := 2 - contextual : Bool := false - memoize : Bool := true - singlePass : Bool := false - zeta : Bool := true - beta : Bool := true - eta : Bool := true - etaStruct : EtaStructMode := .all - iota : Bool := true - proj : Bool := true - decide : Bool := true - arith : Bool := false - autoUnfold : Bool := false - /-- - If `dsimp := true`, then switches to `dsimp` on dependent arguments where there is no congruence theorem that allows - `simp` to visit them. If `dsimp := false`, then argument is not visited. - -/ - dsimp : Bool := true - /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all` - will fail if they do not make progress. -/ - failIfUnchanged : Bool := true - /-- If `ground := true`, then ground terms are reduced. A term is ground when - it does not contain free or meta variables. Reduction is interrupted at a function application `f ...` - if `f` is marked to not be unfolded. -/ - ground : Bool := false - /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all` - will unfold even partial applications of `f` when we request `f` to be unfolded. -/ - unfoldPartialApp : 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 - autoUnfold := false - ground := false -} - -end Simp - -inductive Occurrences where - | all - | pos (idxs : List Nat) - | neg (idxs : List Nat) - deriving Inhabited, BEq +deriving instance Repr for TransparencyMode, EtaStructMode, DSimp.Config, Simp.Config def Occurrences.contains : Occurrences → Nat → Bool | all, _ => true diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean new file mode 100644 index 0000000000..d00e5d8629 --- /dev/null +++ b/src/Init/MetaTypes.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) Leonardo de Moura. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Core + +namespace Lean + +structure NameGenerator where + namePrefix : Name := `_uniq + idx : Nat := 1 + deriving Inhabited + +/-- Syntax objects for a Lean module. -/ +structure Module where + header : Syntax + commands : Array Syntax + +namespace Meta + +inductive TransparencyMode where + | all | default | reducible | instances + deriving Inhabited, BEq + +inductive EtaStructMode where + /-- Enable eta for structure and classes. -/ + | all + /-- Enable eta only for structures that are not classes. -/ + | notClasses + /-- Disable eta for structures and classes. -/ + | none + deriving Inhabited, BEq + +namespace DSimp + +structure Config where + zeta : Bool := true + beta : Bool := true + eta : Bool := true + etaStruct : EtaStructMode := .all + iota : Bool := true + proj : Bool := true + decide : Bool := false + autoUnfold : Bool := false + /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all` + will fail if they do not make progress. -/ + failIfUnchanged : Bool := true + /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all` + will unfold even partial applications of `f` when we request `f` to be unfolded. -/ + unfoldPartialApp : Bool := false + deriving Inhabited, BEq + +end DSimp + +namespace Simp + +def defaultMaxSteps := 100000 + +structure Config where + maxSteps : Nat := defaultMaxSteps + maxDischargeDepth : Nat := 2 + contextual : Bool := false + memoize : Bool := true + singlePass : Bool := false + zeta : Bool := true + beta : Bool := true + eta : Bool := true + etaStruct : EtaStructMode := .all + iota : Bool := true + proj : Bool := true + decide : Bool := true + arith : Bool := false + autoUnfold : Bool := false + /-- + If `dsimp := true`, then switches to `dsimp` on dependent arguments where there is no congruence theorem that allows + `simp` to visit them. If `dsimp := false`, then argument is not visited. + -/ + dsimp : Bool := true + /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all` + will fail if they do not make progress. -/ + failIfUnchanged : Bool := true + /-- If `ground := true`, then ground terms are reduced. A term is ground when + it does not contain free or meta variables. Reduction is interrupted at a function application `f ...` + if `f` is marked to not be unfolded. -/ + ground : Bool := false + /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all` + will unfold even partial applications of `f` when we request `f` to be unfolded. -/ + unfoldPartialApp : Bool := false + deriving Inhabited, BEq + +-- 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 + autoUnfold := false + ground := false +} + +end Simp + +inductive Occurrences where + | all + | pos (idxs : List Nat) + | neg (idxs : List Nat) + deriving Inhabited, BEq + +end Lean.Meta diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 6c985eafdc..1e45834e8b 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -5,12 +5,13 @@ Author: Leonardo de Moura -/ prelude import Init.SizeOf +import Init.MetaTypes import Init.WF /-- Unfold definitions commonly used in well founded relation definitions. This is primarily intended for internal use in `decreasing_tactic`. -/ macro "simp_wf" : tactic => - `(tactic| try simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]) + `(tactic| try simp (config := { unfoldPartialApp := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]) /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case" reasoning after applying lexicographic order lemmas.