refactor: eliminate ref plumbing
This commit is contained in:
Leonardo de Moura
parent
46f5670ba3
commit
5ba9aad7a3
16 changed files with 268 additions and 261 deletions
|
|
@ -285,7 +285,7 @@ fType ← instantiateMVars fType;
|
|||
trace `Elab.app.args $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
|
||||
unless (namedArgs.isEmpty && args.isEmpty) $
|
||||
tryPostponeIfMVar fType;
|
||||
ref ← getCurrRef;
|
||||
ref ← getRef;
|
||||
elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
|
||||
|
||||
/-- Auxiliary inductive datatype that represents the resolution of an `LVal`. -/
|
||||
|
|
@ -554,20 +554,19 @@ candidates.filter $ fun c => match c with
|
|||
| EStateM.Result.ok _ _ => true
|
||||
| _ => false
|
||||
|
||||
private def toMessageData (msg : Message) (stx : Syntax) : TermElabM MessageData := do
|
||||
strPos ← getPos stx;
|
||||
pos ← getPosition strPos;
|
||||
private def toMessageData (msg : Message) : TermElabM MessageData := do
|
||||
pos ← getRefPosition;
|
||||
if pos == msg.pos then
|
||||
pure msg.data
|
||||
else
|
||||
pure $ toString msg.pos.line ++ ":" ++ toString msg.pos.column ++ " " ++ msg.data
|
||||
|
||||
private def mergeFailures {α} (failures : Array TermElabResult) (stx : Syntax) : TermElabM α := do
|
||||
private def mergeFailures {α} (failures : Array TermElabResult) : TermElabM α := do
|
||||
msgs ← failures.mapM $ fun failure =>
|
||||
match failure with
|
||||
| EStateM.Result.ok _ _ => unreachable!
|
||||
| EStateM.Result.error errMsg s => toMessageData errMsg stx;
|
||||
throwErrorAt stx ("overloaded, errors " ++ MessageData.ofArray msgs)
|
||||
| EStateM.Result.error errMsg s => toMessageData errMsg;
|
||||
throwError ("overloaded, errors " ++ MessageData.ofArray msgs)
|
||||
|
||||
private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) : TermElabM Expr := do
|
||||
/- TODO: if `f` contains `choice` or overloaded symbols, `mayPostpone == true`, and `expectedType? == some ?m` where `?m` is not assigned,
|
||||
|
|
@ -590,7 +589,7 @@ else
|
|||
| _ => unreachable!;
|
||||
throwErrorAt f ("ambiguous, possible interpretations " ++ MessageData.ofArray msgs)
|
||||
else
|
||||
mergeFailures candidates f
|
||||
withRef f $ mergeFailures candidates
|
||||
|
||||
private partial def expandApp (stx : Syntax) : TermElabM (Syntax × Array NamedArg × Array Arg) := do
|
||||
let f := stx.getArg 0;
|
||||
|
|
|
|||
|
|
@ -46,6 +46,7 @@ structure Context :=
|
|||
(cmdPos : String.Pos := 0)
|
||||
(macroStack : MacroStack := [])
|
||||
(currMacroScope : MacroScope := firstFrontendMacroScope)
|
||||
(ref : Syntax := Syntax.missing)
|
||||
|
||||
instance Exception.inhabited : Inhabited Exception := ⟨Exception.error $ arbitrary _⟩
|
||||
|
||||
|
|
@ -53,6 +54,14 @@ abbrev CommandElabCoreM (ε) := ReaderT Context (EIO ε)
|
|||
abbrev CommandElabM := CommandElabCoreM Exception
|
||||
abbrev CommandElab := Syntax → CommandElabM Unit
|
||||
|
||||
@[inline] def getCurrRef : CommandElabM Syntax := do
|
||||
ctx ← read;
|
||||
pure ctx.ref
|
||||
|
||||
/- Execute `x` using using `ref` as the default Syntax for providing position information to error messages. -/
|
||||
@[inline] def withRef {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM α := do
|
||||
adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
|
||||
|
||||
def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
|
||||
mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
|
||||
|
||||
|
|
@ -63,14 +72,14 @@ mkMessageAux ctx ref (addMacroStack (toString err) ctx.macroStack) MessageSeveri
|
|||
@[inline] def liftIOCore {α} (ctx : Context) (ref : Syntax) (x : IO α) : EIO Exception α :=
|
||||
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
|
||||
@[inline] def liftIO {α} (x : IO α) : CommandElabM α :=
|
||||
fun ctx => liftIOCore ctx ctx.ref x
|
||||
|
||||
private def getState : CommandElabM State :=
|
||||
fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.get
|
||||
fun ctx => liftIOCore ctx ctx.ref $ ctx.stateRef.get
|
||||
|
||||
private def setState (s : State) : CommandElabM Unit :=
|
||||
fun ctx => liftIOCore ctx Syntax.missing $ ctx.stateRef.set s
|
||||
fun ctx => liftIOCore ctx ctx.ref $ ctx.stateRef.set s
|
||||
|
||||
@[inline] private def modifyGetState {α} (f : State → α × State) : CommandElabM α := do
|
||||
s ← getState; let (a, s) := f s; setState s; pure a
|
||||
|
|
@ -89,7 +98,7 @@ env ← getEnv; opts ← getOptions;
|
|||
pure (MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msg)
|
||||
|
||||
instance CommandElabM.monadLog : MonadLog CommandElabM :=
|
||||
{ getCmdPos := do ctx ← read; pure ctx.cmdPos,
|
||||
{ getRef := do ctx ← read; pure ctx.ref,
|
||||
getFileMap := do ctx ← read; pure ctx.fileMap,
|
||||
getFileName := do ctx ← read; pure ctx.fileName,
|
||||
addContext := addContext,
|
||||
|
|
@ -98,20 +107,24 @@ instance CommandElabM.monadLog : MonadLog CommandElabM :=
|
|||
/--
|
||||
Throws an error with the given `msgData` and extracting position information from `ref`.
|
||||
If `ref` does not contain position information, then use `cmdPos` -/
|
||||
def throwError {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α := do
|
||||
def throwError {α} (msgData : MessageData) : CommandElabM α := do
|
||||
ctx ← read;
|
||||
let ref := getBetterRef ref ctx.macroStack;
|
||||
let ref := getBetterRef ctx.ref ctx.macroStack;
|
||||
let msgData := addMacroStack msgData ctx.macroStack;
|
||||
msg ← mkMessage msgData MessageSeverity.error ref;
|
||||
throw (Exception.error msg)
|
||||
withRef ref do
|
||||
msg ← mkMessage msgData MessageSeverity.error;
|
||||
throw (Exception.error msg)
|
||||
|
||||
def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : CommandElabM Unit := do
|
||||
def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α :=
|
||||
withRef ref $ throwError msgData
|
||||
|
||||
def logTrace (cls : Name) (msg : MessageData) : CommandElabM Unit := do
|
||||
msg ← addContext $ MessageData.tagged cls msg;
|
||||
logInfo ref msg
|
||||
logInfo msg
|
||||
|
||||
@[inline] def trace (cls : Name) (ref : Syntax) (msg : Unit → MessageData) : CommandElabM Unit := do
|
||||
@[inline] def trace (cls : Name) (msg : Unit → MessageData) : CommandElabM Unit := do
|
||||
opts ← getOptions;
|
||||
when (checkTraceOption opts cls) $ logTrace cls ref (msg ())
|
||||
when (checkTraceOption opts cls) $ logTrace cls (msg ())
|
||||
|
||||
def throwUnsupportedSyntax {α} : CommandElabM α :=
|
||||
throw Elab.Exception.unsupportedSyntax
|
||||
|
|
@ -133,15 +146,15 @@ unsafe def mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab) :=
|
|||
mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
|
||||
@[init mkCommandElabAttribute] constant commandElabAttribute : KeyedDeclsAttribute CommandElab := arbitrary _
|
||||
|
||||
@[inline] def withIncRecDepth {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM α := do
|
||||
@[inline] def withIncRecDepth {α} (x : CommandElabM α) : CommandElabM α := do
|
||||
ctx ← read; s ← get;
|
||||
when (ctx.currRecDepth == s.maxRecDepth) $ throwError ref maxRecDepthErrorMessage;
|
||||
when (ctx.currRecDepth == s.maxRecDepth) $ throwError maxRecDepthErrorMessage;
|
||||
adaptReader (fun (ctx : Context) => { ctx with currRecDepth := ctx.currRecDepth + 1 }) x
|
||||
|
||||
private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → CommandElabM Unit
|
||||
| [] => do
|
||||
let refFmt := stx.prettyPrint;
|
||||
throwError stx ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
throwError ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
|
||||
| (elabFn::elabFns) => catch (elabFn stx)
|
||||
(fun ex => match ex with
|
||||
| Exception.error _ => throw ex
|
||||
|
|
@ -158,18 +171,18 @@ instance : MonadMacroAdapter CommandElabM :=
|
|||
setNextMacroScope := fun next => modify $ fun s => { s with nextMacroScope := next },
|
||||
getCurrRecDepth := do ctx ← read; pure ctx.currRecDepth,
|
||||
getMaxRecDepth := do s ← get; pure s.maxRecDepth,
|
||||
throwError := @throwError,
|
||||
throwError := @throwErrorAt,
|
||||
throwUnsupportedSyntax := @throwUnsupportedSyntax}
|
||||
|
||||
partial def elabCommand : Syntax → CommandElabM Unit
|
||||
| stx => withIncRecDepth stx $ withFreshMacroScope $ match stx with
|
||||
| stx => withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
|
||||
| Syntax.node k args =>
|
||||
if k == nullKind then
|
||||
-- list of commands => elaborate in order
|
||||
-- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
|
||||
args.forM elabCommand
|
||||
else do
|
||||
trace `Elab.step stx $ fun _ => stx;
|
||||
trace `Elab.step fun _ => stx;
|
||||
s ← get;
|
||||
stxNew? ← catch
|
||||
(do newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx))
|
||||
|
|
@ -183,8 +196,8 @@ partial def elabCommand : Syntax → CommandElabM Unit
|
|||
let k := stx.getKind;
|
||||
match table.find? k with
|
||||
| some elabFns => elabCommandUsing s stx elabFns
|
||||
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
|
||||
| _ => throwError stx "unexpected command"
|
||||
| none => throwError ("elaboration function for '" ++ toString k ++ "' has not been implemented")
|
||||
| _ => throwError "unexpected command"
|
||||
|
||||
/-- Adapt a syntax transformation to a regular, command-producing elaborator. -/
|
||||
def adaptExpander (exp : Syntax → CommandElabM Syntax) : CommandElab :=
|
||||
|
|
@ -199,13 +212,13 @@ let scope := s.scopes.head!;
|
|||
fileMap := ctx.fileMap,
|
||||
currRecDepth := ctx.currRecDepth,
|
||||
maxRecDepth := s.maxRecDepth,
|
||||
cmdPos := ctx.cmdPos,
|
||||
declName? := declName?,
|
||||
macroStack := ctx.macroStack,
|
||||
currMacroScope := ctx.currMacroScope,
|
||||
currNamespace := scope.currNamespace,
|
||||
levelNames := scope.levelNames,
|
||||
openDecls := scope.openDecls }
|
||||
openDecls := scope.openDecls,
|
||||
ref := ctx.ref }
|
||||
|
||||
private def mkTermState (s : State) : Term.State :=
|
||||
{ env := s.env,
|
||||
|
|
@ -257,25 +270,25 @@ modify $ fun s => {
|
|||
scopes := { s.scopes.head! with kind := kind, header := header, currNamespace := newNamespace } :: s.scopes
|
||||
}
|
||||
|
||||
private def addScopes (ref : Syntax) (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
|
||||
private def addScopes (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
|
||||
| Name.anonymous => pure ()
|
||||
| Name.str p header _ => do
|
||||
addScopes p;
|
||||
currNamespace ← getCurrNamespace;
|
||||
addScope kind header (if updateNamespace then currNamespace ++ header else currNamespace)
|
||||
| _ => throwError ref "invalid scope"
|
||||
| _ => throwError "invalid scope"
|
||||
|
||||
private def addNamespace (ref : Syntax) (header : Name) : CommandElabM Unit :=
|
||||
addScopes ref "namespace" true header
|
||||
private def addNamespace (header : Name) : CommandElabM Unit :=
|
||||
addScopes "namespace" true header
|
||||
|
||||
@[builtinCommandElab «namespace»] def elabNamespace : CommandElab :=
|
||||
fun stx => match_syntax stx with
|
||||
| `(namespace $n) => addNamespace stx n.getId
|
||||
| `(namespace $n) => addNamespace n.getId
|
||||
| _ => throw Exception.unsupportedSyntax
|
||||
|
||||
@[builtinCommandElab «section»] def elabSection : CommandElab :=
|
||||
fun stx => match_syntax stx with
|
||||
| `(section $header:ident) => addScopes stx "section" false header.getId
|
||||
| `(section $header:ident) => addScopes "section" false header.getId
|
||||
| `(section) => do currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
|
||||
| _ => throw Exception.unsupportedSyntax
|
||||
|
||||
|
|
@ -303,14 +316,14 @@ fun stx => do
|
|||
else do {
|
||||
-- we keep "root" scope
|
||||
modify $ fun s => { s with scopes := s.scopes.drop (s.scopes.length - 1) };
|
||||
throwError stx "invalid 'end', insufficient scopes"
|
||||
throwError "invalid 'end', insufficient scopes"
|
||||
};
|
||||
match header? with
|
||||
| none => unless (checkAnonymousScope scopes) $ throwError stx "invalid 'end', name is missing"
|
||||
| some header => unless (checkEndHeader header scopes) $ throwError stx "invalid 'end', name mismatch"
|
||||
| none => unless (checkAnonymousScope scopes) $ throwError "invalid 'end', name is missing"
|
||||
| some header => unless (checkEndHeader header scopes) $ throwError "invalid 'end', name mismatch"
|
||||
|
||||
@[inline] def withNamespace {α} (ref : Syntax) (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
|
||||
addNamespace ref ns;
|
||||
@[inline] def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α := do
|
||||
addNamespace ns;
|
||||
a ← elabFn;
|
||||
modify $ fun s => { s with scopes := s.scopes.drop ns.getNumParts };
|
||||
pure a
|
||||
|
|
@ -325,14 +338,15 @@ modify $ fun s =>
|
|||
def getLevelNames : CommandElabM (List Name) := do
|
||||
scope ← getScope; pure scope.levelNames
|
||||
|
||||
def throwAlreadyDeclaredUniverseLevel {α} (ref : Syntax) (u : Name) : CommandElabM α :=
|
||||
throwError ref ("a universe level named '" ++ toString u ++ "' has already been declared")
|
||||
def throwAlreadyDeclaredUniverseLevel {α} (u : Name) : CommandElabM α :=
|
||||
throwError ("a universe level named '" ++ toString u ++ "' has already been declared")
|
||||
|
||||
def addUnivLevel (idStx : Syntax) : CommandElabM Unit := do
|
||||
def addUnivLevel (idStx : Syntax) : CommandElabM Unit :=
|
||||
withRef idStx do
|
||||
let id := idStx.getId;
|
||||
levelNames ← getLevelNames;
|
||||
if levelNames.elem id then
|
||||
throwAlreadyDeclaredUniverseLevel idStx id
|
||||
throwAlreadyDeclaredUniverseLevel id
|
||||
else
|
||||
modifyScope $ fun scope => { scope with levelNames := id :: scope.levelNames }
|
||||
|
||||
|
|
@ -367,13 +381,13 @@ fun stx => do
|
|||
| Except.ok env => setEnv env
|
||||
| Except.error ex => do
|
||||
opts ← getOptions;
|
||||
throwError stx (ex.toMessageData opts)
|
||||
throwError (ex.toMessageData opts)
|
||||
|
||||
def getOpenDecls : CommandElabM (List OpenDecl) := do
|
||||
scope ← getScope; pure scope.openDecls
|
||||
|
||||
def logUnknownDecl (stx : Syntax) (declName : Name) : CommandElabM Unit :=
|
||||
logError stx ("unknown declaration '" ++ toString declName ++ "'")
|
||||
def logUnknownDecl (declName : Name) : CommandElabM Unit :=
|
||||
logError ("unknown declaration '" ++ toString declName ++ "'")
|
||||
|
||||
def resolveNamespace (id : Name) : CommandElabM Name := do
|
||||
env ← getEnv;
|
||||
|
|
@ -389,7 +403,7 @@ fun stx => do
|
|||
let id := stx.getIdAt 1;
|
||||
ns ← resolveNamespace id;
|
||||
currNamespace ← getCurrNamespace;
|
||||
when (ns == currNamespace) $ throwError stx "invalid 'export', self export";
|
||||
when (ns == currNamespace) $ throwError "invalid 'export', self export";
|
||||
env ← getEnv;
|
||||
let ids := (stx.getArg 3).getArgs;
|
||||
aliases ← ids.foldlM
|
||||
|
|
@ -399,7 +413,7 @@ fun stx => do
|
|||
if env.contains declName then
|
||||
pure $ (currNamespace ++ id, declName) :: aliases
|
||||
else do
|
||||
logUnknownDecl idStx declName;
|
||||
withRef idStx $ logUnknownDecl declName;
|
||||
pure aliases
|
||||
})
|
||||
[];
|
||||
|
|
@ -427,7 +441,7 @@ ids.forArgsM $ fun idStx => do
|
|||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit id declName)
|
||||
else
|
||||
logUnknownDecl idStx declName
|
||||
withRef idStx $ logUnknownDecl declName
|
||||
|
||||
-- `open` id `hiding` id+
|
||||
def elabOpenHiding (n : SyntaxNode) : CommandElabM Unit := do
|
||||
|
|
@ -441,7 +455,7 @@ ids : List Name ← idsStx.foldArgsM (fun idStx ids => do
|
|||
if env.contains declName then
|
||||
pure (id::ids)
|
||||
else do
|
||||
logUnknownDecl idStx declName;
|
||||
withRef idStx $ logUnknownDecl declName;
|
||||
pure ids)
|
||||
[];
|
||||
addOpenDecl (OpenDecl.simple ns ids)
|
||||
|
|
@ -459,7 +473,7 @@ rs.forSepArgsM $ fun stx => do
|
|||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit toId declName)
|
||||
else
|
||||
logUnknownDecl stx declName
|
||||
withRef stx $ logUnknownDecl declName
|
||||
|
||||
@[builtinCommandElab «open»] def elabOpen : CommandElab :=
|
||||
fun n => do
|
||||
|
|
@ -501,13 +515,13 @@ fun stx => do
|
|||
e ← Term.elabTerm term none;
|
||||
Term.synthesizeSyntheticMVars false;
|
||||
type ← Term.inferType e;
|
||||
logInfo stx (e ++ " : " ++ type);
|
||||
logInfo (e ++ " : " ++ type);
|
||||
pure ()
|
||||
|
||||
def hasNoErrorMessages : CommandElabM Bool := do
|
||||
s ← get; pure $ !s.messages.hasErrors
|
||||
|
||||
def failIfSucceeds (ref : Syntax) (x : CommandElabM Unit) : CommandElabM Unit := do
|
||||
def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
|
||||
let resetMessages : CommandElabM MessageLog := do {
|
||||
s ← get;
|
||||
let messages := s.messages;
|
||||
|
|
@ -523,20 +537,20 @@ succeeded ← finally
|
|||
(do x; hasNoErrorMessages)
|
||||
(fun ex => match ex with
|
||||
| Exception.error msg => do modify (fun s => { s with messages := s.messages.add msg }); pure false
|
||||
| Exception.unsupportedSyntax => do logError ref "unsupported syntax"; pure false))
|
||||
| Exception.unsupportedSyntax => do logError "unsupported syntax"; pure false))
|
||||
(restoreMessages prevMessages);
|
||||
when succeeded $
|
||||
throwError ref "unexpected success"
|
||||
throwError "unexpected success"
|
||||
|
||||
@[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab :=
|
||||
fun stx => failIfSucceeds stx $ elabCheck stx
|
||||
fun stx => failIfSucceeds $ elabCheck stx
|
||||
|
||||
def addDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.addDecl decl
|
||||
def compileDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.compileDecl decl
|
||||
|
||||
def addInstance (ref : Syntax) (declName : Name) : CommandElabM Unit := do
|
||||
def addInstance (declName : Name) : CommandElabM Unit := do
|
||||
env ← getEnv;
|
||||
env ← liftIO ref $ Meta.addGlobalInstance env declName;
|
||||
env ← liftIO $ Meta.addGlobalInstance env declName;
|
||||
setEnv env
|
||||
|
||||
unsafe def elabEvalUnsafe : CommandElab :=
|
||||
|
|
@ -569,8 +583,8 @@ fun stx => withoutModifyingEnv do
|
|||
| Except.error e => Term.throwError e
|
||||
| Except.ok act => pure $ act env opts
|
||||
};
|
||||
(out, res) ← liftIO ref $ IO.Prim.withIsolatedStreams act;
|
||||
logInfo ref out;
|
||||
(out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
|
||||
logInfo out;
|
||||
match res with
|
||||
| Except.error e => throw $ Exception.error $ ioErrorToMessage ctx ref e
|
||||
| Except.ok env => do setEnv env; pure ()
|
||||
|
|
@ -588,8 +602,8 @@ fun stx => withoutModifyingEnv do
|
|||
| Except.error e => Term.throwError e
|
||||
| Except.ok act => pure act
|
||||
};
|
||||
(out, res) ← liftIO ref $ IO.Prim.withIsolatedStreams act;
|
||||
logInfo ref out;
|
||||
(out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
|
||||
logInfo out;
|
||||
match res with
|
||||
| Except.error e => throw $ Exception.error $ ioErrorToMessage ctx ref e
|
||||
| Except.ok _ => pure ()
|
||||
|
|
@ -604,19 +618,18 @@ constant elabEval : CommandElab := arbitrary _
|
|||
|
||||
@[builtinCommandElab «synth»] def elabSynth : CommandElab :=
|
||||
fun stx => do
|
||||
let ref := stx;
|
||||
let term := stx.getArg 1;
|
||||
withoutModifyingEnv $ runTermElabM `_synth_cmd $ fun _ => do
|
||||
inst ← Term.elabTerm term none;
|
||||
Term.synthesizeSyntheticMVars false;
|
||||
inst ← Term.instantiateMVars inst;
|
||||
val ← Term.liftMetaM $ Meta.synthInstance inst;
|
||||
logInfo stx val;
|
||||
logInfo val;
|
||||
pure ()
|
||||
|
||||
def setOption (ref : Syntax) (optionName : Name) (val : DataValue) : CommandElabM Unit := do
|
||||
decl ← liftIO ref $ getOptionDecl optionName;
|
||||
unless (decl.defValue.sameCtor val) $ throwError ref "type mismatch at set_option";
|
||||
def setOption (optionName : Name) (val : DataValue) : CommandElabM Unit := do
|
||||
decl ← liftIO $ getOptionDecl optionName;
|
||||
unless (decl.defValue.sameCtor val) $ throwError "type mismatch at set_option";
|
||||
modifyScope $ fun scope => { scope with opts := scope.opts.insert optionName val };
|
||||
match optionName, val with
|
||||
| `maxRecDepth, DataValue.ofNat max => modify $ fun s => { s with maxRecDepth := max }
|
||||
|
|
@ -624,19 +637,18 @@ match optionName, val with
|
|||
|
||||
@[builtinCommandElab «set_option»] def elabSetOption : CommandElab :=
|
||||
fun stx => do
|
||||
let ref := stx;
|
||||
let optionName := stx.getIdAt 1;
|
||||
let val := stx.getArg 2;
|
||||
match val.isStrLit? with
|
||||
| some str => setOption ref optionName (DataValue.ofString str)
|
||||
| some str => setOption optionName (DataValue.ofString str)
|
||||
| none =>
|
||||
match val.isNatLit? with
|
||||
| some num => setOption ref optionName (DataValue.ofNat num)
|
||||
| some num => setOption optionName (DataValue.ofNat num)
|
||||
| none =>
|
||||
match val with
|
||||
| Syntax.atom _ "true" => setOption ref optionName (DataValue.ofBool true)
|
||||
| Syntax.atom _ "false" => setOption ref optionName (DataValue.ofBool false)
|
||||
| _ => logError val ("unexpected set_option value " ++ toString val)
|
||||
| Syntax.atom _ "true" => setOption optionName (DataValue.ofBool true)
|
||||
| Syntax.atom _ "false" => setOption optionName (DataValue.ofBool false)
|
||||
| _ => withRef val $ logError ("unexpected set_option value " ++ toString val)
|
||||
|
||||
/-
|
||||
`declId` is of the form
|
||||
|
|
@ -666,12 +678,12 @@ levelNames ←
|
|||
(fun levelNames idStx =>
|
||||
let id := idStx.getId;
|
||||
if levelNames.elem id then
|
||||
throwAlreadyDeclaredUniverseLevel idStx id
|
||||
withRef idStx $ throwAlreadyDeclaredUniverseLevel id
|
||||
else
|
||||
pure (id :: levelNames))
|
||||
savedLevelNames
|
||||
};
|
||||
let ref := declId;
|
||||
withRef declId $
|
||||
-- extract (optional) namespace part of id, after decoding macro scopes that would interfere with the check
|
||||
let scpView := extractMacroScopes id;
|
||||
match scpView.name with
|
||||
|
|
@ -679,10 +691,10 @@ match scpView.name with
|
|||
/- Add back macro scopes. We assume a declaration like `def a.b[1,2] ...` with macro scopes `[1,2]`
|
||||
is always meant to mean `namespace a def b[1,2] ...`. -/
|
||||
let id := { scpView with name := mkNameSimple s }.review;
|
||||
withNamespace ref pre $ do
|
||||
withNamespace pre $ do
|
||||
modifyScope $ fun scope => { scope with levelNames := levelNames };
|
||||
finally (f id) (modifyScope $ fun scope => { scope with levelNames := savedLevelNames })
|
||||
| _ => throwError ref "invalid declaration name"
|
||||
| _ => throwError "invalid declaration name"
|
||||
|
||||
/--
|
||||
Sort the given list of `usedParams` using the following order:
|
||||
|
|
|
|||
|
|
@ -67,11 +67,11 @@ def elabAttr (stx : Syntax) : CommandElabM Attribute := do
|
|||
-- rawIdent >> many attrArg
|
||||
let nameStx := stx.getArg 0;
|
||||
attrName ← match nameStx.isIdOrAtom? with
|
||||
| none => throwError nameStx "identifier expected"
|
||||
| none => withRef nameStx $ throwError "identifier expected"
|
||||
| some str => pure $ mkNameSimple str;
|
||||
env ← getEnv;
|
||||
unless (isAttribute env attrName) $
|
||||
throwError stx ("unknown attribute [" ++ attrName ++ "]");
|
||||
throwError ("unknown attribute [" ++ attrName ++ "]");
|
||||
let args := stx.getArg 1;
|
||||
-- the old frontend passes Syntax.missing for empty args, for reasons
|
||||
let args := if args.getNumArgs == 0 then Syntax.missing else args;
|
||||
|
|
@ -95,14 +95,14 @@ docString ← match docCommentStx.getOptional? with
|
|||
| none => pure none
|
||||
| some s => match s.getArg 1 with
|
||||
| Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
|
||||
| _ => throwError s ("unexpected doc string " ++ toString (s.getArg 1));
|
||||
| _ => throwErrorAt s ("unexpected doc string " ++ toString (s.getArg 1));
|
||||
visibility ← match visibilityStx.getOptional? with
|
||||
| none => pure Visibility.regular
|
||||
| some v =>
|
||||
let kind := v.getKind;
|
||||
if kind == `Lean.Parser.Command.private then pure Visibility.private
|
||||
else if kind == `Lean.Parser.Command.protected then pure Visibility.protected
|
||||
else throwError v "unexpected visibility modifier";
|
||||
else throwErrorAt v "unexpected visibility modifier";
|
||||
attrs ← match attrsStx.getOptional? with
|
||||
| none => pure #[]
|
||||
| some attrs => elabAttrs attrs;
|
||||
|
|
@ -115,51 +115,51 @@ pure {
|
|||
attrs := attrs
|
||||
}
|
||||
|
||||
def checkNotAlreadyDeclared (ref : Syntax) (declName : Name) : CommandElabM Unit := do
|
||||
def checkNotAlreadyDeclared (declName : Name) : CommandElabM Unit := do
|
||||
env ← getEnv;
|
||||
when (env.contains declName) $
|
||||
match privateToUserName? declName with
|
||||
| none => throwError ref ("'" ++ declName ++ "' has already been declared")
|
||||
| some declName => throwError ref ("private declaration '" ++ declName ++ "' has already been declared");
|
||||
| none => throwError ("'" ++ declName ++ "' has already been declared")
|
||||
| some declName => throwError ("private declaration '" ++ declName ++ "' has already been declared");
|
||||
when (env.contains (mkPrivateName env declName)) $
|
||||
throwError ref ("a private declaration '" ++ declName ++ "' has already been declared");
|
||||
throwError ("a private declaration '" ++ declName ++ "' has already been declared");
|
||||
match privateToUserName? declName with
|
||||
| none => pure ()
|
||||
| some declName =>
|
||||
when (env.contains declName) $
|
||||
throwError ref ("a non-private declaration '" ++ declName ++ "' has already been declared")
|
||||
throwError ("a non-private declaration '" ++ declName ++ "' has already been declared")
|
||||
|
||||
def applyVisibility (ref : Syntax) (visibility : Visibility) (declName : Name) : CommandElabM Name :=
|
||||
def applyVisibility (visibility : Visibility) (declName : Name) : CommandElabM Name :=
|
||||
match visibility with
|
||||
| Visibility.private => do
|
||||
env ← getEnv;
|
||||
let declName := mkPrivateName env declName;
|
||||
checkNotAlreadyDeclared ref declName;
|
||||
checkNotAlreadyDeclared declName;
|
||||
pure declName
|
||||
| Visibility.protected => do
|
||||
checkNotAlreadyDeclared ref declName;
|
||||
checkNotAlreadyDeclared declName;
|
||||
env ← getEnv;
|
||||
let env := addProtected env declName;
|
||||
setEnv env;
|
||||
pure declName
|
||||
| _ => do
|
||||
checkNotAlreadyDeclared ref declName;
|
||||
checkNotAlreadyDeclared declName;
|
||||
pure declName
|
||||
|
||||
def mkDeclName (ref : Syntax) (modifiers : Modifiers) (atomicName : Name) : CommandElabM Name := do
|
||||
def mkDeclName (modifiers : Modifiers) (atomicName : Name) : CommandElabM Name := do
|
||||
currNamespace ← getCurrNamespace;
|
||||
let declName := currNamespace ++ atomicName;
|
||||
applyVisibility ref modifiers.visibility declName
|
||||
applyVisibility modifiers.visibility declName
|
||||
|
||||
def applyAttributes (ref : Syntax) (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
|
||||
def applyAttributes (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
|
||||
attrs.forM $ fun attr => do
|
||||
env ← getEnv;
|
||||
match getAttributeImpl env attr.name with
|
||||
| Except.error errMsg => throwError ref errMsg
|
||||
| Except.error errMsg => throwError errMsg
|
||||
| Except.ok attrImpl =>
|
||||
when (attrImpl.applicationTime == applicationTime) $ do
|
||||
env ← getEnv;
|
||||
env ← liftIO ref $ attrImpl.add env declName attr.args true;
|
||||
env ← liftIO $ attrImpl.add env declName attr.args true;
|
||||
setEnv env
|
||||
|
||||
end Command
|
||||
|
|
|
|||
|
|
@ -59,7 +59,7 @@ let (binders, type) := expandDeclSig (stx.getArg 2);
|
|||
let modifiers := modifiers.addAttribute { name := `instance };
|
||||
declId ← match (stx.getArg 1).getOptional? with
|
||||
| some declId => pure declId
|
||||
| none => throwError stx "not implemented yet";
|
||||
| none => throwError "not implemented yet";
|
||||
elabDefLike {
|
||||
ref := stx, kind := DefKind.def, modifiers := modifiers,
|
||||
declId := declId, binders := binders, type? := type, val := stx.getArg 3
|
||||
|
|
@ -81,8 +81,8 @@ let declId := stx.getArg 1;
|
|||
let (binders, typeStx) := expandDeclSig (stx.getArg 2);
|
||||
scopeLevelNames ← getLevelNames;
|
||||
withDeclId declId $ fun name => do
|
||||
declName ← mkDeclName declId modifiers name;
|
||||
applyAttributes stx declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
|
||||
declName ← mkDeclName modifiers name;
|
||||
applyAttributes declName modifiers.attrs AttributeApplicationTime.beforeElaboration;
|
||||
allUserLevelNames ← getLevelNames;
|
||||
decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
|
||||
type ← Term.elabType typeStx;
|
||||
|
|
@ -103,8 +103,8 @@ withDeclId declId $ fun name => do
|
|||
}
|
||||
};
|
||||
addDecl decl;
|
||||
applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
applyAttributes stx declName modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
applyAttributes declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
applyAttributes declName modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
|
||||
/-
|
||||
parser! "inductive " >> declId >> optDeclSig >> many ctor
|
||||
|
|
@ -113,23 +113,23 @@ parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
|
|||
Remark: numTokens == 1 for regular `inductive` and 2 for `class inductive`.
|
||||
-/
|
||||
private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (numTokens := 1) : CommandElabM InductiveView := do
|
||||
checkValidInductiveModifier decl modifiers;
|
||||
checkValidInductiveModifier modifiers;
|
||||
let (binders, type?) := expandOptDeclSig (decl.getArg (numTokens + 1));
|
||||
let declId := decl.getArg numTokens;
|
||||
withDeclId declId fun name => do
|
||||
levelNames ← getLevelNames;
|
||||
declName ← mkDeclName declId modifiers name;
|
||||
ctors ← (decl.getArg (numTokens + 2)).getArgs.mapM fun ctor => do {
|
||||
declName ← mkDeclName modifiers name;
|
||||
ctors ← (decl.getArg (numTokens + 2)).getArgs.mapM fun ctor => withRef ctor do {
|
||||
-- def ctor := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
|
||||
ctorModifiers ← elabModifiers (ctor.getArg 1);
|
||||
when (ctorModifiers.isPrivate && modifiers.isPrivate) $
|
||||
throwError ctor "invalid 'private' constructor in a 'private' inductive datatype";
|
||||
throwError "invalid 'private' constructor in a 'private' inductive datatype";
|
||||
when (ctorModifiers.isProtected && modifiers.isPrivate) $
|
||||
throwError ctor "invalid 'protected' constructor in a 'private' inductive datatype";
|
||||
checkValidCtorModifier ctor ctorModifiers;
|
||||
throwError "invalid 'protected' constructor in a 'private' inductive datatype";
|
||||
checkValidCtorModifier ctorModifiers;
|
||||
let ctorName := ctor.getIdAt 2;
|
||||
let ctorName := declName ++ ctorName;
|
||||
ctorName ← applyVisibility (ctor.getArg 2) ctorModifiers.visibility ctorName;
|
||||
ctorName ← withRef (ctor.getArg 2) $ applyVisibility ctorModifiers.visibility ctorName;
|
||||
let inferMod := !(ctor.getArg 3).isNone;
|
||||
let (binders, type?) := expandOptDeclSig (ctor.getArg 4);
|
||||
pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
|
||||
|
|
@ -184,7 +184,7 @@ fun stx => do
|
|||
else if declKind == `Lean.Parser.Command.structure then
|
||||
elabStructure modifiers decl
|
||||
else
|
||||
throwError stx "unexpected declaration"
|
||||
throwError "unexpected declaration"
|
||||
|
||||
/- Return true if all elements of the mutual-block are inductive declarations. -/
|
||||
private def isMutualInductive (stx : Syntax) : Bool :=
|
||||
|
|
@ -243,7 +243,7 @@ fun stx => do
|
|||
if isMutualInductive stx then
|
||||
elabMutualInductive (stx.getArg 1).getArgs
|
||||
else
|
||||
throwError stx "invalid mutual block"
|
||||
throwError "invalid mutual block"
|
||||
|
||||
end Command
|
||||
end Elab
|
||||
|
|
|
|||
|
|
@ -119,12 +119,12 @@ else if kind == `Lean.Parser.Command.declValEqns then
|
|||
else
|
||||
Term.throwUnsupportedSyntax
|
||||
|
||||
def elabDefLike (view : DefView) : CommandElabM Unit := do
|
||||
let ref := view.ref;
|
||||
def elabDefLike (view : DefView) : CommandElabM Unit :=
|
||||
withRef view.ref do
|
||||
scopeLevelNames ← getLevelNames;
|
||||
withDeclId view.declId $ fun name => do
|
||||
declName ← mkDeclName view.declId view.modifiers name;
|
||||
applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
|
||||
declName ← withRef view.declId $ mkDeclName view.modifiers name;
|
||||
applyAttributes declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration;
|
||||
allUserLevelNames ← getLevelNames;
|
||||
decl? ← runTermElabM declName $ fun vars => Term.elabBinders view.binders.getArgs $ fun xs =>
|
||||
match view.type? with
|
||||
|
|
@ -144,9 +144,9 @@ withDeclId view.declId $ fun name => do
|
|||
| none => pure ()
|
||||
| some decl => do
|
||||
addDecl decl;
|
||||
applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
compileDecl decl;
|
||||
applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
applyAttributes declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
registerTraceClass `Elab.definition;
|
||||
|
|
|
|||
|
|
@ -15,24 +15,24 @@ namespace Lean
|
|||
namespace Elab
|
||||
namespace Command
|
||||
|
||||
def checkValidInductiveModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
def checkValidInductiveModifier (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in inductive declaration";
|
||||
throwError "invalid use of 'noncomputable' in inductive declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in inductive declaration";
|
||||
throwError "invalid use of 'partial' in inductive declaration";
|
||||
unless (modifiers.attrs.size == 0 || (modifiers.attrs.size == 1 && (modifiers.attrs.get! 0).name == `class)) $
|
||||
throwError ref "invalid use of attributes in inductive declaration";
|
||||
throwError "invalid use of attributes in inductive declaration";
|
||||
pure ()
|
||||
|
||||
def checkValidCtorModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
def checkValidCtorModifier (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in constructor declaration";
|
||||
throwError "invalid use of 'noncomputable' in constructor declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in constructor declaration";
|
||||
throwError "invalid use of 'partial' in constructor declaration";
|
||||
when modifiers.isUnsafe $
|
||||
throwError ref "invalid use of 'unsafe' in constructor declaration";
|
||||
throwError "invalid use of 'unsafe' in constructor declaration";
|
||||
when (modifiers.attrs.size != 0) $
|
||||
throwError ref "invalid use of attributes in constructor declaration";
|
||||
throwError "invalid use of attributes in constructor declaration";
|
||||
pure ()
|
||||
|
||||
|
||||
|
|
@ -490,7 +490,7 @@ decl ← runTermElabM view0.declName $ fun vars => Term.withRef ref $ mkInductiv
|
|||
addDecl decl;
|
||||
mkAuxConstructions views;
|
||||
-- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
|
||||
views.forM fun view => applyAttributes ref view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
views.forM fun view => applyAttributes view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
pure ()
|
||||
|
||||
end Command
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ namespace Level
|
|||
structure Context :=
|
||||
(fileName : String)
|
||||
(fileMap : FileMap)
|
||||
(cmdPos : String.Pos)
|
||||
(ref : Syntax)
|
||||
(levelNames : List Name)
|
||||
|
||||
structure State :=
|
||||
|
|
@ -24,11 +24,14 @@ structure State :=
|
|||
abbrev LevelElabM := ReaderT Context (EStateM Exception State)
|
||||
|
||||
instance LevelElabM.MonadLog : MonadPosInfo LevelElabM :=
|
||||
{ getCmdPos := do ctx ← read; pure ctx.cmdPos,
|
||||
{ getRef := do ctx ← read; pure ctx.ref,
|
||||
getFileMap := do ctx ← read; pure ctx.fileMap,
|
||||
getFileName := do ctx ← read; pure ctx.fileName,
|
||||
addContext := fun msg => pure msg }
|
||||
|
||||
@[inline] def withRef {α} (ref : Syntax) (x : LevelElabM α) : LevelElabM α := do
|
||||
adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
|
||||
|
||||
def mkFreshId : LevelElabM Name := do
|
||||
s ← get;
|
||||
let id := s.ngen.curr;
|
||||
|
|
@ -41,7 +44,7 @@ modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
|
|||
pure $ mkLevelMVar mvarId
|
||||
|
||||
partial def elabLevel : Syntax → LevelElabM Level
|
||||
| stx => do
|
||||
| stx => withRef stx do
|
||||
let kind := stx.getKind;
|
||||
if kind == `Lean.Parser.Level.paren then
|
||||
elabLevel (stx.getArg 1)
|
||||
|
|
@ -66,19 +69,19 @@ partial def elabLevel : Syntax → LevelElabM Level
|
|||
else if kind == `Lean.Parser.Level.num then do
|
||||
match (stx.getArg 0).isNatLit? with
|
||||
| some val => pure (Level.ofNat val)
|
||||
| none => throwError stx "ill-formed universe level syntax"
|
||||
| none => throwError "ill-formed universe level syntax"
|
||||
else if kind == `Lean.Parser.Level.ident then do
|
||||
let paramName := stx.getIdAt 0;
|
||||
ctx ← read;
|
||||
unless (ctx.levelNames.contains paramName) $ throwError stx ("unknown universe level " ++ paramName);
|
||||
unless (ctx.levelNames.contains paramName) $ throwError ("unknown universe level " ++ paramName);
|
||||
pure $ mkLevelParam paramName
|
||||
else if kind == `Lean.Parser.Level.addLit then do
|
||||
lvl ← elabLevel (stx.getArg 0);
|
||||
match (stx.getArg 2).isNatLit? with
|
||||
| some val => pure (lvl.addOffset val)
|
||||
| none => throwError stx "ill-formed universe level syntax"
|
||||
| none => throwError "ill-formed universe level syntax"
|
||||
else
|
||||
throwError stx "unexpected universe level syntax kind"
|
||||
throwError "unexpected universe level syntax kind"
|
||||
|
||||
end Level
|
||||
|
||||
|
|
|
|||
|
|
@ -9,13 +9,18 @@ import Lean.Elab.Exception
|
|||
namespace Lean
|
||||
namespace Elab
|
||||
|
||||
def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
|
||||
match ref.getPos with
|
||||
| some _ => ref
|
||||
| _ => oldRef
|
||||
|
||||
class MonadPosInfo (m : Type → Type) :=
|
||||
(getFileMap : m FileMap)
|
||||
(getFileName : m String)
|
||||
(getCmdPos : m String.Pos)
|
||||
(getRef : m Syntax)
|
||||
(addContext : MessageData → m MessageData)
|
||||
|
||||
export MonadPosInfo (getFileMap getFileName getCmdPos)
|
||||
export MonadPosInfo (getFileMap getFileName getRef)
|
||||
|
||||
class MonadLog (m : Type → Type) extends MonadPosInfo m :=
|
||||
(logMessage : Message → m Unit)
|
||||
|
|
@ -24,26 +29,24 @@ export MonadLog (logMessage)
|
|||
|
||||
variables {m : Type → Type} [Monad m]
|
||||
|
||||
def getPosition [MonadPosInfo m] (pos : Option String.Pos := none) : m Position := do
|
||||
fileMap ← getFileMap;
|
||||
cmdPos ← getCmdPos;
|
||||
pure $ fileMap.toPosition (pos.getD cmdPos)
|
||||
def getRefPos [MonadPosInfo m] : m String.Pos := do
|
||||
ref ← getRef;
|
||||
pure $ ref.getPos.getD 0
|
||||
|
||||
def mkMessageAt [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (pos : Option String.Pos := none) : m Message := do
|
||||
def getRefPosition [MonadPosInfo m] : m Position := do
|
||||
pos ← getRefPos;
|
||||
fileMap ← getFileMap;
|
||||
pure $ fileMap.toPosition pos
|
||||
|
||||
def mkMessageAt [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : m Message := do
|
||||
fileMap ← getFileMap;
|
||||
fileName ← getFileName;
|
||||
cmdPos ← getCmdPos;
|
||||
let pos := fileMap.toPosition (pos.getD cmdPos);
|
||||
let pos := fileMap.toPosition pos;
|
||||
msgData ← MonadPosInfo.addContext msgData;
|
||||
pure { fileName := fileName, pos := pos, data := msgData, severity := severity }
|
||||
|
||||
def getPos [MonadPosInfo m] (stx : Syntax) : m String.Pos :=
|
||||
match stx.getPos with
|
||||
| some p => pure p
|
||||
| none => getCmdPos
|
||||
|
||||
def mkMessage [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (stx : Syntax) : m Message := do
|
||||
pos ← getPos stx;
|
||||
def mkMessage [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) : m Message := do
|
||||
pos ← getRefPos;
|
||||
mkMessageAt msgData severity pos
|
||||
|
||||
def logAt [MonadLog m] (pos : String.Pos) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do
|
||||
|
|
@ -53,25 +56,21 @@ logMessage msg
|
|||
def logInfoAt [MonadLog m] (pos : String.Pos) (msgData : MessageData) : m Unit :=
|
||||
logAt pos MessageSeverity.information msgData
|
||||
|
||||
def log [MonadLog m] (stx : Syntax) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do
|
||||
pos ← getPos stx;
|
||||
def log [MonadLog m] (severity : MessageSeverity) (msgData : MessageData) : m Unit := do
|
||||
pos ← getRefPos;
|
||||
logAt pos severity msgData
|
||||
|
||||
def logError [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
|
||||
log stx MessageSeverity.error msgData
|
||||
def logError [MonadLog m] (msgData : MessageData) : m Unit :=
|
||||
log MessageSeverity.error msgData
|
||||
|
||||
def logWarning [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
|
||||
log stx MessageSeverity.warning msgData
|
||||
def logWarning [MonadLog m] (msgData : MessageData) : m Unit :=
|
||||
log MessageSeverity.warning msgData
|
||||
|
||||
def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
|
||||
log stx MessageSeverity.information msgData
|
||||
def logInfo [MonadLog m] (msgData : MessageData) : m Unit :=
|
||||
log MessageSeverity.information msgData
|
||||
|
||||
def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
|
||||
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;
|
||||
def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
|
||||
msg ← mkMessage msgData MessageSeverity.error;
|
||||
throw (Exception.error msg)
|
||||
|
||||
end Elab
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@ namespace Lean
|
|||
namespace Elab
|
||||
namespace Command
|
||||
|
||||
private def throwUnknownId (ref : Syntax) (id : Name) : CommandElabM Unit :=
|
||||
throwError ref ("unknown identifier '" ++ toString id ++ "'")
|
||||
private def throwUnknownId (id : Name) : CommandElabM Unit :=
|
||||
throwError ("unknown identifier '" ++ toString id ++ "'")
|
||||
|
||||
private def lparamsToMessageData (lparams : List Name) : MessageData :=
|
||||
match lparams with
|
||||
|
|
@ -30,19 +30,19 @@ let (m, id) := match privateToUserName? id : _ → MessageData × Name with
|
|||
let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type;
|
||||
pure m
|
||||
|
||||
private def printDefLike (ref : Syntax) (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
|
||||
private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
|
||||
m ← mkHeader kind id lparams type isUnsafe;
|
||||
let m := m ++ " :=" ++ Format.line ++ value;
|
||||
logInfo ref m
|
||||
logInfo m
|
||||
|
||||
private def printAxiomLike (ref : Syntax) (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
|
||||
private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
|
||||
m ← mkHeader kind id lparams type isUnsafe;
|
||||
logInfo ref m
|
||||
logInfo m
|
||||
|
||||
private def printQuot (ref : Syntax) (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
|
||||
printAxiomLike ref "Quotient primitive" id lparams type
|
||||
private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
|
||||
printAxiomLike "Quotient primitive" id lparams type
|
||||
|
||||
private def printInduct (ref : Syntax) (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
|
||||
private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
|
||||
(ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
|
||||
env ← getEnv;
|
||||
m ← mkHeader "inductive" id lparams type isUnsafe;
|
||||
|
|
@ -53,28 +53,28 @@ m ← ctors.foldlM
|
|||
| some v => pure $ m ++ Format.line ++ ctor ++ " : " ++ v.type
|
||||
| none => pure m)
|
||||
m;
|
||||
logInfo ref m
|
||||
logInfo m
|
||||
|
||||
private def printIdCore (ref : Syntax) (id : Name) : CommandElabM Unit := do
|
||||
private def printIdCore (id : Name) : CommandElabM Unit := do
|
||||
env ← getEnv;
|
||||
match env.find? id with
|
||||
| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "axiom" id us t u
|
||||
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike ref "def" id us t v u
|
||||
| ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike ref "theorem" id us t v.get
|
||||
| ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "constant" id us t u
|
||||
| ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot ref kind id us t
|
||||
| ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "constructor" id us t u
|
||||
| ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike ref "recursor" id us t u
|
||||
| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
|
||||
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
|
||||
| ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v.get
|
||||
| ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
|
||||
| ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t
|
||||
| ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
|
||||
| ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
|
||||
| ConstantInfo.inductInfo { lparams := us, nparams := nparams, nindices := nindices, type := t, ctors := ctors, isUnsafe := u, .. } =>
|
||||
printInduct ref id us nparams nindices t ctors u
|
||||
| none => throwUnknownId ref id
|
||||
printInduct id us nparams nindices t ctors u
|
||||
| none => throwUnknownId id
|
||||
|
||||
private def printId (ref : Syntax) (id : Name) : CommandElabM Unit := do
|
||||
private def printId (id : Name) : CommandElabM Unit := do
|
||||
cs ← liftTermElabM none $ Term.resolveGlobalName id;
|
||||
let cs := cs.filter fun ⟨_, ps⟩ => ps.isEmpty;
|
||||
let cs := cs.map fun ⟨c, _⟩ => c;
|
||||
when cs.isEmpty $ throwUnknownId ref id;
|
||||
cs.forM fun c => printIdCore ref c
|
||||
when cs.isEmpty $ throwUnknownId id;
|
||||
cs.forM fun c => printIdCore c
|
||||
|
||||
@[builtinCommandElab «print»] def elabPrint : CommandElab :=
|
||||
fun stx =>
|
||||
|
|
@ -82,12 +82,12 @@ fun stx =>
|
|||
if numArgs == 2 then
|
||||
let arg := stx.getArg 1;
|
||||
if arg.isIdent then
|
||||
printId stx arg.getId
|
||||
printId arg.getId
|
||||
else match arg.isStrLit? with
|
||||
| some val => logInfo stx val
|
||||
| none => throwError stx "WIP"
|
||||
| some val => logInfo val
|
||||
| none => throwError "WIP"
|
||||
else
|
||||
throwError stx "invalid #print command"
|
||||
throwError "invalid #print command"
|
||||
|
||||
end Command
|
||||
end Elab
|
||||
|
|
|
|||
|
|
@ -411,7 +411,7 @@ structure OldContext :=
|
|||
(open_nss : List Name)
|
||||
|
||||
private def oldRunTermElabM {α} (ctx : OldContext) (x : TermElabM α) : Except String α := do
|
||||
match x {fileName := "foo", fileMap := FileMap.ofString "", cmdPos := 0,
|
||||
match x {fileName := "foo", fileMap := FileMap.ofString "",
|
||||
currNamespace := ctx.env.getNamespace, currRecDepth := 0, maxRecDepth := 10000,
|
||||
openDecls := ctx.open_nss.map $ fun n => OpenDecl.simple n [],
|
||||
lctx := ctx.locals.foldl (fun lctx l => LocalContext.mkLocalDecl lctx l l exprPlaceholder) $ LocalContext.mkEmpty ()}
|
||||
|
|
|
|||
|
|
@ -100,31 +100,32 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
|
|||
let optCtor := structStx.getArg 6;
|
||||
if optCtor.isNone then
|
||||
pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
|
||||
else do
|
||||
else
|
||||
let ctor := optCtor.getArg 0;
|
||||
withRef ctor do
|
||||
ctorModifiers ← elabModifiers (ctor.getArg 0);
|
||||
checkValidCtorModifier ctor ctorModifiers;
|
||||
checkValidCtorModifier ctorModifiers;
|
||||
when (ctorModifiers.isPrivate && structModifiers.isPrivate) $
|
||||
throwError ctor "invalid 'private' constructor in a 'private' structure";
|
||||
throwError "invalid 'private' constructor in a 'private' structure";
|
||||
when (ctorModifiers.isProtected && structModifiers.isPrivate) $
|
||||
throwError ctor "invalid 'protected' constructor in a 'private' structure";
|
||||
throwError "invalid 'protected' constructor in a 'private' structure";
|
||||
let inferMod := !(ctor.getArg 2).isNone;
|
||||
let name := ctor.getIdAt 1;
|
||||
let declName := structDeclName ++ name;
|
||||
declName ← applyVisibility ctor ctorModifiers.visibility declName;
|
||||
declName ← applyVisibility ctorModifiers.visibility declName;
|
||||
pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }
|
||||
|
||||
def checkValidFieldModifier (ref : Syntax) (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
|
||||
when modifiers.isNoncomputable $
|
||||
throwError ref "invalid use of 'noncomputable' in field declaration";
|
||||
throwError "invalid use of 'noncomputable' in field declaration";
|
||||
when modifiers.isPartial $
|
||||
throwError ref "invalid use of 'partial' in field declaration";
|
||||
throwError "invalid use of 'partial' in field declaration";
|
||||
when modifiers.isUnsafe $
|
||||
throwError ref "invalid use of 'unsafe' in field declaration";
|
||||
throwError "invalid use of 'unsafe' in field declaration";
|
||||
when (modifiers.attrs.size != 0) $
|
||||
throwError ref "invalid use of attributes in field declaration";
|
||||
throwError "invalid use of attributes in field declaration";
|
||||
when modifiers.isPrivate $
|
||||
throwError ref "private fields are not supported yet";
|
||||
throwError "private fields are not supported yet";
|
||||
pure ()
|
||||
|
||||
/-
|
||||
|
|
@ -138,19 +139,19 @@ def structFields := parser! many (structExplicitBinder <|> structImplici
|
|||
private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
|
||||
let fieldBinders := ((structStx.getArg 7).getArg 0).getArgs;
|
||||
fieldBinders.foldlM
|
||||
(fun (views : Array StructFieldView) fieldBinder => do
|
||||
(fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
|
||||
let k := fieldBinder.getKind;
|
||||
binfo ←
|
||||
if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
|
||||
else if k == `Lean.Parser.Command.structImplicitBinder then pure BinderInfo.implicit
|
||||
else if k == `Lean.Parser.Command.structInstBinder then pure BinderInfo.instImplicit
|
||||
else throwError fieldBinder "unexpected kind of structure field";
|
||||
else throwError "unexpected kind of structure field";
|
||||
fieldModifiers ← elabModifiers (fieldBinder.getArg 0);
|
||||
checkValidFieldModifier fieldBinder fieldModifiers;
|
||||
checkValidFieldModifier fieldModifiers;
|
||||
when (fieldModifiers.isPrivate && structModifiers.isPrivate) $
|
||||
throwError fieldBinder "invalid 'private' field in a 'private' structure";
|
||||
throwError "invalid 'private' field in a 'private' structure";
|
||||
when (fieldModifiers.isProtected && structModifiers.isPrivate) $
|
||||
throwError fieldBinder "invalid 'protected' field in a 'private' structure";
|
||||
throwError "invalid 'protected' field in a 'private' structure";
|
||||
let inferMod := !(fieldBinder.getArg 3).isNone;
|
||||
let (binders, type?) :=
|
||||
if binfo == BinderInfo.default then
|
||||
|
|
@ -168,12 +169,12 @@ fieldBinders.foldlM
|
|||
some $ (optBinderDefault.getArg 0).getArg 1;
|
||||
let idents := (fieldBinder.getArg 2).getArgs;
|
||||
idents.foldlM
|
||||
(fun (views : Array StructFieldView) ident => do
|
||||
(fun (views : Array StructFieldView) ident => withRef ident do
|
||||
let name := ident.getId;
|
||||
when (isInternalSubobjectFieldName name) $
|
||||
throwError ident ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
|
||||
throwError ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
|
||||
let declName := structDeclName ++ name;
|
||||
declName ← applyVisibility ident fieldModifiers.visibility declName;
|
||||
declName ← applyVisibility fieldModifiers.visibility declName;
|
||||
pure $ views.push {
|
||||
ref := ident,
|
||||
modifiers := fieldModifiers,
|
||||
|
|
@ -465,11 +466,11 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
|
|||
@[extern "lean_mk_projections"]
|
||||
private constant mkProjections (env : Environment) (structName : @& Name) (projs : @& List ProjectionInfo) (isClass : Bool) : Except String Environment := arbitrary _
|
||||
|
||||
private def addProjections (ref : Syntax) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : CommandElabM Unit := do
|
||||
private def addProjections (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : CommandElabM Unit := do
|
||||
env ← getEnv;
|
||||
match mkProjections env structName projs isClass with
|
||||
| Except.ok env => setEnv env
|
||||
| Except.error msg => throwError ref msg
|
||||
| Except.error msg => throwError msg
|
||||
|
||||
private def mkAuxConstructions (declName : Name) : CommandElabM Unit := do
|
||||
env ← getEnv;
|
||||
|
|
@ -480,7 +481,7 @@ modifyEnv fun env => mkRecOn env declName;
|
|||
when hasUnit $ modifyEnv fun env => mkCasesOn env declName;
|
||||
when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env declName
|
||||
|
||||
private def addDefaults (ref : Syntax) (mctx : MetavarContext) (lctx : LocalContext) (localInsts : LocalInstances)
|
||||
private def addDefaults (mctx : MetavarContext) (lctx : LocalContext) (localInsts : LocalInstances)
|
||||
(defaultAuxDecls : Array (Name × Expr × Expr)) : CommandElabM Unit :=
|
||||
liftTermElabM none $ Term.withLocalContext lctx localInsts do
|
||||
Term.setMCtx mctx;
|
||||
|
|
@ -505,7 +506,7 @@ def structCtor := parser! try (declModifiers >> ident >> optional infe
|
|||
|
||||
-/
|
||||
def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
|
||||
checkValidInductiveModifier stx modifiers;
|
||||
checkValidInductiveModifier modifiers;
|
||||
let isClass := (stx.getArg 0).getKind == `Lean.Parser.Command.classTk;
|
||||
let modifiers := if isClass then modifiers.addAttribute { name := `class } else modifiers;
|
||||
let declId := stx.getArg 1;
|
||||
|
|
@ -516,7 +517,7 @@ let optType := stx.getArg 4;
|
|||
type ← if optType.isNone then `(Type _) else pure $ (optType.getArg 0).getArg 1;
|
||||
scopeLevelNames ← getLevelNames;
|
||||
withDeclId declId $ fun name => do
|
||||
declName ← mkDeclName declId modifiers name;
|
||||
declName ← mkDeclName modifiers name;
|
||||
allUserLevelNames ← getLevelNames;
|
||||
ctor ← expandCtor stx modifiers declName;
|
||||
fields ← expandFields stx modifiers declName;
|
||||
|
|
@ -536,11 +537,11 @@ withDeclId declId $ fun name => do
|
|||
};
|
||||
let ref := declId;
|
||||
addDecl r.decl;
|
||||
addProjections ref declName r.projInfos isClass;
|
||||
addProjections declName r.projInfos isClass;
|
||||
mkAuxConstructions declName;
|
||||
applyAttributes ref declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
r.projInstances.forM $ addInstance ref;
|
||||
addDefaults ref r.mctx r.lctx r.localInsts r.defaultAuxDecls;
|
||||
applyAttributes declName modifiers.attrs AttributeApplicationTime.afterTypeChecking;
|
||||
r.projInstances.forM addInstance;
|
||||
addDefaults r.mctx r.lctx r.localInsts r.defaultAuxDecls;
|
||||
pure ()
|
||||
|
||||
end Command
|
||||
|
|
|
|||
|
|
@ -189,7 +189,7 @@ fun stx => do
|
|||
let catName := stx.getIdAt 1;
|
||||
let attrName := catName.appendAfter "Parser";
|
||||
env ← getEnv;
|
||||
env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
|
||||
env ← liftIO $ Parser.registerParserCategory env attrName catName;
|
||||
setEnv env;
|
||||
declareSyntaxCatQuotParser catName
|
||||
|
||||
|
|
@ -222,7 +222,7 @@ def «syntax» := parser! "syntax " >> optPrecedence >> optKind >> many1 sy
|
|||
fun stx => do
|
||||
env ← getEnv;
|
||||
let cat := (stx.getIdAt 5).eraseMacroScopes;
|
||||
unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 5) ("unknown category '" ++ cat ++ "'");
|
||||
unless (Parser.isParserCategory env cat) $ throwErrorAt (stx.getArg 5) ("unknown category '" ++ cat ++ "'");
|
||||
let prec := (Term.expandOptPrecedence (stx.getArg 1)).getD Parser.maxPrec;
|
||||
kind ← elabKind (stx.getArg 2) cat;
|
||||
let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
|
||||
|
|
@ -232,7 +232,7 @@ fun stx => do
|
|||
`(@[$catParserId:ident] def myParser : Lean.TrailingParserDescr := ParserDescr.trailingNode $(quote kind) $(quote prec) $val)
|
||||
else
|
||||
`(@[$catParserId:ident] def myParser : Lean.ParserDescr := ParserDescr.node $(quote kind) $(quote prec) $val);
|
||||
trace `Elab stx $ fun _ => d;
|
||||
trace `Elab fun _ => d;
|
||||
withMacroExpansion stx d $ elabCommand d
|
||||
|
||||
/-
|
||||
|
|
@ -256,13 +256,13 @@ alts ← alts.mapSepElemsM $ fun alt => do {
|
|||
pure alt
|
||||
else if k' == choiceKind then do
|
||||
match quot.getArgs.find? $ fun quotAlt => quotAlt.getKind == k with
|
||||
| none => throwError alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
|
||||
| none => throwErrorAt alt ("invalid macro_rules alternative, expected syntax node kind '" ++ k ++ "'")
|
||||
| some quot => do
|
||||
pat ← `(`($quot));
|
||||
let lhs := lhs.setArg 0 pat;
|
||||
pure $ alt.setArg 0 lhs
|
||||
else
|
||||
throwError alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
|
||||
throwErrorAt alt ("invalid macro_rules alternative, unexpected syntax node kind '" ++ k' ++ "'")
|
||||
| stx => throwUnsupportedSyntax
|
||||
};
|
||||
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
|
||||
|
|
@ -275,7 +275,7 @@ match_syntax (alt.getArg 0).getArg 0 with
|
|||
def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
k ← inferMacroRulesAltKind (alts.get! 0);
|
||||
if k == choiceKind then
|
||||
throwError (alts.get! 0)
|
||||
throwErrorAt (alts.get! 0)
|
||||
"invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
|
||||
else do
|
||||
altsK ← alts.filterSepElemsM (fun alt => do k' ← inferMacroRulesAltKind alt; pure $ k == k');
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ when val.hasExprMVar $ throwError ("tactic failed, result still contain metavari
|
|||
def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
|
||||
modify $ fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId };
|
||||
remainingGoals ← liftTacticElabM mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
|
||||
ref ← getCurrRef;
|
||||
ref ← getRef;
|
||||
let tailRef := ref.getTailWithPos.getD ref;
|
||||
withRef tailRef do
|
||||
unless remainingGoals.isEmpty (reportUnsolvedGoals remainingGoals);
|
||||
|
|
@ -157,8 +157,7 @@ s.syntheticMVars.forM $ fun mvarSyntheticDecl =>
|
|||
| SyntheticMVarKind.typeClass =>
|
||||
withMVarContext mvarSyntheticDecl.mvarId $ do
|
||||
mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId;
|
||||
logError mvarSyntheticDecl.ref $
|
||||
"failed to create type class instance for " ++ indentExpr mvarDecl.type
|
||||
logError $ "failed to create type class instance for " ++ indentExpr mvarDecl.type
|
||||
| SyntheticMVarKind.coe expectedType eType e f? =>
|
||||
withMVarContext mvarSyntheticDecl.mvarId $ do
|
||||
mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId;
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
|
|||
MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
|
||||
|
||||
def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
|
||||
ref ← Term.getCurrRef;
|
||||
ref ← getRef;
|
||||
let tailRef := ref.getTailWithPos.getD ref;
|
||||
Term.throwErrorAt tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
|
||||
|
||||
|
|
@ -63,7 +63,7 @@ fun ctx s => match x ctx.toTermCtx s.toTermState with
|
|||
def liftMetaM {α} (x : MetaM α) : TacticM α := liftTermElabM $ Term.liftMetaM x
|
||||
|
||||
@[inline] def withRef {α} (ref : Syntax) (x : TacticM α) : TacticM α := do
|
||||
adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x
|
||||
adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
|
||||
|
||||
def getEnv : TacticM Environment := do s ← get; pure s.env
|
||||
def getMCtx : TacticM MetavarContext := do s ← get; pure s.mctx
|
||||
|
|
@ -91,7 +91,7 @@ let s := Lean.collectMVars {} e;
|
|||
pure s.result.toList
|
||||
|
||||
instance monadLog : MonadLog TacticM :=
|
||||
{ getCmdPos := do ctx ← read; pure ctx.cmdPos,
|
||||
{ getRef := do ctx ← read; pure ctx.ref,
|
||||
getFileMap := do ctx ← read; pure ctx.fileMap,
|
||||
getFileName := do ctx ← read; pure ctx.fileName,
|
||||
addContext := addContext,
|
||||
|
|
@ -127,7 +127,7 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
|
|||
mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"
|
||||
@[init mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic := arbitrary _
|
||||
|
||||
def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : TacticM Unit := liftTermElabM $ Term.logTrace cls ref msg
|
||||
def logTrace (cls : Name) (msg : MessageData) : TacticM Unit := liftTermElabM $ Term.logTrace cls msg
|
||||
@[inline] def trace (cls : Name) (msg : Unit → MessageData) : TacticM Unit := liftTermElabM $ Term.trace cls msg
|
||||
@[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TacticM Unit := liftTermElabM $ Term.traceAtCmdPos cls msg
|
||||
def dbgTrace {α} [HasToString α] (a : α) : TacticM Unit :=_root_.dbgTrace (toString a) $ fun _ => pure ()
|
||||
|
|
@ -316,7 +316,7 @@ fun stx =>
|
|||
@[builtinTactic traceState] def evalTraceState : Tactic :=
|
||||
fun stx => do
|
||||
gs ← getUnsolvedGoals;
|
||||
logInfo stx (goalsToMessageData gs)
|
||||
logInfo (goalsToMessageData gs)
|
||||
|
||||
@[builtinTactic «assumption»] def evalAssumption : Tactic :=
|
||||
fun stx => liftMetaTactic $ fun mvarId => do Meta.assumption mvarId; pure []
|
||||
|
|
|
|||
|
|
@ -23,7 +23,6 @@ namespace Term
|
|||
structure Context extends Meta.Context :=
|
||||
(fileName : String)
|
||||
(fileMap : FileMap)
|
||||
(cmdPos : String.Pos)
|
||||
(currNamespace : Name)
|
||||
(declName? : Option Name := none)
|
||||
(levelNames : List Name := [])
|
||||
|
|
@ -140,7 +139,7 @@ env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
|
|||
pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)
|
||||
|
||||
instance monadLog : MonadLog TermElabM :=
|
||||
{ getCmdPos := do ctx ← read; pure ctx.cmdPos,
|
||||
{ getRef := do ctx ← read; pure ctx.ref,
|
||||
getFileMap := do ctx ← read; pure ctx.fileMap,
|
||||
getFileName := do ctx ← read; pure ctx.fileName,
|
||||
addContext := addContext,
|
||||
|
|
@ -148,24 +147,20 @@ instance monadLog : MonadLog TermElabM :=
|
|||
|
||||
/- Execute `x` using using `ref` as the default Syntax for providing position information to error messages. -/
|
||||
@[inline] def withRef {α} (ref : Syntax) (x : TermElabM α) : TermElabM α := do
|
||||
adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x
|
||||
adaptReader (fun (ctx : Context) => { ctx with ref := replaceRef ref ctx.ref }) x
|
||||
|
||||
def getCurrRef : TermElabM Syntax := do
|
||||
ctx ← read; pure ctx.ref
|
||||
|
||||
/--
|
||||
Throws an error with the given `msgData` and extracting position information from `ref`.
|
||||
If `ref` does not contain position information, then use `cmdPos` -/
|
||||
def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : TermElabM α := do
|
||||
/-- Throws an error with the given `msgData` and extracting position information from `ctx.ref`. -/
|
||||
def throwError {α} (msgData : MessageData) : TermElabM α := do
|
||||
ctx ← read;
|
||||
ref ← getRef;
|
||||
let ref := getBetterRef ref ctx.macroStack;
|
||||
let msgData := if ctx.macroStackAtErr then addMacroStack msgData ctx.macroStack else msgData;
|
||||
msg ← mkMessage msgData MessageSeverity.error ref;
|
||||
throw (Exception.ex (Elab.Exception.error msg))
|
||||
withRef ref do
|
||||
msg ← mkMessage msgData MessageSeverity.error;
|
||||
throw (Exception.ex (Elab.Exception.error msg))
|
||||
|
||||
def throwError {α} (msgData : MessageData) : TermElabM α := do
|
||||
ref ← getCurrRef;
|
||||
throwErrorAt ref msgData
|
||||
def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : TermElabM α :=
|
||||
withRef ref $ throwError msgData
|
||||
|
||||
def throwUnsupportedSyntax {α} : TermElabM α :=
|
||||
throw (Exception.ex Elab.Exception.unsupportedSyntax)
|
||||
|
|
@ -216,17 +211,16 @@ def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do mctx ← getMCtx
|
|||
def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
|
||||
def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modify $ fun s => { s with mctx := s.mctx.assignLevel mvarId val }
|
||||
|
||||
def logTrace (cls : Name) (ref : Syntax) (msg : MessageData) : TermElabM Unit := do
|
||||
def logTrace (cls : Name) (msg : MessageData) : TermElabM Unit := do
|
||||
ctx ← read;
|
||||
s ← get;
|
||||
logInfo ref $
|
||||
logInfo $
|
||||
MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } $
|
||||
MessageData.tagged cls msg
|
||||
|
||||
@[inline] def trace (cls : Name) (msg : Unit → MessageData) : TermElabM Unit := do
|
||||
opts ← getOptions;
|
||||
ref ← getCurrRef;
|
||||
when (checkTraceOption opts cls) $ logTrace cls ref (msg ())
|
||||
when (checkTraceOption opts cls) $ logTrace cls (msg ())
|
||||
|
||||
def logDbgTrace (msg : MessageData) : TermElabM Unit := do
|
||||
trace `Elab.debug $ fun _ => msg
|
||||
|
|
@ -245,7 +239,8 @@ _root_.dbgTrace (toString a) $ fun _ => pure ()
|
|||
|
||||
/-- Auxiliary function for `liftMetaM` -/
|
||||
private def mkMessageAux (ctx : Context) (msgData : MessageData) (severity : MessageSeverity) : Message :=
|
||||
mkMessageCore ctx.fileName ctx.fileMap msgData severity (ctx.ref.getPos.getD ctx.cmdPos)
|
||||
let pos := ctx.ref.getPos.getD 0;
|
||||
mkMessageCore ctx.fileName ctx.fileMap msgData severity pos
|
||||
|
||||
/-- Auxiliary function for `liftMetaM` -/
|
||||
private def fromMetaException (ctx : Context) (ex : Meta.Exception) : Exception :=
|
||||
|
|
@ -328,7 +323,7 @@ finally x (modify $ fun s => { s with mctx := mctx })
|
|||
|
||||
def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
|
||||
fun ctx s =>
|
||||
let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap, cmdPos := ctx.cmdPos, levelNames := ctx.levelNames };
|
||||
let lvlCtx : Level.Context := { fileName := ctx.fileName, fileMap := ctx.fileMap, ref := ctx.ref, levelNames := ctx.levelNames };
|
||||
match (x lvlCtx).run { ngen := s.ngen, mctx := s.mctx } with
|
||||
| EStateM.Result.ok a newS => EStateM.Result.ok a { s with mctx := newS.mctx, ngen := newS.ngen }
|
||||
| EStateM.Result.error ex newS => EStateM.Result.error (Exception.ex ex) s
|
||||
|
|
@ -353,7 +348,7 @@ adaptReader (fun (ctx : Context) => { ctx with macroStack := { before := beforeS
|
|||
Add the given metavariable to the list of pending synthetic metavariables.
|
||||
The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/
|
||||
def registerSyntheticMVar (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
|
||||
ref ← getCurrRef;
|
||||
ref ← getRef;
|
||||
modify $ fun s => { s with syntheticMVars := { mvarId := mvarId, ref := ref, kind := kind } :: s.syntheticMVars }
|
||||
|
||||
/-
|
||||
|
|
@ -1287,7 +1282,6 @@ instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
|
|||
config := { opts := opts },
|
||||
fileName := "<TermElabM>",
|
||||
fileMap := arbitrary _,
|
||||
cmdPos := 0,
|
||||
currNamespace := Name.anonymous,
|
||||
currRecDepth := 0,
|
||||
maxRecDepth := getMaxRecDepth opts
|
||||
|
|
|
|||
|
|
@ -16,9 +16,9 @@ inductive1.lean:49:0: error: invalid mutually inductive types, binder annotation
|
|||
inductive1.lean:59:0: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes
|
||||
inductive1.lean:69:2: error: 'Boo.T1.bla' has already been declared
|
||||
inductive1.lean:73:10: error: 'Boo.T1' has already been declared
|
||||
inductive1.lean:80:8: error: invalid use of 'partial' in inductive declaration
|
||||
inductive1.lean:81:14: error: invalid use of 'noncomputable' in inductive declaration
|
||||
inductive1.lean:82:10: error: invalid use of attributes in inductive declaration
|
||||
inductive1.lean:80:0: error: invalid use of 'partial' in inductive declaration
|
||||
inductive1.lean:81:0: error: invalid use of 'noncomputable' in inductive declaration
|
||||
inductive1.lean:82:0: error: invalid use of attributes in inductive declaration
|
||||
inductive1.lean:85:0: error: invalid 'private' constructor in a 'private' inductive datatype
|
||||
inductive1.lean:93:7: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
|
||||
inductive1.lean:100:0: error: constructor resulting type must be specified in inductive family declaration
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue