From: Ferruccio Guidi Date: Thu, 21 Jul 2016 14:54:59 +0000 (+0000) Subject: - initial page for osn ... X-Git-Tag: make_still_working~551 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ed87c2c166f9f5db2729772e55154d7858dae4d6 - initial page for osn ... - some bug fixed --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 8f0cd608f..32510e3c2 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index e940d1f64..ab26a1c37 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -102,7 +102,7 @@ -
Contents of the Specification [spacer] +
Contents of the Specification [butterfly]
This specification comprises a collection of checked applications of λδ version 2. @@ -122,7 +122,7 @@ Helena 0.8. -
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -198,7 +198,7 @@ The MLTT1 component is started. -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -258,6 +258,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 70bbe5da7..18634b2f7 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -102,7 +102,7 @@
-
Abstract Syntax and Behavior [spacer] +
Abstract Syntax and Behavior [butterfly]
This is a summary of available syntactic items and reductions (block structure).
@@ -164,7 +164,7 @@
* In terms only.
-
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -251,7 +251,7 @@ Specification starts. -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -823,6 +823,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index d8c7887cd..0a049471c 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -114,7 +114,7 @@ **** Sort level k in terms only. --> -
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -144,29 +144,29 @@ sizes files - 150 + 154 characters - 128505 + 136477 nodes - 646562 + 748562 propositions theorems 45 lemmas - 476 + 500 total - 521 + 545 concepts declared 23 defined - 37 + 38 total - 60 + 61 @@ -335,7 +335,7 @@ λδ version 2 is started. -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -811,6 +811,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index accd82d10..4de89dc53 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -102,7 +102,7 @@
-
Documentation [spacer] +
Documentation [butterfly]
BibTeX database of λδ documentation: @@ -113,7 +113,7 @@ (revised 2015-09).
- [spacer] λδ version 3 (proposed)
+ [butterfly] λδ version 3 (proposed)
The main source of information is J3a.
@@ -136,7 +136,7 @@
- [spacer] λδ version 2 (active)
+ [butterfly] λδ version 2 (active)
The main source of information is R2c.
@@ -243,7 +243,7 @@
- [spacer] λδ version 1 (superseded)
+ [butterfly] λδ version 1 (superseded)
The main source of information is J1a. A summary is available in P1e. @@ -401,6 +401,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:48 +0200
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index 370730fda..6c56317af 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -102,7 +102,7 @@
-
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -177,7 +177,7 @@ Specification starts. -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -291,6 +291,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 5ac333cb3..dc3c8a194 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -102,7 +102,7 @@
-
Summary of the Specification [spacer] +
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -132,29 +132,29 @@ sizes files - 92 + 94 characters - 125262 + 129419 nodes - 265747 + 291484 propositions theorems - 33 + 35 lemmas - 588 + 610 total - 621 + 645 concepts declared - 60 + 61 defined - 63 + 64 total - 123 + 125 @@ -195,7 +195,7 @@ Specification starts. -
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -262,6 +262,7 @@ generic rt-transition counter rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 ) + rtc_isrc ( 𝐑𝐓⦃?, ?⦄ ) rtc_shift ( ↓? ) rtc_plus ( ? + ? ) @@ -303,9 +304,6 @@
- -
-
@@ -823,6 +821,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index e680bb04b..3a681dbe5 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -102,7 +102,7 @@
-
Tools [spacer] +
Tools [butterfly]
-
Foreword [spacer] +
Foreword [butterfly]
The formal systems of the λδ (\lambda\delta) family are typed λ-calculi aiming to support @@ -128,7 +128,7 @@ "Tools" menu → "Internet Options" entry → "General" tab → "Fonts" button.
-
Citations [spacer] +
Citations [butterfly]
This is a list of publications citing λδ documentation. @@ -183,7 +183,7 @@ -
Disclaimer [spacer] +
Disclaimer [butterfly]
The systems of the λδ family are not related intentionally to @@ -283,6 +283,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:48 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index a74a3a701..711995896 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -103,7 +103,7 @@
-
Milestones [spacer] +
Milestones [butterfly]
  • @@ -336,7 +336,7 @@
