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.

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

WIP:Format formalization #30

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
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
74 changes: 74 additions & 0 deletions Documentation/mds.bnf
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
;;
;; BNF formalization of MDS file grammar.
;;

;;
;; This specification takes some liberties to reduce absurd verbosity.
;; Care must be taken to ensure the extensions are explained in clear terms
;; accompanied by proofs if necessary. Given the 'classes', identifiers
;; between angle-brackets '<' and '>', as sets, set theory operations
;; will be used to describe other classes when convenient. To make things
;; clearer the regular equality sign will be used when the right side of a
;; class definition uses set operations and their notation. General use
;; of `where` will also be used for the addition of lexically scoped
;; classes when convenient.
;;

<whitespace> ::= " "
<ws> ::= <whitespace>

<optional-whitespace> ::= " " | ""
<opt-ws> ::= <optional-whitespace>

;; <newline> is used to stick each component/record of the format together.
;; As such, it is illegal inside <string>
<newline> ::= \n | \r\n | <whitespace> <newline>
<nl> ::= <newline>

;; Any characters that are not valid for <newline>.
<line> ::= <character'> | <character'> <string>
where
<character'> = <newline> △ <character>

;; Do we need all of utf8?
;; I tend to prefer generality, but maybe this is too much.
<character> ::= <set of all valid utf8>
Comment on lines +30 to +35
Copy link
Author

Choose a reason for hiding this comment

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

The main deviation I have made is here. Both <newline> △ <character> and <set of all valid utf8> (I should add codepoints to that text) are shortcuts, but otherwise we need to define our <string> class by including EVERY character we want to be valid in this file. Even with just lower and uppercase ascii that will add clutter, but if we want to make sure that Asian, Arabic, Jewish, etc... authors can add their real given name to MDS files, then the grammar should include more than ascii. Defining such a class without shortcuts would mean a seriously long class definition where we would need to include all of the characters (many have to be represented as strings, since they are multibyte).

NB. Multibyte strings don't break the C or ascii rules, so allowing all utf8 codepoints doesn't require any changes in your code (probably).

Copy link
Author

Choose a reason for hiding this comment

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

Given the massive class definitions that would be in the file without the Set based shortcuts I think it would be harder to implement parsers. At least, to make it easier we would need comments explaining what the giant right side content is, so we would essentially have some ad hoc implementation of these shortcuts as informal comments. Anyway, I just thought this perspective would help us think about it. If you think the current approach is fine, then I guess we have no issue. I will work on a formalization for the MDM files in whatever free time I get this week ;)

Copy link
Member

Choose a reason for hiding this comment

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

Let's keep it that way then. No need to be 100% BNF compliant.

I tried to explore other ways this evening, it's just not worth it. Your current implementation is good!

Copy link
Author

Choose a reason for hiding this comment

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

In case we want anything from the established extended BNFs https://en.m.wikipedia.org/wiki/Extended_Backus%E2%80%93Naur_form


<substrate> ::= <line>

<author> ::= <line>

<description> ::= <line>

<digit> ::= 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 0

<digits> ::= <digit> | <digit><digits>

<int> ::= -<digits> | <digits> | +<digits>

<double> ::= -<double'> | <double'> | +<digits>
where
<double'> ::= <digits>.<digits>

<atom> ::= <x> <ws> <y> <ws> <z> <ws> <id> <ws> <charge>
where
<x>,
<y>,
<z> ::= <double>
<id> ::= <int>
<charge> ::= <double>

<atom-block> ::= <atom> | <atom-block> <newline> <atom>

<bond> ::= <x> <ws> <y> <ws> <K>
where
<x>, <y> ::= <int>
<K> ::= <double>

<bond-block> ::= <bond> | <bond-block> <newline> <bond>

<mds> ::= <substrate> <nl>
<author> <nl>
<description> <nl>
<atom-block> <nl>
<bond-block> (<nl><eof>|<eof>)