From afd8df3b895e78c6f3e10794502d49eb9c24db49 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?William=20S=C3=B8rensen?= <ws423@cam.ac.uk>
Date: Wed, 14 Aug 2024 15:06:38 +0100
Subject: [PATCH] fix: comments

---
 Qpf/Macro/Data/Constructors.lean | 12 +++++++++---
 Qpf/Macro/Data/View.lean         | 14 ++++++++------
 2 files changed, 17 insertions(+), 9 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..4fd9280 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)
+  := view.getExpectedTypeWithName view.shortDeclName
 
 /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/
 def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term