From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 4 Apr 2016 22:16:36 +0000 (+0000)
Subject: EBNF definition of OSN begins ...
X-Git-Tag: make_still_working~613
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=6b2413506392a9e62fdd8c560ab40d98ccc4ba08

EBNF definition of OSN begins ...
---

diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css
index 16fc502df..a735efdac 100644
--- a/helm/www/lambdadelta/css/ld_web.css
+++ b/helm/www/lambdadelta/css/ld_web.css
@@ -68,11 +68,6 @@ span.emph {
    font-size: medium;
 }
 
-span.date {
-   font-weight: bold;
-   font-size: medium;
-}
-
 /* tables *******************************************************************/
 
 table {
@@ -114,7 +109,7 @@ img.w3c {
    height: 32px; /* this should be 31px */
 }
 
-/* foreground colors (life cycle) *******************************************/
+/* foreground colors (life cycle, grammar) **********************************/
 
 .delta {
   color:#500000;
@@ -132,6 +127,10 @@ img.w3c {
   color:#000000;
 }
 
+.ebnf {
+  color:#000080;
+}
+
 /* background colors ********************************************************/
 
 .white {
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 6d0237d98..229c5e88b 100644
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -159,23 +159,50 @@
       and contains the next tokens:
    </body>
    <list><item>
-      &lt;symbol&gt; a non-empty sequence of the 66 characters + - . 0..9 A..Z _ a..z <newline/>
-      this sequence can represents the identifiers and the numerical constants of most programming languages 
+      <ebnf>
+         <prod of="symbol"/> <def/> 
+            <prod of="symbol_char"/> <prod of="symbol_char"/> <star/>
+         <stop/> <newline/>
+         <prod of="symbol_char"/> <def/>
+            <chr of="+"/> <or/> <chr of="-"/> <or/> <chr of="."/> <or/>
+            <chr of="0"/> <or/> <etc/> <or/> <chr of="9"/> <or/>
+            <chr of="A"/> <or/> <etc/> <or/> <chr of="Z"/> <or/>
+            <chr of="_"/> <or/> <chr of="a"/> <or/> <etc/> <or/> <chr of="z"/>
+         <stop/>
+      </ebnf> <newline/>
+      this token can represent the identifiers and the numerical constants of most programming languages;
    </item><item>
-      &lt;string&gt; a sequence of characters wrapped with the delimiter " <newline/>
+      <ebnf>
+         <prod of="string"/> <def/>
+            <chr of="&quot;"/> <open/>
+            <prod of="string_char"/> <or/>
+            <chr of="\"/> <prod of="escape"/>
+            <close/> <star/> <chr of="&quot;"/>
+         <stop/>
+      </ebnf> <newline/>
       every valid UTF-8 character whose code point is greater than U+001F is accepted eccept " \ <newline/>
       the next commonly accepted escape sequences are recognized: \0 \a \b \t \n \v \f \r \e \" \\ <newline/>
       morover, the escape sequences \x &lt;two hexadecimal digits&gt; and \u &lt;four hexadecimal digits&gt;
       allow to specify a character by its code point <newline/>
       finally the escape sequences \( for U+0002 and \) for U+0003 are available
    </item><item>
-      &lt;qualifier&gt; the character :
+      <ebnf>
+         <prod of="qualifier"/> <def/> <chr of=":"/> <stop/>
+      </ebnf>
    </item><item>
-      &lt;left&gt; each of the characters ( &lt; [ { <newline/>
-      this token starts a compound symbolic expression
+      <ebnf>
+         <prod of="left"/> <def/>
+            <chr of="("/> <or/> <chr of="&lt;"/> <or/> <chr of="["/> <or/> <chr of="{"/>
+         <stop/>
+      </ebnf> <newline/>
+      this token starts a compound symbolic expression;
    </item><item>
-      &lt;right&gt; each of the characters ) &gt; ] } <newline/>
-      this token ends a compound symbolic expression
+      <ebnf>
+         <prod of="right"/> <def/>
+            <chr of=")"/> <or/> <chr of="&gt;"/> <or/> <chr of="]"/> <or/> <chr of="}"/>
+         <stop/>
+      </ebnf> <newline/>
+      this token ends a compound symbolic expression;
    </item><item>
       &lt;ignored&gt; each of the characters U+0009..U+000D U+0020 , ; = <newline/>
       these characters are ignored and separate the other tokens
diff --git a/helm/www/lambdadelta/xslt/ld_web.xsl b/helm/www/lambdadelta/xslt/ld_web.xsl
index c5dc6b449..61c64b8fb 100644
--- a/helm/www/lambdadelta/xslt/ld_web.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web.xsl
@@ -10,6 +10,7 @@
 <xsl:strip-space elements="*"/>
 
 <xsl:include href="xhtbl.xsl"/>
+<xsl:include href="ld_web_ebnf.xsl"/>
 <xsl:include href="ld_web_library.xsl"/>
 <xsl:include href="ld_web_root.xsl"/>
 
diff --git a/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl b/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl
new file mode 100644
index 000000000..5599defa6
--- /dev/null
+++ b/helm/www/lambdadelta/xslt/ld_web_ebnf.xsl
@@ -0,0 +1,76 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0"
+                xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                xmlns:ld="http://lambdadelta.info/"
+                xmlns="http://www.w3.org/1999/xhtml"
+>
+
+<xsl:template match="ld:ebnf">
+   <span class="emph ebnf">
+      <xsl:apply-templates/>
+   </span>
+</xsl:template>
+
+<xsl:template match="ld:prod">
+   <xsl:text>&lt;</xsl:text>
+   <xsl:value-of select="@of"/>
+   <xsl:text>&gt;</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:def">
+   <xsl:text>=</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:str">
+   <xsl:text>"</xsl:text>
+   <xsl:value-of select="@of"/>
+   <xsl:text>"</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:chr">
+   <xsl:text>'</xsl:text>
+   <xsl:value-of select="@of"/>
+   <xsl:text>'</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:or">
+   <xsl:text>|</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:etc">
+   <xsl:text>...</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:open">
+   <xsl:text>(</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:close">
+   <xsl:text>)</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:star">
+   <xsl:text>*</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:plus">
+   <xsl:text>+</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:stop">
+   <xsl:text>;</xsl:text>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+</xsl:stylesheet>