From 7111eb4d79b08a851d43891e3df64a6fa463fdcd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Oct 2020 13:30:43 -0700 Subject: [PATCH] chore: move to new frontend --- src/Lean/Attributes.lean | 468 ++++++++-------- src/Lean/CoreM.lean | 118 ++-- src/Lean/Delaborator.lean | 2 +- src/Lean/Exception.lean | 101 ++-- src/Lean/Message.lean | 325 ++++++----- src/Lean/PrettyPrinter/Formatter.lean | 503 +++++++++--------- src/Lean/PrettyPrinter/Meta.lean | 4 +- src/Lean/PrettyPrinter/Parenthesizer.lean | 442 ++++++++------- tests/compiler/termparsertest1.lean | 7 +- tests/lean/envExtensionSealed.lean | 5 +- .../lean/envExtensionSealed.lean.expected.out | 8 +- 11 files changed, 963 insertions(+), 1020 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index fbc4408413..a8e505e451 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -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 diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 7014bed464..286447c324 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -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 diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean index 964d2b6ee2..c757860293 100644 --- a/src/Lean/Delaborator.lean +++ b/src/Lean/Delaborator.lean @@ -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!) diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index c772b3b29f..c77a7187e9 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -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 diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index ab6846a6dc..1c4a2adc4b 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -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 => "" | 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 diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index bbf6066dc1..8b85b18b3e 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Meta.lean b/src/Lean/PrettyPrinter/Meta.lean index 1927ad1e53..5c6808f7d4 100644 --- a/src/Lean/PrettyPrinter/Meta.lean +++ b/src/Lean/PrettyPrinter/Meta.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index d351410f34..7b1e864751 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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 diff --git a/tests/compiler/termparsertest1.lean b/tests/compiler/termparsertest1.lean index 858b2acf9c..a5fcfb643b 100644 --- a/tests/compiler/termparsertest1.lean +++ b/tests/compiler/termparsertest1.lean @@ -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 ""; +let env ← mkEmptyEnvironment; +let stx ← IO.ofExcept $ runParserCategory env `term 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 "" with | Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx)) | Except.error msg => IO.println ("failed as expected, error: " ++ msg) diff --git a/tests/lean/envExtensionSealed.lean b/tests/lean/envExtensionSealed.lean index 22ed3e1018..248f3d72d9 100644 --- a/tests/lean/envExtensionSealed.lean +++ b/tests/lean/envExtensionSealed.lean @@ -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 diff --git a/tests/lean/envExtensionSealed.lean.expected.out b/tests/lean/envExtensionSealed.lean.expected.out index 607c0709af..d6f283d6da 100644 --- a/tests/lean/envExtensionSealed.lean.expected.out +++ b/tests/lean/envExtensionSealed.lean.expected.out @@ -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