xml: first ld to xml stylesheets

Makefile: we now generate index.txt
dual_rg: automath encoding fixed

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index e235d685e707e803cf4a33c63a090f03d22297cb..fe670cb6cb87ae21017dee6f2022c8e5299585d9 100644 (file)
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -1,9 +1,17 @@
+lib/nUri.cmi: 
 lib/nUri.cmo: lib/nUri.cmi 
 lib/nUri.cmx: lib/nUri.cmi 
+lib/cps.cmo: 
+lib/cps.cmx: 
+lib/share.cmo: 
+lib/share.cmx: 
+lib/log.cmi: 
 lib/log.cmo: lib/cps.cmx lib/log.cmi 
 lib/log.cmx: lib/cps.cmx lib/log.cmi 
 lib/time.cmo: lib/log.cmi 
 lib/time.cmx: lib/log.cmx 
+automath/aut.cmo: 
+automath/aut.cmx: 
 automath/autProcess.cmi: automath/aut.cmx 
 automath/autProcess.cmo: automath/aut.cmx automath/autProcess.cmi 
 automath/autProcess.cmx: automath/aut.cmx automath/autProcess.cmi 
@@ -17,8 +25,10 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
 automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi 
 automath/autLexer.cmo: lib/log.cmi automath/autParser.cmi 
 automath/autLexer.cmx: lib/log.cmx automath/autParser.cmx 
+common/hierarchy.cmi: 
 common/hierarchy.cmo: lib/cps.cmx common/hierarchy.cmi 
 common/hierarchy.cmx: lib/cps.cmx common/hierarchy.cmi 
+common/output.cmi: 
 common/output.cmo: lib/log.cmi common/output.cmi 
 common/output.cmx: lib/log.cmx common/output.cmi 
 common/entity.cmo: lib/nUri.cmi automath/aut.cmx 

diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index 665972224cdcff6a47925ba76abd3a3f3018af74..96412768cc7cbdb171b666c101fcacab34c080b7 100644 (file)
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -35,3 +35,16 @@ hal: $(MAIN).opt
 xml-si: $(MAIN).opt
        @echo "  HELENA -u -x $(INPUT)"
        $(H)./$(MAIN).opt -u -x -s 2 -S 1 $(INPUT) > log.txt
+
+html:
+       @$(MAKE) --no-print-directory grundlagen/l/not.ld
+
+%.ld: BASEURL = --stringparam baseurl $(STATIC)
+
+%.ld:
+       @echo "  XSLT $@"
+       $(H)mkdir -p static/$(@D)
+       $(H)$(XSLT) -o static/$@.html $(BASEURL) xml/ld-html.xsl xml/$@.xml
+
+index:
+       find xml -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > xml/index.txt

diff --git a/helm/software/lambda-delta/Makefile.common b/helm/software/lambda-delta/Makefile.common
index 1af0e3abbd6ca9232e385809898b6ecf026aa74d..0cf1f84ac14c454e6cbf72e4a10daf6f3a22f068 100644 (file)
--- a/helm/software/lambda-delta/Makefile.common
+++ b/helm/software/lambda-delta/Makefile.common
@@ -1,5 +1,7 @@
 H=@
 
+STATIC = http://helm.cs.unibo.it/lambda-delta/static
+
 DIRECTORIES = $(shell cat Make)
 
 INCLUDES = $(DIRECTORIES:%=-I %) 
@@ -9,6 +11,7 @@ OCAMLOPT  = ocamlfind opt -linkpkg -package "$(REQUIRES)" $(INCLUDES)
 OCAMLLEX  = ocamllex.opt
 OCAMLYACC = ocamlyacc -v
 XMLLINT   = xmllint --noout
+XSLT      = xsltproc
 TAR       = tar -czf $(MAIN:%=%.tgz)
 
 define DIR_TEMPLATE

