diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eda612f..ef297bb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -20,8 +20,9 @@ jobs: - "4.8.0" - "4.9.0" - "4.10.0" - - "4.11.0-rc1" + - "4.11.0-rc3" - "nightly-2024-08-09" + - "nightly-2024-08-29" platform: - os: ubuntu-latest installer: | diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean index 14aa90c..a522d75 100644 --- a/src/compat/SubVerso/Compat.lean +++ b/src/compat/SubVerso/Compat.lean @@ -45,6 +45,28 @@ elab "%first_succeeding" "[" es:term,* "]" : term <= ty => do throwError m!"No alternative succeeded. Attempts were: " ++ indentD (MessageData.joinSep msgErrs Format.line) +scoped syntax "export_from_namespaces " "(" ident+ ") " "(" ident+ ")" : command + +elab_rules : command + | `(export_from_namespaces ($nss*) ($xs*)) => do + let env ← getEnv + let mut toAlias := #[] + for x in xs do + let x' := x.getId + let mut found := none + for ns in nss do + let ns' := ns.getId + let y := ns' ++ x' + if env.contains y then + found := some (ns, x) + break + if let some ok := found then + toAlias := toAlias.push ok + else + throwErrorAt x "'{x}' not found in namespaces {indentD <| toMessageData nss}" + for (ns, x) in toAlias do + Command.elabCommand <| ← `(export $ns ($x)) + open Command in elab "%if_bound" x:ident cmd:command : command => do if (← getEnv).contains x.getId then elabCommand cmd @@ -71,7 +93,17 @@ def refIdentCase (ri : Lsp.RefIdent) ] abbrev Parsec (α : Type) : Type := - %first_succeeding [(Lean.Parsec α : Type), (Lean.Parsec String.Iterator α : Type)] + %first_succeeding [ + (Lean.Parsec α : Type), + (Lean.Parsec String.Iterator α : Type), + (Std.Internal.Parsec String.Iterator α : Type) + ] + +namespace Parsec +export_from_namespaces + (Lean.Parsec.String Lean.Parsec Std.Internal.Parsec.String Std.Internal.Parsec) + (ws skipString skipChar many1Chars satisfy) +end Parsec def HashMap := %first_succeeding [Std.HashMap, Lean.HashMap] def HashSet := %first_succeeding [Std.HashSet, Lean.HashSet] diff --git a/src/examples/SubVerso/Examples/Slice.lean b/src/examples/SubVerso/Examples/Slice.lean index 4cbd96d..963d790 100644 --- a/src/examples/SubVerso/Examples/Slice.lean +++ b/src/examples/SubVerso/Examples/Slice.lean @@ -3,15 +3,15 @@ Copyright (c) 2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Data.Parsec +import Lean.Data.Json import Lean.Data.Position import Lean.Syntax import Lean.Elab.Command import SubVerso.Compat import SubVerso.Examples.Slice.Attribute +open Lean (SourceInfo Syntax Environment FileMap MonadEnv MonadError MonadFileMap getFileMap getEnv nullKind) -open Lean hiding Parsec HashMap open SubVerso.Compat (Parsec HashMap) namespace SubVerso.Examples.Slice @@ -71,7 +71,7 @@ deriving Repr private def SliceCommand.beginRange := SliceCommand.mk true private def SliceCommand.endRange := SliceCommand.mk false -open Lean.Parsec String in +open SubVerso.Compat.Parsec String in private def sliceCommand (range : String.Range) : Parsec SliceCommand := do ws skipString "!!"