feat: add new CommandElabM and TermElabM

src/Init/Lean/Elab/Command.lean

@@ -4,24 +4,93 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Lean.Elab.Util
 import Init.Lean.Elab.Alias
+import Init.Lean.Elab.Exception
 import Init.Lean.Elab.ResolveName
 import Init.Lean.Elab.Term
 
 namespace Lean
 namespace Elab
+namespace Command
 
+structure Context :=
+(fileName : String)
+(fileMap  : FileMap)
 
+structure Scope :=
+(cmd         : String)
+(header      : Name)
+(options     : Options := {})
+(ns          : Name := Name.anonymous) -- current namespace
+(openDecls   : List OpenDecl := [])
+(univs       : List Name := [])
+(varDecls    : List Syntax := [])
 
-/-
-private def addScopes (cmd : String) (updateNamespace : Bool) : Name → List ElabScope → List ElabScope
+instance Scope.inhabited : Inhabited Scope := ⟨{ cmd := "", header := arbitrary _ }⟩
+
+private def addScopes (cmd : String) (updateNamespace : Bool) : Name → List Scope → List Scope
 | Name.anonymous, scopes => scopes
 | Name.str p h _, scopes =>
   let scopes := addScopes p scopes;
   let ns     := scopes.head!.ns;
   let ns     := if updateNamespace then mkNameStr ns h else ns;
   { cmd := cmd, header := h, ns := ns } :: scopes
