From 5884b9c19aef7cb10a0b10f4838445f8be7a40bb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2020 18:06:22 -0800
Subject: [PATCH] feat: add support for `instance ... where`

@Kha The fields are not mutually recursive yet, but it is good enough
 for writing examples in the manual.

See new test
---
 src/Lean/Elab/MutualDef.lean      | 42 ++++++++++++++++++++++++++++++-
 src/Lean/Parser/Command.lean      |  2 +-
 tests/lean/run/instanceWhere.lean | 23 +++++++++++++++++
 3 files changed, 65 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/instanceWhere.lean

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 1ef3568a90..d5b4b91e04 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -122,6 +122,44 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
       k fvars
   loop 0 #[]
 
+private def expandWhereDeclsAsStructInst (whereDecls : Syntax) : MacroM Syntax := do
+  /- def whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";")) -/
+  let letDecls ← whereDecls[1].getArgs.mapM fun stx => do
+    unless stx[0].isNone do
+      Macro.throwErrorAt stx "attributes are 'where' elements are currently not supported here"
+    let mut letDecl := stx[1]
+    if letDecl[0].isOfKind `Lean.Parser.Term.letPatDecl then
+      Macro.throwErrorAt stx "patterns are not allowed here"
+    if letDecl[0].getKind == `Lean.Parser.Term.letEqnsDecl then
+      letDecl := letDecl.setArg 0 (← expandLetEqnsDecl letDecl[0])
+    pure letDecl
+  let structInstFields ← letDecls.mapM fun letDecl => do
+    let letIdDecl := letDecl[0]
+    let fieldId   := letIdDecl[0]
+    let mut val   := letIdDecl[4]
+    let optType   := letIdDecl[2]
+    let binders   := letIdDecl[1]
+    unless optType.isNone do
+      let type := optType[0][1]
+      val ← `(($val : $type))
+    unless binders.isNone do
+      let binders := binders.getArgs
+      val ← `(fun $binders* => $val:term)
+      val := val.copyInfo letIdDecl
+    return Syntax.node `Lean.Parser.Term.structInstField #[
+      fieldId, mkNullNode, mkAtomFrom fieldId ":=", val
+    ]
+  let ref := whereDecls
+  let structInst := Syntax.node `Lean.Parser.Term.structInst #[
+      mkAtomFrom ref "{",
+      mkNullNode,
+      mkNullNode <| structInstFields.map fun field => mkNullNode #[field, mkNullNode],
+      mkNullNode,
+      mkNullNode,
+      mkAtomFrom ref "}"
+    ]
+  return structInst
+
 /-
 Recall that
 ```
@@ -131,7 +169,7 @@ withPosition $ fun pos =>
   sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 def declValSimple    := parser! " :=\n" >> termParser >> optional Term.whereDecls
 def declValEqns      := parser! Term.matchAltsWhereDecls
-def declVal          := declValSimple <|> declValEqns
+def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
 ```
 -/
 private def declValToTerm (declVal : Syntax) : MacroM Syntax :=
@@ -139,6 +177,8 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax :=
     return expandWhereDeclsOpt declVal declVal[2] declVal[1]
   else if declVal.isOfKind `Lean.Parser.Command.declValEqns then
     expandMatchAltsWhereDecls declVal declVal[0]
+  else if declVal.isOfKind `Lean.Parser.Term.whereDecls then
+    expandWhereDeclsAsStructInst declVal
   else
     Macro.throwErrorAt declVal "unexpected definition value"
 
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 5dcff3a1d8..4226a17a60 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -37,7 +37,7 @@ def declSig          := parser! many (ppSpace >> (Term.simpleBinderWithoutType <
 def optDeclSig       := parser! many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
 def declValSimple    := parser! " :=\n" >> termParser >> optional Term.whereDecls
 def declValEqns      := parser! Term.matchAltsWhereDecls
-def declVal          := declValSimple <|> declValEqns
+def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
 def «abbrev»         := parser! "abbrev " >> declId >> optDeclSig >> declVal
 def «def»            := parser! "def " >> declId >> optDeclSig >> declVal
 def «theorem»        := parser! "theorem " >> declId >> declSig >> declVal
diff --git a/tests/lean/run/instanceWhere.lean b/tests/lean/run/instanceWhere.lean
new file mode 100644
index 0000000000..85a10d65e5
--- /dev/null
+++ b/tests/lean/run/instanceWhere.lean
@@ -0,0 +1,23 @@
+namespace Exp
+universes u v w
+
+def StateT' (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+  σ → m (α × σ)
+
+instance [Monad m] : Monad (StateT' σ m) where
+  pure a := fun s => pure (a, s)
+
+  bind x f := fun s => do
+    let (a, s) ← x s
+    f a s
+
+  map f x := fun s => do
+    let (a, s) ← x s
+    pure (f a, s)
+
+instance [ToString α] [ToString β] : ToString (Sum α β) where
+  toString : Sum α β → String
+    | Sum.inr a => "inl" ++ toString a
+    | Sum.inl b => "inr" ++ toString b
+
+end Exp