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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-21 13:30:43 -07:00
parent 21132d6c63
commit 7111eb4d79
11 changed files with 963 additions and 1020 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

468
src/Lean/Attributes.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -11,187 +12,170 @@ import Lean.ResolveName
namespace Lean
inductive AttributeApplicationTime
| afterTypeChecking | afterCompilation | beforeElaboration
| afterTypeChecking | afterCompilation | beforeElaboration
def AttributeApplicationTime.beq : AttributeApplicationTime → AttributeApplicationTime → Bool
| AttributeApplicationTime.afterTypeChecking, AttributeApplicationTime.afterTypeChecking => true
| AttributeApplicationTime.afterCompilation, AttributeApplicationTime.afterCompilation => true
| AttributeApplicationTime.beforeElaboration, AttributeApplicationTime.beforeElaboration => true
| _, _ => false
| AttributeApplicationTime.afterTypeChecking, AttributeApplicationTime.afterTypeChecking => true
| AttributeApplicationTime.afterCompilation, AttributeApplicationTime.afterCompilation => true
| AttributeApplicationTime.beforeElaboration, AttributeApplicationTime.beforeElaboration => true
| _, _ => false
instance AttributeApplicationTime.hasBeq : HasBeq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩
structure Attr.Context :=
(currNamespace : Name)
(openDecls : List OpenDecl)
(currNamespace : Name)
(openDecls : List OpenDecl)
abbrev AttrM := ReaderT Attr.Context CoreM
instance attrResolveName : MonadResolveName AttrM :=
{ getCurrNamespace := do ctx ← read; pure ctx.currNamespace,
getOpenDecls := do ctx ← read; pure ctx.openDecls }
instance attrResolveName : MonadResolveName AttrM := {
getCurrNamespace := do pure (← read).currNamespace,
getOpenDecls := do pure (← read).openDecls
}
-- TODO: after we delete the old frontend, we should use `EIO` with a richer exception kind at AttributeImpl.
-- We must perform a similar modification at `PersistentEnvExtension`
structure AttributeImpl :=
(name : Name)
(descr : String)
(add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit)
/-
(addScoped (env : Environment) (decl : Name) (args : Syntax) : IO Environment
:= throw (IO.userError ("attribute '" ++ toString name ++ "' does not support scopes")))
(erase (env : Environment) (decl : Name) (persistent : Bool) : IO Environment
:= throw (IO.userError ("attribute '" ++ toString name ++ "' does not support removal")))
(activateScoped (env : Environment) (scope : Name) : IO Environment := pure env)
(pushScope (env : Environment) : IO Environment := pure env)
(popScope (env : Environment) : IO Environment := pure env)
-/
(applicationTime := AttributeApplicationTime.afterTypeChecking)
(name : Name)
(descr : String)
(add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit)
(applicationTime : AttributeApplicationTime := AttributeApplicationTime.afterTypeChecking)
instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
instance : Inhabited AttributeImpl :=
⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
open Std (PersistentHashMap)
def mkAttributeMapRef : IO (IO.Ref (PersistentHashMap Name AttributeImpl)) :=
IO.mkRef {}
@[builtinInit mkAttributeMapRef]
constant attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) := arbitrary _
builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) ← IO.mkRef {}
/- Low level attribute registration function. -/
def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
m ← attributeMapRef.get;
when (m.contains attr.name) $ throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attr.name ++ "' has already been used"));
initializing ← IO.initializing;
unless initializing $ throw (IO.userError ("failed to register attribute, attributes can only be registered during initialization"));
attributeMapRef.modify (fun m => m.insert attr.name attr)
let m ← attributeMapRef.get
if m.contains attr.name then throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attr.name ++ "' has already been used"))
unless (← IO.initializing) do throw (IO.userError "failed to register attribute, attributes can only be registered during initialization")
attributeMapRef.modify fun m => m.insert attr.name attr
abbrev AttributeImplBuilder := List DataValue → Except String AttributeImpl
abbrev AttributeImplBuilderTable := Std.HashMap Name AttributeImplBuilder
def mkAttributeImplBuilderTable : IO (IO.Ref AttributeImplBuilderTable) := IO.mkRef {}
@[builtinInit mkAttributeImplBuilderTable] constant attributeImplBuilderTableRef : IO.Ref AttributeImplBuilderTable := arbitrary _
builtin_initialize attributeImplBuilderTableRef : IO.Ref AttributeImplBuilderTable ← IO.mkRef {}
def registerAttributeImplBuilder (builderId : Name) (builder : AttributeImplBuilder) : IO Unit := do
table ← attributeImplBuilderTableRef.get;
when (table.contains builderId) $ throw (IO.userError ("attribute implementation builder '" ++ toString builderId ++ "' has already been declared"));
attributeImplBuilderTableRef.modify $ fun table => table.insert builderId builder
let table ← attributeImplBuilderTableRef.get
if table.contains builderId then throw (IO.userError ("attribute implementation builder '" ++ toString builderId ++ "' has already been declared"))
attributeImplBuilderTableRef.modify fun table => table.insert builderId builder
def mkAttributeImplOfBuilder (builderId : Name) (args : List DataValue) : IO AttributeImpl := do
table ← attributeImplBuilderTableRef.get;
match table.find? builderId with
| none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString builderId ++ "'"))
| some builder => IO.ofExcept $ builder args
let table ← attributeImplBuilderTableRef.get
match table.find? builderId with
| none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString builderId ++ "'"))
| some builder => IO.ofExcept $ builder args
inductive AttributeExtensionOLeanEntry
| decl (declName : Name) -- `declName` has type `AttributeImpl`
| builder (builderId : Name) (args : List DataValue)
| decl (declName : Name) -- `declName` has type `AttributeImpl`
| builder (builderId : Name) (args : List DataValue)
structure AttributeExtensionState :=
(newEntries : List AttributeExtensionOLeanEntry := [])
(map : PersistentHashMap Name AttributeImpl)
(newEntries : List AttributeExtensionOLeanEntry := [])
(map : PersistentHashMap Name AttributeImpl)
abbrev AttributeExtension := PersistentEnvExtension AttributeExtensionOLeanEntry (AttributeExtensionOLeanEntry × AttributeImpl) AttributeExtensionState
instance AttributeExtensionState.inhabited : Inhabited AttributeExtensionState := ⟨{ map := {} }⟩
instance : Inhabited AttributeExtensionState := ⟨{ map := {} }⟩
private def AttributeExtension.mkInitial : IO AttributeExtensionState := do
map ← attributeMapRef.get;
pure { map := map }
let map ← attributeMapRef.get
pure { map := map }
unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl :=
match env.find? declName with
| none => throw ("unknow constant '" ++ toString declName ++ "'")
| some info =>
match info.type with
| Expr.const `Lean.AttributeImpl _ _ => env.evalConst AttributeImpl opts declName
| _ => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected")
match env.find? declName with
| none => throw ("unknow constant '" ++ toString declName ++ "'")
| some info =>
match info.type with
| Expr.const `Lean.AttributeImpl _ _ => env.evalConst AttributeImpl opts declName
| _ => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected")
@[implementedBy mkAttributeImplOfConstantUnsafe]
constant mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl := arbitrary _
constant mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl
def mkAttributeImplOfEntry (env : Environment) (opts : Options) (e : AttributeExtensionOLeanEntry) : IO AttributeImpl :=
match e with
| AttributeExtensionOLeanEntry.decl declName => IO.ofExcept $ mkAttributeImplOfConstant env opts declName
| AttributeExtensionOLeanEntry.builder builderId args => mkAttributeImplOfBuilder builderId args
match e with
| AttributeExtensionOLeanEntry.decl declName => IO.ofExcept $ mkAttributeImplOfConstant env opts declName
| AttributeExtensionOLeanEntry.builder builderId args => mkAttributeImplOfBuilder builderId args
private def AttributeExtension.addImported (es : Array (Array AttributeExtensionOLeanEntry)) : ImportM AttributeExtensionState := do
ctx ← read;
map ← attributeMapRef.get;
map ← es.foldlM
(fun map entries =>
entries.foldlM
(fun (map : PersistentHashMap Name AttributeImpl) entry => do
attrImpl ← liftM $ mkAttributeImplOfEntry ctx.env ctx.opts entry;
pure $ map.insert attrImpl.name attrImpl)
map)
map;
pure { map := map }
let ctx ← read
let map ← attributeMapRef.get
let map ← es.foldlM
(fun map entries =>
entries.foldlM
(fun (map : PersistentHashMap Name AttributeImpl) entry => do
let attrImpl ← liftM $ mkAttributeImplOfEntry ctx.env ctx.opts entry
pure $ map.insert attrImpl.name attrImpl)
map)
map
pure { map := map }
private def AttributeExtension.addEntry (s : AttributeExtensionState) (e : AttributeExtensionOLeanEntry × AttributeImpl) : AttributeExtensionState :=
{ s with map := s.map.insert e.2.name e.2, newEntries := e.1 :: s.newEntries }
private def addAttrEntry (s : AttributeExtensionState) (e : AttributeExtensionOLeanEntry × AttributeImpl) : AttributeExtensionState :=
{ s with map := s.map.insert e.2.name e.2, newEntries := e.1 :: s.newEntries }
def mkAttributeExtension : IO AttributeExtension :=
registerPersistentEnvExtension {
name := `attrExt,
mkInitial := AttributeExtension.mkInitial,
addImportedFn := AttributeExtension.addImported,
addEntryFn := AttributeExtension.addEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => format "number of local entries: " ++ format s.newEntries.length
}
@[builtinInit mkAttributeExtension]
def attributeExtension : AttributeExtension := arbitrary _
builtin_initialize attributeExtension : AttributeExtension ←
registerPersistentEnvExtension {
name := `attrExt,
mkInitial := AttributeExtension.mkInitial,
addImportedFn := AttributeExtension.addImported,
addEntryFn := addAttrEntry,
exportEntriesFn := fun s => s.newEntries.reverse.toArray,
statsFn := fun s => format "number of local entries: " ++ format s.newEntries.length
}
/- Return true iff `n` is the name of a registered attribute. -/
@[export lean_is_attribute]
def isBuiltinAttribute (n : Name) : IO Bool := do
m ← attributeMapRef.get; pure (m.contains n)
let m ← attributeMapRef.get; pure (m.contains n)
/- Return the name of all registered attributes. -/
def getBuiltinAttributeNames : IO (List Name) := do
m ← attributeMapRef.get; pure $ m.foldl (fun r n _ => n::r) []
let m ← attributeMapRef.get; pure $ m.foldl (fun r n _ => n::r) []
def getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl := do
m ← attributeMapRef.get;
match m.find? attrName with
| some attr => pure attr
| none => throw (IO.userError ("unknown attribute '" ++ toString attrName ++ "'"))
let m ← attributeMapRef.get
match m.find? attrName with
| some attr => pure attr
| none => throw (IO.userError ("unknown attribute '" ++ toString attrName ++ "'"))
@[export lean_attribute_application_time]
def getBuiltinAttributeApplicationTime (n : Name) : IO AttributeApplicationTime := do
attr ← getBuiltinAttributeImpl n;
pure attr.applicationTime
let attr ← getBuiltinAttributeImpl n
pure attr.applicationTime
def isAttribute (env : Environment) (attrName : Name) : Bool :=
(attributeExtension.getState env).map.contains attrName
(attributeExtension.getState env).map.contains attrName
def getAttributeNames (env : Environment) : List Name :=
let m := (attributeExtension.getState env).map;
m.foldl (fun r n _ => n::r) []
let m := (attributeExtension.getState env).map
m.foldl (fun r n _ => n::r) []
def getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl :=
let m := (attributeExtension.getState env).map;
match m.find? attrName with
| some attr => pure attr
| none => throw ("unknown attribute '" ++ toString attrName ++ "'")
let m := (attributeExtension.getState env).map
match m.find? attrName with
| some attr => pure attr
| none => throw ("unknown attribute '" ++ toString attrName ++ "'")
def registerAttributeOfDecl (env : Environment) (opts : Options) (attrDeclName : Name) : Except String Environment := do
attrImpl ← mkAttributeImplOfConstant env opts attrDeclName;
if isAttribute env attrImpl.name then
throw ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used")
else
pure $ attributeExtension.addEntry env (AttributeExtensionOLeanEntry.decl attrDeclName, attrImpl)
let attrImpl ← mkAttributeImplOfConstant env opts attrDeclName
if isAttribute env attrImpl.name then
throw ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used")
else
pure $ attributeExtension.addEntry env (AttributeExtensionOLeanEntry.decl attrDeclName, attrImpl)
def registerAttributeOfBuilder (env : Environment) (builderId : Name) (args : List DataValue) : IO Environment := do
attrImpl ← mkAttributeImplOfBuilder builderId args;
if isAttribute env attrImpl.name then
throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used"))
else
pure $ attributeExtension.addEntry env (AttributeExtensionOLeanEntry.builder builderId args, attrImpl)
let attrImpl ← mkAttributeImplOfBuilder builderId args
if isAttribute env attrImpl.name then
throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attrImpl.name ++ "' has already been used"))
else
pure $ attributeExtension.addEntry env (AttributeExtensionOLeanEntry.builder builderId args, attrImpl)
namespace Environment
@ -204,9 +188,9 @@ namespace Environment
TODO: delete after we remove old frontend. -/
@[export lean_add_attribute]
def addAttributeOld (env : Environment) (decl : Name) (attrName : Name) (args : Syntax := Syntax.missing) (persistent := true) : IO Environment := do
attr ← IO.ofExcept $ getAttributeImpl env attrName;
(_, s) ← ((attr.add decl args persistent).run { currNamespace := Name.anonymous, openDecls := [] }).toIO {} { env := env };
pure s.env
let attr ← IO.ofExcept $ getAttributeImpl env attrName
let (_, s) ← ((attr.add decl args persistent).run { currNamespace := Name.anonymous, openDecls := [] }).toIO {} { env := env }
pure s.env
/-
/- Add a scoped attribute `attr` to declaration `decl` with arguments `args` and scope `decl.getPrefix`.
@ -250,25 +234,25 @@ attrs.foldlM (fun env attr => attr.activateScoped env scope) env
It activates scoped attributes in the new resulting namespace. -/
@[export lean_push_scope]
def pushScope (env : Environment) (header : Name) (isNamespace : Bool) : IO Environment := do
let env := Lean.TODELETE.pushScopeCore env header isNamespace;
-- attrs ← attributeArrayRef.get;
-- attrs.foldlM (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env
pure env
let env := Lean.TODELETE.pushScopeCore env header isNamespace
-- attrs ← attributeArrayRef.get;
-- attrs.foldlM (fun env attr => do env ← attr.pushScope env; if isNamespace then attr.activateScoped env ns else pure env) env
pure env
/- We use this function to implement commands `end foo` for closing namespaces and sections. -/
@[export lean_pop_scope]
def popScope (env : Environment) : IO Environment := do
let env := Lean.TODELETE.popScopeCore env;
-- attrs ← attributeArrayRef.get;
-- attrs.foldlM (fun env attr => attr.popScope env) env
pure env
let env := Lean.TODELETE.popScopeCore env
-- attrs ← attributeArrayRef.get;
-- attrs.foldlM (fun env attr => attr.popScope env) env
pure env
end Environment
def addAttribute (decl : Name) (attrName : Name) (args : Syntax) (persistent : Bool := true) : AttrM Unit := do
env ← getEnv;
attr ← ofExcept $ getAttributeImpl env attrName;
attr.add decl args persistent
let env ← getEnv
let attr ← ofExcept $ getAttributeImpl env attrName
attr.add decl args persistent
/--
@ -280,44 +264,44 @@ attr.add decl args persistent
They provide the predicate `tagAttr.hasTag env decl` which returns true iff declaration `decl`
is tagged in the environment `env`. -/
structure TagAttribute :=
(attr : AttributeImpl)
(ext : PersistentEnvExtension Name Name NameSet)
(attr : AttributeImpl)
(ext : PersistentEnvExtension Name Name NameSet)
def registerTagAttribute (name : Name) (descr : String) (validate : Name → AttrM Unit := fun _ => pure ()) : IO TagAttribute := do
ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
name := name,
mkInitial := pure {},
addImportedFn := fun _ _ => pure {},
addEntryFn := fun (s : NameSet) n => s.insert n,
exportEntriesFn := fun es =>
let r : Array Name := es.fold (fun a e => a.push e) #[];
r.qsort Name.quickLt,
statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
};
let attrImpl : AttributeImpl := {
name := name,
descr := descr,
add := fun decl args persistent => do
when args.hasArgs $ throwError ("invalid attribute '" ++ toString name ++ "', unexpected argument");
unless persistent $ throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
env ← getEnv;
unless (env.getModuleIdxFor? decl).isNone $
throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
validate decl;
env ← getEnv;
setEnv $ ext.addEntry env decl
};
registerBuiltinAttribute attrImpl;
pure { attr := attrImpl, ext := ext }
let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
name := name,
mkInitial := pure {},
addImportedFn := fun _ _ => pure {},
addEntryFn := fun (s : NameSet) n => s.insert n,
exportEntriesFn := fun es =>
let r : Array Name := es.fold (fun a e => a.push e) #[]
r.qsort Name.quickLt,
statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
}
let attrImpl : AttributeImpl := {
name := name,
descr := descr,
add := fun decl args persistent => do
if args.hasArgs then throwError! "invalid attribute '{name}', unexpected argument"
unless persistent do throwError! "invalid attribute '{name}', must be persistent"
let env ← getEnv
unless (env.getModuleIdxFor? decl).isNone do
throwError! "invalid attribute '{name}', declaration is in an imported module"
validate decl
let env ← getEnv
setEnv $ ext.addEntry env decl
}
registerBuiltinAttribute attrImpl
pure { attr := attrImpl, ext := ext }
namespace TagAttribute
instance : Inhabited TagAttribute := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
match env.getModuleIdxFor? decl with
| some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
| none => (attr.ext.getState env).contains decl
match env.getModuleIdxFor? decl with
| some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
| none => (attr.ext.getState env).contains decl
end TagAttribute
@ -328,60 +312,60 @@ end TagAttribute
They provide the function `pAttr.getParam env decl` which returns `some p` iff declaration `decl`
contains the attribute `pAttr` with parameter `p`. -/
structure ParametricAttribute (α : Type) :=
(attr : AttributeImpl)
(ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
(attr : AttributeImpl)
(ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String)
(getParam : Name → Syntax → AttrM α)
(afterSet : Name → α → AttrM Unit := fun env _ _ => pure ())
(appTime := AttributeApplicationTime.afterTypeChecking)
: IO (ParametricAttribute α) := do
ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
name := name,
mkInitial := pure {},
addImportedFn := fun _ _ => pure {},
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
exportEntriesFn := fun m =>
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[];
r.qsort (fun a b => Name.quickLt a.1 b.1),
statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
};
let attrImpl : AttributeImpl := {
name := name,
descr := descr,
applicationTime := appTime,
add := fun decl args persistent => do
unless persistent $ throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
env ← getEnv;
unless (env.getModuleIdxFor? decl).isNone $
throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
val ← getParam decl args;
let env' := ext.addEntry env (decl, val);
setEnv env';
catch (afterSet decl val) (fun _ => setEnv env)
};
registerBuiltinAttribute attrImpl;
pure { attr := attrImpl, ext := ext }
let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
name := name,
mkInitial := pure {},
addImportedFn := fun _ _ => pure {},
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
exportEntriesFn := fun m =>
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[]
r.qsort (fun a b => Name.quickLt a.1 b.1),
statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
}
let attrImpl : AttributeImpl := {
name := name,
descr := descr,
applicationTime := appTime,
add := fun decl args persistent => do
unless persistent do throwError! "invalid attribute '{name}', must be persistent"
let env ← getEnv
unless (env.getModuleIdxFor? decl).isNone do
throwError! "invalid attribute '{name}', declaration is in an imported module"
let val ← getParam decl args
let env' := ext.addEntry env (decl, val)
setEnv env'
try afterSet decl val catch _ => setEnv env
}
registerBuiltinAttribute attrImpl
pure { attr := attrImpl, ext := ext }
namespace ParametricAttribute
instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := arbitrary _, ext := arbitrary _}⟩
def getParam {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α :=
match env.getModuleIdxFor? decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some (_, val) => some val
| none => none
| none => (attr.ext.getState env).find? decl
match env.getModuleIdxFor? decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some (_, val) => some val
| none => none
| none => (attr.ext.getState env).find? decl
def setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
if (env.getModuleIdxFor? decl).isSome then
Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, declaration is in an imported module")
else if ((attr.ext.getState env).find? decl).isSome then
Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, attribute has already been set")
else
Except.ok (attr.ext.addEntry env (decl, param))
if (env.getModuleIdxFor? decl).isSome then
Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, declaration is in an imported module")
else if ((attr.ext.getState env).find? decl).isSome then
Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, attribute has already been set")
else
Except.ok (attr.ext.addEntry env (decl, param))
end ParametricAttribute
@ -390,57 +374,57 @@ end ParametricAttribute
associating a value `a_i` with an declaration. `α` is usually an enumeration type.
Note that whenever we register an `EnumAttributes`, we create `n` attributes, but only one environment extension. -/
structure EnumAttributes (α : Type) :=
(attrs : List AttributeImpl)
(ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
(attrs : List AttributeImpl)
(ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α))
(validate : Name → α → AttrM Unit := fun _ _ => pure ())
(applicationTime := AttributeApplicationTime.afterTypeChecking) : IO (EnumAttributes α) := do
ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
name := extName,
mkInitial := pure {},
addImportedFn := fun _ _ => pure {},
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
exportEntriesFn := fun m =>
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[];
r.qsort (fun a b => Name.quickLt a.1 b.1),
statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
};
let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => {
name := name,
descr := descr,
applicationTime := applicationTime,
add := (fun decl args persistent => do
unless persistent $ throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
env ← getEnv;
unless (env.getModuleIdxFor? decl).isNone $
throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
validate decl val;
setEnv $ ext.addEntry env (decl, val))
: AttributeImpl
};
attrs.forM registerBuiltinAttribute;
pure { ext := ext, attrs := attrs }
let ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
name := extName,
mkInitial := pure {},
addImportedFn := fun _ _ => pure {},
addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2,
exportEntriesFn := fun m =>
let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[]
r.qsort (fun a b => Name.quickLt a.1 b.1),
statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
}
let attrs := attrDescrs.map fun (name, descr, val) => {
name := name,
descr := descr,
add := fun decl args persistent => do
unless persistent do throwError! "invalid attribute '{name}', must be persistent"
let env ← getEnv
unless (env.getModuleIdxFor? decl).isNone do
throwError! "invalid attribute '{name}', declaration is in an imported module"
validate decl val
setEnv $ ext.addEntry env (decl, val),
applicationTime := applicationTime
: AttributeImpl
}
attrs.forM registerBuiltinAttribute
pure { ext := ext, attrs := attrs }
namespace EnumAttributes
instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := arbitrary _}⟩
def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α :=
match env.getModuleIdxFor? decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some (_, val) => some val
| none => none
| none => (attr.ext.getState env).find? decl
match env.getModuleIdxFor? decl with
| some modIdx =>
match (attr.ext.getModuleEntries env modIdx).binSearch (decl, arbitrary _) (fun a b => Name.quickLt a.1 b.1) with
| some (_, val) => some val
| none => none
| none => (attr.ext.getState env).find? decl
def setValue {α : Type} (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment :=
if (env.getModuleIdxFor? decl).isSome then
Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, declaration is in an imported module")
else if ((attrs.ext.getState env).find? decl).isSome then
Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, attribute has already been set")
else
Except.ok (attrs.ext.addEntry env (decl, val))
if (env.getModuleIdxFor? decl).isSome then
Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, declaration is in an imported module")
else if ((attrs.ext.getState env).find? decl).isSome then
Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, attribute has already been set")
else
Except.ok (attrs.ext.addEntry env (decl, val))
end EnumAttributes
@ -451,13 +435,13 @@ end EnumAttributes
Remark: in the future, attributes should define their own parsers, and we should use `match_syntax` to
decode the Syntax object. -/
def attrParamSyntaxToIdentifier (s : Syntax) : Option Name :=
match s with
| Syntax.node k args =>
if k == nullKind && args.size == 1 then match args.get! 0 with
| Syntax.ident _ _ id _ => some id
| _ => none
else
none
| _ => none
match s with
| Syntax.node k args =>
if k == nullKind && args.size == 1 then match args.get! 0 with
| Syntax.ident _ _ id _ => some id
| _ => none
else
none
| _ => none
end Lean

118
src/Lean/CoreM.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -15,95 +16,106 @@ namespace Lean
namespace Core
structure State :=
(env : Environment)
(nextMacroScope : MacroScope := firstFrontendMacroScope + 1)
(ngen : NameGenerator := {})
(traceState : TraceState := {})
(env : Environment)
(nextMacroScope : MacroScope := firstFrontendMacroScope + 1)
(ngen : NameGenerator := {})
(traceState : TraceState := {})
instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩
instance : Inhabited State := ⟨{ env := arbitrary _ }⟩
structure Context :=
(options : Options := {})
(currRecDepth : Nat := 0)
(maxRecDepth : Nat := 1000)
(ref : Syntax := Syntax.missing)
(options : Options := {})
(currRecDepth : Nat := 0)
(maxRecDepth : Nat := 1000)
(ref : Syntax := Syntax.missing)
abbrev CoreM := ReaderT Context $ StateRefT State $ EIO Exception
instance CoreM.inhabited {α} : Inhabited (CoreM α) :=
⟨fun _ _ => throw $ arbitrary _⟩
instance {α} : Inhabited (CoreM α) := ⟨fun _ _ => throw $ arbitrary _⟩
instance : Ref CoreM :=
{ getRef := do ctx ← read; pure ctx.ref,
withRef := fun α ref x => withReader (fun ctx => { ctx with ref := ref }) x }
instance : Ref CoreM := {
getRef := do let ctx ← read; pure ctx.ref,
withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
}
instance : MonadEnv CoreM :=
{ getEnv := do s ← get; pure s.env,
modifyEnv := fun f => modify fun s => { s with env := f s.env } }
instance : MonadEnv CoreM := {
getEnv := do pure (← get).env,
modifyEnv := fun f => modify fun s => { s with env := f s.env }
}
instance : MonadOptions CoreM :=
{ getOptions := do ctx ← read; pure ctx.options }
instance : MonadOptions CoreM := {
getOptions := do pure (← read).options
}
instance : AddMessageContext CoreM :=
{ addMessageContext := addMessageContextPartial }
instance : AddMessageContext CoreM := {
addMessageContext := addMessageContextPartial
}
instance : MonadNameGenerator CoreM :=
{ getNGen := do s ← get; pure s.ngen,
instance : MonadNameGenerator CoreM := {
getNGen := do pure (← get).ngen,
setNGen := fun ngen => modify fun s => { s with ngen := ngen } }
instance : MonadRecDepth CoreM :=
{ withRecDepth := fun α d x => withReader (fun ctx => { ctx with currRecDepth := d }) x,
getRecDepth := do ctx ← read; pure ctx.currRecDepth,
getMaxRecDepth := do ctx ← read; pure ctx.maxRecDepth }
instance : MonadRecDepth CoreM := {
withRecDepth := fun d x => withReader (fun ctx => { ctx with currRecDepth := d }) x,
getRecDepth := do pure (← read).currRecDepth,
getMaxRecDepth := do pure (← read).maxRecDepth
}
@[inline] def liftIOCore {α} (x : IO α) : CoreM α := do
ref ← getRef;
liftM $ (adaptExcept (fun (err : IO.Error) => Exception.error ref (toString err)) x : EIO Exception α)
let ref ← getRef
liftM (adaptExcept (fun (err : IO.Error) => Exception.error ref (toString err)) x : EIO Exception α)
instance : MonadIO CoreM :=
{ liftIO := @liftIOCore }
instance : MonadIO CoreM := {
liftIO := @liftIOCore
}
instance : MonadTrace CoreM :=
{ getTraceState := do s ← get; pure s.traceState,
modifyTraceState := fun f => modify $ fun s => { s with traceState := f s.traceState } }
instance : MonadTrace CoreM := {
getTraceState := do pure (← get).traceState,
modifyTraceState := fun f => modify fun s => { s with traceState := f s.traceState }
}
private def mkFreshNameImp (n : Name) : CoreM Name := do
fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 });
env ← getEnv;
pure $ addMacroScope env.mainModule n fresh
let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 });
let env ← getEnv;
pure $ addMacroScope env.mainModule n fresh
def mkFreshUserName {m} [MonadLiftT CoreM m] (n : Name) : m Name :=
liftM $ mkFreshNameImp n
liftM $ mkFreshNameImp n
@[inline] def CoreM.run {α} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
(x.run ctx).run s
(x ctx).run s
@[inline] def CoreM.run' {α} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
Prod.fst <$> x.run ctx s
Prod.fst <$> x.run ctx s
@[inline] def CoreM.toIO {α} (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
e ← (x.run ctx s).toIO';
match e with
| Except.error (Exception.error _ msg) => do e ← msg.toString; throw $ IO.userError e
| Except.error (Exception.internal id) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
| Except.ok a => pure a
match (← (x.run ctx s).toIO') with
| Except.error (Exception.error _ msg) => do let e ← msg.toString; throw $ IO.userError e
| Except.error (Exception.internal id) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
| Except.ok a => pure a
instance hasEval {α} [MetaHasEval α] : MetaHasEval (CoreM α) :=
⟨fun env opts x _ => do
(a, s) ← (finally x printTraces).toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env};
MetaHasEval.eval s.env opts a true /- hideUnit -/⟩
instance {α} [MetaHasEval α] : MetaHasEval (CoreM α) := {
eval := fun env opts x _ => do
let x : CoreM α := do try x finally printTraces
let (a, s) ← x.toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env}
MetaHasEval.eval s.env opts a (hideUnit := true)
}
end Core
export Core (CoreM mkFreshUserName)
@[inline] def catchInternalId {α} {m : Type → Type} [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exception → m α) : m α :=
catch x fun ex => match ex with
@[inline] def catchInternalId {α} {m : Type → Type} [Monad m] [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exception → m α) : m α := do
try
x
catch ex => match ex with
| Exception.error _ _ => throw ex
| Exception.internal id' => if id == id' then h ex else throw ex
@[inline] def catchInternalIds {α} {m : Type → Type} [MonadExcept Exception m] (ids : List InternalExceptionId) (x : m α) (h : Exception → m α) : m α :=
catch x fun ex => match ex with
@[inline] def catchInternalIds {α} {m : Type → Type} [Monad m] [MonadExcept Exception m] (ids : List InternalExceptionId) (x : m α) (h : Exception → m α) : m α := do
try
x
catch ex => match ex with
| Exception.error _ _ => throw ex
| Exception.internal id => if ids.contains id then h ex else throw ex

