From 628be67e664955eb7088e146a4bceeb29ab1a34f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jul 2020 16:48:45 -0700
Subject: [PATCH] feat: remove unused scope variables

---
 src/Lean/Elab/Inductive.lean | 14 ++++++-------
 src/Lean/Elab/Structure.lean | 38 +++++++++++++++++++++++++++++++++---
 2 files changed, 42 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index b0eec274f2..5bbbf32707 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -270,14 +270,13 @@ private def getResultingUniverse (ref : Syntax) : List InductiveType → TermEla
   | Expr.sort u _ => pure u
   | _             => Term.throwError ref "unexpected inductive type resulting type"
 
-private def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
+def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
 
 /--
-  Return true if the resulting universe level is of the form `?m + k`.
-  Return false if the resulting universe level does not contain universe metavariables.
-  Throw exeception otherwise. -/
-private def shouldInferResultUniverse (ref : Syntax) (indTypes : List InductiveType) : TermElabM Bool := do
-u ← getResultingUniverse ref indTypes;
+  Return true if `u` is of the form `?m + k`.
+  Return false if `u` does not contain universe metavariables.
+  Throw exception otherwise. -/
+def shouldInferResultUniverse (ref : Syntax) (u : Level) : TermElabM Bool := do
 u ← Term.instantiateLevelMVars ref u;
 if u.hasMVar then
   match u.getLevelOffset with
@@ -449,7 +448,8 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
       [];
     let indTypes := indTypes.reverse;
     Term.synthesizeSyntheticMVars false;  -- resolve pending
-    inferLevel ← shouldInferResultUniverse ref indTypes;
+    u ← getResultingUniverse ref indTypes;
+    inferLevel ← shouldInferResultUniverse ref u;
     withUsed ref vars indTypes $ fun vars => do
       let numParams := vars.size + numExplicitParams;
       indTypes ← updateParams ref vars indTypes;
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 7dc668d330..a86c1e2dd1 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -254,13 +254,45 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
   else
     k infos
 
+private def getResultUniverse (ref : Syntax) (type : Expr) : TermElabM Level := do
+type ← Term.whnf ref type;
+match type with
+| Expr.sort u _ => pure u
+| _             => Term.throwError ref "unexpected structure resulting type"
+
+private def removeUnused (ref : Syntax) (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
+    : TermElabM (LocalContext × LocalInstances × Array Expr) := do
+used ← params.foldlM (Term.collectUsedFVars ref) {};
+used ← fieldInfos.foldlM
+  (fun (used : CollectFVars.State) info => do
+    fvarType ← Term.inferType ref info.fvar;
+    used ← Term.collectUsedFVars ref used fvarType;
+    match info.value? with
+    | none       => pure used
+    | some value => Term.collectUsedFVars ref used value)
+  used;
+Term.removeUnused ref scopeVars used
+
+private def withUsed {α} (ref : Syntax) (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (k : Array Expr → TermElabM α)
+    : TermElabM α := do
+(lctx, localInsts, vars) ← removeUnused ref scopeVars params fieldInfos;
+Term.withLCtx lctx localInsts $ k vars
+
 private def elabStructureView (view : StructView) : TermElabM ElabStructResult := do
+let numExplicitParams := view.params.size;
 type ← Term.elabType view.type;
 unless (validStructType type) $ Term.throwError view.type "expected Type";
+let ref := view.ref;
 withParents view 0 #[] fun fieldInfos =>
-withFields view.fields 0 fieldInfos fun fieldInfos =>
-  -- TODO
-  Term.throwError view.ref "WIP"
+withFields view.fields 0 fieldInfos fun fieldInfos => do
+  Term.synthesizeSyntheticMVars false;  -- resolve pending
+  u ← getResultUniverse ref type;
+  inferLevel ← shouldInferResultUniverse ref u;
+  withUsed ref view.scopeVars view.params fieldInfos $ fun scopeVars => do
+    let numParams := scopeVars.size + numExplicitParams;
+
+    -- TODO
+    Term.throwError view.ref ("WIP " ++ toString scopeVars)
 
 /-
 parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields