From 88111babd4bf43d099ca47ead8a957c8b0632b3d Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 2 Jun 2023 12:48:56 +0000 Subject: [PATCH] feat: `notation3` delaborator generation (#4533) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Gives the `notation3` command the ability to generate a delaborator in most common situations. When it succeeds, `notation3`-defined syntax is pretty printable. Examples: ``` (⋃ (i : ι) (i' : ι'), s i i') = ⋃ (i' : ι') (i : ι), s i i' (⨆ (g : α → ℝ≥0∞) (_ : Measurable g) (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ) = ∫⁻ (a : α), f a ∂μ ``` Co-authored-by: Mario Carneiro --- Mathlib/Data/Pi/Lex.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 2 +- Mathlib/Mathport/Notation.lean | 521 ++++++++++++++++-- Mathlib/MeasureTheory/Integral/Lebesgue.lean | 17 - .../Measure/MeasureSpaceDef.lean | 4 +- Mathlib/Order/CompleteLattice.lean | 14 - Mathlib/Order/Filter/FilterProduct.lean | 2 +- test/notation3.lean | 34 +- 8 files changed, 513 insertions(+), 83 deletions(-) diff --git a/Mathlib/Data/Pi/Lex.lean b/Mathlib/Data/Pi/Lex.lean index becb0ee25d23c..4b1a25bafcff6 100644 --- a/Mathlib/Data/Pi/Lex.lean +++ b/Mathlib/Data/Pi/Lex.lean @@ -51,7 +51,7 @@ protected def Lex (x y : ∀ i, β i) : Prop := /- This unfortunately results in a type that isn't delta-reduced, so we keep the notation out of the basic API, just in case -/ /-- The notation `Πₗ i, α i` refers to a pi type equipped with the lexicographic order. -/ -notation3 "Πₗ "(...)", "r:(scoped p => Lex (∀ i, p i)) => r +notation3 (prettyPrint := false) "Πₗ "(...)", "r:(scoped p => Lex (∀ i, p i)) => r @[simp] theorem toLex_apply (x : ∀ i, β i) (i : ι) : toLex x i = x i := diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index f37338d5aa6f9..3f367b25b6756 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean @@ -522,7 +522,7 @@ def isoCycle' : { f : Perm α // IsCycle f } ≃ { s : Cycle α // s.Nodup ∧ s #align equiv.perm.iso_cycle' Equiv.Perm.isoCycle' notation3 "c["(l", "* => foldr (h t => List.cons h t) List.nil)"]" => - Cycle.formPerm (↑l) (Cycle.nodup_coe_iff.mpr _) + Cycle.formPerm (Cycle.ofList l) (Iff.mpr Cycle.nodup_coe_iff _) unsafe instance repr_perm [Repr α] : Repr (Perm α) := ⟨fun f _ => repr (Multiset.pmap (fun (g : Perm α) (hg : g.IsCycle) => isoCycle ⟨g, hg⟩) diff --git a/Mathlib/Mathport/Notation.lean b/Mathlib/Mathport/Notation.lean index 262e76c09ba0f..58bf75704b92a 100644 --- a/Mathlib/Mathport/Notation.lean +++ b/Mathlib/Mathport/Notation.lean @@ -1,10 +1,11 @@ /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mario Carneiro +Authors: Mario Carneiro, Kyle Miller -/ import Mathlib.Lean.Expr import Mathlib.Util.Syntax +import Std.Data.Option.Basic /-! # The notation3 macro, simulating Lean 3's notation. @@ -13,11 +14,14 @@ import Mathlib.Util.Syntax -- To fix upstream: -- * bracketedExplicitBinders doesn't support optional types -namespace Lean - -namespace Parser.Command +namespace Mathlib.Notation3 +open Lean Parser Meta Elab Command PrettyPrinter.Delaborator SubExpr open Std.ExtendedBinder +initialize registerTraceClass `notation3 + +/-! ### Syntaxes supporting `notation3` -/ + /-- Expands binders into nested combinators. For example, the familiar exists is given by: @@ -67,55 +71,482 @@ syntax identOptScoped := ident (":" "(" "scoped " ident " => " term ")")? -- Note: there is deliberately no ppSpace between items -- so that the space in the literals themselves stands out syntax notation3Item := strLit <|> bindersItem <|> identOptScoped <|> foldAction + +/-! ### Expression matching + +A more complicated part of `notation3` is the delaborator generator. +While `notation` relies on generating app unexpanders, we instead generate a +delaborator directly so that we can control how binders are formatted (we want +to be able to know the types of binders, whether a lambda is a constant function, +and whether it is `Prop`-valued, which are not things we can answer once we pass +to app unexpanders). +-/ + +/-- The dynamic state of a `Matcher`. -/ +structure MatchState where + /-- This stores the assignments of variables to subexpressions (and their contexts) + that have been found so far during the course of the matching algorithm. + We store the contexts since we need to delaborate expressions after we leave + scoping constructs. -/ + vars : HashMap Name (SubExpr × LocalContext × LocalInstances) + /-- The binders accumulated when matching a `scoped` expression. -/ + scopeState : Array (TSyntax ``extBinderParenthesized) + /-- The arrays of delaborated `Term`s accumulated while matching + `foldl` and `foldr` expressions. For `foldl`, the arrays are stored in reverse order. -/ + foldState : HashMap Name (Array Term) + +/-- A matcher is a delaboration function that transforms `MatchState`s. -/ +def Matcher := MatchState → DelabM MatchState + deriving Inhabited + +/-- The initial state. -/ +def MatchState.empty : MatchState where + vars := {} + scopeState := #[] + foldState := {} + +/-- Evaluate `f` with the given variable's value as the `SubExpr` and within that subexpression's +saved context. Fails if the variable has no value. -/ +def MatchState.withVar (s : MatchState) (name : Name) + (m : DelabM α) : DelabM α := do + let some (se, lctx, linsts) := s.vars.find? name | failure + withLCtx lctx linsts <| withTheReader SubExpr (fun _ => se) <| m + +/-- Delaborate the given variable's value. Fails if the variable has no value. +If `checkNot` is provided, then checks that the expression being delaborated is not +the given one (this is used to prevent infinite loops). -/ +def MatchState.delabVar (s : MatchState) (name : Name) (checkNot? : Option Expr := none) : + DelabM Term := + s.withVar name do + if let some checkNot := checkNot? then + guard <| checkNot != (← getExpr) + delab + +/-- Assign a variable to the current `SubExpr`, capturing the local context. -/ +def MatchState.captureSubexpr (s : MatchState) (name : Name) : DelabM MatchState := do + return {s with vars := s.vars.insert name (← readThe SubExpr, ← getLCtx, ← getLocalInstances)} + +/-- Push a binder onto the binder array. For `scoped`. -/ +def MatchState.pushBinder (s : MatchState) (b : TSyntax ``extBinderParenthesized) : + DelabM MatchState := do + let binders := s.scopeState + -- TODO merge binders as an inverse to `satisfies_binder_pred%` + let binders := binders.push b + return {s with scopeState := binders} + +/-- Get the accumulated array of delaborated terms for a given foldr/foldl. +Returns `#[]` if nothing has been pushed yet. -/ +def MatchState.getFoldArray (s : MatchState) (name : Name) : Array Term := + (s.foldState.find? name).getD #[] + +/-- Push an delaborated term onto a foldr/foldl array. -/ +def MatchState.pushFold (s : MatchState) (name : Name) (t : Term) : MatchState := + let ts := (s.getFoldArray name).push t + {s with foldState := s.foldState.insert name ts} + +/-- Matcher that assigns the current `SubExpr` into the match state; +if a value already exists, then it checks for equality. -/ +def matchVar (c : Name) : Matcher := fun s => do + if let some (se, _, _) := s.vars.find? c then + guard <| se.expr == (← getExpr) + return s + else + s.captureSubexpr c + +/-- Matcher for `Expr.const`. -/ +def matchConst (c : Name) : Matcher := fun s => do + guard <| (← getExpr).isConstOf c + return s + +/-- Matcher for `Expr.fvar`. This is only used for `local notation3`. +It checks that the user name agrees, which isn't completely accurate, but probably sufficient. -/ +def matchFVar (userName : Name) : Matcher := fun s => do + let .fvar fvarId ← getExpr | failure + guard <| userName == (← fvarId.getUserName) + return s + +/-- Matches raw nat lits and `OfNat.ofNat` expressions. -/ +def natLitMatcher (n : Nat) : Matcher := fun s => do + let mut e ← getExpr + if e.isAppOfArity ``OfNat.ofNat 3 then + e := e.getArg! 1 + guard <| e.natLit? == n + return s + +/-- Given an identifier `f`, returns +(1) the resolved constant (if it's not an fvar) +(2) a Term for a matcher for the function +(3) the arity +(4) the positions at which the function takes an explicit argument -/ +def getExplicitArgIndices (f : Syntax) : + OptionT TermElabM (Option Name × Term × Nat × Array Nat) := do + let fe? ← try liftM <| Term.resolveId? f catch _ => pure none + match fe? with + | some fe@(.const f _) => + return (some f, ← ``(matchConst $(quote f)), ← collectIdxs (← inferType fe)) + | some fe@(.fvar fvarId) => + let userName ← fvarId.getUserName + return (none, ← ``(matchFVar $(quote userName)), ← collectIdxs (← inferType fe)) + | _ => + trace[notation3] "could not resolve name {f}" + failure +where + collectIdxs (ty : Expr) : MetaM (Nat × Array Nat) := do + let (_, binderInfos, _) ← Meta.forallMetaTelescope ty + let mut idxs := #[] + for bi in binderInfos, i in [0:binderInfos.size] do + if bi.isExplicit then + idxs := idxs.push i + return (binderInfos.size, idxs) + +/-- A matcher that runs `matchf` for the function and the `matchers` for the associated +argument indices. Fails if the function doesn't have exactly `arity` arguments. -/ +def fnArgMatcher (arity : Nat) (matchf : Matcher) (matchers : Array (Nat × Matcher)) : + Matcher := fun s => do + let mut s := s + let nargs := (← getExpr).getAppNumArgs + guard <| nargs == arity + s ← withNaryFn <| matchf s + for (i, matcher) in matchers do + s ← withNaryArg i <| matcher s + return s + +/-- Returns a `Term` that represents a `Matcher` for the given pattern `stx`. +The `boundNames` set determines which identifiers are variables in the pattern. +Fails in the `OptionT` sense if it comes across something it's unable to handle. + +Also returns constant names that could serve as a key for a delaborator. +For example, if it's for a function `f`, then `app.f`. -/ +partial def mkExprMatcher (stx : Term) (boundNames : HashSet Name) : + OptionT TermElabM (List Name × Term) := do + let stx'? ← liftM <| (liftMacroM <| expandMacro? stx : TermElabM (Option Syntax)) + match stx'? with + | some stx' => mkExprMatcher ⟨stx'⟩ boundNames + | none => + match stx with + | `(_) => return ([], ← `(pure)) + | `($n:ident) => + if boundNames.contains n.getId then + return ([], ← ``(matchVar $(quote n.getId))) + else + processFn n #[] + | `($f:ident $args*) => processFn f args + | `(term| $n:num) => return ([], ← ``(natLitMatcher $n)) + | `(($stx)) => + if Term.hasCDot stx then + failure + else + mkExprMatcher stx boundNames + | _ => + trace[notation3] "mkExprMatcher can't handle {stx}" + failure +where + processFn (f : Term) (args : TSyntaxArray `term) : OptionT TermElabM (List Name × Term) := do + let (name?, matchf, arity, idxs) ← getExplicitArgIndices f + unless args.size ≤ idxs.size do + trace[notation3] "Function {f} has been given more explicit arguments than expected" + failure + let mut matchers := #[] + for i in idxs, arg in args do + let (_, matcher) ← mkExprMatcher arg boundNames + matchers := matchers.push <| ← `(($(quote i), $matcher)) + -- `arity'` is the number of arguments (including trailing implicits) given these + -- explicit arguments. This reflects how the function would be elaborated. + let arity' := if _ : args.size < idxs.size then idxs[args.size] else arity + let key? := name?.map (`app ++ ·) + return (key?.toList, ← ``(fnArgMatcher $(quote arity') $matchf #[$matchers,*])) + +/-- Matcher for processing `scoped` syntax. Assumes the expression to be matched +against is in the `lit` variable. + +Runs `smatcher`, extracts the resulting `scopeId` variable, processes this value +(which must be a lambda) to produce a binder, and loops. + +Succeeds even if it matches nothing, so it is up to the caller to decide if the +empty scope state is ok. -/ +partial def matchScoped (lit scopeId : Name) (smatcher : Matcher) : Matcher := fun s => do + -- `lit` is bound to the SubExpr that the `scoped` syntax produced + s.withVar lit do + try + -- Run `smatcher` at `lit`, clearing the `scopeId` variable so that it can get a fresh value + let s ← smatcher {s with vars := s.vars.erase scopeId} + s.withVar scopeId do + guard (← getExpr).isLambda + let prop ← try Meta.isProp (← getExpr).bindingDomain! catch _ => pure false + let isDep := (← getExpr).bindingBody!.hasLooseBVar 0 + let ppTypes ← getPPOption getPPPiBinderTypes -- the same option controlling ∀ + let dom ← withBindingDomain delab + withBindingBodyUnusedName <| fun x => do + let x : Ident := ⟨x⟩ + let binder ← + if prop && !isDep then + -- this underscore is used to support binder predicates, since it indicates + -- the variable is unused and this binder is safe to merge into another + `(extBinderParenthesized|(_ : $dom)) + else if prop || ppTypes then + `(extBinderParenthesized|($x:ident : $dom)) + else + `(extBinderParenthesized|($x:ident)) + -- Now use the body of the lambda for `lit` for the next iteration + let s ← s.captureSubexpr lit + let s ← s.pushBinder binder + matchScoped lit scopeId smatcher s + catch _ => + return s + +/-- Like `matchScoped` but ensures that it matches at least one binder. -/ +partial def matchScoped' (lit scopeId : Name) (smatcher : Matcher) : Matcher := fun s => do + guard <| s.scopeState.isEmpty + let s ← matchScoped lit scopeId smatcher s + guard <| !s.scopeState.isEmpty + return s + +/- Create a `Term` that represents a matcher for `scoped` notation. +Fails in the `OptionT` sense if a matcher couldn't be constructed. +Also returns a delaborator key like in `mkExprMatcher`. +Reminder: `$lit:ident : (scoped $scopedId:ident => $scopedTerm:Term)` -/ +partial def mkScopedMatcher (lit scopeId : Name) (scopedTerm : Term) (boundNames : HashSet Name) : + OptionT TermElabM (List Name × Term) := do + -- Build the matcher for `scopedTerm` with `scopeId` as an additional variable + let (keys, smatcher) ← mkExprMatcher scopedTerm (boundNames.insert scopeId) + return (keys, ← ``(matchScoped' $(quote lit) $(quote scopeId) $smatcher)) + +/-- Matcher for expressions produced by `foldl`. -/ +partial def matchFoldl (lit x y : Name) (smatcher : Matcher) (sinit : Matcher) : + Matcher := fun s => do + s.withVar lit do + let expr ← getExpr + -- Clear x and y state before running smatcher so it can store new values + let s := {s with vars := s.vars |>.erase x |>.erase y} + let some s ← try some <$> smatcher s catch _ => pure none + | -- We put this here rather than using a big try block to prevent backtracking. + -- We have `smatcher` match greedily, and then require that `sinit` *must* succeed + sinit s + -- y gives the next element of the list + let s := s.pushFold lit (← s.delabVar y expr) + -- x gives the next lit + let some newLit := s.vars.find? x | failure + -- If progress was not made, fail + if newLit.1.expr == expr then failure + -- Progress was made, so recurse + let s := {s with vars := s.vars.insert lit newLit} + matchFoldl lit x y smatcher sinit s + +/-- Create a `Term` that represents a matcher for `foldl` notation. +Reminder: `( lit ","* => foldl (x y => scopedTerm) init )` -/ +partial def mkFoldlMatcher (lit x y : Name) (scopedTerm init : Term) (boundNames : HashSet Name) : + OptionT TermElabM (List Name × Term) := do + -- Build the `scopedTerm` matcher with `x` and `y` as additional variables + let boundNames' := boundNames |>.insert x |>.insert y + let (keys, smatcher) ← mkExprMatcher scopedTerm boundNames' + let (keys', sinit) ← mkExprMatcher init boundNames + return (keys ++ keys', ← ``(matchFoldl $(quote lit) $(quote x) $(quote y) $smatcher $sinit)) + +/-- Create a `Term` that represents a matcher for `foldr` notation. +Reminder: `( lit ","* => foldr (x y => scopedTerm) init )` -/ +partial def mkFoldrMatcher (lit x y : Name) (scopedTerm init : Term) (boundNames : HashSet Name) : + OptionT TermElabM (List Name × Term) := do + -- Build the `scopedTerm` matcher with `x` and `y` as additional variables + let boundNames' := boundNames |>.insert x |>.insert y + let (keys, smatcher) ← mkExprMatcher scopedTerm boundNames' + let (keys', sinit) ← mkExprMatcher init boundNames + -- N.B. by swapping `x` and `y` we can just use the foldl matcher + return (keys ++ keys', ← ``(matchFoldl $(quote lit) $(quote y) $(quote x) $smatcher $sinit)) + +/-! ### The `notation3` command -/ + +/-- Create a name that we can use for the `syntax` definition, using the +algorithm from `notation`. -/ +def mkNameFromSyntax (name? : Option (TSyntax ``namedName)) + (syntaxArgs : Array (TSyntax `stx)) (attrKind : TSyntax ``Term.attrKind) : + CommandElabM Name := do + if let some name := name? then + match name with + | `(namedName| (name := $n)) => return n.getId + | _ => pure () + let name ← liftMacroM <| mkNameFromParserSyntax `term (mkNullNode syntaxArgs) + addMacroScopeIfLocal name attrKind + +/-- Used when processing different kinds of variables when building the +final delaborator. -/ +inductive BoundValueType + /-- A normal variable, delaborate its expression. -/ + | normal + /-- A fold variable, use the fold state (but reverse the array). -/ + | foldl + /-- A fold variable, use the fold state (do not reverse the array). -/ + | foldr + +syntax prettyPrintOpt := "(" &"prettyPrint" " := " (&"true" <|> &"false") ")" + +/-- Interpret a `prettyPrintOpt`. The default value is `true`. -/ +def getPrettyPrintOpt (opt? : Option (TSyntax ``prettyPrintOpt)) : Bool := + if let some opt := opt? then + match opt with + | `(prettyPrintOpt| (prettyPrint := false)) => false + | _ => true + else + true + /-- -`notation3` declares notation using Lean 3-style syntax. This command can be used in mathlib4 -but it has an uncertain future and exists primarily for backward compatibility. +`notation3` declares notation using Lean-3-style syntax. + +Examples: +``` +notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) => r +notation3 "MyList[" (x", "* => foldr (a b => MyList.cons a b) MyList.nil) "]" => x +``` +By default notation is unable to mention any variables defined using `variable`, but +`local notation3` is able to use such local variables. + +Use `notation3 (prettyPrint := false)` to keep the command from generating a pretty printer +for the notation. + +This command can be used in mathlib4 but it has an uncertain future and was created primarily +for backward compatibility. -/ -macro doc:(docComment)? attrs:(Parser.Term.attributes)? ak:Term.attrKind - "notation3" prec:(precedence)? name:(namedName)? prio:(namedPrio)? ppSpace - lits:(notation3Item)+ " => " val:term : command => do - let mut boundNames : Lean.HashMap Name Syntax := {} - let mut macroArgs := #[] - for lit in lits do - match (lit : TSyntax ``notation3Item) with +elab doc:(docComment)? attrs?:(Parser.Term.attributes)? attrKind:Term.attrKind + "notation3" prec?:(precedence)? name?:(namedName)? prio?:(namedPrio)? pp?:(prettyPrintOpt)? + ppSpace items:(notation3Item)+ " => " val:term : command => do + -- We use raw `Name`s for variables. This maps variable names back to the + -- identifiers that appear in `items` + let mut boundIdents : HashMap Name Ident := {} + -- Replacements to use for the `macro` + let mut boundValues : HashMap Name Syntax := {} + -- The normal/foldl/foldr type of each variable (for delaborator) + let mut boundType : HashMap Name BoundValueType := {} + -- Function to get the keys of `boundValues`. This set is used when constructing + -- patterns for delaboration. + let getBoundNames (boundValues : HashMap Name Syntax) : HashSet Name := + HashSet.empty.insertMany <| boundValues.toArray.map Prod.fst + -- Function to update `syntaxArgs` and `pattArgs` using `macroArg` syntax + let pushMacro (syntaxArgs : Array (TSyntax `stx)) (pattArgs : Array Syntax) + (mac : TSyntax ``macroArg) := do + let (syntaxArg, pattArg) ← expandMacroArg mac + return (syntaxArgs.push syntaxArg, pattArgs.push pattArg) + -- Arguments for the `syntax` command + let mut syntaxArgs := #[] + -- Arguments for the LHS pattern in the `macro`. Also used to construct the syntax + -- when delaborating + let mut pattArgs := #[] + -- The matchers to assemble into a delaborator + let mut matchers := #[] + -- Whether we've seen a `(...)` item + let mut hasBindersItem := false + -- Whether we've seen a `scoped` item + let mut hasScoped := false + for item in items do + match item with | `(notation3Item| $lit:str) => - macroArgs := macroArgs.push (← `(macroArg| $lit:str)) + -- Can't use `pushMacro` since it inserts an extra variable into the pattern for `str`, which + -- breaks our delaborator + syntaxArgs := syntaxArgs.push (← `(stx| $lit:str)) + pattArgs := pattArgs.push <| mkAtomFrom lit lit.1.isStrLit?.get! | `(notation3Item| $_:bindersItem) => + if hasBindersItem then + throwErrorAt item "Cannot have more than one `(...)` item." + hasBindersItem := true -- HACK: Lean 3 traditionally puts a space after the main binder atom, resulting in -- notation3 "∑ "(...)", "r:(scoped f => sum f) => r -- but extBinders already has a space before it so we strip the trailing space of "∑ " - if let `(macroArg| $lit:str) := macroArgs.back then - macroArgs := macroArgs.pop.push (← `(macroArg| $(quote lit.getString.trimRight):str)) - macroArgs := macroArgs.push (← `(macroArg| binders:extBinders)) + if let `(stx| $lit:str) := syntaxArgs.back then + syntaxArgs := syntaxArgs.pop.push (← `(stx| $(quote lit.getString.trimRight):str)) + (syntaxArgs, pattArgs) ← pushMacro syntaxArgs pattArgs (← `(macroArg| binders:extBinders)) | `(notation3Item| ($id:ident $sep:str* => $kind ($x $y => $scopedTerm) $init)) => - macroArgs := macroArgs.push (← `(macroArg| $id:ident:sepBy(term, $sep:str))) - let scopedTerm ← scopedTerm.replaceM fun - | Syntax.ident _ _ id .. => pure $ boundNames.find? id - | _ => pure none - let init ← init.replaceM fun - | Syntax.ident _ _ id .. => pure $ boundNames.find? id - | _ => pure none - let stx ← match kind with - | `(foldKind| foldl) => `(expand_foldl% ($x $y => $scopedTerm) $init [$$(.ofElems $id),*]) - | `(foldKind| foldr) => `(expand_foldr% ($x $y => $scopedTerm) $init [$$(.ofElems $id),*]) - | _ => Macro.throwUnsupported - boundNames := boundNames.insert id.getId stx + (syntaxArgs, pattArgs) ← pushMacro syntaxArgs pattArgs <| ← + `(macroArg| $id:ident:sepBy(term, $sep:str)) + -- N.B. `Syntax.getId` returns `.anonymous` for non-idents + let scopedTerm' ← scopedTerm.replaceM fun s => pure (boundValues.find? s.getId) + let init' ← init.replaceM fun s => pure (boundValues.find? s.getId) + boundIdents := boundIdents.insert id.getId id + match kind with + | `(foldKind| foldl) => + boundValues := boundValues.insert id.getId <| ← + `(expand_foldl% ($x $y => $scopedTerm') $init' [$$(.ofElems $id),*]) + boundType := boundType.insert id.getId .foldl + matchers := matchers.push <| + mkFoldlMatcher id.getId x.getId y.getId scopedTerm init (getBoundNames boundValues) + | `(foldKind| foldr) => + boundValues := boundValues.insert id.getId <| ← + `(expand_foldr% ($x $y => $scopedTerm') $init' [$$(.ofElems $id),*]) + boundType := boundType.insert id.getId .foldr + matchers := matchers.push <| + mkFoldrMatcher id.getId x.getId y.getId scopedTerm init (getBoundNames boundValues) + | _ => throwUnsupportedSyntax | `(notation3Item| $lit:ident : (scoped $scopedId:ident => $scopedTerm)) => - let id := lit.getId - macroArgs := macroArgs.push (← `(macroArg| $lit:ident:term)) - let scopedTerm ← scopedTerm.replaceM fun - | Syntax.ident _ _ id .. => pure $ boundNames.find? id - | _ => pure none - boundNames := boundNames.insert id <| - ← `(expand_binders% ($scopedId => $scopedTerm) $$binders:extBinders, + if hasScoped then + throwErrorAt item "Cannot have more than one `scoped` item." + hasScoped := true + (syntaxArgs, pattArgs) ← pushMacro syntaxArgs pattArgs (← `(macroArg| $lit:ident:term)) + matchers := matchers.push <| + mkScopedMatcher lit.getId scopedId.getId scopedTerm (getBoundNames boundValues) + let scopedTerm' ← scopedTerm.replaceM fun s => pure (boundValues.find? s.getId) + boundIdents := boundIdents.insert lit.getId lit + boundValues := boundValues.insert lit.getId <| ← + `(expand_binders% ($scopedId => $scopedTerm') $$binders:extBinders, $(⟨lit.1.mkAntiquotNode `term⟩):term) | `(notation3Item| $lit:ident) => - macroArgs := macroArgs.push (← `(macroArg| $lit:ident:term)) - boundNames := boundNames.insert lit.getId <| lit.1.mkAntiquotNode `term - | stx => Macro.throwUnsupported - let val ← val.replaceM fun - | Syntax.ident _ _ id .. => pure $ boundNames.find? id - | _ => pure none - `($[$doc]? $(attrs)? $ak macro $(prec)? $(name)? $(prio)? $[$macroArgs]* : term => do `($val)) - -end Parser.Command + (syntaxArgs, pattArgs) ← pushMacro syntaxArgs pattArgs (← `(macroArg| $lit:ident:term)) + boundIdents := boundIdents.insert lit.getId lit + boundValues := boundValues.insert lit.getId <| lit.1.mkAntiquotNode `term + | stx => throwUnsupportedSyntax + if hasScoped && !hasBindersItem then + throwError "If there is a `scoped` item then there must be a `(...)` item for binders." + + -- 1. The `syntax` command + let name ← mkNameFromSyntax name? syntaxArgs attrKind + elabCommand <| ← `(command| + $[$doc]? $(attrs?)? $attrKind + syntax $(prec?)? (name := $(Lean.mkIdent name)) $(prio?)? $[$syntaxArgs]* : term) + + -- 2. The `macro_rules` + let currNamespace : Name ← getCurrNamespace + -- The `syntax` command puts definitions into the current namespace; we need this + -- to make the syntax `pat`. + let fullName := currNamespace ++ name + trace[notation3] "syntax declaration has name {fullName}" + let pat : Term := ⟨mkNode fullName pattArgs⟩ + let val' ← val.replaceM fun s => pure (boundValues.find? s.getId) + let mut macroDecl ← `(macro_rules | `($pat) => `($val')) + if isLocalAttrKind attrKind then + -- For local notation, take section variables into account + macroDecl ← `(section set_option quotPrecheck.allowSectionVars true $macroDecl end) + elabCommand macroDecl + + -- 3. Create a delaborator + if getPrettyPrintOpt pp? then + matchers := matchers.push <| Mathlib.Notation3.mkExprMatcher val (getBoundNames boundValues) + -- The matchers need to run in reverse order, so may as well reverse them here. + let matchersM? := (matchers.reverse.mapM id).run + -- We let local notations have access to `variable` declarations + let matchers? ← if isLocalAttrKind attrKind then + runTermElabM fun _ => matchersM? + else + liftTermElabM matchersM? + if let some ms := matchers? then + trace[notation3] "Matcher creation succeeded; assembling delaborator" + let delabName := name ++ `delab + let matcher ← ms.foldrM (fun m t => `($(m.2) >=> $t)) (← `(pure)) + trace[notation3] "matcher: {indentD matcher}" + let mut result ← `(`($pat)) + for (name, id) in boundIdents.toArray do + match boundType.findD name .normal with + | .normal => result ← `(MatchState.delabVar s $(quote name) (some e) >>= fun $id => $result) + | .foldl => result ← + `(let $id := (MatchState.getFoldArray s $(quote name)).reverse; $result) + | .foldr => result ← + `(let $id := MatchState.getFoldArray s $(quote name); $result) + if hasBindersItem then + result ← `(`(extBinders| $$(MatchState.scopeState s)*) >>= fun binders => $result) + elabCommand <| ← `(command| + def $(Lean.mkIdent delabName) : Delab := whenPPOption getPPNotation <| + getExpr >>= fun e => $matcher MatchState.empty >>= fun s => $result) + trace[notation3] "Defined delaborator {currNamespace ++ delabName}" + let delabKeys := ms.foldr (·.1 ++ ·) [] + trace[notation3] "Adding `delab` attribute for keys {delabKeys}" + for key in delabKeys do + elabCommand <| ← `(command| attribute [delab $(mkIdent key)] $(Lean.mkIdent delabName)) + else + logWarning s!"Could not generate matchers for a delaborator, so notation will not be pretty{ + ""} printed. Consider either adjusting the expansions or use{ + ""} `notation3 (prettyPrint := false)`." diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index c822d85e1a05b..f5d23c6f1be3a 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -117,23 +117,6 @@ notation3 "∫⁻ "(...)" in "s", "r:(scoped f => f)" ∂"μ => lintegral (Measu @[inherit_doc MeasureTheory.lintegral] notation3 "∫⁻ "(...)" in "s", "r:(scoped f => lintegral (Measure.restrict volume s) f) => r -open Lean in -@[app_unexpander MeasureTheory.lintegral] -def _root_.unexpandLIntegral : PrettyPrinter.Unexpander - | `($(_) $μ fun $x:ident => $b) => - match μ with - | `(Measure.restrict volume $s) => `(∫⁻ $x:ident in $s, $b) - | `(volume) => `(∫⁻ $x:ident, $b) - | `(Measure.restrict $ν $s) => `(∫⁻ $x:ident in $s, $b ∂$ν) - | _ => `(∫⁻ $x:ident, $b ∂$μ) - | `($(_) $μ fun ($x:ident : $t) => $b) => - match μ with - | `(Measure.restrict volume $s) => `(∫⁻ ($x:ident : $t) in $s, $b) - | `(volume) => `(∫⁻ ($x:ident : $t), $b) - | `(Measure.restrict $ν $s) => `(∫⁻ ($x:ident : $t) in $s, $b ∂$ν) - | _ => `(∫⁻ ($x:ident : $t), $b ∂$μ) - | _ => throw () - theorem SimpleFunc.lintegral_eq_lintegral {m : MeasurableSpace α} (f : α →ₛ ℝ≥0∞) (μ : Measure α) : (∫⁻ a, f a ∂μ) = f.lintegral μ := by rw [MeasureTheory.lintegral] diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean index 9add601dc1ec0..9bd3c811bb8ef 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean @@ -638,11 +638,11 @@ section MeasureSpace -- mathport name: «expr∀ᵐ , » notation3 "∀ᵐ "(...)", "r:(scoped P => - Filter.Eventually P MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r + Filter.Eventually P <| MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r -- mathport name: «expr∃ᵐ , » notation3 "∃ᵐ "(...)", "r:(scoped P => - Filter.Frequently P MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r + Filter.Frequently P <| MeasureTheory.Measure.ae MeasureTheory.MeasureSpace.volume) => r /-- The tactic `exact volume`, to be used in optional (`autoParam`) arguments. -/ macro "volume_tac" : tactic => diff --git a/Mathlib/Order/CompleteLattice.lean b/Mathlib/Order/CompleteLattice.lean index dda776c5a2a97..ce33fc3535d48 100644 --- a/Mathlib/Order/CompleteLattice.lean +++ b/Mathlib/Order/CompleteLattice.lean @@ -110,23 +110,9 @@ macro_rules /-- Indexed supremum. -/ notation3 "⨆ "(...)", "r:(scoped f => iSup f) => r -/-- Unexpander for the indexed supremum notation.-/ -@[app_unexpander iSup] -def iSup.unexpander : Lean.PrettyPrinter.Unexpander - | `($_ fun $x:ident ↦ $p) => `(⨆ $x:ident, $p) - | `($_ fun ($x:ident : $ty:term) ↦ $p) => `(⨆ ($x:ident : $ty:term), $p) - | _ => throw () - /-- Indexed infimum. -/ notation3 "⨅ "(...)", "r:(scoped f => iInf f) => r -/-- Unexpander for the indexed infimum notation.-/ -@[app_unexpander iInf] -def iInf.unexpander : Lean.PrettyPrinter.Unexpander - | `($_ fun $x:ident ↦ $p) => `(⨅ $x:ident, $p) - | `($_ fun ($x:ident : $ty:term) ↦ $p) => `(⨅ ($x:ident : $ty:term), $p) - | _ => throw () - instance OrderDual.supSet (α) [InfSet α] : SupSet αᵒᵈ := ⟨(sInf : Set α → α)⟩ diff --git a/Mathlib/Order/Filter/FilterProduct.lean b/Mathlib/Order/Filter/FilterProduct.lean index 5c5d0251b4ed7..522d4c701e5aa 100644 --- a/Mathlib/Order/Filter/FilterProduct.lean +++ b/Mathlib/Order/Filter/FilterProduct.lean @@ -32,7 +32,7 @@ open Classical namespace Filter -local notation3 "∀* "(...)", "r:(scoped p => Filter.Eventually p φ) => r +local notation3 "∀* "(...)", "r:(scoped p => Filter.Eventually p (Ultrafilter.toFilter φ)) => r namespace Germ diff --git a/test/notation3.lean b/test/notation3.lean index 92298455b6ae7..fd7e09861b7f2 100644 --- a/test/notation3.lean +++ b/test/notation3.lean @@ -3,6 +3,8 @@ import Mathlib.Init.Data.Nat.Lemmas namespace Test +-- set_option trace.notation3 true + def Filter (α : Type) : Type := (α → Prop) → Prop def Filter.atTop [Preorder α] : Filter α := fun _ => True def Filter.eventually (p : α → Prop) (f : Filter α) := f p @@ -16,10 +18,38 @@ notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) => notation3 "∃' " (...) ", " r:(scoped p => Exists p) => r #check ∃' x < 3, x < 3 +def func (x : α) : α := x +notation3 "func! " (...) ", " r:(scoped p => func p) => r +-- Make sure it handles additional arguments. Should not consume `(· * 2)`. +-- Note: right now this causes the notation to not pretty print at all. +#check (func! (x : Nat → Nat), x) (· * 2) -notation3 "~{" (x";"* => foldl (a b => (a, b)) ()) "}~" => x +structure MyUnit +notation3 "~{" (x"; "* => foldl (a b => Prod.mk a b) MyUnit) "}~" => x #check ~{1; true; ~{2}~}~ #check ~{}~ -notation3 "%[" (x","* => foldr (a b => a :: b) []) "]" => x +notation3 "%[" (x", "* => foldr (a b => List.cons a b) List.nil) "]" => x #check %[1, 2, 3] + +def foo (a : Nat) (f : Nat → Nat) := a + f a +def bar (a b : Nat) := a * b +notation3 "*[" x "] " (...) ", " v:(scoped c => bar x (foo x c)) => v +#check *[1] (x) (y), x + y +#check bar 1 + +-- Checking that the `<|` macro is expanded when making matcher +def foo' (a : Nat) (f : Nat → Nat) := a + f a +def bar' (a b : Nat) := a * b +notation3 "*'[" x "] " (...) ", " v:(scoped c => bar' x <| foo' x c) => v +#check *'[1] (x) (y), x + y +#check bar' 1 + +-- Currently does not pretty print due to pi type +notation3 (prettyPrint := false) "MyPi " (...) ", " r:(scoped p => (x : _) → p x) => r +#check MyPi (x : Nat) (y : Nat), x < y + +-- The notation parses fine, but the delaborator never succeeds, which is expected +def myId (x : α) := x +notation3 "BAD " c "; " (x", "* => foldl (a b => b) c) " DAB" => myId x +#check BAD 1; 2, 3 DAB