diff --git a/lake-manifest.json b/lake-manifest.json index b986c9f..b8a3c63 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/subverso.git", "type": "git", "subDir": null, - "rev": "771681e14ea506d41aa0c6969ba3a34727d64ab0", + "rev": "9f51556e14f14fbf7880b69e3cb1654e60ab66a2", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 6b26dd5..be51c72 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0-rc1 +leanprover/lean4:nightly-2024-04-07 diff --git a/src/verso-blog/Verso/Genre/Blog.lean b/src/verso-blog/Verso/Genre/Blog.lean index e3284a7..85bfbf8 100644 --- a/src/verso-blog/Verso/Genre/Blog.lean +++ b/src/verso-blog/Verso/Genre/Blog.lean @@ -66,7 +66,7 @@ def html : DirectiveExpander def blob : DirectiveExpander | #[.anon (.name blobName)], stxs => do if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents" - let actualName ← resolveGlobalConstNoOverloadWithInfo blobName + let actualName ← realizeGlobalConstNoOverloadWithInfo blobName let val ← ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[]) pure #[val] | _, _ => throwUnsupportedSyntax @@ -75,7 +75,7 @@ def blob : DirectiveExpander def inlineBlob : RoleExpander | #[.anon (.name blobName)], stxs => do if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents" - let actualName ← resolveGlobalConstNoOverloadWithInfo blobName + let actualName ← realizeGlobalConstNoOverloadWithInfo blobName let val ← ``(Inline.other (Blog.InlineExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[]) pure #[val] | _, _ => throwUnsupportedSyntax @@ -312,7 +312,7 @@ structure LeanBlockConfig where name : Option Name := none error : Option Bool := none -def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : ArgParse m LeanBlockConfig := +def LeanBlockConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanBlockConfig := LeanBlockConfig.mk <$> .positional `exampleContext .ident <*> .named `show .bool true <*> .named `keep .bool true <*> .named `name .name true <*> .named `error .bool true @[code_block_expander leanInit] @@ -405,7 +405,7 @@ structure LeanOutputConfig where severity : Option MessageSeverity summarize : Bool -def LeanOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : ArgParse m LeanOutputConfig := +def LeanOutputConfig.parser [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m LeanOutputConfig := LeanOutputConfig.mk <$> .positional `name output <*> .named `severity sev true <*> ((·.getD false) <$> .named `summarize .bool true) where output : ValDesc m Ident := { @@ -420,7 +420,7 @@ where description := open MessageSeverity in m!"The expected severity: '{``error}', '{``warning}', or '{``information}'", get := open MessageSeverity in fun | .name b => do - let b' ← resolveGlobalConstNoOverloadWithInfo b + let b' ← realizeGlobalConstNoOverloadWithInfo b if b' == ``MessageSeverity.error then pure MessageSeverity.error else if b' == ``MessageSeverity.warning then pure MessageSeverity.warning else if b' == ``MessageSeverity.information then pure MessageSeverity.information @@ -490,7 +490,7 @@ where open Lean Elab Command in elab "#defineLexerBlock" blockName:ident " ← " lexerName:ident : command => do - let lexer ← resolveGlobalConstNoOverloadWithInfo lexerName + let lexer ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo lexerName elabCommand <| ← `(@[code_block_expander $blockName] def $blockName : Doc.Elab.CodeBlockExpander | #[], str => do diff --git a/src/verso/Verso/Doc/ArgParse.lean b/src/verso/Verso/Doc/ArgParse.lean index a6099ff..b0b84dd 100644 --- a/src/verso/Verso/Doc/ArgParse.lean +++ b/src/verso/Verso/Doc/ArgParse.lean @@ -23,8 +23,6 @@ structure ValDesc (α) where description : MessageData get : ArgVal → m α - - inductive ArgParse (m) : Type → Type 1 where | fail (stx? : Option Syntax) (message? : Option MessageData) : ArgParse m α | pure (val : α) : ArgParse m α @@ -150,13 +148,13 @@ where return none end -variable {m} [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] +variable {m} [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] [MonadLiftT CoreM m] def ValDesc.bool : ValDesc m Bool where description := m!"{true} or {false}" get | .name b => do - let b' ← resolveGlobalConstNoOverloadWithInfo b + let b' ← liftM <| realizeGlobalConstNoOverloadWithInfo b if b' == ``true then pure true else if b' == ``false then pure false else throwErrorAt b "Expected 'true' or 'false'" diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index a69fe2a..9d92f1c 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -81,11 +81,19 @@ where @[combinator_formatter completeDocument] def completeDocument.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous -partial def findGenre [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m Unit - | `($g:ident) => discard <| resolveGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument - | `(($e)) => findGenre e +open Lean.Elab Command in +partial def findGenreCmd : Syntax → Lean.Elab.Command.CommandElabM Unit + | `($g:ident) => discard <| liftTermElabM <| realizeGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument + | `(($e)) => findGenreCmd e | _ => pure () +open Lean.Elab Term in +partial def findGenreTm : Syntax → TermElabM Unit + | `($g:ident) => discard <| realizeGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument + | `(($e)) => findGenreTm e + | _ => pure () + + def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM.State) : m Unit := do for r in internalRefs st'.linkDefs st.linkRefs do for stx in r.syntax do @@ -95,7 +103,7 @@ def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM. pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:document ":::::::" : command => open Lean Elab Command PartElabM DocElabM in do - findGenre genre + findGenreCmd genre let endTok := match ← getRef with | .node _ _ t => @@ -122,7 +130,7 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do - findGenre genre + findGenreTm genre let endPos := eof.raw.getTailPos?.get! let .node _ _ blocks := text.raw | dbg_trace "nope {ppSyntax text.raw}" throwUnsupportedSyntax @@ -162,7 +170,7 @@ def currentDocName [Monad m] [MonadEnv m] : m Name := do elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eoi : command => open Lean Elab Term Command PartElabM DocElabM in do - findGenre genre + findGenreCmd genre if eof.raw.isMissing then throwError "Syntax error prevents processing document" else diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean index 031feb9..d962895 100644 --- a/src/verso/Verso/Doc/Elab.lean +++ b/src/verso/Verso/Doc/Elab.lean @@ -95,7 +95,7 @@ def _root_.Verso.Syntax.role.expand : InlineExpander withRef inline <| withFreshMacroScope <| withIncRecDepth <| do let ⟨.node _ _ subjectArr⟩ := subjects | throwUnsupportedSyntax - let name ← resolveGlobalConstNoOverloadWithInfo name + let name ← realizeGlobalConstNoOverloadWithInfo name let exp ← roleExpandersFor name let argVals ← parseArgs args for e in exp do @@ -292,7 +292,7 @@ def _root_.Verso.Syntax.block_role.expand : BlockExpander := fun block => match block with | `(block|block_role{$name $args*}) => do withRef block <| withFreshMacroScope <| withIncRecDepth <| do - let name ← resolveGlobalConstNoOverloadWithInfo name + let name ← realizeGlobalConstNoOverloadWithInfo name let exp ← blockRoleExpandersFor name let argVals ← parseArgs args for e in exp do @@ -394,7 +394,7 @@ def _root_.Verso.Syntax.blockquote.expand : BlockExpander @[block_expander Verso.Syntax.codeblock] def _root_.Verso.Syntax.codeblock.expand : BlockExpander | ` => do - let name ← resolveGlobalConstNoOverloadWithInfo nameStx + let name ← realizeGlobalConstNoOverloadWithInfo nameStx let exp ← codeBlockExpandersFor name -- TODO typed syntax here let args ← parseArgs <| argsStx.map (⟨·⟩) @@ -417,7 +417,7 @@ def _root_.Verso.Syntax.codeblock.expand : BlockExpander @[block_expander Verso.Syntax.directive] def _root_.Verso.Syntax.directive.expand : BlockExpander | ` => do - let name ← resolveGlobalConstNoOverloadWithInfo nameStx + let name ← realizeGlobalConstNoOverloadWithInfo nameStx let exp ← directiveExpandersFor name -- TODO typed syntax here let args ← parseArgs <| argsStx.map (⟨·⟩) diff --git a/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean b/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean index cb8e449..6cbfe4c 100644 --- a/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean +++ b/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean @@ -15,7 +15,7 @@ unsafe def mkDocExpanderAttrUnsafe (attrName typeName : Name) (descr : String) ( descr := descr, valueTypeName := typeName, evalKey := fun _ stx => do - Elab.resolveGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx) + Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx) -- return (← Attribute.Builtin.getIdent stx).getId } attrDeclName diff --git a/src/verso/Verso/Method.lean b/src/verso/Verso/Method.lean index ffce0eb..d9990c1 100644 --- a/src/verso/Verso/Method.lean +++ b/src/verso/Verso/Method.lean @@ -49,7 +49,7 @@ def elabMethodDecl : CommandElab := fun stx => do | .node info ``method args => pure (some (.node info ``Parser.Command.declaration args)) | _ => pure none let decl' := open Parser.Command in - Syntax.node .none ``declaration #[decl[0][0], .node .none ``«def» decl[0].args[1:7]] + Syntax.node .none ``declaration #[decl[0][0], .node .none ``definition decl[0].args[1:7]] elabCommand decl' where inRoot : Name → Name