feat: elaborate binders

src/Init/Lean/Elab/Command.lean

@@ -24,7 +24,7 @@ structure Scope :=
 (ns          : Name := Name.anonymous) -- current namespace
 (openDecls   : List OpenDecl := [])
 (univNames   : List Name := [])
-(varDecls    : List Syntax := [])
+(varDecls    : Array Syntax := #[])
 
 instance Scope.inhabited : Inhabited Scope := ⟨{ kind := "", header := "" }⟩
 
@@ -95,25 +95,33 @@ stx.ifNode
     | none      => logError stx ("command '" ++ toString k ++ "' has not been implemented"))
   (fun _ => logErrorUsingCmdPos ("unexpected command"))
 
-@[specialize] def runTermElabM {α} (x : TermElabM α) : CommandElabM α :=
-fun ctx s =>
-  let scope := s.scopes.head!;
-  let termCtx : Term.Context := {
-    config         := { opts := scope.options, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
-    fileName       := ctx.fileName,
-    fileMap        := ctx.fileMap,
-    cmdPos         := s.cmdPos,
-    ns             := scope.ns,
-    univNames      := scope.univNames,
-    openDecls      := scope.openDecls
-  };
-  let termState : Term.State := {
-    env      := s.env,
-    messages := s.messages
-  };
-  match (tracingAtPos s.cmdPos x) termCtx termState with
-  | EStateM.Result.ok a newS     => EStateM.Result.ok a { env := newS.env, messages := newS.messages, .. s }
-  | EStateM.Result.error ex newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s }
+private def mkTermContext (ctx : Context) (s : State) : Term.Context :=
+let scope := s.scopes.head!;
+{ config         := { opts := scope.options, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
+  fileName       := ctx.fileName,
+  fileMap        := ctx.fileMap,
+  cmdPos         := s.cmdPos,
+  ns             := scope.ns,
+  univNames      := scope.univNames,
+  openDecls      := scope.openDecls }
+
+private def mkTermState (s : State) : Term.State :=
+{ env      := s.env,
+  messages := s.messages }
+
+private def getVarDecls (s : State) : Array Syntax :=
+s.scopes.head!.varDecls
+
+private def toCommandResult {α} (s : State) (result : EStateM.Result Exception Term.State α) : EStateM.Result Exception State α :=
+match result with
+| EStateM.Result.ok a newS     => EStateM.Result.ok a { env := newS.env, messages := newS.messages, .. s }
+| EStateM.Result.error ex newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s }
+
+@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α :=
+fun ctx s => toCommandResult s $ tracingAtPos s.cmdPos (Term.elabBinders (getVarDecls s) x) (mkTermContext ctx s) (mkTermState s)
+
+def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit :=
+_root_.dbgTrace (toString a) $ fun _ => pure ()
 
 def getEnv : CommandElabM Environment :=
 do s ← get; pure s.env
