feat: extensible elaboration functions
@kha `termParserAttr.lean` has a small example
This commit is contained in:
Leonardo de Moura
parent
f60c8c6249
commit
f73ff914eb
11 changed files with 148 additions and 100 deletions
|
|
@ -14,24 +14,24 @@ namespace Term
|
|||
@[builtinTermElab dollar] def elabDollar : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `($f $ $a) => `($f $a)
|
||||
| _ => throwUnexpectedSyntax stx "application"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab dollarProj] def elabDollarProj : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `($term $.$field) => `($(term).$field)
|
||||
| _ => throwUnexpectedSyntax stx "$."
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab «if»] def elabIf : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `(if $h : $cond then $t else $e) => let h := mkTermIdFromIdent h; `(dite $cond (fun $h => $t) (fun $h => $e))
|
||||
| `(if $cond then $t else $e) => `(ite $cond $t $e)
|
||||
| _ => throwUnexpectedSyntax stx "if-then-else"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab subtype] def elabSubtype : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `({ $x : $type // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : $type) => $p))
|
||||
| `({ $x // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : _) => $p))
|
||||
| _ => throwUnexpectedSyntax stx "subtype"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab anonymousCtor] def elabAnoymousCtor : TermElab :=
|
||||
fun stx expectedType? => do
|
||||
|
|
@ -59,7 +59,7 @@ match expectedType? with
|
|||
@[builtinTermElab «show»] def elabShow : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
|
||||
| _ => throwUnexpectedSyntax stx "show-from"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab «have»] def elabHave : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
|
|
@ -67,7 +67,7 @@ adaptExpander $ fun stx => match_syntax stx with
|
|||
| `(have $type := $val; $body) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
|
||||
| `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
|
||||
| `(have $x : $type := $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
|
||||
| _ => throwUnexpectedSyntax stx "have"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[termElab «where»] def elabWhere : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
|
|
@ -76,7 +76,7 @@ adaptExpander $ fun stx => match_syntax stx with
|
|||
decls.foldrM
|
||||
(fun decl body => `(let $decl; $body))
|
||||
body
|
||||
| _ => throwUnexpectedSyntax stx "where"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[termElab «parser!»] def elabParserMacro : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
|
|
@ -90,7 +90,7 @@ adaptExpander $ fun stx => match_syntax stx with
|
|||
`(HasOrelse.orelse (Lean.Parser.mkAntiquot $s (some $kind) true) (Lean.Parser.leadingNode $kind $e))
|
||||
| none => throwError stx "invalid `parser!` macro, it must be used in definitions"
|
||||
| _ => throwError stx "invalid `parser!` macro, unexpected declaration name"
|
||||
| _ => throwUnexpectedSyntax stx "parser!"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[termElab «tparser!»] def elabTParserMacro : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
|
|
@ -99,7 +99,7 @@ adaptExpander $ fun stx => match_syntax stx with
|
|||
match declName? with
|
||||
| some declName => let kind := quote declName; `(Lean.Parser.trailingNode $kind $e)
|
||||
| none => throwError stx "invalid `tparser!` macro, it must be used in definitions"
|
||||
| _ => throwUnexpectedSyntax stx "tparser!"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
def elabInfix (f : Syntax) : TermElab :=
|
||||
fun stx expectedType? => do
|
||||
|
|
|
|||
|
|
@ -44,6 +44,8 @@ structure Context :=
|
|||
(macroStack : List Syntax := [])
|
||||
(currMacroScope : MacroScope := 0)
|
||||
|
||||
instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
|
||||
|
||||
abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
|
||||
abbrev CommandElabM := CommandElabCoreM Exception
|
||||
abbrev CommandElab := SyntaxNode → CommandElabM Unit
|
||||
|
|
@ -55,7 +57,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
|
|||
mkMessageAux ctx ref (toString err) MessageSeverity.error
|
||||
|
||||
@[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
|
||||
EIO.adaptExcept (ioErrorToMessage ctx ref) x
|
||||
EIO.adaptExcept (fun ex => Exception.error $ ioErrorToMessage ctx ref ex) x
|
||||
|
||||
@[inline] def liftIO {α} (ref : Syntax) (x : IO α) : CommandElabM α :=
|
||||
fun ctx => liftIOCore ctx ref x
|
||||
|
|
@ -121,13 +123,7 @@ def throwError {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α :=
|
|||
ref ← getBetterRef ref;
|
||||
msgData ← addMacroStack msgData;
|
||||
msg ← mkMessage msgData MessageSeverity.error ref;
|
||||
throw msg
|
||||
|
||||
def throwUnexpectedSyntax {α} (ref : Syntax) (expectedMsg : Option String := none) : CommandElabM α := do
|
||||
refFmt ← prettyPrint ref;
|
||||
match expectedMsg with
|
||||
| none => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
| some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
throw (Exception.error msg)
|
||||
|
||||
protected def getCurrMacroScope : CommandElabM Nat := do
|
||||
ctx ← read;
|
||||
|
|
@ -184,6 +180,15 @@ def mkCommandElabAttribute : IO CommandElabAttribute :=
|
|||
mkElabAttribute CommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" builtinCommandElabTable
|
||||
@[init mkCommandElabAttribute] constant commandElabAttribute : CommandElabAttribute := arbitrary _
|
||||
|
||||
private def elabCommandUsing (stxNode : SyntaxNode) : List CommandElab → CommandElabM Unit
|
||||
| [] => do
|
||||
refFmt ← prettyPrint stxNode.val;
|
||||
throwError stxNode.val ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
| (elabFn::elabFns) => catch (elabFn stxNode)
|
||||
(fun ex => match ex with
|
||||
| Exception.error _ => throw ex
|
||||
| Exception.unsupportedSyntax => elabCommandUsing elabFns)
|
||||
|
||||
def elabCommand (stx : Syntax) : CommandElabM Unit :=
|
||||
stx.ifNode
|
||||
(fun n => do
|
||||
|
|
@ -191,8 +196,8 @@ stx.ifNode
|
|||
let table := (commandElabAttribute.ext.getState s.env).table;
|
||||
let k := n.getKind;
|
||||
match table.find? k with
|
||||
| some elab => elab n
|
||||
| none => throwError stx ("command '" ++ toString k ++ "' has not been implemented"))
|
||||
| some elabFns => elabCommandUsing n elabFns
|
||||
| none => throwError stx ("command '" ++ toString k ++ "' has not been implemented"))
|
||||
(fun _ => throwError stx ("unexpected command"))
|
||||
|
||||
/- Elaborate `x` with `stx` on the macro stack -/
|
||||
|
|
@ -228,9 +233,10 @@ s.scopes.head!.varDecls
|
|||
|
||||
private def toCommandResult {α} (ctx : Context) (s : State) (result : EStateM.Result Term.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, nextMacroScope := newS.nextMacroScope, .. s }
|
||||
| EStateM.Result.error (Term.Exception.error ex) newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
|
||||
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
|
||||
| EStateM.Result.ok a newS => EStateM.Result.ok a { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
|
||||
| EStateM.Result.error (Term.Exception.ex ex) newS =>
|
||||
EStateM.Result.error ex { env := newS.env, messages := newS.messages, nextMacroScope := newS.nextMacroScope, .. s }
|
||||
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
|
||||
|
||||
instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
|
||||
⟨throw $ arbitrary _⟩
|
||||
|
|
@ -239,12 +245,14 @@ instance CommandElabM.inhabited {α} : Inhabited (CommandElabM α) :=
|
|||
ctx ← read;
|
||||
s ← get;
|
||||
match (Term.elabBinders (getVarDecls s) elab (mkTermContext ctx s declName?)).run (mkTermState s) with
|
||||
| EStateM.Result.ok a newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
|
||||
| EStateM.Result.error (Term.Exception.error ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
|
||||
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
|
||||
| EStateM.Result.ok a newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; pure a
|
||||
| EStateM.Result.error (Term.Exception.ex ex) newS => do modify $ fun s => { env := newS.env, messages := newS.messages, .. s }; throw ex
|
||||
| EStateM.Result.error Term.Exception.postpone newS => unreachable!
|
||||
|
||||
@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
|
||||
catch x (fun ex => do logMessage ex; pure ())
|
||||
catch x (fun ex => match ex with
|
||||
| Exception.error ex => do logMessage ex; pure ()
|
||||
| Exception.unsupportedSyntax => unreachable!)
|
||||
|
||||
@[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit :=
|
||||
fun ctx => EIO.catchExceptions (withLogging x ctx) (fun _ => pure ())
|
||||
|
|
@ -278,13 +286,13 @@ addScopes ref "namespace" true header
|
|||
@[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
|
||||
fun stx => match_syntax stx.val with
|
||||
| `(namespace $n) => addNamespace stx.val n.getId
|
||||
| _ => throwUnexpectedSyntax stx.val "namespace"
|
||||
| _ => throw Exception.unsupportedSyntax
|
||||
|
||||
@[builtinCommandElab «section»] def elabSection : CommandElab :=
|
||||
fun stx => match_syntax stx.val with
|
||||
| `(section $header:ident) => addScopes stx.val "section" false header.getId
|
||||
| `(section) => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
|
||||
| _ => throwUnexpectedSyntax stx.val "section"
|
||||
| _ => throw Exception.unsupportedSyntax
|
||||
|
||||
def getScopes : CommandElabM (List Scope) := do
|
||||
s ← get; pure s.scopes
|
||||
|
|
@ -373,7 +381,7 @@ currNamespace ← getCurrNamespace;
|
|||
openDecls ← getOpenDecls;
|
||||
match Elab.resolveNamespace env currNamespace openDecls id with
|
||||
| some ns => pure ns
|
||||
| none => throwErrorUsingCmdPos ("unknown namespace '" ++ toString id ++ "'")
|
||||
| none => throw Exception.unsupportedSyntax
|
||||
|
||||
@[builtinCommandElab «export»] def elabExport : CommandElab :=
|
||||
fun stx => do
|
||||
|
|
|
|||
|
|
@ -123,7 +123,7 @@ if kind == `Lean.Parser.Command.declValSimple then
|
|||
else if kind == `Lean.Parser.Command.declValEqns then
|
||||
Term.throwError defVal "equations have not been implemented yet"
|
||||
else
|
||||
Term.throwUnexpectedSyntax defVal "definition body"
|
||||
Term.throwUnsupportedSyntax
|
||||
|
||||
def elabDefLike (view : DefView) : CommandElabM Unit :=
|
||||
let ref := view.ref;
|
||||
|
|
|
|||
|
|
@ -9,7 +9,16 @@ import Init.Lean.Meta
|
|||
namespace Lean
|
||||
namespace Elab
|
||||
|
||||
abbrev Exception := Message
|
||||
inductive Exception
|
||||
| error : Message → Exception
|
||||
| unsupportedSyntax : Exception
|
||||
|
||||
instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
|
||||
|
||||
instance Exception.hasToString : HasToString Exception :=
|
||||
⟨fun ex => match ex with
|
||||
| Exception.error msg => toString msg
|
||||
| Exception.unsupportedSyntax => "unsupported syntax"⟩
|
||||
|
||||
def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
|
||||
let pos := fileMap.toPosition pos;
|
||||
|
|
@ -17,7 +26,7 @@ let pos := fileMap.toPosition pos;
|
|||
|
||||
def mkExceptionCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (pos : String.Pos) : Exception :=
|
||||
let pos := fileMap.toPosition pos;
|
||||
{ fileName := fileName, pos := pos, data := msgData, severity := MessageSeverity.error }
|
||||
Exception.error { fileName := fileName, pos := pos, data := msgData, severity := MessageSeverity.error }
|
||||
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -68,12 +68,12 @@ def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
|
|||
log stx MessageSeverity.information msgData
|
||||
|
||||
def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
|
||||
msg ← mkMessage msgData MessageSeverity.error ref; throw msg
|
||||
msg ← mkMessage msgData MessageSeverity.error ref; throw (Exception.error msg)
|
||||
|
||||
def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
|
||||
cmdPos ← getCmdPos;
|
||||
msg ← mkMessageAt msgData MessageSeverity.error cmdPos;
|
||||
throw msg
|
||||
throw (Exception.error msg)
|
||||
|
||||
end Elab
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -61,12 +61,12 @@ instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
|
|||
|
||||
Remark: `Exception.postpone` is used only when `mayPostpone == true` in the `Context`. -/
|
||||
inductive Exception
|
||||
| error : Elab.Exception → Exception
|
||||
| ex : Elab.Exception → Exception
|
||||
| postpone : Exception
|
||||
|
||||
instance Exception.inhabited : Inhabited Exception := ⟨Exception.postpone⟩
|
||||
instance Exception.hasToString : HasToString Exception :=
|
||||
⟨fun ex => match ex with | Exception.postpone => "postponed" | Exception.error ex => toString ex⟩
|
||||
⟨fun ex => match ex with | Exception.postpone => "postponed" | Exception.ex ex => toString ex⟩
|
||||
|
||||
/-
|
||||
Term elaborator Monad. In principle, we could track statically which methods
|
||||
|
|
@ -79,7 +79,7 @@ abbrev TermElab := SyntaxNode → Option Expr → TermElabM Expr
|
|||
instance TermElabM.inhabited {α} : Inhabited (TermElabM α) :=
|
||||
⟨throw $ Exception.postpone⟩
|
||||
|
||||
abbrev TermElabResult := EStateM.Result Elab.Exception State Expr
|
||||
abbrev TermElabResult := EStateM.Result Message State Expr
|
||||
instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩
|
||||
|
||||
/--
|
||||
|
|
@ -89,17 +89,17 @@ instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Resul
|
|||
@[inline] def observing (x : TermElabM Expr) : TermElabM TermElabResult :=
|
||||
fun ctx s =>
|
||||
match x ctx s with
|
||||
| EStateM.Result.error Exception.postpone newS => EStateM.Result.error Exception.postpone newS
|
||||
| EStateM.Result.error (Exception.error ex) newS => EStateM.Result.ok (EStateM.Result.error ex newS) s
|
||||
| EStateM.Result.ok e newS => EStateM.Result.ok (EStateM.Result.ok e newS) s
|
||||
| EStateM.Result.error (Exception.ex (Elab.Exception.error errMsg)) newS => EStateM.Result.ok (EStateM.Result.error errMsg newS) s
|
||||
| EStateM.Result.error ex newS => EStateM.Result.error ex newS
|
||||
| EStateM.Result.ok e newS => EStateM.Result.ok (EStateM.Result.ok e newS) s
|
||||
|
||||
/--
|
||||
Apply the result/exception and state captured with `observing`.
|
||||
We use this method to implement overloaded notation and symbols. -/
|
||||
def applyResult (result : TermElabResult) : TermElabM Expr :=
|
||||
match result with
|
||||
| EStateM.Result.ok e s => do set s; pure e
|
||||
| EStateM.Result.error ex s => do set s; throw (Exception.error ex)
|
||||
| EStateM.Result.ok e s => do set s; pure e
|
||||
| EStateM.Result.error errMsg s => do set s; throw (Exception.ex (Elab.Exception.error errMsg))
|
||||
|
||||
def getEnv : TermElabM Environment := do s ← get; pure s.env
|
||||
def getMCtx : TermElabM MetavarContext := do s ← get; pure s.mctx
|
||||
|
|
@ -150,13 +150,10 @@ def throwError {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
|
|||
ref ← getBetterRef ref;
|
||||
msgData ← addMacroStack msgData;
|
||||
msg ← mkMessage msgData MessageSeverity.error ref;
|
||||
throw (Exception.error msg)
|
||||
throw (Exception.ex (Elab.Exception.error msg))
|
||||
|
||||
def throwUnexpectedSyntax {α} (ref : Syntax) (expectedMsg : Option String := none) : TermElabM α := do
|
||||
refFmt ← prettyPrint ref;
|
||||
match expectedMsg with
|
||||
| none => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
| some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
def throwUnsupportedSyntax {α} : TermElabM α :=
|
||||
throw (Exception.ex Elab.Exception.unsupportedSyntax)
|
||||
|
||||
protected def getCurrMacroScope : TermElabM MacroScope := do
|
||||
ctx ← read;
|
||||
|
|
@ -259,7 +256,7 @@ mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmd
|
|||
|
||||
/-- Auxiliary function for `liftMetaM` -/
|
||||
private def fromMetaException (ctx : Context) (ref : Syntax) (ex : Meta.Exception) : Exception :=
|
||||
Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error
|
||||
Exception.ex $ Elab.Exception.error $ mkMessageAux ctx ref ex.toMessageData MessageSeverity.error
|
||||
|
||||
/-- Auxiliary function for `liftMetaM` -/
|
||||
private def fromMetaState (ref : Syntax) (ctx : Context) (s : State) (newS : Meta.State) (oldTraceState : TraceState) : State :=
|
||||
|
|
@ -310,7 +307,7 @@ def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
|
|||
fun ctx s =>
|
||||
match (x { .. ctx }).run { .. s } with
|
||||
| EStateM.Result.ok a newS => EStateM.Result.ok a { mctx := newS.mctx, ngen := newS.ngen, .. s }
|
||||
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.error ex) s
|
||||
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.ex ex) s
|
||||
|
||||
def elabLevel (stx : Syntax) : TermElabM Level :=
|
||||
liftLevelM $ Level.elabLevel stx
|
||||
|
|
@ -445,14 +442,14 @@ def expandCDot? : Syntax → TermElabM (Option Syntax)
|
|||
pure none
|
||||
| _ => pure none
|
||||
|
||||
private def exceptionToSorry (ref : Syntax) (ex : Elab.Exception) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
private def exceptionToSorry (ref : Syntax) (errMsg : Message) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
expectedType : Expr ← match expectedType? with
|
||||
| none => mkFreshTypeMVar ref
|
||||
| some expectedType => pure expectedType;
|
||||
u ← getLevel ref expectedType;
|
||||
-- TODO: should be `(sorryAx.{$u} $expectedType true) when we support antiquotations at that place
|
||||
let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true);
|
||||
unless ex.data.hasSyntheticSorry $ logMessage ex;
|
||||
unless errMsg.data.hasSyntheticSorry $ logMessage errMsg;
|
||||
pure syntheticSorry
|
||||
|
||||
/-- If `mayPostpone == true`, throw `Expection.postpone`. -/
|
||||
|
|
@ -476,6 +473,39 @@ ctx ← read;
|
|||
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack);
|
||||
pure mvar
|
||||
|
||||
/-
|
||||
Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
|
||||
an error is found. -/
|
||||
private def elabTermUsing (s : State) (stxNode : SyntaxNode) (expectedType? : Option Expr) (errToSorry : Bool) (catchExPostpone : Bool)
|
||||
: List TermElab → TermElabM Expr
|
||||
| [] => do
|
||||
refFmt ← prettyPrint stxNode.val;
|
||||
throwError stxNode.val ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
| (elabFn::elabFns) => catch (elabFn stxNode expectedType?)
|
||||
(fun ex => match ex with
|
||||
| Exception.ex (Elab.Exception.error errMsg) => if errToSorry then exceptionToSorry stxNode.val errMsg expectedType? else throw ex
|
||||
| Exception.ex Elab.Exception.unsupportedSyntax => elabTermUsing elabFns
|
||||
| Exception.postpone =>
|
||||
if catchExPostpone then do
|
||||
/- If `elab` threw `Exception.postpone`, we reset any state modifications.
|
||||
For example, we want to make sure pending synthetic metavariables created by `elab` before
|
||||
it threw `Exception.postpone` are discarded.
|
||||
Note that we are also discarding the messages created by `elab`.
|
||||
|
||||
For example, consider the expression.
|
||||
`((f.x a1).x a2).x a3`
|
||||
Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
|
||||
Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
|
||||
because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
|
||||
finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
|
||||
keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
|
||||
wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
|
||||
and new metavariables are created for the nested functions. -/
|
||||
set s;
|
||||
postponeElabTerm stxNode.val expectedType?
|
||||
else
|
||||
throw ex)
|
||||
|
||||
/--
|
||||
Main function for elaborating terms.
|
||||
It extracts the elaboration methods from the environment using the node kind.
|
||||
|
|
@ -496,32 +526,8 @@ withFreshMacroScope $ withNode stx $ fun node => do
|
|||
let table := (termElabAttribute.ext.getState s.env).table;
|
||||
let k := node.getKind;
|
||||
match table.find? k with
|
||||
| some elab =>
|
||||
catch
|
||||
(elab node expectedType?)
|
||||
(fun ex => match ex with
|
||||
| Exception.error err => if errToSorry then exceptionToSorry stx err expectedType? else throw ex
|
||||
| Exception.postpone =>
|
||||
if catchExPostpone then do
|
||||
/- If `elab` threw `Exception.postpone`, we reset any state modifications.
|
||||
For example, we want to make sure pending synthetic metavariables created by `elab` before
|
||||
it threw `Exception.postpone` are discarded.
|
||||
Note that we are also discarding the messages created by `elab`.
|
||||
|
||||
For example, consider the expression.
|
||||
`((f.x a1).x a2).x a3`
|
||||
Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
|
||||
Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
|
||||
because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
|
||||
finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
|
||||
keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
|
||||
wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
|
||||
and new metavariables are created for the nested functions. -/
|
||||
set s;
|
||||
postponeElabTerm stx expectedType?
|
||||
else
|
||||
throw ex)
|
||||
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
|
||||
| some elabFns => elabTermUsing s node expectedType? errToSorry catchExPostpone elabFns
|
||||
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
|
||||
|
||||
/-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
|
||||
private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
|
||||
|
|
@ -594,8 +600,13 @@ withMVarContext mvarId $ do
|
|||
assignExprMVar mvarId result;
|
||||
pure true)
|
||||
(fun ex => match ex with
|
||||
| Exception.postpone => pure false
|
||||
| Exception.error msg => if postponeOnError then do set s; pure false else do logMessage msg; pure true)
|
||||
| Exception.postpone => pure false
|
||||
| Exception.ex Elab.Exception.unsupportedSyntax => unreachable!
|
||||
| Exception.ex (Elab.Exception.error msg) =>
|
||||
if postponeOnError then do
|
||||
set s; pure false
|
||||
else do
|
||||
logMessage msg; pure true)
|
||||
|
||||
/- Try to synthesize metavariable using type class resolution.
|
||||
This method assumes the local context and local instances of `instMVar` coincide
|
||||
|
|
@ -629,8 +640,8 @@ private def synthesizePendingInstMVar (ref : Syntax) (instMVar : MVarId) : TermE
|
|||
withMVarContext instMVar $ catch
|
||||
(synthesizeInstMVarCore ref instMVar)
|
||||
(fun ex => match ex with
|
||||
| Exception.error ex => do logMessage ex; pure true
|
||||
| Exception.postpone => unreachable!)
|
||||
| Exception.ex (Elab.Exception.error errMsg) => do logMessage errMsg; pure true
|
||||
| _ => unreachable!)
|
||||
|
||||
/--
|
||||
Return `true` iff `mvarId` is assigned to a term whose the
|
||||
|
|
|
|||
|
|
@ -189,22 +189,23 @@ match eType.getAppFn, lval with
|
|||
| _, _ =>
|
||||
throwLValError ref e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
|
||||
|
||||
private partial def resolveLValLoop (ref : Syntax) (e : Expr) (lval : LVal) : Expr → Array Elab.Exception → TermElabM LValResolution
|
||||
private partial def resolveLValLoop (ref : Syntax) (e : Expr) (lval : LVal) : Expr → Array Message → TermElabM LValResolution
|
||||
| eType, previousExceptions => do
|
||||
eType ← whnfCore ref eType;
|
||||
tryPostponeIfMVar eType;
|
||||
catch (resolveLValAux ref e eType lval)
|
||||
(fun ex =>
|
||||
match ex with
|
||||
| Exception.postpone => throw ex
|
||||
| Exception.error ex => do
|
||||
| Exception.postpone => throw ex
|
||||
| Exception.ex Elab.Exception.unsupportedSyntax => throw ex
|
||||
| Exception.ex (Elab.Exception.error errMsg) => do
|
||||
eType? ← unfoldDefinition? ref eType;
|
||||
match eType? with
|
||||
| some eType => resolveLValLoop eType (previousExceptions.push ex)
|
||||
| some eType => resolveLValLoop eType (previousExceptions.push errMsg)
|
||||
| none => do
|
||||
previousExceptions.forM $ fun ex =>
|
||||
logMessage ex;
|
||||
throw (Exception.error ex))
|
||||
logMessage errMsg;
|
||||
throw (Exception.ex (Elab.Exception.error errMsg)))
|
||||
|
||||
private def resolveLVal (ref : Syntax) (e : Expr) (lval : LVal) : TermElabM LValResolution := do
|
||||
eType ← inferType ref e;
|
||||
|
|
@ -331,7 +332,7 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
|
|||
s ← observing $ elabAppLVals ref f (lvals' ++ lvals) namedArgs args expectedType? explicit;
|
||||
pure $ acc.push s)
|
||||
acc
|
||||
| _ => throwUnexpectedSyntax id "identifier"
|
||||
| _ => throwUnsupportedSyntax
|
||||
| _ => do
|
||||
f ← elabTerm f none;
|
||||
s ← observing $ elabAppLVals ref f lvals namedArgs args expectedType? explicit;
|
||||
|
|
@ -353,8 +354,8 @@ else
|
|||
private def mergeFailures {α} (failures : Array TermElabResult) (stx : Syntax) : TermElabM α := do
|
||||
msgs ← failures.mapM $ fun failure =>
|
||||
match failure with
|
||||
| EStateM.Result.ok _ _ => unreachable!
|
||||
| EStateM.Result.error ex s => toMessageData ex stx;
|
||||
| EStateM.Result.ok _ _ => unreachable!
|
||||
| EStateM.Result.error errMsg s => toMessageData errMsg stx;
|
||||
throwError stx ("overloaded, errors " ++ MessageData.ofArray msgs)
|
||||
|
||||
private def elabAppAux (ref : Syntax) (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@ else
|
|||
else if kind == `Lean.Parser.Term.binderTactic then do
|
||||
throwError modifier "not implemented yet"
|
||||
else
|
||||
throwUnexpectedSyntax modifier "default argument or tactic name"
|
||||
throwUnsupportedSyntax
|
||||
|
||||
private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
|
||||
withNode stx $ fun node => do
|
||||
|
|
@ -143,12 +143,12 @@ fun stx _ => match_syntax stx.val with
|
|||
elabBinders binders $ fun xs => do
|
||||
e ← elabType term;
|
||||
mkForall stx.val xs e
|
||||
| _ => throwUnexpectedSyntax stx.val "forall"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab arrow] def elabArrow : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `($dom:term -> $rng) => `(forall (a : $dom), $rng)
|
||||
| _ => throwUnexpectedSyntax stx "->"
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab depArrow] def elabDepArrow : TermElab :=
|
||||
fun stx _ =>
|
||||
|
|
|
|||
|
|
@ -37,7 +37,12 @@ structure ElabAttributeOLeanEntry :=
|
|||
structure ElabAttributeEntry (γ : Type) extends ElabAttributeOLeanEntry :=
|
||||
(elabFn : γ)
|
||||
|
||||
abbrev ElabFnTable (γ : Type) := SMap SyntaxNodeKind γ
|
||||
abbrev ElabFnTable (γ : Type) := SMap SyntaxNodeKind (List γ)
|
||||
|
||||
def ElabFnTable.insert {γ} (table : ElabFnTable γ) (k : SyntaxNodeKind) (f : γ) : ElabFnTable γ :=
|
||||
match table.find? k with
|
||||
| some fs => table.insert k (f::fs)
|
||||
| none => table.insert k [f]
|
||||
|
||||
structure ElabAttributeExtensionState (γ : Type) :=
|
||||
(newEntries : List ElabAttributeOLeanEntry := [])
|
||||
|
|
@ -75,8 +80,8 @@ match env.find? constName with
|
|||
@[implementedBy mkElabFnOfConstantUnsafe]
|
||||
constant mkElabFnOfConstant (γ : Type) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ := throw ""
|
||||
|
||||
private def ElabAttribute.addImportedParsers {γ} (typeName : Name) (builtinTableRef : IO.Ref (ElabFnTable γ)) (env : Environment) (es : Array (Array ElabAttributeOLeanEntry))
|
||||
: IO (ElabAttributeExtensionState γ) := do
|
||||
private def ElabAttribute.addImportedParsers {γ} (typeName : Name) (builtinTableRef : IO.Ref (ElabFnTable γ))
|
||||
(env : Environment) (es : Array (Array ElabAttributeOLeanEntry)) : IO (ElabAttributeExtensionState γ) := do
|
||||
table ← builtinTableRef.get;
|
||||
table ← es.foldlM
|
||||
(fun table entries =>
|
||||
|
|
|
|||
|
|
@ -3,6 +3,8 @@ new_frontend
|
|||
variable {m : Type → Type}
|
||||
variable [s : Functor m]
|
||||
|
||||
#check @Nat.rec
|
||||
|
||||
#check s.map
|
||||
|
||||
/-
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ do env ← MetaIO.getEnv;
|
|||
pure ()
|
||||
|
||||
open Lean.Parser
|
||||
@[termParser] def tst := parser! "(|" >> termParser >> "|)"
|
||||
@[termParser] def tst := parser! "(|" >> termParser >> optional (", " >> termParser) >> "|)"
|
||||
|
||||
@[termParser] def boo : ParserDescr :=
|
||||
ParserDescr.node `boo
|
||||
|
|
@ -25,8 +25,9 @@ ParserDescr.node `boo
|
|||
open Lean.Elab.Term
|
||||
|
||||
@[termElab tst] def elabTst : TermElab :=
|
||||
fun stx expected? =>
|
||||
elabTerm (stx.getArg 1) expected?
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `((| $e |)) => pure e
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[termElab boo] def elabBoo : TermElab :=
|
||||
fun stx expected? =>
|
||||
|
|
@ -34,3 +35,14 @@ fun stx expected? =>
|
|||
|
||||
#eval run "#check [| @id.{1} Nat |]"
|
||||
#eval run "#check (| id 1 |)"
|
||||
-- #eval run "#check (| id 1, id 1 |)" -- it will fail
|
||||
|
||||
@[termElab tst] def elabTst2 : TermElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `((| $e1, $e2 |)) => `(($e1, $e2))
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
-- Now both work
|
||||
|
||||
#eval run "#check (| id 1 |)"
|
||||
#eval run "#check (| id 1, id 2 |)"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue