From 13dd278508539147b11d8b9b1d1ce5c59eff0cef Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 18 Dec 2024 15:06:22 +0000
Subject: [PATCH] fix elaboration code

---
 Qpf/Macro/Data.lean      | 8 +++++---
 Qpf/Macro/Data/View.lean | 7 +++----
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
index 866af88..36d48f2 100644
--- a/Qpf/Macro/Data.lean
+++ b/Qpf/Macro/Data.lean
@@ -139,7 +139,8 @@ def mkHeadT (view : InductiveView) : CommandElabM Name := do
   }
 
   withQPFTraceNode "elabInductiveViews" <|
-    elabInductiveViews #[view]
+    runTermElabM <| fun vars =>
+      elabInductiveViews vars #[view]
   pure declName
 
 open Parser Parser.Term Parser.Command in
@@ -358,7 +359,8 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do
   return ⟨r, declName, PName, do
     withQPFTraceNode "mkShape effects" <| do
 
-    elabInductiveViews #[view]
+    runTermElabM <| fun vars =>
+      elabInductiveViews vars #[view]
 
     let headTName ← mkHeadT view
     let childTName ← mkChildT view r headTName
@@ -444,7 +446,7 @@ open Macro Comp in
 def elabData : CommandElab := fun stx =>
   withQPFTraceNode "elabData" (tag := "elabData") (collapsed := false) <| do
 
-  let modifiers ← elabModifiers stx[0]
+  let modifiers ← elabModifiers ⟨stx[0]⟩
   let decl := stx[1]
 
   let view ← dataSyntaxToView modifiers decl
diff --git a/Qpf/Macro/Data/View.lean b/Qpf/Macro/Data/View.lean
index 77bbb83..9d756db 100644
--- a/Qpf/Macro/Data/View.lean
+++ b/Qpf/Macro/Data/View.lean
@@ -270,11 +270,11 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
   let (binders, type?) := expandOptDeclSig decl[2]
 
   let declId  : TSyntax ``declId := ⟨decl[1]⟩
-  let ⟨name, declName, levelNames⟩ ← expandDeclId declId modifiers
-  addDeclarationRanges declName decl
+  let ⟨name, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) declId modifiers
+  -- addDeclarationRanges declName decl
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     -- def ctor := leading_parser optional docComment >> "\n| " >> declModifiers >> rawIdent >> optDeclSig
-    let mut ctorModifiers ← elabModifiers ctor[2]
+    let mut ctorModifiers ← elabModifiers ⟨ctor[2]⟩
     if let some leadingDocComment := ctor[0].getOptional? then
       if ctorModifiers.docString?.isSome then
         logErrorAt leadingDocComment "duplicate doc string"
@@ -289,7 +289,6 @@ def dataSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM Data
     let ctorName ← withRef ctor[3] $ applyVisibility ctorModifiers.visibility ctorName
     let (binders, type?) := expandOptDeclSig ctor[4]
     addDocString' ctorName ctorModifiers.docString?
-    addAuxDeclarationRanges ctorName ctor ctor[3]
     return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, binders := binders, type? := type? : CtorView }
   let classes ← liftCoreM <| getOptDerivingClasses decl[5]