-| _, _ => [] -- unreachable
+| _, _ => unreachable!
+
+structure State :=
+(env      : Environment)
+(messages : MessageLog := {})
+(cmdPos   : String.Pos := 0)
+(scopes   : List Scope := [{ cmd := "root", header := Name.anonymous }])
+
+abbrev CommandElabM := ReaderT Context (EStateM Exception State)
+abbrev CommandElab  := SyntaxNode → CommandElabM Unit
+
+abbrev CommandElabTable := SMap SyntaxNodeKind CommandElab
+def mkBuiltinCommandElabTable : IO (IO.Ref CommandElabTable) := IO.mkRef {}
+@[init mkBuiltinCommandElabTable] constant builtinCommandElabTable : IO.Ref CommandElabTable := arbitrary _
+
+def addBuiltinCommandElab (k : SyntaxNodeKind) (declName : Name) (elab : CommandElab) : IO Unit :=
+do m ← builtinCommandElabTable.get;
+   when (m.contains k) $
+     throw (IO.userError ("invalid builtin command elaborator, elaborator for '" ++ toString k ++ "' has already been defined"));
+   builtinCommandElabTable.modify $ fun m => m.insert k elab
+
+def declareBuiltinCommandElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
+let name := `_regBuiltinCommandElab ++ declName;
+let type := mkApp (mkConst `IO) (mkConst `Unit);
+let val  := mkAppN (mkConst `addBuiltinCommandElab) #[toExpr kind, toExpr declName, mkConst declName];
+let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
+match env.addAndCompile {} decl with
+-- TODO: pretty print error
+| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin command elaborator '" ++ toString declName ++ "'"))
+| Except.ok env  => IO.ofExcept (setInitAttr env name)
+
+@[init] def registerBuiltinCommandElabAttr : IO Unit :=
+registerAttribute {
+ name  := `builtinCommandElab,
+ descr := "Builtin command elaborator",
+ add   := fun env declName arg persistent => do {
+   unless persistent $ throw (IO.userError ("invalid attribute 'builtinCommandElab', must be persistent"));
+   kind ← syntaxNodeKindOfAttrParam env `Lean.Parser.Command arg;
+   match env.find declName with
+   | none  => throw "unknown declaration"
+   | some decl =>
+     match decl.type with
+     | Expr.const `Lean.CommandElab _ _ => declareBuiltinCommandElab env kind declName
+     | _ => throw (IO.userError ("unexpected command elaborator type at '" ++ toString declName ++ "' `CommandElab` expected"))
+ },
+ applicationTime := AttributeApplicationTime.afterCompilation
+}
+
+abbrev CommandElabAttribute := ElabAttribute CommandElabTable
+def mkCommandElabAttribute : IO CommandElabAttribute := mkElabAttribute `commandTerm "command" builtinCommandElabTable
+@[init mkCommandElabAttribute] constant commandElabAttribute : CommandElabAttribute := arbitrary _
+
+end Command
+
+/-
 
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
 fun n => do

src/Init/Lean/Elab/Term.lean

@@ -4,10 +4,87 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Lean.Meta
+import Init.Lean.Elab.Util
 import Init.Lean.Elab.Alias
+import Init.Lean.Elab.Exception
+import Init.Lean.Elab.ResolveName
 
 namespace Lean
 namespace Elab
+namespace Term
+
+structure Context extends Meta.Context :=
+(fileName    : String)
+(fileMap     : FileMap)
+(cmdPos      : String.Pos)
+(ns          : Name) -- current Namespace
+(openDecls   : List OpenDecl := [])
+
+inductive SyntheticMVarInfo
+| typeClass : SyntheticMVarInfo
+| tactic (tacticCode : Syntax) : SyntheticMVarInfo
+| postponed (macroStack : List Syntax) : SyntheticMVarInfo
+
+structure State extends Meta.State :=
+(macroStack     : List Syntax)
+(syntheticMVars : List (MVarId × SyntheticMVarInfo))
+
+abbrev TermElabM := ReaderT Context (EStateM Exception State)
+abbrev TermElab  := SyntaxNode → Option Expr → TermElabM Expr
+
+abbrev TermElabTable := SMap SyntaxNodeKind TermElab
+def mkBuiltinTermElabTable : IO (IO.Ref TermElabTable) :=  IO.mkRef {}
+@[init mkBuiltinTermElabTable] constant builtinTermElabTable : IO.Ref TermElabTable := arbitrary _
+
+def addBuiltinTermElab (k : SyntaxNodeKind) (declName : Name) (elab : TermElab) : IO Unit :=
+do m ← builtinTermElabTable.get;
+   when (m.contains k) $
+     throw (IO.userError ("invalid builtin term elaborator, elaborator for '" ++ toString k ++ "' has already been defined"));
+   builtinTermElabTable.modify $ fun m => m.insert k elab
+
+def declareBuiltinTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
+let name := `_regBuiltinTermElab ++ declName;
+let type := mkApp (mkConst `IO) (mkConst `Unit);
+let val  := mkAppN (mkConst `addBuiltinTermElab) #[toExpr kind, toExpr declName, mkConst declName];
+let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
+match env.addAndCompile {} decl with
+-- TODO: pretty print error
+| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin term elaborator '" ++ toString declName ++ "'"))
+| Except.ok env  => IO.ofExcept (setInitAttr env name)
+
+@[init] def registerBuiltinTermElabAttr : IO Unit :=
+registerAttribute {
+ name  := `builtinTermElab,
+ descr := "Builtin term elaborator",
+ add   := fun env declName arg persistent => do {
+   unless persistent $ throw (IO.userError ("invalid attribute 'builtinTermElab', must be persistent"));
+   kind ← syntaxNodeKindOfAttrParam env `Lean.Parser.Term arg;
+   match env.find declName with
+   | none  => throw "unknown declaration"
+   | some decl =>
+     match decl.type with
+     | Expr.const `Lean.TermElab _ _ => declareBuiltinTermElab env kind declName
+     | _ => throw (IO.userError ("unexpected term elaborator type at '" ++ toString declName ++ "' `TermElab` expected"))
+ },
+ applicationTime := AttributeApplicationTime.afterCompilation
+}
+
+abbrev TermElabAttribute := ElabAttribute TermElabTable
+def mkTermElabAttribute : IO TermElabAttribute := mkElabAttribute `elabTerm "term" builtinTermElabTable
+@[init mkTermElabAttribute] constant termElabAttribute : TermElabAttribute := arbitrary _
+
+@[inline] def liftMetaM {α} (x : Meta.MetaM α) : TermElabM α :=
+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 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
+
+end Term
+
 /-
 partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax Expr)
 | stx, expectedType, expanding => stx.ifNode