2
src/Lean/Delaborator.lean
View file

@ -677,7 +677,7 @@ end Delaborator
/-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
opts ← getOptions;
opts ← MonadOptions.getOptions;
catchInternalId Delaborator.delabFailureId
(Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })
(fun _ => unreachable!)

101
src/Lean/Exception.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -11,102 +12,98 @@ namespace Lean
/- Exception type used in most Lean monads -/
inductive Exception
| error (ref : Syntax) (msg : MessageData)
| internal (id : InternalExceptionId)
| error (ref : Syntax) (msg : MessageData)
| internal (id : InternalExceptionId)
def Exception.toMessageData : Exception → MessageData
| Exception.error _ msg => msg
| Exception.internal id => id.toString
| Exception.error _ msg => msg
| Exception.internal id => id.toString
def Exception.getRef : Exception → Syntax
| Exception.error ref _ => ref
| Exception.internal _ => Syntax.missing
| Exception.error ref _ => ref
| Exception.internal _ => Syntax.missing
instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
instance : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
class Ref (m : Type → Type) :=
(getRef : m Syntax)
(withRef {α} : Syntax → m α → m α)
(getRef : m Syntax)
(withRef {α} : Syntax → m α → m α)
export Ref (getRef)
instance refTrans (m n : Type → Type) [Ref m] [MonadFunctor m m n n] [MonadLift m n] : Ref n :=
{ getRef := liftM (getRef : m _),
withRef := fun α ref x => monadMap (fun α => Ref.withRef ref : forall {α}, m α → m α) x }
instance (m n : Type → Type) [Ref m] [MonadFunctor m m n n] [MonadLift m n] : Ref n := {
getRef := liftM (getRef : m _),
withRef := fun ref x => monadMap (m := m) (Ref.withRef ref) x
}
def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
match ref.getPos with
| some _ => ref
| _ => oldRef
match ref.getPos with
| some _ => ref
| _ => oldRef
@[inline] def withRef {m : Type → Type} [Monad m] [Ref m] {α} (ref : Syntax) (x : m α) : m α := do
oldRef ← getRef;
let ref := replaceRef ref oldRef;
Ref.withRef ref x
let oldRef ← getRef
let ref := replaceRef ref oldRef
Ref.withRef ref x
/- Similar to `AddMessageContext`, but for error messages.
The default instance just uses `AddMessageContext`.
In error messages, we may want to provide additional information (e.g., macro expansion stack),
and refine the `(ref : Syntax)`. -/
class AddErrorMessageContext (m : Type → Type) :=
(add : Syntax → MessageData → m (Syntax × MessageData))
(add : Syntax → MessageData → m (Syntax × MessageData))
instance addErrorMessageContextDefault (m : Type → Type) [AddMessageContext m] [Monad m] : AddErrorMessageContext m :=
{ add := fun ref msg => do
msg ← addMessageContext msg;
pure (ref, msg) }
instance addErrorMessageContextDefault (m : Type → Type) [AddMessageContext m] [Monad m] : AddErrorMessageContext m := {
add := fun ref msg => do
msg ← addMessageContext msg
pure (ref, msg)
}
section Methods
variables {m : Type → Type} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
def throwError {α} (msg : MessageData) : m α := do
ref ← getRef;
(ref, msg) ← AddErrorMessageContext.add ref msg;
throw $ Exception.error ref msg
let ref ← getRef
let (ref, msg) ← AddErrorMessageContext.add ref msg
throw $ Exception.error ref msg
def throwUnknownConstant {α} (constName : Name) : m α :=
throwError ("unknown constant '" ++ mkConst constName ++ "'")
throwError msg!"unknown constant '{mkConst constName}'"
def throwErrorAt {α} (ref : Syntax) (msg : MessageData) : m α := do
withRef ref $ throwError msg
withRef ref $ throwError msg
def ofExcept {ε α} [HasToString ε] (x : Except ε α) : m α :=
match x with
| Except.ok a => pure a
| Except.error e => throwError $ toString e
match x with
| Except.ok a => pure a
| Except.error e => throwError $ toString e
def throwKernelException {α} [MonadOptions m] (ex : KernelException) : m α := do
opts ← getOptions;
throwError $ ex.toMessageData opts
throwError $ ex.toMessageData (← getOptions)
end Methods
class MonadRecDepth (m : Type → Type) :=
(withRecDepth {α} : Nat → m α → m α)
(getRecDepth : m Nat)
(getMaxRecDepth : m Nat)
(withRecDepth {α} : Nat → m α → m α)
(getRecDepth : m Nat)
(getMaxRecDepth : m Nat)
instance ReaderT.MonadRecDepth {ρ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) :=
{ withRecDepth := fun α d x ctx => MonadRecDepth.withRecDepth d (x ctx),
getRecDepth := fun _ => MonadRecDepth.getRecDepth,
getMaxRecDepth := fun _ => MonadRecDepth.getMaxRecDepth }
instance {ρ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) := {
withRecDepth := fun d x ctx => MonadRecDepth.withRecDepth d (x ctx),
getRecDepth := fun _ => MonadRecDepth.getRecDepth,
getMaxRecDepth := fun _ => MonadRecDepth.getMaxRecDepth
}
instance StateRefT.monadRecDepth {ω σ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
inferInstanceAs (MonadRecDepth (ReaderT _ _))
instance {ω σ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
inferInstanceAs (MonadRecDepth (ReaderT _ _))
@[inline] def withIncRecDepth {α m} [Monad m] [MonadRecDepth m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
(x : m α) : m α := do
curr ← MonadRecDepth.getRecDepth;
max ← MonadRecDepth.getMaxRecDepth;
when (curr == max) $ throwError maxRecDepthErrorMessage;
MonadRecDepth.withRecDepth (curr+1) x
end Lean
new_frontend
namespace Lean
let curr ← MonadRecDepth.getRecDepth
let max ← MonadRecDepth.getMaxRecDepth
if curr == max then throwError maxRecDepthErrorMessage
MonadRecDepth.withRecDepth (curr+1) x
syntax "throwError! " ((interpolatedStr term) <|> term) : term
syntax "throwErrorAt! " term:max ((interpolatedStr term) <|> term) : term

325
src/Lean/Message.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -14,281 +15,271 @@ import Lean.Util.PPExt
import Lean.Util.PPGoal
namespace Lean
namespace MonadOptions end MonadOptions -- hack for old frontend
export MonadOptions (getOptions) -- hack for old frontend
def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : String :=
fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ toString msg
fileName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ toString msg
inductive MessageSeverity
| information | warning | error
| information | warning | error
structure MessageDataContext :=
(env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options)
(env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options)
structure NamingContext :=
(currNamespace : Name) (openDecls : List OpenDecl)
(currNamespace : Name) (openDecls : List OpenDecl)
/- Structure message data. We use it for reporting errors, trace messages, etc. -/
inductive MessageData
| ofFormat : Format → MessageData
| ofSyntax : Syntax → MessageData
| ofExpr : Expr → MessageData
| ofLevel : Level → MessageData
| ofName : Name → MessageData
| ofGoal : MVarId → MessageData
/- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
| withContext : MessageDataContext → MessageData → MessageData
| withNamingContext : NamingContext → MessageData → MessageData
/- Lifted `Format.nest` -/
| nest : Nat → MessageData → MessageData
/- Lifted `Format.group` -/
| group : MessageData → MessageData
/- Lifted `Format.compose` -/
| compose : MessageData → MessageData → MessageData
/- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
| tagged : Name → MessageData → MessageData
| node : Array MessageData → MessageData
| ofFormat : Format → MessageData
| ofSyntax : Syntax → MessageData
| ofExpr : Expr → MessageData
| ofLevel : Level → MessageData
| ofName : Name → MessageData
| ofGoal : MVarId → MessageData
/- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
| withContext : MessageDataContext → MessageData → MessageData
| withNamingContext : NamingContext → MessageData → MessageData
/- Lifted `Format.nest` -/
| nest : Nat → MessageData → MessageData
/- Lifted `Format.group` -/
| group : MessageData → MessageData
/- Lifted `Format.compose` -/
| compose : MessageData → MessageData → MessageData
/- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
| tagged : Name → MessageData → MessageData
| node : Array MessageData → MessageData
namespace MessageData
def nil : MessageData :=
ofFormat Format.nil
ofFormat Format.nil
def isNil : MessageData → Bool
| ofFormat Format.nil => true
| _ => false
| ofFormat Format.nil => true
| _ => false
def isNest : MessageData → Bool
| nest _ _ => true
| _ => false
| nest _ _ => true
| _ => false
instance : Inhabited MessageData := ⟨MessageData.ofFormat (arbitrary _)⟩
def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
{ env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,
currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }
def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := {
env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts,
currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls
}
partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format
| _, _, ofFormat fmt => pure fmt
| _, _, ofLevel u => pure $ fmt u
| _, _, ofName n => pure $ fmt n
| nCtx, some ctx, ofSyntax s => ppTerm (mkPPContext nCtx ctx) s -- HACK: might not be a term
| _, none, ofSyntax s => pure $ s.formatStx
| _, none, ofExpr e => pure $ format (toString e)
| nCtx, some ctx, ofExpr e => ppExpr (mkPPContext nCtx ctx) e
| _, none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId)
| nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId
| nCtx, _, withContext ctx d => formatAux nCtx ctx d
| _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d
| nCtx, ctx, tagged cls d => do d ← formatAux nCtx ctx d; pure $ Format.sbracket (format cls) ++ " " ++ d
| nCtx, ctx, nest n d => Format.nest n <$> formatAux nCtx ctx d
| nCtx, ctx, compose d₁ d₂ => do d₁ ← formatAux nCtx ctx d₁; d₂ ← formatAux nCtx ctx d₂; pure $ d₁ ++ d₂
| nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d
| nCtx, ctx, node ds => Format.nest 2 <$> ds.foldlM (fun r d => do d ← formatAux nCtx ctx d; pure $ r ++ Format.line ++ d) Format.nil
| _, _, ofFormat fmt => pure fmt
| _, _, ofLevel u => pure $ fmt u
| _, _, ofName n => pure $ fmt n
| nCtx, some ctx, ofSyntax s => ppTerm (mkPPContext nCtx ctx) s -- HACK: might not be a term
| _, none, ofSyntax s => pure $ s.formatStx
| _, none, ofExpr e => pure $ format (toString e)
| nCtx, some ctx, ofExpr e => ppExpr (mkPPContext nCtx ctx) e
| _, none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId)
| nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId
| nCtx, _, withContext ctx d => formatAux nCtx ctx d
| _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d
| nCtx, ctx, tagged cls d => do let d ← formatAux nCtx ctx d; pure $ Format.sbracket (format cls) ++ " " ++ d
| nCtx, ctx, nest n d => Format.nest n <$> formatAux nCtx ctx d
| nCtx, ctx, compose d₁ d₂ => do let d₁ ← formatAux nCtx ctx d₁; let d₂ ← formatAux nCtx ctx d₂; pure $ d₁ ++ d₂
| nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d
| nCtx, ctx, node ds => Format.nest 2 <$> ds.foldlM (fun r d => do let d ← formatAux nCtx ctx d; pure $ r ++ Format.line ++ d) Format.nil
protected def format (msgData : MessageData) : IO Format :=
formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData
protected def toString (msgData : MessageData) : IO String := do
fmt ← msgData.format;
pure $ toString fmt
let fmt ← msgData.format
pure $ toString fmt
instance : HasAppend MessageData := ⟨compose⟩
instance hasCoeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance hasCoeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance hasCoeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance hasCoeOfName : HasCoe Name MessageData := ⟨ofName⟩
instance hasCoeOfSyntax : HasCoe Syntax MessageData := ⟨ofSyntax⟩
instance hasCoeOfOptExpr : HasCoe (Option Expr) MessageData :=
⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
instance : Coe String MessageData := ⟨ofFormat ∘ format⟩
instance : Coe Format MessageData := ⟨ofFormat⟩
instance : Coe Level MessageData := ⟨ofLevel⟩
instance : Coe Expr MessageData := ⟨ofExpr⟩
instance : Coe Name MessageData := ⟨ofName⟩
instance : Coe Syntax MessageData := ⟨ofSyntax⟩
instance : Coe (Option Expr) MessageData := ⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
instance coeOfString : Coe String MessageData := ⟨ofFormat ∘ format⟩
instance coeOfFormat : Coe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : Coe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : Coe Expr MessageData := ⟨ofExpr⟩
instance coeOfName : Coe Name MessageData := ⟨ofName⟩
instance coeOfSyntax : Coe Syntax MessageData := ⟨ofSyntax⟩
instance coeOfOptExpr : Coe (Option Expr) MessageData :=
⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
-- TODO: delete
instance : HasCoe Format MessageData := ⟨ofFormat⟩
instance : HasCoe Level MessageData := ⟨ofLevel⟩
instance : HasCoe Expr MessageData := ⟨ofExpr⟩
instance : HasCoe Name MessageData := ⟨ofName⟩
instance : HasCoe Syntax MessageData := ⟨ofSyntax⟩
instance : HasCoe (Option Expr) MessageData := ⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
partial def arrayExpr.toMessageData (es : Array Expr) : Nat → MessageData → MessageData
| i, acc =>
partial def arrayExpr.toMessageData (es : Array Expr) (i : Nat) (acc : MessageData) : MessageData :=
if h : i < es.size then
let e := es.get ⟨i, h⟩;
let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
arrayExpr.toMessageData (i+1) acc
toMessageData es (i+1) acc
else
acc ++ "]"
instance hasCoeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
instance coeOfArrayExpr : Coe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
instance : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
instance : Coe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
def bracket (l : String) (f : MessageData) (r : String) : MessageData := group (nest l.length $ l ++ f ++ r)
def paren (f : MessageData) : MessageData := bracket "(" f ")"
def sbracket (f : MessageData) : MessageData := bracket "[" f "]"
def joinSep : List MessageData → MessageData → MessageData
| [], sep => Format.nil
| [a], sep => a
| a::as, sep => a ++ sep ++ joinSep as sep
| [], sep => Format.nil
| [a], sep => a
| a::as, sep => a ++ sep ++ joinSep as sep
def ofList: List MessageData → MessageData
| [] => "[]"
| xs => sbracket $ joinSep xs ("," ++ Format.line)
| [] => "[]"
| xs => sbracket $ joinSep xs ("," ++ Format.line)
def ofArray (msgs : Array MessageData) : MessageData :=
ofList msgs.toList
ofList msgs.toList
instance hasCoeOfList : HasCoe (List MessageData) MessageData := ⟨ofList⟩
instance hasCoeOfListExpr : HasCoe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
instance : HasCoe (List MessageData) MessageData := ⟨ofList⟩
instance : HasCoe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
instance coeOfList : Coe (List MessageData) MessageData := ⟨ofList⟩
instance coeOfListExpr : Coe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
instance : Coe (List MessageData) MessageData := ⟨ofList⟩
instance : Coe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
end MessageData
structure Message :=
(fileName : String)
(pos : Position)
(endPos : Option Position := none)
(severity : MessageSeverity := MessageSeverity.error)
(caption : String := "")
(data : MessageData)
(fileName : String)
(pos : Position)
(endPos : Option Position := none)
(severity : MessageSeverity := MessageSeverity.error)
(caption : String := "")
(data : MessageData)
@[export lean_mk_message]
def mkMessageEx (fileName : String) (pos : Position) (endPos : Option Position) (severity : MessageSeverity) (caption : String) (text : String) : Message :=
{ fileName := fileName, pos := pos, endPos := endPos, severity := severity, caption := caption, data := text }
{ fileName := fileName, pos := pos, endPos := endPos, severity := severity, caption := caption, data := text }
namespace Message
protected def toString (msg : Message) : IO String := do
str ← msg.data.toString;
pure $ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
((match msg.severity with
| MessageSeverity.information => ""
| MessageSeverity.warning => "warning: "
| MessageSeverity.error => "error: ") ++
(if msg.caption == "" then "" else msg.caption ++ ":\n") ++ str)
let str ← msg.data.toString
pure $ mkErrorStringWithPos msg.fileName msg.pos.line msg.pos.column
((match msg.severity with
| MessageSeverity.information => ""
| MessageSeverity.warning => "warning: "
| MessageSeverity.error => "error: ") ++
(if msg.caption == "" then "" else msg.caption ++ ":\n") ++ str)
instance : Inhabited Message :=
⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
instance : Inhabited Message := ⟨{ fileName := "", pos := ⟨0, 1⟩, data := arbitrary _}⟩
@[export lean_message_pos] def getPostEx (msg : Message) : Position := msg.pos
@[export lean_message_severity] def getSeverityEx (msg : Message) : MessageSeverity := msg.severity
@[export lean_message_string] unsafe def getMessageStringEx (msg : Message) : String :=
match unsafeIO (msg.data.toString) with -- hack: this is going to be deleted
| Except.ok msg => msg
| Except.error e => "error formatting message: " ++ toString e
match unsafeIO (msg.data.toString) with -- hack: this is going to be deleted
| Except.ok msg => msg
| Except.error e => "error formatting message: " ++ toString e
end Message
structure MessageLog :=
(msgs : Std.PersistentArray Message := {})
(msgs : Std.PersistentArray Message := {})
namespace MessageLog
def empty : MessageLog := ⟨{}⟩
def isEmpty (log : MessageLog) : Bool :=
log.msgs.isEmpty
log.msgs.isEmpty
instance : Inhabited MessageLog := ⟨{}⟩
def add (msg : Message) (log : MessageLog) : MessageLog :=
⟨log.msgs.push msg⟩
⟨log.msgs.push msg⟩
protected def append (l₁ l₂ : MessageLog) : MessageLog :=
⟨l₁.msgs ++ l₂.msgs⟩
⟨l₁.msgs ++ l₂.msgs⟩
instance : HasAppend MessageLog :=
⟨MessageLog.append⟩
⟨MessageLog.append⟩
def hasErrors (log : MessageLog) : Bool :=
log.msgs.any $ fun m => match m.severity with
| MessageSeverity.error => true
| _ => false
log.msgs.any fun m => match m.severity with
| MessageSeverity.error => true
| _ => false
def errorsToWarnings (log : MessageLog) : MessageLog :=
{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
{ msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
def getInfoMessages (log : MessageLog) : MessageLog :=
{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
log.msgs.forM f
log.msgs.forM f
def toList (log : MessageLog) : List Message :=
(log.msgs.foldl (fun acc msg => msg :: acc) []).reverse
(log.msgs.foldl (fun acc msg => msg :: acc) []).reverse
end MessageLog
def MessageData.nestD (msg : MessageData) : MessageData :=
MessageData.nest 2 msg
MessageData.nest 2 msg
def indentD (msg : MessageData) : MessageData :=
MessageData.nestD (Format.line ++ msg)
MessageData.nestD (Format.line ++ msg)
def indentExpr (e : Expr) : MessageData :=
indentD e
indentD e
namespace KernelException
private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
MessageData.withContext { env := env, mctx := {}, lctx := lctx, opts := opts } msg
def toMessageData (e : KernelException) (opts : Options) : MessageData :=
match e with
| unknownConstant env constName => mkCtx env {} opts $ "(kernel) unknown constant " ++ constName
| alreadyDeclared env constName => mkCtx env {} opts $ "(kernel) constant has already been declared " ++ constName
| declTypeMismatch env decl givenType =>
let process (n : Name) (expectedType : Expr) : MessageData :=
"(kernel) declaration type mismatch " ++ n
++ Format.line ++ "has type" ++ indentExpr givenType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
match decl with
| Declaration.defnDecl { name := n, type := type, .. } => process n type
| Declaration.thmDecl { name := n, type := type, .. } => process n type
| _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
| declHasMVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has metavariables " ++ constName
| declHasFVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has free variables " ++ constName
| funExpected env lctx e => mkCtx env lctx opts $ "(kernel) function expected" ++ indentExpr e
| typeExpected env lctx e => mkCtx env lctx opts $ "(kernel) type expected" ++ indentExpr e
| letTypeMismatch env lctx n _ _ => mkCtx env lctx opts $ "(kernel) let-declaration type mismatch " ++ n
| exprTypeMismatch env lctx e _ => mkCtx env lctx opts $ "(kernel) type mismatch at " ++ indentExpr e
| appTypeMismatch env lctx e fnType argType =>
mkCtx env lctx opts $
"application type mismatch" ++ indentExpr e
++ Format.line ++ "argument has type" ++ indentExpr argType
++ Format.line ++ "but function has type" ++ indentExpr fnType
| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
| other msg => "(kernel) " ++ msg
match e with
| unknownConstant env constName => mkCtx env {} opts $ "(kernel) unknown constant " ++ constName
| alreadyDeclared env constName => mkCtx env {} opts $ "(kernel) constant has already been declared " ++ constName
| declTypeMismatch env decl givenType =>
let process (n : Name) (expectedType : Expr) : MessageData :=
"(kernel) declaration type mismatch " ++ n
++ Format.line ++ "has type" ++ indentExpr givenType
++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType;
match decl with
| Declaration.defnDecl { name := n, type := type, .. } => process n type
| Declaration.thmDecl { name := n, type := type, .. } => process n type
| _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information
| declHasMVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has metavariables " ++ constName
| declHasFVars env constName _ => mkCtx env {} opts $ "(kernel) declaration has free variables " ++ constName
| funExpected env lctx e => mkCtx env lctx opts $ "(kernel) function expected" ++ indentExpr e
| typeExpected env lctx e => mkCtx env lctx opts $ "(kernel) type expected" ++ indentExpr e
| letTypeMismatch env lctx n _ _ => mkCtx env lctx opts $ "(kernel) let-declaration type mismatch " ++ n
| exprTypeMismatch env lctx e _ => mkCtx env lctx opts $ "(kernel) type mismatch at " ++ indentExpr e
| appTypeMismatch env lctx e fnType argType =>
mkCtx env lctx opts $
"application type mismatch" ++ indentExpr e
++ Format.line ++ "argument has type" ++ indentExpr argType
++ Format.line ++ "but function has type" ++ indentExpr fnType
| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
| other msg => "(kernel) " ++ msg
end KernelException
class AddMessageContext (m : Type → Type) :=
(addMessageContext : MessageData → m MessageData)
(addMessageContext : MessageData → m MessageData)
export AddMessageContext (addMessageContext)
instance addMessageContextTrans (m n) [AddMessageContext m] [MonadLift m n] : AddMessageContext n :=
{ addMessageContext := fun msg => liftM (addMessageContext msg : m _) }
instance (m n) [AddMessageContext m] [MonadLift m n] : AddMessageContext n :=
{ addMessageContext := fun msg => liftM (addMessageContext msg : m _) }
def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
env ← getEnv;
opts ← getOptions;
pure $ MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData
let env ← getEnv
let opts ← getOptions
pure $ MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData
def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
env ← getEnv;
mctx ← getMCtx;
lctx ← getLCtx;
opts ← getOptions;
pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData
end Lean
new_frontend
namespace Lean
let env ← getEnv
let mctx ← getMCtx
let lctx ← getLCtx
let opts ← getOptions
pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData
class ToMessageData (α : Type) :=
(toMessageData : α → MessageData)
@ -296,9 +287,9 @@ class ToMessageData (α : Type) :=
export ToMessageData (toMessageData)
def stringToMessageData (str : String) : MessageData :=
let lines := str.split (· == '\n')
let lines := lines.map (MessageData.ofFormat ∘ fmt)
MessageData.joinSep lines (MessageData.ofFormat Format.line)
let lines := str.split (· == '\n')
let lines := lines.map (MessageData.ofFormat ∘ fmt)
MessageData.joinSep lines (MessageData.ofFormat Format.line)
instance {α} [HasFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ fmt⟩
instance : ToMessageData Expr := ⟨MessageData.ofExpr⟩
@ -316,9 +307,9 @@ instance : ToMessageData (Option Expr) := ⟨fun | none => "<not-available>" | s
syntax:max "msg!" (interpolatedStr term) : term
macro_rules
| `(msg! $interpStr) => do
let chunks := interpStr.getArgs
let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toMessageData $a))
`(($r : MessageData))
| `(msg! $interpStr) => do
let chunks := interpStr.getArgs
let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toMessageData $a))
`(($r : MessageData))
end Lean

503
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -20,67 +21,65 @@ import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Backtrack
namespace Lean
namespace Syntax namespace MonadTraverser end MonadTraverser end Syntax -- Hack for old frontend
namespace Parser end Parser -- Hack for old frontend
namespace PrettyPrinter
namespace Formatter
structure Context :=
(options : Options)
(table : Parser.TokenTable)
(options : Options)
(table : Parser.TokenTable)
structure State :=
(stxTrav : Syntax.Traverser)
-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
-- content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly.
(leadWord : String := "")
-- Stack of generated Format objects, analogous to the Syntax stack in the parser.
-- Note, however, that the stack is reversed because of the right-to-left traversal.
(stack : Array Format := #[])
(stxTrav : Syntax.Traverser)
-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
-- content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly.
(leadWord : String := "")
-- Stack of generated Format objects, analogous to the Syntax stack in the parser.
-- Note, however, that the stack is reversed because of the right-to-left traversal.
(stack : Array Format := #[])
end Formatter
abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State $ CoreM
@[inline] def FormatterM.orelse {α} (p₁ p₂ : FormatterM α) : FormatterM α := do
s ← get;
catchInternalId backtrackExceptionId
p₁
(fun _ => do set s; p₂)
let s ← get
catchInternalId backtrackExceptionId
p₁
(fun _ => do set s; p₂)
instance Formatter.orelse {α} : HasOrelse (FormatterM α) := ⟨FormatterM.orelse⟩
abbrev Formatter := FormatterM Unit
unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) :=
KeyedDeclsAttribute.init {
builtinName := `builtinFormatter,
name := `formatter,
descr := "Register a formatter for a parser.
KeyedDeclsAttribute.init {
builtinName := `builtinFormatter,
name := `formatter,
descr := "Register a formatter for a parser.
[formatter k] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `SyntaxNodeKind` `k`.",
valueTypeName := `Lean.PrettyPrinter.Formatter,
evalKey := fun builtin args => do
env ← getEnv;
match attrParamSyntaxToIdentifier args with
| some id =>
-- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
-- synthesize a formatter for it immediately, so we just check for a declaration in this case
if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
else throwError ("invalid [formatter] argument, unknown syntax kind '" ++ toString id ++ "'")
| none => throwError "invalid [formatter] argument, expected identifier"
} `Lean.PrettyPrinter.formatterAttribute
[formatter k] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `SyntaxNodeKind` `k`.",
valueTypeName := `Lean.PrettyPrinter.Formatter,
evalKey := fun builtin args => do
let env ← getEnv
match attrParamSyntaxToIdentifier args with
| some id =>
-- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
-- synthesize a formatter for it immediately, so we just check for a declaration in this case
if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
else throwError ("invalid [formatter] argument, unknown syntax kind '" ++ toString id ++ "'")
| none => throwError "invalid [formatter] argument, expected identifier"
} `Lean.PrettyPrinter.formatterAttribute
@[builtinInit mkFormatterAttribute] constant formatterAttribute : KeyedDeclsAttribute Formatter := arbitrary _
unsafe def mkCombinatorFormatterAttribute : IO ParserCompiler.CombinatorAttribute :=
ParserCompiler.registerCombinatorAttribute
`combinatorFormatter
"Register a formatter for a parser combinator.
ParserCompiler.registerCombinatorAttribute
`combinatorFormatter
"Register a formatter for a parser combinator.
[combinatorFormatter c] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `Parser` declaration `c`.
Note that, unlike with [formatter], this is not a node kind since combinators usually do not introduce their own node kinds.
The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced
with `Formatter` in the parameter types."
[combinatorFormatter c] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `Parser` declaration `c`.
Note that, unlike with [formatter], this is not a node kind since combinators usually do not introduce their own node kinds.
The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced
with `Formatter` in the parameter types."
@[builtinInit mkCombinatorFormatterAttribute] constant combinatorFormatterAttribute : ParserCompiler.CombinatorAttribute := arbitrary _
namespace Formatter
@ -94,352 +93,328 @@ throw $ Exception.internal backtrackExceptionId
instance FormatterM.monadTraverser : Syntax.MonadTraverser FormatterM := ⟨{
get := State.stxTrav <$> get,
set := fun t => modify (fun st => { st with stxTrav := t }),
modifyGet := fun _ f => modifyGet (fun st => let (a, t) := f st.stxTrav; (a, { st with stxTrav := t })) }⟩
modifyGet := fun f => modifyGet (fun st => let (a, t) := f st.stxTrav; (a, { st with stxTrav := t }))
}⟩
open Syntax.MonadTraverser
def getStack : FormatterM (Array Format) := do
st ← get;
pure st.stack
let st ← get
pure st.stack
def getStackSize : FormatterM Nat := do
stack ← getStack;
pure stack.size
let stack ← getStack;
pure stack.size
def setStack (stack : Array Format) : FormatterM Unit :=
modify fun st => { st with stack := stack }
modify fun st => { st with stack := stack }
def push (f : Format) : FormatterM Unit :=
modify fun st => { st with stack := st.stack.push f }
modify fun st => { st with stack := st.stack.push f }
def pushLine : FormatterM Unit := do
push Format.line;
modify fun st => { st with leadWord := "" }
push Format.line;
modify fun st => { st with leadWord := "" }
/-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/
def visitArgs (x : FormatterM Unit) : FormatterM Unit := do
stx ← getCur;
when (stx.getArgs.size > 0) $
goDown (stx.getArgs.size - 1) *> x <* goUp;
goLeft
let stx ← getCur
if stx.getArgs.size > 0 then
goDown (stx.getArgs.size - 1) *> x <* goUp
goLeft
/-- Execute `x`, pass array of generated Format objects to `fn`, and push result. -/
def fold (fn : Array Format → Format) (x : FormatterM Unit) : FormatterM Unit := do
sp ← getStackSize;
x;
stack ← getStack;
let f := fn $ stack.extract sp stack.size;
setStack $ (stack.shrink sp).push f
let sp ← getStackSize
x
let stack ← getStack
let f := fn $ stack.extract sp stack.size
setStack $ (stack.shrink sp).push f
/-- Execute `x` and concatenate generated Format objects. -/
def concat (x : FormatterM Unit) : FormatterM Unit := do
fold (Array.foldl (fun acc f => if acc.isNil then f else f ++ acc) Format.nil) x
fold (Array.foldl (fun acc f => if acc.isNil then f else f ++ acc) Format.nil) x
def indent (x : Formatter) (indent : Option Int := none) : Formatter := do
concat x;
ctx ← read;
let indent := indent.getD $ Format.getIndent ctx.options;
modify fun st => { st with stack := st.stack.pop.push (Format.nest indent st.stack.back) }
concat x
let ctx ← read
let indent := indent.getD $ Format.getIndent ctx.options
modify fun st => { st with stack := st.stack.pop.push (Format.nest indent st.stack.back) }
def group (x : Formatter) : Formatter := do
concat x;
modify fun st => { st with stack := st.stack.pop.push (Format.fill st.stack.back) }
concat x
modify fun st => { st with stack := st.stack.pop.push (Format.fill st.stack.back) }
@[combinatorFormatter Lean.Parser.orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter :=
-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-- them in turn. Uses the syntax traverser non-linearly!
p1 <|> p2
-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-- them in turn. Uses the syntax traverser non-linearly!
p1 <|> p2
-- `mkAntiquot` is quite complex, so we'd rather have its formatter synthesized below the actual parser definition.
-- Note that there is a mutual recursion
-- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
-- anyway.
@[extern "lean_mk_antiquot_formatter"]
constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter :=
arbitrary _
constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter
def formatterForKind (k : SyntaxNodeKind) : Formatter := do
env ← getEnv;
p::_ ← pure $ formatterAttribute.getValues env k
| throwError $ "no known formatter for kind '" ++ k ++ "'";
p
let env ← getEnv
let p::_ ← pure $ formatterAttribute.getValues env k
| throwError! "no known formatter for kind '{k}'"
p
@[combinatorFormatter Lean.Parser.withAntiquot]
def withAntiquot.formatter (antiP p : Formatter) : Formatter :=
-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
-- fix the backtracking hack outright.
orelse.formatter antiP p
-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
-- fix the backtracking hack outright.
orelse.formatter antiP p
@[combinatorFormatter Lean.Parser.categoryParser]
def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
stx ← getCur;
if stx.getKind == `choice then
visitArgs do {
stx ← getCur;
sp ← getStackSize;
stx.getArgs.forM fun stx => formatterForKind stx.getKind;
stack ← getStack;
when (stack.size > sp && stack.anyRange sp stack.size fun f => f.pretty != (stack.get! sp).pretty)
panic! "Formatter.visit: inequal choice children";
-- discard all but one child format
setStack $ stack.extract 0 (sp+1)
}
else
withAntiquot.formatter (mkAntiquot.formatter' cat.toString none) (formatterForKind stx.getKind)
let stx ← getCur
if stx.getKind == `choice then
visitArgs do
let stx ← getCur;
let sp ← getStackSize
stx.getArgs.forM fun stx => formatterForKind stx.getKind
let stack ← getStack
if stack.size > sp && stack.anyRange sp stack.size fun f => f.pretty != (stack.get! sp).pretty then
panic! "Formatter.visit: inequal choice children";
-- discard all but one child format
setStack $ stack.extract 0 (sp+1)
else
withAntiquot.formatter (mkAntiquot.formatter' cat.toString none) (formatterForKind stx.getKind)
@[combinatorFormatter Lean.Parser.categoryParserOfStack]
def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
st ← get;
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset);
categoryParser.formatter stx.getId
let st ← get
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
categoryParser.formatter stx.getId
@[combinatorFormatter Lean.Parser.error]
def error.formatter (msg : String) : Formatter :=
pure ()
def error.formatter (msg : String) : Formatter := pure ()
@[combinatorFormatter Lean.Parser.try]
def try.formatter (p : Formatter) : Formatter :=
p
def try.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.lookahead]
def lookahead.formatter (p : Formatter) : Formatter :=
pure ()
def lookahead.formatter (p : Formatter) : Formatter := pure ()
@[combinatorFormatter Lean.Parser.notFollowedBy]
def notFollowedBy.formatter (p : Formatter) : Formatter :=
pure ()
def notFollowedBy.formatter (p : Formatter) : Formatter := pure ()
@[combinatorFormatter Lean.Parser.andthen]
def andthen.formatter (p1 p2 : Formatter) : Formatter :=
p2 *> p1
def andthen.formatter (p1 p2 : Formatter) : Formatter := p2 *> p1
def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
stx ← getCur;
when (k != stx.getKind) $ do {
trace! `PrettyPrinter.format.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
throwBacktrack
}
let stx ← getCur
if k != stx.getKind then
trace[PrettyPrinter.format.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
throwBacktrack
@[combinatorFormatter Lean.Parser.node]
def node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter := do
checkKind k;
visitArgs p
checkKind k;
visitArgs p
@[combinatorFormatter Lean.Parser.trailingNode]
def trailingNode.formatter (k : SyntaxNodeKind) (_ : Nat) (p : Formatter) : Formatter := do
checkKind k;
visitArgs do
p;
-- leading term, not actually produced by `p`
categoryParser.formatter `foo
checkKind k
visitArgs do
p;
-- leading term, not actually produced by `p`
categoryParser.formatter `foo
def parseToken (s : String) : FormatterM ParserState := do
ctx ← read;
env ← getEnv;
pure $ Parser.tokenFn { input := s, fileName := "", fileMap := FileMap.ofString "", prec := 0, env := env, tokens := ctx.table } (Parser.mkParserState s)
let ctx ← read
let env ← getEnv
pure $ Parser.tokenFn { input := s, fileName := "", fileMap := FileMap.ofString "", prec := 0, env := env, tokens := ctx.table } (Parser.mkParserState s)
def pushTokenCore (tk : String) : FormatterM Unit :=
if tk.toSubstring.dropRightWhile (fun s => s == ' ') == tk.toSubstring then
push tk
else do
pushLine;
push tk.trimRight
def pushTokenCore (tk : String) : FormatterM Unit := do
if tk.toSubstring.dropRightWhile (fun s => s == ' ') == tk.toSubstring then
push tk
else
pushLine
push tk.trimRight
def pushToken (tk : String) : FormatterM Unit := do
st ← get;
-- If there is no space between `tk` and the next word, compare parsing `tk` with and without the next word
if st.leadWord != "" && tk.trimRight == tk then do
t1 ← parseToken tk.trimLeft;
t2 ← parseToken $ tk.trimLeft ++ st.leadWord;
if t1.pos == t2.pos then do
-- same result => use `tk` as is, extend `leadWord` if not prefixed by whitespace
pushTokenCore tk;
modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
else do
-- different result => add space
pushTokenCore $ tk ++ " ";
let st ← get
-- If there is no space between `tk` and the next word, compare parsing `tk` with and without the next word
if st.leadWord != "" && tk.trimRight == tk then
let t1 ← parseToken tk.trimLeft
let t2 ← parseToken $ tk.trimLeft ++ st.leadWord
if t1.pos == t2.pos then
-- same result => use `tk` as is, extend `leadWord` if not prefixed by whitespace
pushTokenCore tk
modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
else
-- different result => add space
pushTokenCore $ tk ++ " "
modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
else
-- already separated => use `tk` as is
pushTokenCore tk
modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
else do {
-- already separated => use `tk` as is
pushTokenCore tk;
modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
}
@[combinatorFormatter symbol]
@[combinatorFormatter Lean.Parser.symbol]
def symbol.formatter (sym : String) : Formatter := do
stx ← getCur;
if stx.isToken sym then do
pushToken sym;
goLeft
else do
trace! `PrettyPrinter.format.backtrack ("unexpected syntax '" ++ stx ++ "', expected symbol '" ++ sym ++ "'");
throwBacktrack
let stx ← getCur
if stx.isToken sym then do
pushToken sym;
goLeft
else do
trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{stx}', expected symbol '{sym}'"
throwBacktrack
@[combinatorFormatter nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
@[combinatorFormatter Lean.Parser.nonReservedSymbol] def nonReservedSymbol.formatter := symbol.formatter
@[combinatorFormatter unicodeSymbol]
@[combinatorFormatter Lean.Parser.unicodeSymbol]
def unicodeSymbol.formatter (sym asciiSym : String) : Formatter := do
stx ← getCur;
Syntax.atom _ val ← pure stx
| throwError $ "not an atom: " ++ toString stx;
if val == sym.trim then
pushToken sym
else
pushToken asciiSym;
goLeft
let stx ← getCur
let Syntax.atom _ val ← pure stx
| throwError $ "not an atom: " ++ toString stx
if val == sym.trim then
pushToken sym
else
pushToken asciiSym;
goLeft
@[combinatorFormatter identNoAntiquot]
@[combinatorFormatter Lean.Parser.identNoAntiquot]
def identNoAntiquot.formatter : Formatter := do
checkKind identKind;
stx ← getCur;
let id := stx.getId;
let id := id.simpMacroScopes;
let s := id.toString;
if id.isAnonymous then
pushToken "[anonymous]"
else if isInaccessibleUserName id || id.components.any Name.isNum ||
-- loose bvar
"#".isPrefixOf s then
-- not parsable anyway, output as-is
pushToken s
else do {
-- try to parse `s` as-is; if it fails, escape
pst ← parseToken s;
if pst.stxStack == #[stx] then
checkKind identKind;
let stx ← getCur
let id := stx.getId
let id := id.simpMacroScopes
let s := id.toString;
if id.isAnonymous then
pushToken "[anonymous]"
else if isInaccessibleUserName id || id.components.any Name.isNum ||
-- loose bvar
"#".isPrefixOf s then
-- not parsable anyway, output as-is
pushToken s
else
let n := stx.getId;
-- TODO: do something better than escaping all parts
let n := (n.components.map fun c => "«" ++ toString c ++ "»").foldl mkNameStr Name.anonymous;
pushToken n.toString
};
goLeft
-- try to parse `s` as-is; if it fails, escape
let pst ← parseToken s
if pst.stxStack == #[stx] then
pushToken s
else
let n := stx.getId
-- TODO: do something better than escaping all parts
let n := (n.components.map fun c => "«" ++ toString c ++ "»").foldl mkNameStr Name.anonymous
pushToken n.toString
goLeft
@[combinatorFormatter rawIdent] def rawIdent.formatter : Formatter := do
checkKind identKind;
stx ← getCur;
pushToken stx.getId.toString;
goLeft
@[combinatorFormatter Lean.Parser.rawIdent] def rawIdent.formatter : Formatter := do
checkKind identKind
let stx ← getCur
pushToken stx.getId.toString;
goLeft
@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter := rawIdent.formatter
@[combinatorFormatter Lean.Parser.identEq] def identEq.formatter (id : Name) := rawIdent.formatter
def visitAtom (k : SyntaxNodeKind) : Formatter := do
stx ← getCur;
when (k != Name.anonymous) $
checkKind k;
Syntax.atom _ val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
| throwError $ "not an atom: " ++ toString stx;
pushToken val;
goLeft
let stx ← getCur
if k != Name.anonymous then
checkKind k
let Syntax.atom _ val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
| throwError $ "not an atom: " ++ toString stx
pushToken val
goLeft
@[combinatorFormatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@[combinatorFormatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
@[combinatorFormatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
@[combinatorFormatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
@[combinatorFormatter fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
@[combinatorFormatter Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@[combinatorFormatter Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind
@[combinatorFormatter Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind
@[combinatorFormatter Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind
@[combinatorFormatter Lean.Parser.fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind
@[combinatorFormatter many]
@[combinatorFormatter Lean.Parser.many]
def many.formatter (p : Formatter) : Formatter := do
stx ← getCur;
visitArgs $ stx.getArgs.size.forM fun _ => p
let stx ← getCur
visitArgs $ stx.getArgs.size.forM fun _ => p
@[combinatorFormatter many1] def many1.formatter (p : Formatter) : Formatter :=
many.formatter p
@[combinatorFormatter Lean.Parser.many1] def many1.formatter (p : Formatter) : Formatter := many.formatter p
@[combinatorFormatter Parser.optional]
def optional.formatter (p : Formatter) : Formatter := do
visitArgs p
@[combinatorFormatter Lean.Parser.optional]
def optional.formatter (p : Formatter) : Formatter := visitArgs p
@[combinatorFormatter Parser.many1Unbox]
@[combinatorFormatter Lean.Parser.many1Unbox]
def many1Unbox.formatter (p : Formatter) : Formatter := do
stx ← getCur;
if stx.getKind == nullKind then do
many.formatter p
else
p
let stx ← getCur
if stx.getKind == nullKind then do
many.formatter p
else
p
@[combinatorFormatter sepBy]
@[combinatorFormatter Lean.Parser.sepBy]
def sepBy.formatter (p pSep : Formatter) : Formatter := do
stx ← getCur;
visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep
let stx ← getCur
visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep
@[combinatorFormatter sepBy1] def sepBy1.formatter := sepBy.formatter
@[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := do
p
@[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := do
p
@[combinatorFormatter Lean.Parser.withForbidden] def withForbidden.formatter (tk : Token) (p : Formatter) : Formatter := do
p
@[combinatorFormatter Lean.Parser.withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := do
p
@[combinatorFormatter Lean.Parser.sepBy1] def sepBy1.formatter := sepBy.formatter
@[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.withForbidden] def withForbidden.formatter (tk : Token) (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.setExpected]
def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :=
p
def setExpected.formatter (expected : List String) (p : Formatter) : Formatter := p
@[combinatorFormatter Lean.Parser.toggleInsideQuot]
def toggleInsideQuot.formatter (p : Formatter) : Formatter :=
p
def toggleInsideQuot.formatter (p : Formatter) : Formatter := p
@[combinatorFormatter checkWsBefore] def checkWsBefore.formatter : Formatter := do
st ← get;
when (st.leadWord != "") $
pushLine
@[combinatorFormatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do
let st ← get
if st.leadWord != "" then
pushLine
@[combinatorFormatter checkPrec] def checkPrec.formatter : Formatter := pure ()
@[combinatorFormatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
@[combinatorFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := pure ()
@[combinatorFormatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
@[combinatorFormatter checkColGe] def checkColGe.formatter : Formatter := pure ()
@[combinatorFormatter checkColGt] def checkColGt.formatter : Formatter := pure ()
@[combinatorFormatter checkLineEq] def checkLineEq.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkPrec] def checkPrec.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkStackTop] def checkStackTop.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkTailWs] def checkTailWs.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkColGe] def checkColGe.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkColGt] def checkColGt.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkLineEq] def checkLineEq.formatter : Formatter := pure ()
@[combinatorFormatter eoi] def eoi.formatter : Formatter := pure ()
@[combinatorFormatter notFollowedByCategoryToken] def notFollowedByCategoryToken.formatter : Formatter := pure ()
@[combinatorFormatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.eoi] def eoi.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.notFollowedByCategoryToken] def notFollowedByCategoryToken.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkInsideQuot] def checkInsideQuot.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.checkOutsideQuot] def checkOutsideQuot.formatter : Formatter := pure ()
@[combinatorFormatter Lean.Parser.skip] def skip.formatter : Formatter := pure ()
@[combinatorFormatter pushNone] def pushNone.formatter : Formatter := goLeft
@[combinatorFormatter Lean.Parser.pushNone] def pushNone.formatter : Formatter := goLeft
-- TODO: delete with old frontend
@[combinatorFormatter quotedSymbol] def quotedSymbol.formatter : Formatter := do
checkKind quotedSymbolKind;
visitArgs do
push "`"; goLeft;
visitAtom Name.anonymous;
push "`"; goLeft
@[combinatorFormatter Lean.Parser.quotedSymbol] def quotedSymbol.formatter : Formatter := do
checkKind quotedSymbolKind
visitArgs do
push "`"; goLeft
visitAtom Name.anonymous
push "`"; goLeft
@[combinatorFormatter Lean.Parser.interpolatedStr]
def interpolatedStr.formatter (p : Formatter) : Formatter :=
throwError "NIY"
def interpolatedStr.formatter (p : Formatter) : Formatter := throwError "NIY"
@[combinatorFormatter unquotedSymbol] def unquotedSymbol.formatter := visitAtom Name.anonymous
@[combinatorFormatter Lean.Parser.unquotedSymbol] def unquotedSymbol.formatter := visitAtom Name.anonymous
@[combinatorFormatter ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Formatter) : Formatter :=
if c then t else e
if c then t else e
end Formatter
open Formatter
def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
options ← getOptions;
table ← Parser.builtinTokenTable.get;
let options ← getOptions
let table ← Parser.builtinTokenTable.get
catchInternalId backtrackExceptionId
(do
(_, st) ← (concat formatter { table := table, options := options }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
let (_, st) ← (concat formatter { table := table, options := options }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
pure $ Format.fill $ st.stack.get! 0)
(fun _ => throwError "format: uncaught backtrack exception")
def formatTerm := format $ categoryParser.formatter `term
def formatCommand := format $ categoryParser.formatter `command
@[builtinInit] private def regTraceClasses : IO Unit := do
registerTraceClass `PrettyPrinter.format;
pure ()
builtin_initialize registerTraceClass `PrettyPrinter.format;
end PrettyPrinter
end Lean

4
src/Lean/PrettyPrinter/Meta.lean
View file

@ -35,14 +35,14 @@ unsafe def interpretParserDescr : ParserDescr → AttrM Parenthesizer
| ParserDescr.sepBy1 d₁ d₂ => sepBy1.parenthesizer <$> interpretParserDescr d₁ <*> interpretParserDescr d₂
| ParserDescr.node k prec d => leadingNode.parenthesizer k prec <$> interpretParserDescr d
| ParserDescr.trailingNode k prec d => trailingNode.parenthesizer k prec <$> interpretParserDescr d
| ParserDescr.symbol tk => pure $ symbol.parenthesizer
| ParserDescr.symbol tk => pure $ symbol.parenthesizer tk
| ParserDescr.numLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer
| ParserDescr.strLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer
| ParserDescr.charLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer
| ParserDescr.nameLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer
| ParserDescr.ident => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer
| ParserDescr.interpolatedStr d => interpolatedStr.parenthesizer <$> interpretParserDescr d
| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.parenthesizer
| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.parenthesizer tk includeIdent
| ParserDescr.noWs => pure $ checkNoWsBefore.parenthesizer
| ParserDescr.parser constName => interpretParser (ctx interpretParserDescr) constName
| ParserDescr.cat catName prec => pure $ categoryParser.parenthesizer catName prec

442
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -78,27 +79,24 @@ import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Backtrack
namespace Lean
namespace Syntax namespace MonadTraverser end MonadTraverser end Syntax -- Hack for old frontend
namespace Parser end Parser -- Hack for old frontend
namespace PrettyPrinter
namespace Parenthesizer
structure Context :=
-- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`.
(cat : Name := Name.anonymous)
-- We need to store this `categoryParser` argument to deal with the implicit Pratt parser call in `trailingNode.parenthesizer`.
(cat : Name := Name.anonymous)
structure State :=
(stxTrav : Syntax.Traverser)
--- precedence and category of the current left-most trailing parser, if any; see module doc for details
(contPrec : Option Nat := none)
(contCat := Name.anonymous)
-- current minimum precedence in this Pratt parser call, if any; see module doc for details
(minPrec : Option Nat := none)
-- precedence of the trailing Pratt parser call if any; see module doc for details
(trailPrec : Option Nat := none)
-- true iff we have already visited a token on this parser level; used for detecting trailing parsers
(visitedToken : Bool := false)
structure State :=
(stxTrav : Syntax.Traverser)
--- precedence and category of the current left-most trailing parser, if any; see module doc for details
(contPrec : Option Nat := none)
(contCat : Name := Name.anonymous)
-- current minimum precedence in this Pratt parser call, if any; see module doc for details
(minPrec : Option Nat := none)
-- precedence of the trailing Pratt parser call if any; see module doc for details
(trailPrec : Option Nat := none)
-- true iff we have already visited a token on this parser level; used for detecting trailing parsers
(visitedToken : Bool := false)
end Parenthesizer
@ -106,66 +104,66 @@ abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateRefT Parenthesizer
abbrev Parenthesizer := ParenthesizerM Unit
@[inline] def ParenthesizerM.orelse {α} (p₁ p₂ : ParenthesizerM α) : ParenthesizerM α := do
s ← get;
catchInternalId backtrackExceptionId
p₁
(fun _ => do set s; p₂)
let s ← get
catchInternalId backtrackExceptionId
p₁
(fun _ => do set s; p₂)
instance Parenthesizer.orelse {α} : HasOrelse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩
unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
KeyedDeclsAttribute.init {
builtinName := `builtinParenthesizer,
name := `parenthesizer,
descr := "Register a parenthesizer for a parser.
KeyedDeclsAttribute.init {
builtinName := `builtinParenthesizer,
name := `parenthesizer,
descr := "Register a parenthesizer for a parser.
[parenthesizer k] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `SyntaxNodeKind` `k`.",
valueTypeName := `Lean.PrettyPrinter.Parenthesizer,
evalKey := fun builtin args => do
env ← getEnv;
match attrParamSyntaxToIdentifier args with
| some id =>
-- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
-- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
else throwError ("invalid [parenthesizer] argument, unknown syntax kind '" ++ toString id ++ "'")
| none => throwError "invalid [parenthesizer] argument, expected identifier"
} `Lean.PrettyPrinter.parenthesizerAttribute
@[builtinInit mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer := arbitrary _
[parenthesizer k] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `SyntaxNodeKind` `k`.",
valueTypeName := `Lean.PrettyPrinter.Parenthesizer,
evalKey := fun builtin args => do
let env ← getEnv
match attrParamSyntaxToIdentifier args with
| some id =>
-- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
-- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
else throwError ("invalid [parenthesizer] argument, unknown syntax kind '" ++ toString id ++ "'")
| none => throwError "invalid [parenthesizer] argument, expected identifier"
} `Lean.PrettyPrinter.parenthesizerAttribute
@[builtinInit mkParenthesizerAttribute] constant parenthesizerAttribute : KeyedDeclsAttribute Parenthesizer
abbrev CategoryParenthesizer := forall (prec : Nat), Parenthesizer
unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryParenthesizer) :=
KeyedDeclsAttribute.init {
builtinName := `builtinCategoryParenthesizer,
name := `categoryParenthesizer,
descr := "Register a parenthesizer for a syntax category.
KeyedDeclsAttribute.init {
builtinName := `builtinCategoryParenthesizer,
name := `categoryParenthesizer,
descr := "Register a parenthesizer for a syntax category.
[parenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`,
which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize`
with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized,
but still be traversed for parenthesizing nested categories.",
valueTypeName := `Lean.PrettyPrinter.CategoryParenthesizer,
evalKey := fun _ args => do
env ← getEnv;
match attrParamSyntaxToIdentifier args with
| some id =>
if Parser.isParserCategory env id then pure id
else throwError ("invalid [parenthesizer] argument, unknown parser category '" ++ toString id ++ "'")
| none => throwError "invalid [parenthesizer] argument, expected identifier"
} `Lean.PrettyPrinter.categoryParenthesizerAttribute
@[builtinInit mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer := arbitrary _
[parenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`,
which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize`
with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized,
but still be traversed for parenthesizing nested categories.",
valueTypeName := `Lean.PrettyPrinter.CategoryParenthesizer,
evalKey := fun _ args => do
let env ← getEnv
match attrParamSyntaxToIdentifier args with
| some id =>
if Parser.isParserCategory env id then pure id
else throwError ("invalid [parenthesizer] argument, unknown parser category '" ++ toString id ++ "'")
| none => throwError "invalid [parenthesizer] argument, expected identifier"
} `Lean.PrettyPrinter.categoryParenthesizerAttribute
@[builtinInit mkCategoryParenthesizerAttribute] constant categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer
unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttribute :=
ParserCompiler.registerCombinatorAttribute
`combinatorParenthesizer
"Register a parenthesizer for a parser combinator.
ParserCompiler.registerCombinatorAttribute
`combinatorParenthesizer
"Register a parenthesizer for a parser combinator.
[combinatorParenthesizer c] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `Parser` declaration `c`.
Note that, unlike with [parenthesizer], this is not a node kind since combinators usually do not introduce their own node kinds.
The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced
with `Parenthesizer` in the parameter types."
@[builtinInit mkCombinatorParenthesizerAttribute] constant combinatorParenthesizerAttribute : ParserCompiler.CombinatorAttribute := arbitrary _
[combinatorParenthesizer c] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `Parser` declaration `c`.
Note that, unlike with [parenthesizer], this is not a node kind since combinators usually do not introduce their own node kinds.
The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced
with `Parenthesizer` in the parameter types."
@[builtinInit mkCombinatorParenthesizerAttribute] constant combinatorParenthesizerAttribute : ParserCompiler.CombinatorAttribute
namespace Parenthesizer
@ -178,221 +176,218 @@ throw $ Exception.internal backtrackExceptionId
instance ParenthesizerM.monadTraverser : Syntax.MonadTraverser ParenthesizerM := ⟨{
get := State.stxTrav <$> get,
set := fun t => modify (fun st => { st with stxTrav := t }),
modifyGet := fun _ f => modifyGet (fun st => let (a, t) := f st.stxTrav; (a, { st with stxTrav := t })) }⟩
modifyGet := fun f => modifyGet (fun st => let (a, t) := f st.stxTrav; (a, { st with stxTrav := t }))
}⟩
open Syntax.MonadTraverser
def addPrecCheck (prec : Nat) : ParenthesizerM Unit :=
modify $ fun st => { st with contPrec := Nat.min (st.contPrec.getD prec) prec, minPrec := Nat.min (st.minPrec.getD prec) prec }
modify fun st => { st with contPrec := Nat.min (st.contPrec.getD prec) prec, minPrec := Nat.min (st.minPrec.getD prec) prec }
/-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/
def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
stx ← getCur;
when (stx.getArgs.size > 0) $
goDown (stx.getArgs.size - 1) *> x <* goUp;
goLeft
let stx ← getCur
if stx.getArgs.size > 0 then
goDown (stx.getArgs.size - 1) *> x <* goUp
goLeft
-- Macro scopes in the parenthesizer output are ultimately ignored by the pretty printer,
-- so give a trivial implementation.
instance monadQuotation : MonadQuotation ParenthesizerM := {
getCurrMacroScope := pure $ arbitrary _,
getMainModule := pure $ arbitrary _,
withFreshMacroScope := fun α x => x,
withFreshMacroScope := fun x => x,
}
/-- Run `x` and parenthesize the result using `mkParen` if necessary. -/
def maybeParenthesize (cat : Name) (mkParen : Syntax → Syntax) (prec : Nat) (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
stx ← getCur;
idx ← getIdx;
st ← get;
-- reset precs for the recursive call
set { stxTrav := st.stxTrav : State };
trace! `PrettyPrinter.parenthesize ("parenthesizing (cont := " ++ toString (st.contPrec, st.contCat) ++ ")" ++ MessageData.nest 2 (line ++ stx));
x;
{ minPrec := some minPrec, trailPrec := trailPrec, .. } ← get
| panic! "maybeParenthesize: visited a syntax tree without precedences?!";
trace! `PrettyPrinter.parenthesize ("...precedences are " ++ fmt prec ++ " >? " ++ fmt minPrec ++ ", " ++ fmt (trailPrec, cat) ++ " <=? " ++ fmt (st.contPrec, st.contCat));
-- Should we parenthesize?
when (prec > minPrec || match trailPrec, st.contPrec with some trailPrec, some contPrec => cat == st.contCat && trailPrec <= contPrec | _, _ => false) $ do {
-- The recursive `visit` call, by the invariant, has moved to the preceding node. In order to parenthesize
-- the original node, we must first move to the right, except if we already were at the left-most child in the first
-- place.
when (idx > 0) goRight;
stx ← getCur;
match stx.getHeadInfo, stx.getTailInfo with
| some hi, some ti =>
-- Move leading/trailing whitespace of `stx` outside of parentheses
let stx := (stx.setHeadInfo { hi with leading := "".toSubstring }).setTailInfo { ti with trailing := "".toSubstring };
let stx := mkParen stx;
let stx := (stx.setHeadInfo { hi with trailing := "".toSubstring }).setTailInfo { ti with leading := "".toSubstring };
setCur stx
| _, _ => setCur (mkParen stx);
stx ← getCur; trace! `PrettyPrinter.parenthesize ("parenthesized: " ++ stx.formatStx none);
goLeft;
-- after parenthesization, there is no more trailing parser
modify (fun st => { st with contPrec := Parser.maxPrec, contCat := cat, trailPrec := none })
};
{ trailPrec := trailPrec, .. } ← get;
-- If we already had a token at this level, keep the trailing parser. Otherwise, use the minimum of
-- `prec` and `trailPrec`.
let trailPrec := if st.visitedToken then st.trailPrec else match trailPrec with
| some trailPrec => some (Nat.min trailPrec prec)
| _ => some prec;
modify (fun stP => { stP with minPrec := st.minPrec, trailPrec := trailPrec })
let stx ← getCur
let idx ← getIdx
let st ← get
-- reset precs for the recursive call
set { stxTrav := st.stxTrav : State }
trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){MessageData.nest 2 (line ++ stx)}"
x
let { minPrec := some minPrec, trailPrec := trailPrec, .. } ← get
| panic! "maybeParenthesize: visited a syntax tree without precedences?!"
trace[PrettyPrinter.parenthesize]! "...precedences are {prec} >? {minPrec}, {(trailPrec, cat)} <=? {(st.contPrec, st.contCat)}"
-- Should we parenthesize?
if (prec > minPrec || match trailPrec, st.contPrec with some trailPrec, some contPrec => cat == st.contCat && trailPrec <= contPrec | _, _ => false) then
-- The recursive `visit` call, by the invariant, has moved to the preceding node. In order to parenthesize
-- the original node, we must first move to the right, except if we already were at the left-most child in the first
-- place.
if idx > 0 then goRight
let stx ← getCur
match stx.getHeadInfo, stx.getTailInfo with
| some hi, some ti =>
-- Move leading/trailing whitespace of `stx` outside of parentheses
let stx := (stx.setHeadInfo { hi with leading := "".toSubstring }).setTailInfo { ti with trailing := "".toSubstring }
let stx := mkParen stx
let stx := (stx.setHeadInfo { hi with trailing := "".toSubstring }).setTailInfo { ti with leading := "".toSubstring }
setCur stx
| _, _ => setCur (mkParen stx)
let stx ← getCur; trace! `PrettyPrinter.parenthesize ("parenthesized: " ++ stx.formatStx none)
goLeft
-- after parenthesization, there is no more trailing parser
modify (fun st => { st with contPrec := Parser.maxPrec, contCat := cat, trailPrec := none })
let { trailPrec := trailPrec, .. } ← get
-- If we already had a token at this level, keep the trailing parser. Otherwise, use the minimum of
-- `prec` and `trailPrec`.
let trailPrec := if st.visitedToken then st.trailPrec else match trailPrec with
| some trailPrec => some (Nat.min trailPrec prec)
| _ => some prec
modify (fun stP => { stP with minPrec := st.minPrec, trailPrec := trailPrec })
/-- Adjust state and advance. -/
def visitToken : Parenthesizer := do
modify (fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true });
goLeft
modify fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true }
goLeft
@[combinatorParenthesizer Lean.Parser.orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do
st ← get;
-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-- them in turn. Uses the syntax traverser non-linearly!
p1 <|> p2
let st ← get
-- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try
-- them in turn. Uses the syntax traverser non-linearly!
p1 <|> p2
-- `mkAntiquot` is quite complex, so we'd rather have its parenthesizer synthesized below the actual parser definition.
-- Note that there is a mutual recursion
-- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
-- anyway.
@[extern 8 "lean_mk_antiquot_parenthesizer"]
constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer :=
arbitrary _
constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer
@[inline] def liftCoreM {α} (x : CoreM α) : ParenthesizerM α :=
liftM x
liftM x
def throwError {α} (msg : MessageData) : ParenthesizerM α :=
liftCoreM $ throwError msg
liftCoreM $ Lean.throwError msg
def parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer := do
env ← getEnv;
p::_ ← pure $ parenthesizerAttribute.getValues env k
| throwError $ "no known parenthesizer for kind '" ++ toString k ++ "'";
p
let env ← getEnv
let p::_ ← pure $ parenthesizerAttribute.getValues env k
| throwError! "no known parenthesizer for kind '{k}'"
p
@[combinatorParenthesizer Lean.Parser.withAntiquot]
def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer :=
-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
-- fix the backtracking hack outright.
orelse.parenthesizer antiP p
-- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather
-- fix the backtracking hack outright.
orelse.parenthesizer antiP p
def parenthesizeCategoryCore (cat : Name) (prec : Nat) : Parenthesizer :=
withReader (fun ctx => { ctx with cat := cat }) do
stx ← getCur;
if stx.getKind == `choice then
visitArgs $ stx.getArgs.size.forM $ fun _ => do
stx ← getCur;
parenthesizerForKind stx.getKind
else
withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString none) (parenthesizerForKind stx.getKind);
modify fun st => { st with contCat := cat }
withReader (fun ctx => { ctx with cat := cat }) do
let stx ← getCur
if stx.getKind == `choice then
visitArgs $ stx.getArgs.size.forM $ fun _ => do
stx ← getCur
parenthesizerForKind stx.getKind
else
withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString none) (parenthesizerForKind stx.getKind)
modify fun st => { st with contCat := cat }
@[combinatorParenthesizer Lean.Parser.categoryParser]
def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do
env ← getEnv;
match categoryParenthesizerAttribute.getValues env cat with
| p::_ => p prec
-- Fall back to the generic parenthesizer.
-- In this case this node will never be parenthesized since we don't know which parentheses to use.
| _ => parenthesizeCategoryCore cat prec
let env ← getEnv
match categoryParenthesizerAttribute.getValues env cat with
| p::_ => p prec
-- Fall back to the generic parenthesizer.
-- In this case this node will never be parenthesized since we don't know which parentheses to use.
| _ => parenthesizeCategoryCore cat prec
@[combinatorParenthesizer Lean.Parser.categoryParserOfStack]
def categoryParserOfStack.parenthesizer (offset : Nat) (prec : Nat) : Parenthesizer := do
st ← get;
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset);
categoryParser.parenthesizer stx.getId prec
let st ← get
let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset)
categoryParser.parenthesizer stx.getId prec
@[builtinCategoryParenthesizer term]
def term.parenthesizer : CategoryParenthesizer | prec => do
stx ← getCur;
-- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot`
if stx.getKind == nullKind then
throwBacktrack
else do
maybeParenthesize `term (fun stx => Unhygienic.run `(($stx))) prec $
parenthesizeCategoryCore `term prec
let stx ← getCur
-- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot`
if stx.getKind == nullKind then
throwBacktrack
else do
maybeParenthesize `term (fun stx => Unhygienic.run `(($stx))) prec $
parenthesizeCategoryCore `term prec
@[builtinCategoryParenthesizer tactic]
def tactic.parenthesizer : CategoryParenthesizer | prec => do
maybeParenthesize `tactic (fun stx => Unhygienic.run `(tactic|($stx))) prec $
parenthesizeCategoryCore `tactic prec
maybeParenthesize `tactic (fun stx => Unhygienic.run `(tactic|($stx))) prec $
parenthesizeCategoryCore `tactic prec
@[builtinCategoryParenthesizer level]
def level.parenthesizer : CategoryParenthesizer | prec => do
maybeParenthesize `level (fun stx => Unhygienic.run `(level|($stx))) prec $
parenthesizeCategoryCore `level prec
maybeParenthesize `level (fun stx => Unhygienic.run `(level|($stx))) prec $
parenthesizeCategoryCore `level prec
@[combinatorParenthesizer Lean.Parser.error]
def error.parenthesizer (msg : String) : Parenthesizer :=
pure ()
pure ()
@[combinatorParenthesizer Lean.Parser.try]
def try.parenthesizer (p : Parenthesizer) : Parenthesizer :=
p
p
@[combinatorParenthesizer Lean.Parser.lookahead]
def lookahead.parenthesizer (p : Parenthesizer) : Parenthesizer :=
pure ()
pure ()
@[combinatorParenthesizer Lean.Parser.notFollowedBy]
def notFollowedBy.parenthesizer (p : Parenthesizer) : Parenthesizer :=
pure ()
pure ()
@[combinatorParenthesizer Lean.Parser.andthen]
def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer :=
p2 *> p1
p2 *> p1
@[combinatorParenthesizer Lean.Parser.node]
def node.parenthesizer (k : SyntaxNodeKind) (p : Parenthesizer) : Parenthesizer := do
stx ← getCur;
when (k != stx.getKind) $ do {
trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
-- HACK; see `orelse.parenthesizer`
throwBacktrack
};
visitArgs p
let stx ← getCur
if k != stx.getKind then
trace[PrettyPrinter.parenthesize.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
-- HACK; see `orelse.parenthesizer`
throwBacktrack
visitArgs p
@[combinatorParenthesizer Lean.Parser.checkPrec]
def checkPrec.parenthesizer (prec : Nat) : Parenthesizer :=
addPrecCheck prec
addPrecCheck prec
@[combinatorParenthesizer Lean.Parser.leadingNode]
def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do
node.parenthesizer k p;
addPrecCheck prec;
-- Limit `cont` precedence to `maxPrec-1`.
-- This is because `maxPrec-1` is the precedence of function application, which is the only way to turn a leading parser
-- into a trailing one.
modify fun st => { st with contPrec := Nat.min (Parser.maxPrec-1) prec }
node.parenthesizer k p
addPrecCheck prec
-- Limit `cont` precedence to `maxPrec-1`.
-- This is because `maxPrec-1` is the precedence of function application, which is the only way to turn a leading parser
-- into a trailing one.
modify fun st => { st with contPrec := Nat.min (Parser.maxPrec-1) prec }
@[combinatorParenthesizer Lean.Parser.trailingNode]
def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do
stx ← getCur;
when (k != stx.getKind) $ do {
trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
-- HACK; see `orelse.parenthesizer`
throwBacktrack
};
visitArgs $ do {
p;
addPrecCheck prec;
ctx ← read;
modify fun st => { st with contCat := ctx.cat };
-- After visiting the nodes actually produced by the parser passed to `trailingNode`, we are positioned on the
-- left-most child, which is the term injected by `trailingNode` in place of the recursion. Left recursion is not an
-- issue for the parenthesizer, so we can think of this child being produced by `termParser 0`, or whichever Pratt
-- parser is calling us.
categoryParser.parenthesizer ctx.cat 0
}
let stx ← getCur
if k != stx.getKind then
trace[PrettyPrinter.parenthesize.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
-- HACK; see `orelse.parenthesizer`
throwBacktrack
visitArgs do
p
addPrecCheck prec
let ctx ← read
modify fun st => { st with contCat := ctx.cat }
-- After visiting the nodes actually produced by the parser passed to `trailingNode`, we are positioned on the
-- left-most child, which is the term injected by `trailingNode` in place of the recursion. Left recursion is not an
-- issue for the parenthesizer, so we can think of this child being produced by `termParser 0`, or whichever Pratt
-- parser is calling us.
categoryParser.parenthesizer ctx.cat 0
@[combinatorParenthesizer Lean.Parser.symbol] def symbol.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.unicodeSymbol] def unicodeSymbol.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.symbol] def symbol.parenthesizer (sym : String) := visitToken
@[combinatorParenthesizer Lean.Parser.unicodeSymbol] def unicodeSymbol.parenthesizer (sym asciiSym : String) := visitToken
@[combinatorParenthesizer Lean.Parser.identNoAntiquot] def identNoAntiquot.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.rawIdent] def rawIdent.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.identEq] def identEq.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.nonReservedSymbol] def nonReservedSymbol.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.identEq] def identEq.parenthesizer (id : Name) := visitToken
@[combinatorParenthesizer Lean.Parser.nonReservedSymbol] def nonReservedSymbol.parenthesizer (sym : String) (includeIdent : Bool) := visitToken
@[combinatorParenthesizer Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken
@ -402,49 +397,41 @@ visitArgs $ do {
@[combinatorParenthesizer Lean.Parser.many]
def many.parenthesizer (p : Parenthesizer) : Parenthesizer := do
stx ← getCur;
visitArgs $ stx.getArgs.size.forM fun _ => p
let stx ← getCur
visitArgs $ stx.getArgs.size.forM fun _ => p
@[combinatorParenthesizer Lean.Parser.many1]
def many1.parenthesizer (p : Parenthesizer) : Parenthesizer := do
many.parenthesizer p
many.parenthesizer p
@[combinatorParenthesizer Lean.Parser.many1Unbox]
def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do
stx ← getCur;
if stx.getKind == nullKind then
many.parenthesizer p
else
p
let stx ← getCur
if stx.getKind == nullKind then
many.parenthesizer p
else
p
@[combinatorParenthesizer Lean.Parser.optional]
def optional.parenthesizer (p : Parenthesizer) : Parenthesizer := do
visitArgs p
visitArgs p
@[combinatorParenthesizer Lean.Parser.sepBy]
def sepBy.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do
stx ← getCur;
visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep
let stx ← getCur
visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0 then p else pSep
@[combinatorParenthesizer Lean.Parser.sepBy1] def sepBy1.parenthesizer := sepBy.parenthesizer
@[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
p
@[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
p
@[combinatorParenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := do
p
@[combinatorParenthesizer Lean.Parser.withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := do
p
@[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.setExpected]
def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer :=
p
def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.toggleInsideQuot]
def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer :=
p
def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p
@[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
@[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
@ -466,29 +453,26 @@ p
@[combinatorParenthesizer Lean.Parser.unquotedSymbol] def unquotedSymbol.parenthesizer := visitToken
@[combinatorParenthesizer Lean.Parser.interpolatedStr]
def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer :=
throwError "NIY"
def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := throwError "NIY"
@[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer :=
if c then t else e
if c then t else e
end Parenthesizer
open Parenthesizer
/-- Add necessary parentheses in `stx` parsed by `parser`. -/
def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :=
catchInternalId backtrackExceptionId
(do
(_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx };
pure st.stxTrav.cur)
(fun _ => throwError "parenthesize: uncaught backtrack exception")
catchInternalId backtrackExceptionId
(do
let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx }
pure st.stxTrav.cur)
(fun _ => throwError "parenthesize: uncaught backtrack exception")
def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0
def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command 0
@[builtinInit] private def regTraceClasses : IO Unit := do
registerTraceClass `PrettyPrinter.parenthesize;
pure ()
builtin_initialize registerTraceClass `PrettyPrinter.parenthesize
end PrettyPrinter
end Lean

7
tests/compiler/termparsertest1.lean
View file

@ -1,11 +1,12 @@
#lang lean4
import Lean
open Lean
open Lean.Parser
def testParser (input : String) : IO Unit :=
do
env ← mkEmptyEnvironment;
stx ← IO.ofExcept $ runParserCategory env `term input "<input>";
let env ← mkEmptyEnvironment;
let stx ← IO.ofExcept $ runParserCategory env `term input "<input>";
IO.println stx
def test (is : List String) : IO Unit :=
@ -15,7 +16,7 @@ is.forM $ fun input => do
def testParserFailure (input : String) : IO Unit :=
do
env ← mkEmptyEnvironment;
let env ← mkEmptyEnvironment;
match runParserCategory env `term input "<input>" with
| Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx))
| Except.error msg => IO.println ("failed as expected, error: " ++ msg)

5
tests/lean/envExtensionSealed.lean
View file

@ -1,15 +1,16 @@
#lang lean4
import Lean
namespace Lean
def ex1 : CoreM Nat := do
env ← getEnv;
let env ← getEnv
pure $ privateExt.getState env
#eval ex1
def ex2 : CoreM Nat := do
env ← getEnv;
let env ← getEnv
pure $ { privateExt with idx := 3 }.getState env -- Error
-- #eval ex2

8
tests/lean/envExtensionSealed.lean.expected.out
View file

@ -1,5 +1,3 @@
2
envExtensionSealed.lean:13:7: error: invalid structure notation source, not a structure
Lean.privateExt
which has type
Lean.EnvExtensionInterface.ext Lean.EnvExtensionInterfaceImp Nat
1
envExtensionSealed.lean:14:7: error: invalid {...} notation, source type is not of the form (C ...)
EnvExtensionInterfaceImp.1 Nat