From 1731962ea9026b52880d0ac97e47dd2cb50a946f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 11 Sep 2020 10:42:39 -0700
Subject: [PATCH] feat: elaborate `emptyC` notation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

@Kha this is a little bit ugly. As in Lean3, the notation `{ }` is
overloaded. It can be `HasEmptyc.emptyc` or the empty structure.
Moreover, if we have an instance `HasEmptyc A` for a structure `A`,
then `{ }` is notation for `HasEmptyc.emptyc`. I am not very happy
about this, but it seems users use this feature. It is even used in
our own Lean4 code base :)

BTW, I will try a different alternative later.
First, move the notation `{ }` as a proper parser for `emptyc`.
Then, make sure the elaborator throws an error when
`{ }` is ambiguous. That is, `{}` can be elaborated as the empty
structure `A` and there is an `HasEmptyc A` instance.
Example:
```
structure A :=
(x : Nat := 0)

instance : HasEmptyc A :=
⟨{ x := 10 }⟩
```

The main issue here is that the support for choice+postpone is
currently broken.
---
 src/Lean/Elab/StructInst.lean | 32 +++++++++++++++++++++++++++-----
 tests/lean/run/emptyc.lean    | 22 ++++++++++++++++++++++
 2 files changed, 49 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/emptyc.lean

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index bfa99d8ef1..d6fef9d23a 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -773,6 +773,17 @@ else
   let stxNew   := stx.setArg 4 mkNullNode;
   `(($stxNew : $expected))
 
+private def isEmptyStructInst (stx : Syntax) : Bool :=
+(stx.getArg 1).isNone &&
+(stx.getArg 2).isNone &&
+(stx.getArg 3).isNone &&
+(stx.getArg 4).isNone
+
+@[builtinTermElab emptyC] def expandEmptyC : TermElab :=
+fun stx expectedType? => do
+  stxNew ← `(HasEmptyc.emptyc);
+  withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+
 @[builtinTermElab structInst] def elabStructInst : TermElab :=
 fun stx expectedType? => do
   stxNew? ← liftMacroM $ expandStructInstExpectedType stx;
@@ -784,11 +795,22 @@ fun stx expectedType? => do
     | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
     | none => do
       sourceView ← getStructSource stx;
-      modifyOp?  ← isModifyOp? stx;
-      match modifyOp?, sourceView with
-      | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
-      | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
-      | _,             _                        => elabStructInstAux stx expectedType? sourceView
+      if isEmptyStructInst stx then do
+        /- Recall that we also want to use `{}` as notation for `HasEmptyc.emptyc` -/
+        tryPostponeIfNoneOrMVar expectedType?;
+        match expectedType? with
+        | none => expandEmptyC stx expectedType?
+        | some expectedType =>
+          /- We first try to create `@HasEmptyc.emptyc expectedType _`, if it fails, we elaborate as the empty structure. -/
+          catch
+            (mkAppOptM `HasEmptyc.emptyc #[expectedType, none])
+            (fun _ => elabStructInstAux stx expectedType? sourceView)
+      else do
+        modifyOp?  ← isModifyOp? stx;
+        match modifyOp?, sourceView with
+        | some modifyOp, Source.explicit source _ => elabModifyOp stx modifyOp source expectedType?
+        | some _,        _                        => throwError ("invalid {...} notation, explicit source is required when using '[<index>] := <value>'")
+        | _,             _                        => elabStructInstAux stx expectedType? sourceView
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Elab.struct;
diff --git a/tests/lean/run/emptyc.lean b/tests/lean/run/emptyc.lean
new file mode 100644
index 0000000000..1e477ac9c2
--- /dev/null
+++ b/tests/lean/run/emptyc.lean
@@ -0,0 +1,22 @@
+new_frontend
+
+structure A :=
+(x : Nat := 0)
+
+def foo : A :=
+{}
+
+theorem ex1 : foo = { x := 0 } :=
+rfl
+
+theorem ex2 : foo.x = 0 :=
+rfl
+
+instance : HasEmptyc A :=
+⟨{ x := 10 }⟩
+
+def boo : A :=
+{} -- this HasEmptyc.emptyc
+
+theorem ex3 : boo.x = 10 :=
+rfl