diff --git a/helm/software/lambda-delta/dual_rg/drg.ml b/helm/software/lambda-delta/dual_rg/drg.ml
index 1d94a26437708f409a98f2a5520097554471fd0a..e598a59867d40eb0adf175bfe9c35f324b2a4e74 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drg.ml
+++ b/helm/software/lambda-delta/dual_rg/drg.ml
@@ -28,9 +28,8 @@ and term = Sort of attrs * int              (* attrs, hierarchy index *)
          | LRef of attrs * int              (* attrs, position index *)
          | GRef of attrs * uri              (* attrs, reference *)
          | Cast of attrs * term * term      (* attrs, domain, element *)
-         | Proj of attrs * lenv * term      (* attrs, closure, scope *)
          | Appl of attrs * term list * term (* attrs, arguments, function *)
-        | Bind of bind * term              (* binder, scope *)
+        | Bind of lenv * term              (* closure, scope *)
 
 and lenv = bind list (* local environment *)
 

diff --git a/helm/software/lambda-delta/dual_rg/drgAut.ml b/helm/software/lambda-delta/dual_rg/drgAut.ml
index c978c4a636fe4c1b1e8a0bbf0c8a7d82dfa813c3..3b371afd72a5371a2804d4b623ad4df36f6e2d0f 100644 (file)
--- a/helm/software/lambda-delta/dual_rg/drgAut.ml
+++ b/helm/software/lambda-delta/dual_rg/drgAut.ml
@@ -108,7 +108,7 @@ let rec xlate_term f st lenv = function
    | A.Abst (name, w, t) ->
       let f ww = 
          let b = mk_abst name ww in
-        let f tt = f (D.Bind (b, tt)) in
+        let f tt = f (D.Bind ([b], tt)) in
          xlate_term f st (b :: lenv) t
       in
       xlate_term f st lenv w
@@ -160,7 +160,7 @@ let xlate_entity f st = function
       let f cnt = 
          let f qid = 
             let f ww =
-               let b = D.Abst ([], D.Proj ([], cnt, ww)) in
+               let b = D.Abst ([], D.Bind (cnt, ww)) in
               let entry = st.line, uri_of_qid qid, b in
               H.add st.henv (uri_of_qid qid) cnt;
               f {st with line = succ st.line} (Some entry)
@@ -175,7 +175,7 @@ let xlate_entity f st = function
          let f qid = 
             let f ww vv = 
               let a = if trans then [] else [D.Priv] in
-              let b = D.Abbr (a, D.Proj ([], cnt, D.Cast ([], ww, vv))) in
+              let b = D.Abbr (a, D.Bind (cnt, D.Cast ([], ww, vv))) in
               let entry = st.line, uri_of_qid qid, b in
               H.add st.henv (uri_of_qid qid) cnt;
               f {st with line = succ st.line} (Some entry)

diff --git a/helm/software/lambda-delta/xml/ld-html-entry.xsl b/helm/software/lambda-delta/xml/ld-html-entry.xsl
new file mode 100644 (file)
index 0000000..d6dbedd
--- /dev/null
+++ b/helm/software/lambda-delta/xml/ld-html-entry.xsl
@@ -0,0 +1,31 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:strip-space elements="ABST ABBR VOID"/>
+
+<xsl:template match="ABST">
+   <h2>
+      <xsl:text>Declaration:</xsl:text>
+      <xsl:call-template name="entry"/>
+   </h2>
+   <div><xsl:apply-templates/></div>
+</xsl:template>
+
+<xsl:template match="ABBR">
+   <h2>
+      <xsl:text>Definition:</xsl:text>
+      <xsl:call-template name="entry"/>
+   </h2>
+   <div><xsl:apply-templates/></div>
+</xsl:template>
+
+<xsl:template match="VOID">
+   <h2>
+      <xsl:text>Exclusion:</xsl:text>
+      <xsl:call-template name="entry"/>
+   </h2>
+   <div><xsl:apply-templates/></div>
+</xsl:template>
+
+</xsl:stylesheet>

