From ca70b094a118c29451425b1438cac5d4f9b32925 Mon Sep 17 00:00:00 2001 From: hatzka Date: Sat, 21 Mar 2026 22:21:21 -0600 Subject: [PATCH] feat: modularize --- Parser.lean | 15 ++++++++------- Parser/Basic.lean | 9 ++++++--- Parser/Char.lean | 7 ++++--- Parser/Char/Basic.lean | 6 ++++-- Parser/Char/Numeric.lean | 6 ++++-- Parser/Char/Unicode.lean | 4 +++- Parser/Error.lean | 10 ++++++---- Parser/Parser.lean | 8 ++++++-- Parser/Prelude.lean | 7 ++++--- Parser/RegEx.lean | 5 +++-- Parser/RegEx/Basic.lean | 4 +++- Parser/RegEx/Compile.lean | 5 ++++- Parser/Stream.lean | 8 +++++--- 13 files changed, 60 insertions(+), 34 deletions(-) diff --git a/Parser.lean b/Parser.lean index 44c3621d..4e301a7f 100644 --- a/Parser.lean +++ b/Parser.lean @@ -2,11 +2,12 @@ Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.Basic -import Parser.Char -import Parser.Error -import Parser.Parser -import Parser.Prelude -import Parser.RegEx -import Parser.Stream +public import Parser.Basic +public import Parser.Char +public import Parser.Error +public import Parser.Parser +public import Parser.Prelude +public import Parser.RegEx +public import Parser.Stream diff --git a/Parser/Basic.lean b/Parser/Basic.lean index 75d7d125..67787b62 100644 --- a/Parser/Basic.lean +++ b/Parser/Basic.lean @@ -2,11 +2,14 @@ Copyright © 2022-2024 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module import Parser.Prelude -import Parser.Error -import Parser.Parser -import Parser.Stream +public import Parser.Error +public import Parser.Parser +public import Parser.Stream + +public section namespace Parser variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] diff --git a/Parser/Char.lean b/Parser/Char.lean index 2fa485b5..70742808 100644 --- a/Parser/Char.lean +++ b/Parser/Char.lean @@ -2,7 +2,8 @@ Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.Char.Basic -import Parser.Char.Numeric -import Parser.Char.Unicode +public import Parser.Char.Basic +public import Parser.Char.Numeric +public import Parser.Char.Unicode diff --git a/Parser/Char/Basic.lean b/Parser/Char/Basic.lean index 36fc71d9..9ee07e42 100644 --- a/Parser/Char/Basic.lean +++ b/Parser/Char/Basic.lean @@ -2,10 +2,12 @@ Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.Basic -import Parser.RegEx.Basic +public import Parser.Basic +public import Parser.RegEx.Basic +public section namespace Parser.Char variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] diff --git a/Parser/Char/Numeric.lean b/Parser/Char/Numeric.lean index 893735ae..b8ccdf5a 100644 --- a/Parser/Char/Numeric.lean +++ b/Parser/Char/Numeric.lean @@ -2,10 +2,12 @@ Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.Basic -import Parser.Char.Basic +public import Parser.Basic +public import Parser.Char.Basic +public section namespace Parser.Char.ASCII variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] diff --git a/Parser/Char/Unicode.lean b/Parser/Char/Unicode.lean index 37bd7ef7..b55ce237 100644 --- a/Parser/Char/Unicode.lean +++ b/Parser/Char/Unicode.lean @@ -2,9 +2,11 @@ Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.Char.Basic +public import Parser.Char.Basic +public section namespace Parser.Char.Unicode variable {ε σ m} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] diff --git a/Parser/Error.lean b/Parser/Error.lean index 3c64e0b6..50b5e119 100644 --- a/Parser/Error.lean +++ b/Parser/Error.lean @@ -2,9 +2,11 @@ Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module import Parser.Prelude -import Parser.Stream +public import Parser.Stream +public section /-! # Parser Error @@ -84,7 +86,7 @@ inductive Simple (σ τ) [Parser.Stream σ τ] | addMessage : Simple σ τ → Stream.Position σ → String → Simple σ τ -- The derive handler for `Repr` fails, this is a workaround. -private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : +protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : Simple σ τ → Nat → Std.Format | unexpected pos a, prec => Repr.addAppParen @@ -102,7 +104,7 @@ private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Strea (Std.Format.nest (if prec >= max_prec then 1 else 2) (Std.Format.text "Parser.Error.Simple.addMessage" ++ Std.Format.line ++ - reprPrec e max_prec ++ + Simple.reprPrec e max_prec ++ Std.Format.line ++ reprArg pos ++ Std.Format.line ++ @@ -112,7 +114,7 @@ private def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Strea instance (σ τ) [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] : Repr (Simple σ τ) where reprPrec := Simple.reprPrec -private def Simple.toString {σ τ} [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] : +protected def Simple.toString {σ τ} [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] : Simple σ τ → String | unexpected pos (some tok) => s!"unexpected token {repr tok} at {repr pos}" | unexpected pos none => s!"unexpected token at {repr pos}" diff --git a/Parser/Parser.lean b/Parser/Parser.lean index 80b6284c..42e6ce5c 100644 --- a/Parser/Parser.lean +++ b/Parser/Parser.lean @@ -2,10 +2,13 @@ Copyright © 2022-2024 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module import Parser.Prelude -import Parser.Error -import Parser.Stream +public import Parser.Error +public import Parser.Stream + +public section /-- Parser result type. -/ protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u @@ -19,6 +22,7 @@ protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u `ParserT ε σ τ` is a monad transformer to parse tokens of type `τ` from the stream type `σ` with error type `ε`. -/ +@[expose] def ParserT (ε σ τ : Type _) [Parser.Stream σ τ] [Parser.Error ε σ τ] (m : Type _ → Type _) (α : Type _) : Type _ := σ → m (Parser.Result ε σ α) diff --git a/Parser/Prelude.lean b/Parser/Prelude.lean index 4ba90a1c..8881c05c 100644 --- a/Parser/Prelude.lean +++ b/Parser/Prelude.lean @@ -3,8 +3,9 @@ Copyright © 2022 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights Released under Apache 2.0 license as described in the file LICENSE. -/ -import Batteries -import UnicodeBasic +module +public import Batteries +public import UnicodeBasic -instance : Std.Stream String.Slice Char where +public instance : Std.Stream String.Slice Char where next? s := s.front? >>= fun c => return (c, s.drop 1) diff --git a/Parser/RegEx.lean b/Parser/RegEx.lean index 4127337f..260c4980 100644 --- a/Parser/RegEx.lean +++ b/Parser/RegEx.lean @@ -2,6 +2,7 @@ Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.RegEx.Basic -import Parser.RegEx.Compile +public import Parser.RegEx.Basic +public import Parser.RegEx.Compile diff --git a/Parser/RegEx/Basic.lean b/Parser/RegEx/Basic.lean index b0674d11..02fcfc94 100644 --- a/Parser/RegEx/Basic.lean +++ b/Parser/RegEx/Basic.lean @@ -3,9 +3,11 @@ Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module -import Parser.Basic +public import Parser.Basic +public section namespace Parser /-- Type of regular expressions -/ diff --git a/Parser/RegEx/Compile.lean b/Parser/RegEx/Compile.lean index 92e54524..501c4f7a 100644 --- a/Parser/RegEx/Compile.lean +++ b/Parser/RegEx/Compile.lean @@ -2,10 +2,13 @@ Copyright © 2022-2023 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ +module import Parser.Char import Parser.Char.Numeric -import Parser.RegEx.Basic +public import Parser.RegEx.Basic + +public section /-! ## RegEx Syntax diff --git a/Parser/Stream.lean b/Parser/Stream.lean index e1ae572d..1d40c197 100644 --- a/Parser/Stream.lean +++ b/Parser/Stream.lean @@ -2,8 +2,9 @@ Copyright © 2022-2025 François G. Dorais, Kyrill Serdyuk, Emma Shroyer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ - -import Parser.Prelude +module +public import Parser.Prelude +public section /-! # Parser Stream @@ -42,6 +43,7 @@ attribute [inherit_doc Parser.Stream] Parser.Stream.getPosition Parser.Stream.se namespace Parser.Stream /-- Stream segment type. -/ +@[expose] def Segment (σ) [Parser.Stream σ τ] := Stream.Position σ × Stream.Position σ /-- Start position of stream segment. -/ @@ -55,7 +57,7 @@ abbrev Segment.stop [Parser.Stream σ τ] (s : Segment σ) := s.2 This wrapper uses the entire stream state as position information; this is not efficient. Always prefer tailored `Parser.Stream` instances to this default. -/ -@[nolint unusedArguments] +@[expose] def mkDefault (σ τ) [Std.Stream σ τ] := σ @[reducible]