From d904907dfe321764c4f08720e5249d322bfa9143 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Thu, 25 Jul 2024 09:56:23 +0100 Subject: [PATCH 1/7] refactor: extract ctors --- Qpf/Macro/Data.lean | 97 +++----------------------------- Qpf/Macro/Data/Constructors.lean | 65 +++++++++++++++++++++ Qpf/Macro/Data/View.lean | 17 ++++++ Qpf/Macro/NameUtils.lean | 17 ++++++ 4 files changed, 106 insertions(+), 90 deletions(-) create mode 100644 Qpf/Macro/Data/Constructors.lean create mode 100644 Qpf/Macro/NameUtils.lean diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index 23c4eed..a90f705 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -1,10 +1,12 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Cofix import Mathlib.Data.QPF.Multivariate.Constructions.Fix +import Qpf.Macro.Data.Constructors 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 @@ -58,23 +60,13 @@ end -/ open Elab.Term (TermElabM) -def Name.replacePrefix (old_pref new_pref : Name) : Name → Name - | Name.anonymous => Name.anonymous - | Name.str p s => let p' := if p == old_pref then new_pref - else replacePrefix old_pref new_pref p - Name.mkStr p' s - | Name.num p v => let p' := if p == old_pref then new_pref - else replacePrefix old_pref new_pref p - Name.mkNum p' v -def Name.stripPrefix (old_pref : Name) : Name → Name - := Name.replacePrefix old_pref .anonymous def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView := - let declName := Name.replacePrefix pref new_pref ctor.declName + let declName := Name.replacePrefix2 pref new_pref ctor.declName { declName, ref := ctor.ref @@ -121,7 +113,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.replacePrefix view.declName declName ctor.declName + let declName := Name.replacePrefix2 view.declName declName ctor.declName pure { modifiers, declName, ref := ctor.ref @@ -165,7 +157,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.replacePrefix view.declName headTName ctor.declName + let head := mkIdent $ Name.replacePrefix2 view.declName headTName ctor.declName let counts := countVarOccurences r ctor.type? let counts := counts.map fun n => @@ -229,7 +221,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.replacePrefix shapeView.declName headT.getId ctor.declName + let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName `(matchAltExpr| | $alt:ident $argsId:ident* => ⟨$headAlt:ident, fun i => match i with $( @@ -266,7 +258,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.replacePrefix shapeView.declName headT.getId ctor.declName + let headAlt := mkIdent $ Name.replacePrefix2 shapeView.declName headT.getId ctor.declName 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 @@ -421,20 +413,6 @@ def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := do -/-- - Return a syntax tree for `MvQPF.Fix` or `MvQPF.Cofix` when self is `Data`, resp. `Codata`. --/ -def DataCommand.fixOrCofix : DataCommand → Ident - | .Data => mkIdent ``_root_.MvQPF.Fix - | .Codata => mkIdent ``_root_.MvQPF.Cofix - -/-- - Return a syntax tree for `MvPFunctor.W` or `MvPFunctor.M` when self is `Data`, resp. `Codata`. --/ -def DataCommand.fixOrCofixPolynomial : DataCommand → Ident - | .Data => mkIdent ``_root_.MvPFunctor.W - | .Codata => mkIdent ``_root_.MvPFunctor.M - /-- Take either the fixpoint or cofixpoint of `base` to produce an `Internal` uncurried QPF, and define the desired type as the curried version of `Internal` @@ -472,67 +450,6 @@ def mkType (view : DataView) (base : Term × Term × Term) : CommandElabM Unit : trace[QPF] "elabData.cmd = {cmd}" elabCommand cmd - - -open Parser in -/-- - Count the number of arguments to a constructor --/ -partial def countConstructorArgs : Syntax → Nat - | Syntax.node _ ``Term.arrow #[_, _, tail] => 1 + (countConstructorArgs tail) - | _ => 0 - - -open Elab -/-- - Add convenient constructor functions to the environment --/ -def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do - for ctor in view.ctors do - trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}" - let n_args := (ctor.type?.map countConstructorArgs).getD 0 - - let args ← (List.range n_args).mapM fun _ => - do pure <| mkIdent <|← Elab.Term.mkFreshBinderName - let args := args.toArray - - let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk) - let shapeCtor := mkIdent <| Name.replacePrefix view.declName shape ctor.declName - trace[QPF] "shapeCtor = {shapeCtor}" - - - - let body := if n_args = 0 then - `($mk $shapeCtor) - else - `(fun $args:ident* => $mk ($shapeCtor $args:ident*)) - let body ← body - - let explicit ← view.getExplicitExpectedType - let type : Term := TSyntax.mk <| - (ctor.type?.map fun type => - Replace.replaceAllStx view.getExpectedType explicit type - ).getD explicit - let modifiers : Modifiers := { - isNoncomputable := view.modifiers.isNoncomputable - attrs := #[{ - name := `matchPattern - }] - } - let declId := mkIdent <| Name.stripPrefix (←getCurrNamespace) ctor.declName - - let cmd ← `( - $(quote modifiers):declModifiers - def $declId:ident : $type := $body:term - ) - - trace[QPF] "mkConstructor.cmd = {cmd}" - elabCommand cmd - return () - - - - open Macro Comp in /-- Top-level elaboration for both `data` and `codata` declarations diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean new file mode 100644 index 0000000..ac03b9a --- /dev/null +++ b/Qpf/Macro/Data/Constructors.lean @@ -0,0 +1,65 @@ +import Qpf.Macro.Data.Replace +import Qpf.Macro.Data.View +import Qpf.Macro.NameUtils + +open Lean Meta Elab.Command +open PrettyPrinter (delab) + +namespace Data.Command +open Parser in +/-- + Count the number of arguments to a constructor +-/ +partial def countConstructorArgs : Syntax → Nat + | Syntax.node _ ``Term.arrow #[_, _, tail] => 1 + (countConstructorArgs tail) + | _ => 0 + + +open Elab +/-- + Add convenient constructor functions to the environment +-/ +def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do + for ctor in view.ctors do + trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}" + let n_args := (ctor.type?.map countConstructorArgs).getD 0 + + let args ← (List.range n_args).mapM fun _ => + do pure <| mkIdent <|← Elab.Term.mkFreshBinderName + let args := args.toArray + + let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk) + let shapeCtor := mkIdent <| Name.replacePrefix2 view.declName shape ctor.declName + trace[QPF] "shapeCtor = {shapeCtor}" + + + + let body := if n_args = 0 then + `($mk $shapeCtor) + else + `(fun $args:ident* => $mk ($shapeCtor $args:ident*)) + let body ← body + + let explicit ← view.getExplicitExpectedType + let type : Term := TSyntax.mk <| + (ctor.type?.map fun type => + Replace.replaceAllStx view.getExpectedType explicit type + ).getD explicit + let modifiers : Modifiers := { + isNoncomputable := view.modifiers.isNoncomputable + attrs := #[{ + name := `matchPattern + }] + } + let declId := mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ctor.declName + + let cmd ← `( + $(quote modifiers):declModifiers + def $declId:ident : $type := $body:term + ) + + trace[QPF] "mkConstructor.cmd = {cmd}" + elabCommand cmd + return () + +end Data.Command diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean index 6c78c9a..d202d66 100644 --- a/Qpf/Macro/Data/View.lean +++ b/Qpf/Macro/Data/View.lean @@ -1,3 +1,6 @@ +import Mathlib.Data.QPF.Multivariate.Constructions.Cofix +import Mathlib.Data.QPF.Multivariate.Constructions.Fix + import Lean import Qpf.Macro.Common @@ -26,6 +29,20 @@ instance : ToString DataCommand where | .Data => "data" | .Codata => "codata" +/-- + Return a syntax tree for `MvQPF.Fix` or `MvQPF.Cofix` when self is `Data`, resp. `Codata`. +-/ +def fixOrCofix : DataCommand → Ident + | .Data => mkIdent ``_root_.MvQPF.Fix + | .Codata => mkIdent ``_root_.MvQPF.Cofix + +/-- + Return a syntax tree for `MvPFunctor.W` or `MvPFunctor.M` when self is `Data`, resp. `Codata`. +-/ +def fixOrCofixPolynomial : DataCommand → Ident + | .Data => mkIdent ``_root_.MvPFunctor.W + | .Codata => mkIdent ``_root_.MvPFunctor.M + end DataCommand diff --git a/Qpf/Macro/NameUtils.lean b/Qpf/Macro/NameUtils.lean new file mode 100644 index 0000000..c9bddfc --- /dev/null +++ b/Qpf/Macro/NameUtils.lean @@ -0,0 +1,17 @@ +open Lean Meta + +namespace Lean.Name +-- This function has diffreent behaviour from Name.replacePrefix +def replacePrefix2 (old_pref new_pref : Name) : Name → Name + | Name.anonymous => Name.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 From 05a9195c85f53e4e4f7f2baf8933b6b017ae9b58 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Thu, 25 Jul 2024 10:45:02 +0100 Subject: [PATCH 2/7] refactor: genralize utils --- Qpf/Macro/Data/Constructors.lean | 25 ++++++++++++++----------- Qpf/Macro/Data/View.lean | 8 ++++++-- 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean index ac03b9a..9ef1104 100644 --- a/Qpf/Macro/Data/Constructors.lean +++ b/Qpf/Macro/Data/Constructors.lean @@ -2,7 +2,7 @@ import Qpf.Macro.Data.Replace import Qpf.Macro.Data.View import Qpf.Macro.NameUtils -open Lean Meta Elab.Command +open Lean Meta Elab Elab.Command open PrettyPrinter (delab) namespace Data.Command @@ -15,11 +15,7 @@ partial def countConstructorArgs : Syntax → Nat | _ => 0 -open Elab -/-- - Add convenient constructor functions to the environment --/ -def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do +def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Ident) (ty : Term) := do for ctor in view.ctors do trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}" let n_args := (ctor.type?.map countConstructorArgs).getD 0 @@ -40,18 +36,15 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do `(fun $args:ident* => $mk ($shapeCtor $args:ident*)) let body ← body - let explicit ← view.getExplicitExpectedType let type : Term := TSyntax.mk <| - (ctor.type?.map fun type => - Replace.replaceAllStx view.getExpectedType explicit type - ).getD explicit + (ctor.type?.map fun type => Replace.replaceAllStx view.getExpectedType ty type).getD ty let modifiers : Modifiers := { isNoncomputable := view.modifiers.isNoncomputable attrs := #[{ name := `matchPattern }] } - let declId := mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ctor.declName + let declId := nameGen ctor let cmd ← `( $(quote modifiers):declModifiers @@ -62,4 +55,14 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do elabCommand cmd return () +/-- + Add convenient constructor functions to the environment +-/ +def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do + let explicit ← view.getExplicitExpectedType + let nameGen := (mkIdent <| Name.stripPrefix2 (←getCurrNamespace) ·.declName) + + mkConstructorsWithNameAndType view shape nameGen explicit + + end Data.Command diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean index d202d66..72c6c63 100644 --- a/Qpf/Macro/Data/View.lean +++ b/Qpf/Macro/Data/View.lean @@ -122,11 +122,15 @@ def DataView.addDeclNameSuffix (view : DataView) (suffix : String) : DataView /-- Returns the fully applied form of the type to be defined -/ -def DataView.getExpectedType (view : DataView) : Term - := Syntax.mkApp (mkIdent view.shortDeclName) ( +def DataView.getExpectedTypeWithId (view : DataView) (id : Ident) : Term + := Syntax.mkApp id ( (Macro.getBinderIdents view.binders.getArgs false) ) +/-- Returns the fully applied form of the type to be defined -/ +def DataView.getExpectedType (view : DataView) : Term + := view.getExpectedTypeWithId (mkIdent view.shortDeclName) + /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/ def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term := let args := Macro.getBinderIdents view.binders.getArgs true 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 3/7] 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 4/7] 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 From 83ef0a8ad436e7d2bb01a190cb69e820edb1169d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Thu, 8 Aug 2024 14:58:44 +0100 Subject: [PATCH 5/7] chore: style changes --- Qpf/Macro/Data.lean | 2 +- Qpf/Macro/Data/Constructors.lean | 14 ++++++-------- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index 744014f..861d3a9 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -65,7 +65,7 @@ open Elab.Term (TermElabM) def CtorView.declReplacePrefix (pref new_pref : Name) (ctor: CtorView) : CtorView := - let declName := Name.replacePrefix ctor.declName pref new_pref + let declName := ctor.declName.replacePrefix pref new_pref { declName, ref := ctor.ref diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean index 26b6f3e..179ae04 100644 --- a/Qpf/Macro/Data/Constructors.lean +++ b/Qpf/Macro/Data/Constructors.lean @@ -23,21 +23,19 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}" let n_args := (ctor.type?.map countConstructorArgs).getD 0 - let args ← (List.range n_args).mapM fun _ => - do pure <| mkIdent <|← Elab.Term.mkFreshBinderName - let args := args.toArray + let args := (← (List.range n_args).mapM + fun _ => do pure <| mkIdent <|← Elab.Term.mkFreshBinderName).toArray - let mk := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk) + let pointConstructor := mkIdent ((DataCommand.fixOrCofix view.command).getId ++ `mk) let shapeCtor := mkIdent <| Name.replacePrefix ctor.declName view.declName shape trace[QPF] "shapeCtor = {shapeCtor}" - let body := if n_args = 0 then - `($mk $shapeCtor) + let body ← if n_args = 0 then + `($pointConstructor $shapeCtor) else - `(fun $args:ident* => $mk ($shapeCtor $args:ident*)) - let body ← body + `(fun $args:ident* => $pointConstructor ($shapeCtor $args:ident*)) let explicit ← view.getExplicitExpectedType let type : Term := TSyntax.mk <| From da244f22ff7074cd1b9eb98938793a311f779ed4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= <47296141+Equilibris@users.noreply.github.com> Date: Tue, 13 Aug 2024 17:07:28 +0200 Subject: [PATCH 6/7] chore: fix ws --- Qpf/Macro/Data/Constructors.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean index d04d8d1..3d7bc1b 100644 --- a/Qpf/Macro/Data/Constructors.lean +++ b/Qpf/Macro/Data/Constructors.lean @@ -1,7 +1,7 @@ import Qpf.Macro.Data.Replace import Qpf.Macro.Data.View -open Lean Meta Elab Elab.Command +open Lean Meta Elab Elab.Command open PrettyPrinter (delab) namespace Data.Command From 7ac7a05859ff4bbbaf5cfde2ba9af8352d908826 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?William=20S=C3=B8rensen?= Date: Wed, 14 Aug 2024 15:06:38 +0100 Subject: [PATCH 7/7] fix: comments --- Qpf/Macro/Data/Constructors.lean | 12 +++++++++--- Qpf/Macro/Data/View.lean | 16 +++++++++------- 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/Qpf/Macro/Data/Constructors.lean b/Qpf/Macro/Data/Constructors.lean index 3d7bc1b..bb03706 100644 --- a/Qpf/Macro/Data/Constructors.lean +++ b/Qpf/Macro/Data/Constructors.lean @@ -13,7 +13,13 @@ partial def countConstructorArgs : Syntax → Nat | Syntax.node _ ``Term.arrow #[_, _, tail] => 1 + (countConstructorArgs tail) | _ => 0 -def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Ident) (ty : Term) := do +/-- + Add definitions for constructors + that are generic across two input types shape and name. + Additionally we allow the user to control how names are generated. +-/ +def mkConstructorsWithNameAndType (view : DataView) (shape : Name) + (nameGen : CtorView → Name) (ty : Term) : CommandElabM Unit := do for ctor in view.ctors do trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}" let n_args := (ctor.type?.map countConstructorArgs).getD 0 @@ -38,7 +44,7 @@ def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : Ct name := `matchPattern }] } - let declId := nameGen ctor + let declId := mkIdent $ nameGen ctor let cmd ← `( $(quote modifiers):declModifiers @@ -54,7 +60,7 @@ def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : Ct -/ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do let explicit ← view.getExplicitExpectedType - let nameGen := (mkIdent <| ·.declName.replacePrefix (←getCurrNamespace) .anonymous) + let nameGen := (·.declName.replacePrefix (←getCurrNamespace) .anonymous) mkConstructorsWithNameAndType view shape nameGen explicit diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean index 72c6c63..1d46533 100644 --- a/Qpf/Macro/Data/View.lean +++ b/Qpf/Macro/Data/View.lean @@ -121,15 +121,17 @@ def DataView.addDeclNameSuffix (view : DataView) (suffix : String) : DataView { view with declName, declId, shortDeclName } -/-- Returns the fully applied form of the type to be defined -/ -def DataView.getExpectedTypeWithId (view : DataView) (id : Ident) : Term - := Syntax.mkApp id ( - (Macro.getBinderIdents view.binders.getArgs false) - ) +/-- + Returns the fully applied form of the type to be defined. + The `name` parameter allows the user to control what the const at the bottom of the type is. + This lets the user get types that have the same parameters such as the DeepThunk types. +-/ +def DataView.getExpectedTypeWithName (view : DataView) (name : Name) : Term := + Macro.getBinderIdents view.binders.getArgs false |> Syntax.mkApp (mkIdent name) /-- Returns the fully applied form of the type to be defined -/ -def DataView.getExpectedType (view : DataView) : Term - := view.getExpectedTypeWithId (mkIdent view.shortDeclName) +def DataView.getExpectedType (view : DataView) : Term := + view.getExpectedTypeWithName view.shortDeclName /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/ def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term