diff --git a/helm/software/lambda-delta/xml/ld-html-library.xsl b/helm/software/lambda-delta/xml/ld-html-library.xsl
new file mode 100644 (file)
index 0000000..9e09b44
--- /dev/null
+++ b/helm/software/lambda-delta/xml/ld-html-library.xsl
@@ -0,0 +1,77 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:template name="sp">
+   <xsl:text> </xsl:text>
+</xsl:template>
+
+<xsl:template name="fs">
+   <xsl:text>.</xsl:text>
+</xsl:template>
+
+<xsl:template name="op">
+   <xsl:text>(</xsl:text>
+</xsl:template>
+
+<xsl:template name="cp">
+   <xsl:text>)</xsl:text>
+</xsl:template>
+
+<xsl:template name="oa">
+   <xsl:text>&lt;</xsl:text>
+</xsl:template>
+
+<xsl:template name="ca">
+   <xsl:text>&gt;</xsl:text>
+</xsl:template>
+
+<xsl:template name="cn">
+   <xsl:text>:</xsl:text>
+</xsl:template>
+
+<xsl:template name="eq">
+   <xsl:text>=</xsl:text>
+</xsl:template>
+
+<xsl:template name="lambda">
+   <xsl:text disable-output-escaping="yes">&amp;lambda;</xsl:text>
+</xsl:template>
+
+<xsl:template name="delta">
+   <xsl:text disable-output-escaping="yes">&amp;delta;</xsl:text>
+</xsl:template>
+
+<xsl:template name="chi">
+   <xsl:text disable-output-escaping="yes">&amp;chi;</xsl:text>
+</xsl:template>
+
+<xsl:template name="position">
+   <a name="" title="{@position}">
+      <xsl:value-of select="@name"/>
+   </a>
+</xsl:template>
+
+<xsl:template name="uri">
+   <xsl:variable name="url">
+      <xsl:value-of select="$baseurl"/>
+      <xsl:value-of select="substring-after(@uri,'ld:')"/>
+      <xsl:text>.html</xsl:text>
+   </xsl:variable>
+   <a href="{$url}"><xsl:value-of select="@name"/></a>
+</xsl:template>
+
+<xsl:template name="binder">
+   <xsl:value-of select="@name"/>
+</xsl:template>
+
+<xsl:template name="entry">
+   <xsl:call-template name="sp"/>
+   <xsl:call-template name="uri"/>
+   <xsl:call-template name="sp"/>
+   <xsl:call-template name="op"/>
+   <xsl:value-of select="@uri"/>
+   <xsl:call-template name="cp"/>
+</xsl:template>
+
+</xsl:stylesheet>

diff --git a/helm/software/lambda-delta/xml/ld-html-root.xsl b/helm/software/lambda-delta/xml/ld-html-root.xsl
new file mode 100644 (file)
index 0000000..a0b4907
--- /dev/null
+++ b/helm/software/lambda-delta/xml/ld-html-root.xsl
@@ -0,0 +1,55 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:strip-space elements="ENTRY"/>
+<xsl:template match="/">
+   <html><head>
+      <meta content="Ferruccio Guidi" name="author"/>
+      <meta content="lambda-delta digital library" name="description"/>
+      <title>lambda-delta digital library (LDDL)</title>
+      <link rel="shortcut icon" 
+            href="http://helm.cs.unibo.it/lambda-delta/download/crux-16.ico"
+      />
+   </head><body>
+      <h1 style="text-align: center;">
+         <a href="http://helm.cs.unibo.it/lambda-delta/">
+         <img style="border: 0px solid; width: 32px; height: 32px;" 
+             alt="[lambda-delta-home]"
+              title="lambda-delta home"
+             src="http://helm.cs.unibo.it/lambda-delta/download/crux-32.png"
+        /></a>
+      </h1>
+      <xsl:apply-templates/><h2/>
+      <div style="text-align: center;">
+         <a href="http://validator.w3.org/check?uri=referer">
+         <img alt="[Valid HTML 4.01 Transitional]"
+             title="Valid HTML 4.01 Transitional"
+              src="http://www.w3.org/Icons/valid-html401"
+              style="border: 0px solid ; width: 88px; height: 31px;"
+         /></a>
+        <a href="http://www.anybrowser.org/campaign/">
+        <img alt="[Use any browser here]"
+             title="Use any browser here"
+              src="http://www.cs.unibo.it/%7Efguidi/download/globe-trans.png"
+              style="border: 0px solid ; width: 147px; height: 42px;"
+        /></a>
+        <img style="width: 88px; height: 31px;"
+             alt="[png used here]"
+             title="png used here"
+             src="http://www.cs.unibo.it/%7Efguidi/download/PNGnow2.png"
+        />
+      </div>
+   </body></html>
+</xsl:template>
+
+<xsl:template match="ENTRY">
+   <xsl:apply-templates/><h2/>
+   <div>
+      Validation parameters:
+      sort hierarchy = "<xsl:value-of select="@hierarchy"/>",
+      kernel options = "<xsl:value-of select="@options"/>"
+   </div>
+</xsl:template>
+
+</xsl:stylesheet>