@@ -323,6 +331,22 @@ fun n => do
 @[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()
 @[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure ()
 
+@[builtinCommandElab «variable»] def elabVariable : CommandElab :=
+fun n => do
+  -- `variable` bracktedBinder
+  let binder := n.getArg 1;
+  -- Try to elaborate `binder` for sanity checking
+  runTermElabM $ Term.elabBinder binder $ pure ();
+  modifyScope $ fun scope => { varDecls := scope.varDecls.push binder, .. scope }
+
+@[builtinCommandElab «variables»] def elabVariables : CommandElab :=
+fun n => do
+  -- `variables` bracktedBinder+
+  let binders := (n.getArg 1).getArgs;
+  -- Try to elaborate `binders` for sanity checking
+  runTermElabM $ Term.elabBinders binders $ pure ();
+  modifyScope $ fun scope => { varDecls := scope.varDecls ++ binders, .. scope }
+
 end Command
 
 /-

src/Init/Lean/Elab/Term.lean

@@ -27,9 +27,11 @@ inductive SyntheticMVarInfo
 | postponed (macroStack : List Syntax) : SyntheticMVarInfo
 
 structure State extends Meta.State :=
-(macroStack     : List Syntax := [])
-(syntheticMVars : List (MVarId × SyntheticMVarInfo) := [])
-(messages       : MessageLog := {})
+(macroStack      : List Syntax := [])
+(syntheticMVars  : List (MVarId × SyntheticMVarInfo) := [])
+(messages        : MessageLog := {})
+(instImplicitIdx : Nat := 1)
+(anonymousIdx    : Nat := 1)
 
 abbrev TermElabM := ReaderT Context (EStateM Exception State)
 abbrev TermElab  := SyntaxNode → Option Expr → TermElabM Expr
@@ -86,6 +88,8 @@ fun ctx s => match x ctx.toContext s.toState with
   | EStateM.Result.ok a newS     => EStateM.Result.ok a { toState := newS, .. s }
   | EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s }
 
+def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx
+def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances
 def getOptions : TermElabM Options       := do ctx ← read; pure ctx.config.opts
 def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState
 def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { traceState := traceState, .. s }
@@ -106,24 +110,28 @@ _root_.dbgTrace (toString a) $ fun _ => pure ()
 def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.isDefEq t s
 def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e
 def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e
+def isClass (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass t
 def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
 def mkFreshExprMVar (type : Expr) (userName? : Name := Name.anonymous) (synthetic : Bool := false) : TermElabM Expr :=
 liftMetaM $ Meta.mkFreshExprMVar type userName? synthetic
 
+@[inline] def withNode {α} (stx : Syntax) (x : SyntaxNode → TermElabM α) : TermElabM α :=
+stx.ifNode x (fun _ => throw $ Exception.other "term elaborator failed, unexpected syntax")
+
 def elabTerm (stx : Syntax) (expectedType : Option Expr) : TermElabM Expr :=
-stx.ifNode
-  (fun n => do
-    s ← get;
-    let tables := termElabAttribute.ext.getState s.env;
-    let k := n.getKind;
-    match tables.find k with
-    | some elab => tracingAt stx $ elab n expectedType
-    | none      => throw $ Exception.other ("elaboration function for '" ++ toString k ++ "' has not been implemented"))
-  (fun _ => throw $ Exception.other "term elaborator failed, unexpected syntax")
+withNode stx $ fun node => do
+  s ← get;
+  let tables := termElabAttribute.ext.getState s.env;
+  let k := node.getKind;
+  match tables.find k with
+  | some elab => tracingAt stx $ elab node expectedType
+  | none      => throw $ Exception.other ("elaboration function for '" ++ toString k ++ "' has not been implemented")
 
 def elabType (stx : Syntax) : TermElabM Expr :=
 do u ← mkFreshLevelMVar;
-   elabTerm stx (mkSort u)
+   type ← elabTerm stx (mkSort u);
+   -- TODO: ensure it is a type
+   pure type
 
 @[builtinTermElab «prop»] def elabProp : TermElab :=
 fun _ _ => pure $ mkSort levelZero
@@ -134,6 +142,133 @@ fun _ _ => pure $ mkSort levelZero
 @[builtinTermElab «type»] def elabTypeStx : TermElab :=
 fun _ _ => pure $ mkSort levelOne
 
+@[builtinTermElab «hole»] def elabHole : TermElab :=
+fun _ expectedType? =>
+  match expectedType? with
+  | some expectedType => mkFreshExprMVar expectedType
+  | none              => do u ← mkFreshLevelMVar; mkFreshExprMVar (mkSort u)
+
+private def mkFreshAnonymousName : TermElabM Name :=
+do s ← get;
+   let anonymousIdx := s.anonymousIdx;
+   modify $ fun s => { anonymousIdx := s.anonymousIdx + 1, .. s};
+   pure $ (`_a).appendIndexAfter anonymousIdx
+
+private def mkFreshInstanceName : TermElabM Name :=
+do s ← get;
+   let instIdx := s.instImplicitIdx;
+   modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s};
+   pure $ (`_inst).appendIndexAfter instIdx
+
+def mkHole := mkNode `Lean.Parser.Term.hole [mkAtom "_"]
+
+/-- Given syntax of the form (`:` term)?, return `term` if it is present, and a hole otherwise. -/
+private def expandOptType (stx : Syntax) : Syntax :=
+if stx.getNumArgs == 0 then
+  mkHole
+else
+  stx.getArg 1
+
+/-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/
+private def expandBinderIdent (stx : Syntax) : TermElabM Syntax :=
+if stx.getKind == `Lean.Parser.Term.hole then do
+  id ← mkFreshAnonymousName;
+  pure $ mkIdentFrom stx id
+else
+  pure stx
+
+/-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/
+private def expandOptIdent (stx : Syntax) : TermElabM Syntax :=
+if stx.getNumArgs == 0 then do
+  id ← mkFreshInstanceName; pure $ mkIdentFrom stx id
+else
+  pure $ stx.getArg 0
+
+structure BinderView :=
+(id : Syntax) (type : Syntax) (bi : BinderInfo)
+
+private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
+withNode stx $ fun node => do
+  let k := node.getKind;
+  if k == `Lean.Parser.Term.simpleBinder then
+    -- binderIdent+
+    let ids  := (node.getArg 0).getArgs;
+    let type := mkHole;
+    ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
+  else if k == `Lean.Parser.Term.explicitBinder then
+    -- `(` binderIdent+ (`:` type)? (binderDefault <|> binderTactic)? `)`
+    let ids  := (node.getArg 1).getArgs;
+    let type := expandOptType (node.getArg 2);
+    -- TODO handle `binderDefault` and `binderTactic`
+    ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
+  else if k == `Lean.Parser.Term.implicitBinder then
+    -- `{` binderIdent+ (`:` type)? `}`
+    let ids  := (node.getArg 1).getArgs;
+    let type := expandOptType (node.getArg 2);
+    ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.implicit }
+  else if k == `Lean.Parser.Term.instBinder then do
+    -- `[` optIdent type `]`
+    id ← expandOptIdent (node.getArg 1);
+    let type := node.getArg 2;
+    pure #[ { id := id, type := type, bi := BinderInfo.instImplicit } ]
+  else
+    throw $ Exception.other "term elaborator failed, unexpected binder syntax"
+
+@[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α :=
+adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x
+
+def resetSynthInstanceCache : TermElabM Unit :=
+modify $ fun s => { cache := { synthInstance := {}, .. s.cache }, .. s }
+
+@[inline] def resettingSynthInstanceCache {α} (x : TermElabM α) : TermElabM α :=
+do s ← get;
+   let savedSythInstance := s.cache.synthInstance;
+   resetSynthInstanceCache;
+   finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, .. s.cache }, .. s })
+
+@[inline] def resettingSynthInstanceCacheWhen {α} (b : Bool) (x : TermElabM α) : TermElabM α :=
+if b then resettingSynthInstanceCache x else x
+
+def mkFreshId : TermElabM Name :=
+do s ← get;
+   let id := s.ngen.curr;
+   modify $ fun s => { ngen := s.ngen.next, .. s };
+   pure id
+
+private partial def elabBindersAux (binders : Array Syntax) : Nat → LocalContext → LocalInstances → TermElabM (LocalContext × LocalInstances)
+| i, lctx, localInsts =>
+  if h : i < binders.size then do
+    binderViews ← matchBinder (binders.get ⟨i, h⟩);
+    (lctx, localInsts) ← binderViews.foldlM
+      (fun (p : LocalContext × LocalInstances) binderView => do
+        let (lctx, localInsts) := p;
+        withLCtx lctx localInsts $ do
+          type       ← elabType binderView.type;
+          fvarId     ← mkFreshId;
+          -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
+          let lctx  := lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
+          className? ← isClass type;
+          match className? with
+          | none           => pure (lctx, localInsts)
+          | some className => do
+            resetSynthInstanceCache;
+            let localInsts := localInsts.push { className := className, fvar := mkFVar fvarId };
+            pure (lctx, localInsts))
+      (lctx, localInsts);
+    elabBindersAux (i+1) lctx localInsts
+  else
+    pure (lctx, localInsts)
+
+@[inline] def elabBinders {α} (binders : Array Syntax) (x : TermElabM α) : TermElabM α :=
+do lctx ← getLCtx;
+   localInsts ← getLocalInsts;
+   (lctx, newLocalInsts) ← elabBindersAux binders 0 lctx localInsts;
+   resettingSynthInstanceCacheWhen (newLocalInsts.size > localInsts.size) $
+     adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := newLocalInsts, .. ctx }) x
+
+@[inline] def elabBinder {α} (binder : Syntax) (x : TermElabM α) : TermElabM α :=
+elabBinders #[binder] x
+
 end Term
 
 export Term (TermElabM)

src/Init/Lean/Syntax.lean

@@ -331,10 +331,10 @@ Syntax.node nullKind args
 def mkAtom (val : String) : Syntax :=
 Syntax.atom none val
 
-@[inline] def mkNode (k : SyntaxNodeKind) (args : List (Syntax)) : Syntax :=
+@[inline] def mkNode (k : SyntaxNodeKind) (args : List Syntax) : Syntax :=
 Syntax.node k args.toArray
 
-@[inline] def mkNullNode (args : List (Syntax)) : Syntax :=
+@[inline] def mkNullNode (args : List Syntax) : Syntax :=
 Syntax.node nullKind args.toArray
 
 def mkOptionalNode (arg : Option Syntax) : Syntax :=

tests/lean/run/frontend1.lean

@@ -7,4 +7,12 @@ do (env, messages) ← testFrontend input;
    messages.toList.forM $ fun msg => IO.println msg;
    pure ()
 
-#eval run "import Init.Core universe u universe v section namespace foo.bla end bla end foo end"
+#eval run
+"import Init.Core
+ universe u universe v
+ section namespace foo.bla end bla end foo
+ variable (p q : Prop)
+ variable (_ b : _)
+ variable {α : Type}
+ -- variable [Monad m]
+ end"