max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: save trace at MessageLog

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-08 10:18:58 -08:00
parent 9296bfde3f
commit 984b8f5eba
3 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Command.lean
View file

@ -111,7 +111,7 @@ fun ctx s =>
env := s.env,
messages := s.messages
};
match x termCtx termState with
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 }

19
src/Init/Lean/Elab/Log.lean
View file

@ -41,6 +41,9 @@ def logAt (pos : String.Pos) (severity : MessageSeverity) (msgData : MessageData
do msg ← mkMessage msgData severity pos;
logMessage msg
def logInfoAt (pos : String.Pos) (msgData : MessageData) : m Unit :=
logAt pos MessageSeverity.information msgData
def log (stx : Syntax) (severity : MessageSeverity) (msgData : MessageData) : m Unit :=
do pos ← getPos stx;
logAt pos severity msgData
@ -82,15 +85,21 @@ do trace ← SimpleMonadTracerAdapter.getTraceState;
SimpleMonadTracerAdapter.setTraceState {};
pure trace
private def saveNewTraceAsMessages {m : Type → Type} [Monad m] [MonadLog m] [SimpleMonadTracerAdapter m] (ref : Syntax) (oldTraceState : TraceState) : m Unit :=
private def saveNewTraceAsMessagesAt {m : Type → Type} [Monad m] [MonadLog m] [SimpleMonadTracerAdapter m] (pos : String.Pos) (oldTraceState : TraceState) : m Unit :=
do traces ← SimpleMonadTracerAdapter.getTraces;
traces.forM $ logInfo ref;
traces.forM $ logInfoAt pos;
SimpleMonadTracerAdapter.setTraceState oldTraceState
/-- Execute `x` and save generated trace messages in the `MessageLog` using position information provided by `ref`. -/
@[specialize] def tracingAt {α} {m : Type → Type} [Monad m] [MonadExcept Exception m] [MonadLog m] [SimpleMonadTracerAdapter m] (ref : Syntax) (x : m α) : m α :=
@[inline] def tracingAtPos {α} {m : Type → Type} [Monad m] [MonadExcept Exception m] [MonadLog m] [SimpleMonadTracerAdapter m] (pos : String.Pos) (x : m α) : m α :=
do oldTraceState ← resetTraceState;
finally x (saveNewTraceAsMessages ref oldTraceState)
finally x (saveNewTraceAsMessagesAt pos oldTraceState)
/-- If `ref` provides position information, then execute `x` and save generated trace messages in the `MessageLog` using the position.
Otherwise, just execute `x` -/
@[inline] def tracingAt {α} {m : Type → Type} [Monad m] [MonadExcept Exception m] [MonadLog m] [SimpleMonadTracerAdapter m] (ref : Syntax) (x : m α) : m α :=
match ref.getPos with
| none => x
| some pos => tracingAtPos pos x
end Elab
end Lean

2
src/Init/Lean/Elab/Term.lean
View file

@ -117,7 +117,7 @@ stx.ifNode
let tables := termElabAttribute.ext.getState s.env;
let k := n.getKind;
match tables.find k with
| some elab => elab n expectedType
| 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")