diff --git a/helm/software/lambda-delta/xml/ld-html-term.xsl b/helm/software/lambda-delta/xml/ld-html-term.xsl
new file mode 100644 (file)
index 0000000..a83c080
--- /dev/null
+++ b/helm/software/lambda-delta/xml/ld-html-term.xsl
@@ -0,0 +1,57 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:strip-space elements="Sort LRef GRef Cast Appl Abst Abbr Void"/>
+
+<xsl:template match="Sort">
+   <b><xsl:call-template name="position"/></b>
+</xsl:template>
+
+<xsl:template match="LRef">
+   <xsl:call-template name="position"/>
+</xsl:template>
+
+<xsl:template match="GRef">
+   <xsl:call-template name="uri"/>
+</xsl:template>
+
+<xsl:template match="Cast">
+   <xsl:call-template name="oa"/>
+   <xsl:apply-templates/>
+   <xsl:call-template name="ca"/>   
+   <xsl:call-template name="fs"/>   
+</xsl:template>
+
+<xsl:template match="Appl">
+   <xsl:call-template name="op"/>   
+   <xsl:apply-templates/>
+   <xsl:call-template name="cp"/>
+   <xsl:call-template name="fs"/>   
+</xsl:template>
+
+<xsl:template match="Abst">
+   <xsl:call-template name="lambda"/>
+   <xsl:value-of select="@name"/>
+   <xsl:call-template name="cn"/>   
+   <xsl:apply-templates/>
+   <xsl:call-template name="fs"/>   
+</xsl:template>
+
+<xsl:template match="Abbr">
+   <xsl:call-template name="delta"/>
+   <xsl:call-template name="binder"/>
+   <xsl:call-template name="eq"/>   
+   <xsl:apply-templates/>
+   <xsl:call-template name="fs"/>   
+</xsl:template>
+
+<xsl:template match="Void">
+   <xsl:call-template name="chi"/>
+   <xsl:call-template name="binder"/>
+   <xsl:apply-templates/>
+   <xsl:call-template name="fs"/>
+
+</xsl:template>
+
+</xsl:stylesheet>

diff --git a/helm/software/lambda-delta/xml/ld-html.xsl b/helm/software/lambda-delta/xml/ld-html.xsl
new file mode 100644 (file)
index 0000000..b66dd6f
--- /dev/null
+++ b/helm/software/lambda-delta/xml/ld-html.xsl
@@ -0,0 +1,20 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:param name="baseurl"/>
+
+<xsl:include href="ld-html-library.xsl"/>
+<xsl:include href="ld-html-term.xsl"/>
+<xsl:include href="ld-html-entry.xsl"/>
+<xsl:include href="ld-html-root.xsl"/>
+
+<xsl:output 
+   method="html"
+   doctype-system="html"
+   doctype-public="-//W3C//DTD HTML 4.01 Transitional//EN"
+   encoding="UTF-8"
+   indent="no"
+/>
+
+</xsl:stylesheet>