From: Ferruccio Guidi Date: Sun, 3 Apr 2016 20:52:04 +0000 (+0000) Subject: - initial description of OSN X-Git-Tag: make_still_working~614 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=58e83e119ca3829affae2851cd512748131a766b;p=helm.git - initial description of OSN - ld_web: minor updates --- diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index bd3f4e23b..6d0237d98 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -146,5 +146,45 @@ +

Open Symbolic Notation

+ + Open Symbolic Notation (OSN) is an easy data-interchange textual format + based on symbolic expressions. + OSN is completely language independent but uses widely accepted conventions. + These features make OSN ideal for storing and exchanging tree-like data structures + in a lightweight manner. + + + An OSN text uses the UTF-8 character set + and contains the next tokens: + + + <symbol> a non-empty sequence of the 66 characters + - . 0..9 A..Z _ a..z + this sequence can represents the identifiers and the numerical constants of most programming languages + + <string> a sequence of characters wrapped with the delimiter " + every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ + the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ + morover, the escape sequences \x <two hexadecimal digits> and \u <four hexadecimal digits> + allow to specify a character by its code point + finally the escape sequences $ for U+0002 and $ for U+0003 are available + + <qualifier> the character : + + <left> each of the characters ( < [ { + this token starts a compound symbolic expression + + <right> each of the characters ) > ] } + this token ends a compound symbolic expression + + <ignored> each of the characters U+0009..U+000D U+0020 , ; = + these characters are ignored and separate the other tokens + + <reserved> any character not starting any other token + these characters are not allowed, + and those in the range U+0021..U+007E are + ! # $ % & ' * / ? @ \ ^ ` | ~ + +