-
Visibility [spacer] +
Visibility [butterfly]
  • @@ -380,6 +380,6 @@

    -
    Last update: Mon, 27 Jun 2016 20:56:29 +0200
    +
    Last update: Thu, 21 Jul 2016 16:50:48 +0200
    diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html new file mode 100644 index 000000000..b67c477a3 --- /dev/null +++ b/helm/www/lambdadelta/osn.html @@ -0,0 +1,198 @@ + + + + + + + + + + \lambda\delta home page: Open Symbolic Notation + + + + + + +
    + + [Open Symbolic Notation logo] + +
    +
    Open Symbolic Notation
    +
    + [Spacer] +
    +
    + Open Symbolic Notation, abbreviated OSN, + is an easy and flexible data-interchange text format + intended for the lightweight representation of + generic abstract syntax trees in the domain of formal languages. + In order to meet these design goals, OSN pursues the following features. +
    +
      + +
    • + + Symbolic expressions + based on widely accepted syntactical conventions + provide for a lightweight and generic grammar, + which is both easy for machines to process, + and easy for humans to understand. + As a mean to support efficient information processing, + OSN aims at an economic representation of data + contrary to XML design goal 10. + Compared to other data-interchange formats based on symbolic expressions, + like canonical symbolic expressions, + representing arbitrary data in binary format is a secondary concern in the design of OSN, + as well as the support for canonicalization. + Apparently, these features fall outside the scope of OSN, + which targets the data structures of formal languages. + +
      • + +
      + +
    • + + Optionally qualified symbolic expressions + allow OSN texts to mix data from different domains preserving their own semantics + because name conflicts can be avoided. + As a consequence OSN documents are easy to extend in that + domain-specific OSN applications can work as expected even if + data from different domains is added to the text they process. + +
      • +       +
      + +
    • + + The US-ASCII character set, + extended to UTF-8 in + free-form text strings for the convenience of human readers, + makes OSN documents easy to visualize and transport over communication media. + OSN design aims at supporting application-independent standard encodings. + +
      • +       +
    +
    Grammar [butterfly] +
    +
    + An OSN text uses the UTF-8 character set + and contains the next seven tokens that we define in a very common EBNF variant. + Characters not starting a token are not allowed. + The ones in the range U+0021 ... U+007E are ! # $ % & * / ? @ \ ^ | ~ + and are available for extensions of OSN. +
    +
      +
    • + This token can represent the identifiers and the numerical constants of most programming languages: +
      + symbol = 1 * symbol-char ;
      symbol-char = '+' | '-' | '.' | '0' | ... | '9' | 'A' | ... | 'Z' | '_' | '`' | 'a' | ... | 'z' ;       +
      • +
      +
    • + This token contains free-form text with commonly accepted escape sequences: +
      + string = '"' , * ( string-char | "'" | '\' escape ) , '"' ;
      string-char = ( #0 | ... | #10FFFF ) - ( #0 | ... | #1F | "'" | '\' | '"' | #7F ) ;
      escape = 1 * space | '"' | "'" | '(' | ')' | '0' | '\' | 'a' | 'b' | 'e' | 'f' | 'n' | 'r' | 't' | ( 'u' , 4 * 4 hex ) | 'v' | ( 'x' , 2 * 2 hex ) ;
      space = #9 | ... | #D | #20 ;
      hex = '0' | ... | '9' | 'A' | ... | 'F' | 'a' | ... | 'f' ;       +
      • +
      +
    • + This token is a widely used alternative of the former token: +
      + string-alt = "'" , * ( string-char | '"' | '\' escape ) , "'" ; +
      • +
      +
    • + This token separates the qualifiers of a symbolic expression: +
      + sep = ':' ; +
      • +
      +
    • + This token starts a compound symbolic expression: +
      + open = '(' | '<' | '[' | '{' ; +
      • +
      +
    • + This token ends a compound symbolic expression: +
      + close = ')' | '>' | ']' | '}' ; +
      • +
      +
    • + This token is ignored and separates the other tokens: +
      + gap = space | ',' | ';' | '=' ; +
      • +
    +
    + The grammar of OSN is very liberal by design. + Spaces of the form 1 * gap can appear between any pair of tokens. +
    +
      +
    • + An OSN text: +
      + text = * q-expr ; +
      • +
      +
    • + A qualified symbolic expression: +
      + q-expr = * ( symbol , 1 * sep ) , expr ; +
      • +
      +
    • + An unqualified symbolic expression: +
      + expr = symbol | string | string-alt | ( open , text , close ) ; +
      • +
    +
    Semantics [butterfly] +
    +
    + Forthcoming ... +
    + +
    Implementation [butterfly] +
    +
    + Forthcoming ... +
    +
    + [Spacer] +
    +
    +
    +
    +
    + + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
    +
    +
    +
    +
    Last update: Thu, 21 Jul 2016 16:50:49 +0200
    + + diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 6112c2e5f..dbf2c18af 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -102,7 +102,7 @@
-
Computer-checked formal specifications [spacer] +
Computer-checked formal specifications [butterfly]
The systems of the λδ family are developed as machine-checked digital specifications, @@ -241,14 +241,14 @@
- [spacer] λδ version 3 (proposed)
+ [butterfly] λδ version 3 (proposed)
The formal specification of λδ version 3 is forthcoming.
- [spacer] λδ version 2 (active)
+ [butterfly] λδ version 2 (active)
The formal specification of λδ version 2 is available in the following formats: @@ -280,7 +280,7 @@
- [spacer] λδ version 1 (superseded)
+ [butterfly] λδ version 1 (superseded)
The formal specification of λδ version 1 is available in the following formats: @@ -378,6 +378,6 @@

-
Last update: Mon, 27 Jun 2016 20:56:29 +0200
+
Last update: Thu, 21 Jul 2016 16:50:49 +0200
diff --git a/helm/www/lambdadelta/web/home/osn.ldw.xml b/helm/www/lambdadelta/web/home/osn.ldw.xml index d83efaaaf..1f5601058 100644 --- a/helm/www/lambdadelta/web/home/osn.ldw.xml +++ b/helm/www/lambdadelta/web/home/osn.ldw.xml @@ -10,7 +10,7 @@ Open Symbolic Notation, abbreviated OSN, is an easy and flexible data-interchange text format intended for the lightweight representation of - generic abstract syntax trees in the domain of formal systems. + generic abstract syntax trees in the domain of formal languages. In order to meet these design goals, OSN pursues the following features. - - - - - - Syntax + Grammar An OSN text uses the UTF-8 character set @@ -62,7 +57,8 @@ and are available for extensions of OSN. - + This token can represent the identifiers and the numerical constants of most programming languages: + @@ -73,10 +69,10 @@ - - this token can represent the identifiers and the numerical constants of most programming languages; + - + This token contains free-form text with commonly accepted escape sequences: + @@ -121,10 +117,10 @@ - - this token contains free-form text with commonly accepted escape sequences; + - + This token is a widely used alternative of the former token: + @@ -134,45 +130,89 @@ - - this token is a widely used alternative of the former; + - + This token separates the qualifiers of a symbolic expression: + - - this token separates the qualifiers of a symbolic expression; + - + This token starts a compound symbolic expression: + - - this token starts a compound symbolic expression; + - + This token ends a compound symbolic expression: + - - this token ends a compound symbolic expression; + - + This token is ignored and separates the other tokens: + - - this token is ignored and separates the other tokens. + + The grammar of OSN is very liberal by design. + Spaces of the form can appear between any pair of tokens. + + An OSN text: + + + + + + + A qualified symbolic expression: + + + + + + + + + + An unqualified symbolic expression: + + + + + + + + + + + + + + + Semantics + + Forthcoming ... + + Implementation + + + Forthcoming ... + +
diff --git a/helm/www/lambdadelta/xslt/ld_web_library.xsl b/helm/www/lambdadelta/xslt/ld_web_library.xsl index f7fcb332e..b72f25fd1 100644 --- a/helm/www/lambdadelta/xslt/ld_web_library.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_library.xsl @@ -18,7 +18,7 @@ [spacer] diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 4be8878ff..56ab24894 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -12,6 +12,16 @@
+ +
+ + + + + +
+ +