From 2dcf6dd141b5f1cac125d1c403b342385dd040de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Dec 2019 15:42:37 -0800 Subject: [PATCH] feat: add new `CommandElabM` and `TermElabM` --- src/Init/Lean/Elab/Command.lean | 75 ++++++++++++++++++++++++++++++-- src/Init/Lean/Elab/Term.lean | 77 +++++++++++++++++++++++++++++++++ 2 files changed, 149 insertions(+), 3 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index 42919b858b..ade6929001 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/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 diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 69794ec92f..a24324af27 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/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