From e5710e7101bd6de24167ea14ac25a22f7fd7c41a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Thu, 8 Aug 2024 11:53:06 +0100 Subject: [PATCH 1/2] docs: why replacePrefix2 is different --- Qpf/Macro/NameUtils.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Qpf/Macro/NameUtils.lean b/Qpf/Macro/NameUtils.lean index c9bddfc..3f41546 100644 --- a/Qpf/Macro/NameUtils.lean +++ b/Qpf/Macro/NameUtils.lean @@ -1,9 +1,16 @@ open Lean Meta namespace Lean.Name --- This function has diffreent behaviour from Name.replacePrefix +/-- + This function has different behaviour from Name.replacePrefix that can be viewed in the following example: + + #eval replacePrefix `a `b `a.b -- `a + #eval replacePrefix2 `a `b `a.b -- `b.b + + This comes from the internal declaration of replacePrefix dropping the last named value before continuing +-/ def replacePrefix2 (old_pref new_pref : Name) : Name → Name - | Name.anonymous => Name.anonymous + | Name.anonymous => .anonymous | Name.str p s => let p' := if p == old_pref then new_pref else replacePrefix2 old_pref new_pref p Name.mkStr p' s From 0dc4cb33a6f7225eabc6dbbd930d0ba29df7c725 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Thu, 8 Aug 2024 14:23:25 +0100 Subject: [PATCH 2/2] refactor: use Lean's replacePrefix --- Qpf/Macro/Data.lean | 11 +++++------ Qpf/Macro/Data/Constructors.lean | 5 ++--- Qpf/Macro/NameUtils.lean | 24 ------------------------ 3 files changed, 7 insertions(+), 33 deletions(-) delete mode 100644 Qpf/Macro/NameUtils.lean diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index a90f705..744014f 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -6,7 +6,6 @@ import Qpf.Macro.Data.Replace import Qpf.Macro.Data.Count import Qpf.Macro.Data.View import Qpf.Macro.Data.Ind -import Qpf.Macro.NameUtils import Qpf.Macro.Common import Qpf.Macro.Comp @@ -66,7 +65,7 @@ open Elab.Term (TermElabM) def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView := - let declName := Name.replacePrefix2 pref new_pref ctor.declName + let declName := Name.replacePrefix ctor.declName pref new_pref { declName, ref := ctor.ref @@ -113,7 +112,7 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do } -- The head type is the same as the original type, but with all constructor arguments removed let ctors ← view.ctors.mapM fun ctor => do - let declName := Name.replacePrefix2 view.declName declName ctor.declName + let declName := ctor.declName.replacePrefix view.declName declName pure { modifiers, declName, ref := ctor.ref @@ -157,7 +156,7 @@ def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandEl let target_type := Syntax.mkApp (mkIdent ``TypeVec) #[quote r.arity] let matchAlts ← view.ctors.mapM fun ctor => do - let head := mkIdent $ Name.replacePrefix2 view.declName headTName ctor.declName + let head := Lean.mkIdent (ctor.declName.replacePrefix view.declName headTName) let counts := countVarOccurences r ctor.type? let counts := counts.map fun n => @@ -221,7 +220,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide let boxBody ← ctors.mapM fun (ctor, args) => do let argsId := args.args.map mkIdent let alt := mkIdent ctor.declName - let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName + let headAlt := mkIdent $ ctor.declName.replacePrefix shapeView.declName headT.getId `(matchAltExpr| | $alt:ident $argsId:ident* => ⟨$headAlt:ident, fun i => match i with $( @@ -258,7 +257,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide let unbox_child := mkIdent <|<- Elab.Term.mkFreshBinderName; let unboxBody ← ctors.mapM fun (ctor, args) => do let alt := mkIdent ctor.declName - let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName + let headAlt := mkIdent $ ctor.declName.replacePrefix shapeView.declName headT.getId let args : Array Term ← args.args.mapM fun arg => do -- find the pair `(i, j)` such that the argument is the `j`-th occurence of the `i`-th type diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean index ac03b9a..26b6f3e 100644 --- a/Qpf/Macro/Data/Constructors.lean +++ b/Qpf/Macro/Data/Constructors.lean @@ -1,6 +1,5 @@ import Qpf.Macro.Data.Replace import Qpf.Macro.Data.View -import Qpf.Macro.NameUtils open Lean Meta Elab.Command open PrettyPrinter (delab) @@ -29,7 +28,7 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do let args := args.toArray let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk) - let shapeCtor := mkIdent <| Name.replacePrefix2 view.declName shape ctor.declName + let shapeCtor := mkIdent <| Name.replacePrefix ctor.declName view.declName shape trace[QPF] "shapeCtor = {shapeCtor}" @@ -51,7 +50,7 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do name := `matchPattern }] } - let declId := mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ctor.declName + let declId := mkIdent <| ctor.declName.replacePrefix (←getCurrNamespace) .anonymous let cmd ← `( $(quote modifiers):declModifiers diff --git a/Qpf/Macro/NameUtils.lean b/Qpf/Macro/NameUtils.lean deleted file mode 100644 index 3f41546..0000000 --- a/Qpf/Macro/NameUtils.lean +++ /dev/null @@ -1,24 +0,0 @@ -open Lean Meta - -namespace Lean.Name -/-- - This function has different behaviour from Name.replacePrefix that can be viewed in the following example: - - #eval replacePrefix `a `b `a.b -- `a - #eval replacePrefix2 `a `b `a.b -- `b.b - - This comes from the internal declaration of replacePrefix dropping the last named value before continuing --/ -def replacePrefix2 (old_pref new_pref : Name) : Name → Name - | Name.anonymous => .anonymous - | Name.str p s => let p' := if p == old_pref then new_pref - else replacePrefix2 old_pref new_pref p - Name.mkStr p' s - | Name.num p v => let p' := if p == old_pref then new_pref - else replacePrefix2 old_pref new_pref p - Name.mkNum p' v - - -def stripPrefix2 (old_pref : Name) : Name → Name - := Name.replacePrefix2 old_pref .anonymous -end Lean.Name