search

gallais / idris-tparsec

TParsec - Total Parser Combinators in Idris
https://gallais.github.io/idris-tparsec/
GNU General Public License v3.0
93 stars 10 forks source link

add Lexer and lexing example #28

Closed clayrat closed 4 years ago

clayrat commented 4 years ago

Closes https://github.com/gallais/idris-tparsec/issues/22

gallais commented 4 years ago

More of a design discussion: I am not sure that insisting that the list of keywords is non empty actually brings anything to the table. I am tempted to drop this requirement when I finally update agdarsec to use tries.

clayrat commented 4 years ago

Yeah I was thinking about changing keywords to be a SortedMap instead.

clayrat commented 4 years ago

I've tried changing keywords to SortedMap but that creates problems for the typelevel test, because most of the declarations in that module are either private or export, so we can't evaluate the type completely. Also it doesn't buy us much since we only use it in init by immediately converting to List. OTOH a more specific type would guarantee key uniqueness, WDYT?

Also I've removed implicit declarations for LexParameters, but we'll have to bring most of them back for Idris2 to override the default erasure quantity.

clayrat commented 4 years ago

Btw, is there a reason to use b ** if b then Maybe Tok else () instead of something like Maybe (Maybe Tok)?

gallais commented 4 years ago

I think Maybe (Maybe Token) blurs the intent. Tbh it may be worth introducing a domain-specific sum type:

data MaybeBreaking : Set where
  IsBreaking : Maybe Tok -> MaybeBreaking
  IsNotBreaking : MaybeBreaking
gallais commented 4 years ago

OTOH a more specific type would guarantee key uniqueness, WDYT?

Oh I see. I had not thought of that. An alternative is to use a fresh list, a cute data structure defined by induction recursion for elements types with a decidable equality.

Edit: SortedMap did guarantee that the input was repetition free but had the user called fromList to construct it, they would lose all guarantees... So a list is at least as good as a SortedMap I think, and we can use a fresh list if we really want to enforce uniqueness of keywords.

clayrat commented 4 years ago

An alternative is to use a fresh list, a cute data structure defined by induction recursion for elements types with a decidable equality.

Could you point me to some examples of fresh lists? Anyway I think this can probably be handled in a separate PR.

gallais commented 4 years ago

I have opened a PR to the Agda standard library with an implementation of fresh lists together with documentation & an updated version of the lexer example using fresh lists.

https://github.com/agda/agda-stdlib/pull/878