Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add conversion functions to structural desc of disjoint matches #46

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add conversion functions to structural desc of disjoint matches #46

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 23 additions & 4 deletions src/TyRE/DisjointMatches.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ import Data.SnocList
import Data.List

infix 6 :+:,.+.
infix 7 :<,::

||| A data structure to represent succesful (disjoint) matches in a string.
||| A string is written here as alternatating sequence of substring and matches.
Expand Down Expand Up @@ -35,10 +34,30 @@ data DisjointMatches : Type -> Type where
Suffix : List Char -> DisjointMatches a
Cons : List Char -> a -> DisjointMatches a -> DisjointMatches a

public export
DisjointMatchesExplicit : Type -> Type
DisjointMatchesExplicit a = (List (List Char, a), List Char)

public export
Cast (DisjointMatches a) (DisjointMatchesExplicit a) where
cast (Suffix cs) = ([], cs)
cast (Cons cs x ps) =
let (dsx, cs) = cast {to = DisjointMatchesExplicit a} ps
in ((cs,x) :: dsx, cs)

public export
curryCast : List (List Char, a) -> List Char -> DisjointMatches a
curryCast [] cs = Suffix cs
curryCast ((ds, x) :: dsx) cs = Cons ds x $ curryCast dsx cs

public export
Cast (DisjointMatchesExplicit a) (DisjointMatches a) where
cast = uncurry curryCast

export
(::) : DisjointMatches a -> Char -> DisjointMatches a
(::) (Suffix cs) c = Suffix (c :: cs)
(::) (Cons cs parse tail) c = Cons (c :: cs) parse tail
(::) : Char -> DisjointMatches a -> DisjointMatches a
(::) c (Suffix cs) = Suffix (c :: cs)
(::) c (Cons cs parse tail) = Cons (c :: cs) parse tail

export
(.+.) : a -> DisjointMatches a -> DisjointMatches a
Expand Down
9 changes: 8 additions & 1 deletion src/TyRE/Parser.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,14 +38,21 @@ asDisjointMatches re cs greedy =
then runFromInit (runTillLastAccept cs Nothing)
else runFromInit (runTillFirstAccept cs)
matchesRec : List Char -> DisjointMatchesSnoc a
-> DisjointMatchesSnoc a
-> DisjointMatchesSnoc a
matchesRec [] dm = dm
matchesRec (x :: xs) dm with (parseFunction (x :: xs))
matchesRec (x :: xs) dm | (Nothing, _) = matchesRec xs (dm :< x)
matchesRec (x :: xs) dm | ((Just tree), tail) =
matchesRec tail (dm :+: tree)
in cast (matchesRec cs (Prefix [<]))

export
partial --we should be able to prove totality thanks to `consuming`
disjointMatches : (re : TyRE a) -> {auto 0 consuming : IsConsuming re}
-> List Char -> (greedy : Bool)
-> (List (List Char, a), List Char)
Comment on lines +51 to +53
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The API for our lib is in Data.Regex, so if you want to have this outside of this lib it should most probably be there. I think it's reasonable to drop the current asDisjointMatches from there.

Copy link
Collaborator Author

@ohad ohad Mar 23, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I started by thinking it should be dropped, but then I thought it does express the inductive pattern better, so maybe it's useful to export it. What do you think?

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, I see a benefit in using common data structures instead of ones defined in TyRE. It feels potentially more flexible and easier to understand for the end user. On the other hand, the type looks a bit less pleasant. Otherwise, I don't see much of a difference. I'd decide only for one of those to be exported, but I'm not sure which one it should be.

disjointMatches re str greedy = cast $ asDisjointMatches re str greedy

export
partial
getToken : (r : TyRE a) -> Stream Char -> (greedy : Bool)
Expand Down