From 427efd63045c98ec6381c0c044108ded870111fc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 1 Feb 2012 15:49:09 +0000
Subject: [PATCH] we added summary and timeline to the Basic_2 page
---
helm/www/lambda_delta/bin/xhtbl/Makefile | 20 ++++++++++--------
helm/www/lambda_delta/css/ld_web.css | 4 ++++
helm/www/lambda_delta/css/xhtbl.css | 6 ++++++
helm/www/lambda_delta/ld_basic_2.html | 21 +++++++++++++++++--
.../lambda_delta/web/home/ld_basic_2.ldw.xml | 17 +++++++++++++++
.../{ld_basic_2.tbl => ld_basic_2_src.tbl} | 6 +++---
helm/www/lambda_delta/xslt/ld_web_root.xsl | 7 +++++++
7 files changed, 67 insertions(+), 14 deletions(-)
rename helm/www/lambda_delta/web/home/{ld_basic_2.tbl => ld_basic_2_src.tbl} (95%)
diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile b/helm/www/lambda_delta/bin/xhtbl/Makefile
index 289c0cecd..3cf252d5c 100644
--- a/helm/www/lambda_delta/bin/xhtbl/Makefile
+++ b/helm/www/lambda_delta/bin/xhtbl/Makefile
@@ -10,21 +10,23 @@ include Makefile.common
XSLT = xsltproc
XHTBL = ./xhtbl.native
-XSLS = xhtbl.xsl ld_basic_2.xsl
+LDURL = http://lambda-delta.info/
+XSLDIR = ../../xslt/
+SRCDIR = ../../web/home/
+LDSRCDIR = ../../etc/lambda_delta/
+HOMEDIR = ../../
+
+TBLS = $(SRCDIR)ld_basic_2_src.tbl $(LDSRCDIR)Basic_2/ld_Basic_2_sum.tbl
+XSLS = xhtbl.xsl ld_basic_2_sum.xsl ld_basic_2_src.xsl
LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl
-LDURL = http://lambda-delta.info/
-XSLDIR = ../../xslt/
-SRCDIR = ../../web/home/
-HOMEDIR = ../../
-
%.html: BASEURL = --stringparam baseurl $(LDURL)
test: $(HOMEDIR)ld_basic_2.html
-$(XSLS:%=$(XSLDIR)%): $(SRCDIR)ld_basic_2.tbl $(XHTBL)
- @echo " XHTBL $<"
- $(H)$(XHTBL) -O $(XSLDIR) $<
+$(XSLS:%=$(XSLDIR)%): $(TBLS) $(XHTBL)
+ @echo " XHTBL $(notdir $(TBLS))"
+ $(H)$(XHTBL) -O $(XSLDIR) $(TBLS)
$(HOMEDIR)ld_basic_2.html: $(SRCDIR)ld_basic_2.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%)
@echo " XSLT $<"
diff --git a/helm/www/lambda_delta/css/ld_web.css b/helm/www/lambda_delta/css/ld_web.css
index e553c3a3a..9e7c3fc08 100644
--- a/helm/www/lambda_delta/css/ld_web.css
+++ b/helm/www/lambda_delta/css/ld_web.css
@@ -41,6 +41,10 @@ div.text {
text-align: left;
}
+span.date {
+ font-weight: bold;
+}
+
/* inline decorations *******************************************************/
img.icon32 {
diff --git a/helm/www/lambda_delta/css/xhtbl.css b/helm/www/lambda_delta/css/xhtbl.css
index 7c90c511d..7bc0a30d8 100644
--- a/helm/www/lambda_delta/css/xhtbl.css
+++ b/helm/www/lambda_delta/css/xhtbl.css
@@ -31,6 +31,12 @@ td {
text-transform: lowercase;
}
+.number {
+ text-align: right;
+ font-style: italic;
+ text-transform: lowercase;
+}
+
/* cell borders *************************************************************/
td.nnnn {
diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html
index ad5d7e51e..da3068b93 100644
--- a/helm/www/lambda_delta/ld_basic_2.html
+++ b/helm/www/lambda_delta/ld_basic_2.html
@@ -14,17 +14,34 @@
<link rel="shortcut icon" href="http://lambda-delta.info/images/crux_16.ico"/>
</head>
<body lang="en-US"><div class="spacer"><a href="http://lambda-delta.info/"><img class="icon32" alt="[lambda_delta home]" title="lambda_delta home" src="http://lambda-delta.info/images/crux_32.png"/></a></div><div class="head1">cic:/matita/lambda_delta/Basic_2/ (λδ version 2)</div><div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div>
+ <div class="head2">Summary of the contribution</div>
+ <div class="text">Here is a numerical acount of the contribution's contents
+ and its timeline.
+ </div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">category</td><td class="snns plane grey">objects</td><td class="snnn number grey"><br/></td><td class="snnn plane grey"><br/></td><td class="ssnn number grey"><br/></td></tr><tr><td class="snns component green">propositions</td><td class="snns plane green">theorems</td><td class="snnn number green">39</td><td class="snns plane green">lemmas</td><td class="ssnn number green">333</td></tr><tr><td class="snss component yellow">concepts</td><td class="snss plane yellow">declared</td><td class="snsn number yellow">33</td><td class="snss plane yellow">defined</td><td class="sssn number yellow">46</td></tr></tbody></table></div>
+
+ Support for abstract candidates of reducibility closed.
+
+
+ Confluence of context-sensitive parallel reduction closed.
+
+
+ Confluence of context-free parallel reduction closed.
+
+
+ Specification started.
+
<div class="head2">Logical structure of the contribution</div>
<div class="text">The source files are grouped in planes and components
according to the following table.
The notation for the relations or functions introduced in each file
is shown in parentheses.
</div>
- <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">functional</td><td class="snns plane prune">reduction and type machine</td><td class="snns file prune">rtm</td><td class="snnn file prune">rtm_step ( ? ⨠? )</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="nnns component prune"><br/></td><td class="snns plane prune">unfold</td><td class="snns file prune">lift ( â[?,?] ? )</td><td class="snnn file prune">subst ( [?â?] ? )</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">examples</td><td class="snns plane blue"><br/></td><td class="snns file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">native typing</td><td class="snns plane sky"><br/></td><td class="snns file sky">nty</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">conversion</td><td class="snns plane cyan">context-sensitive conversion</td><td class="snns file cyan">cpcs ( ? ⢠? â¬* ? )</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">computation</td><td class="snns plane water">strongly normalizing computation</td><td class="snns file water">csn ( â¬* ? )</td><td class="snnn file water">csn_cr</td><td class="snnn file water">csn_aaa</td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive computation</td><td class="snns file water">cprs (? ⢠? â¡* ?)</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">local env. ref. for abstract candidates of reducibility</td><td class="snns file water">lsubc ( ? [?] â ? )</td><td class="snnn file water">lsubc_ldrop</td><td class="snnn file water">lsubc_ldrops</td><td class="ssnn file water">lsubc_lsuba</td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">support for abstract computation properties</td><td class="snns file water">acp</td><td class="snnn file water">acp_cr ( â¦?,?⦠ϵ ã?ã )</td><td class="snnn file water">acp_aaa</td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">reducibility</td><td class="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⢠⡠? )</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">cpr ( ? ⢠? â¡ ? )</td><td class="snnn file green">cpr_lift</td><td class="snnn file green">cpr_ltpr</td><td class="ssnn file green">cpr_cpr</td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free normal forms</td><td class="snns file green">twhnf</td><td class="snnn file green">tnf</td><td class="snnn file green">tnf_trf</td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reduction</td><td class="snns file green">ltpr ( ? â¡ ? )</td><td class="snnn file green">ltpr_ldrop</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">tpr ( ? â¡ ? )</td><td class="snnn file green">tpr_lift</td><td class="snnn file green">tpr_tpss</td><td class="ssnn file green">tpr_tpr</td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reducible forms</td><td class="snns file green">trf</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">static type assignment</td><td class="snns file grass">sty</td><td class="snnn file grass">sty_lift</td><td class="snnn file grass">sty_sty</td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ÷â ? )</td><td class="snnn file grass">lsuba_ldrop</td><td class="snnn file grass">lsuba_aaa</td><td class="ssnn file grass">lsuba_lsuba</td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⢠? ÷ ? )</td><td class="snnn file grass">aaa_lift</td><td class="snnn file grass">aaa_lifts</td><td class="ssnn file grass">aaa_aaa</td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">term inverse relocation</td><td class="snns file yellow">delift ( ? ⢠? [?,?] â¡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss ( ? [?,?] â¶* ? )</td><td class="snnn file yellow">ltpss_ldrop</td><td class="snnn file yellow">ltpss_tps</td><td class="ssnn file yellow">ltpss_ltpss</td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⢠? [?,?] â¶* ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="ssnn file yellow">tpss_ltps</td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( â©*[?] ? â¡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( â§*[?] ? â¡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( â§*[?] ? â¡ ? )</td><td class="snnn file yellow">lifts_lift</td><td class="snnn file yellow">lifts_lifts</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @ [ ? ] ? â¡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? â ? â¡ ? )</td><td class="ssnn file yellow">gr2_gr2</td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">ltps ( ? [?,?] ⶠ? )</td><td class="snnn file orange">ltps_ldrop</td><td class="snnn file orange">ltps_tps</td><td class="ssnn file orange">ltps_ltps</td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">tps ( ? ⢠? [?,?] ⶠ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( â©[?] ? â¡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( â©[?,?] ? â¡ ? )</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( â§[?,?] ? â¡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( â§[?,?] ? â¡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">local env. ref. for substitution</td><td class="snns file red">lsubs ( ? [?,?] â¼ ? )</td><td class="snnn file red">lsubs_lsubs</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">term hom.</td><td class="snns file red">thom</td><td class="snnn file red">thom_thom</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @ ? )</td><td class="snnn file red">cl_weight ( #[?,?] )</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #[?] )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #[?] )</td><td class="snnn file red">term_simple</td><td class="ssnn file red">term_vector</td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
+ <div class="text"><table cellpadding="4" cellspacing="0"><tbody><tr><td class="snns component grey">component</td><td class="snns plane grey">plane</td><td class="snns file grey">files</td><td class="snnn file grey"><br/></td><td class="snnn file grey"><br/></td><td class="ssnn file grey"><br/></td></tr><tr><td class="snns component prune">functional</td><td class="snns plane prune">reduction and type machine</td><td class="snns file prune">rtm</td><td class="snnn file prune">rtm_step ( ? ⨠? )</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="nnns component prune"><br/></td><td class="snns plane prune">unfold</td><td class="snns file prune">lift ( â[?,?] ? )</td><td class="snnn file prune">subst ( [?â?] ? )</td><td class="snnn file prune"><br/></td><td class="ssnn file prune"><br/></td></tr><tr><td class="snns component blue">examples</td><td class="snns plane blue"><br/></td><td class="snns file blue"><br/></td><td class="snnn file blue"><br/></td><td class="snnn file blue"><br/></td><td class="ssnn file blue"><br/></td></tr><tr><td class="snns component sky">native typing</td><td class="snns plane sky"><br/></td><td class="snns file sky">nty</td><td class="snnn file sky"><br/></td><td class="snnn file sky"><br/></td><td class="ssnn file sky"><br/></td></tr><tr><td class="snns component cyan">conversion</td><td class="snns plane cyan">context-sensitive conversion</td><td class="snns file cyan">cpcs ( ? ⢠? â¬* ? )</td><td class="snnn file cyan"><br/></td><td class="snnn file cyan"><br/></td><td class="ssnn file cyan"><br/></td></tr><tr><td class="snns component water">computation</td><td class="snns plane water">strongly normalizing computation</td><td class="snns file water">csn ( â¬* ? )</td><td class="snnn file water">csn_cr</td><td class="snnn file water">csn_aaa</td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">context-sensitive computation</td><td class="snns file water">cprs (? ⢠? â¡* ?)</td><td class="snnn file water"><br/></td><td class="snnn file water"><br/></td><td class="ssnn file water"><br/></td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">local env. ref. for abstract candidates of reducibility</td><td class="snns file water">lsubc ( ? [?] â ? )</td><td class="snnn file water">lsubc_ldrop</td><td class="snnn file water">lsubc_ldrops</td><td class="ssnn file water">lsubc_lsuba</td></tr><tr><td class="nnns component water"><br/></td><td class="snns plane water">support for abstract computation properties</td><td class="snns file water">acp</td><td class="snnn file water">acp_cr ( â¦?,?⦠ϵ ã?ã )</td><td class="snnn file water">acp_aaa</td><td class="ssnn file water"><br/></td></tr><tr><td class="snns component green">reducibility</td><td class="snns plane green">context-sensitive reduction</td><td class="snns file green">lcpr ( ? ⢠⡠? )</td><td class="snnn file green"><br/></td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">cpr ( ? ⢠? â¡ ? )</td><td class="snnn file green">cpr_lift</td><td class="snnn file green">cpr_ltpr</td><td class="ssnn file green">cpr_cpr</td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free normal forms</td><td class="snns file green">twhnf ( ððð[?] )</td><td class="snnn file green">tnf ( ð[?] )</td><td class="snnn file green">tnf_tif</td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reduction</td><td class="snns file green">ltpr ( ? â¡ ? )</td><td class="snnn file green">ltpr_ldrop</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="nnns component green"><br/></td><td class="nnns plane green"><br/></td><td class="snns file green">tpr ( ? â¡ ? )</td><td class="snnn file green">tpr_lift</td><td class="snnn file green">tpr_tpss</td><td class="ssnn file green">tpr_tpr</td></tr><tr><td class="nnns component green"><br/></td><td class="snns plane green">context-free reducible forms</td><td class="snns file green">trf ( ð[?] )</td><td class="snnn file green">tif ( ð[?] )</td><td class="snnn file green"><br/></td><td class="ssnn file green"><br/></td></tr><tr><td class="snns component grass">static typing</td><td class="snns plane grass">static type assignment</td><td class="snns file grass">sty</td><td class="snnn file grass">sty_lift</td><td class="snnn file grass">sty_sty</td><td class="ssnn file grass"><br/></td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">local env. ref. for atomic arity assignment</td><td class="snns file grass">lsuba ( ? ÷â ? )</td><td class="snnn file grass">lsuba_ldrop</td><td class="snnn file grass">lsuba_aaa</td><td class="ssnn file grass">lsuba_lsuba</td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">atomic arity assignment</td><td class="snns file grass">aaa ( ? ⢠? ÷ ? )</td><td class="snnn file grass">aaa_lift</td><td class="snnn file grass">aaa_lifts</td><td class="ssnn file grass">aaa_aaa</td></tr><tr><td class="nnns component grass"><br/></td><td class="snns plane grass">parameters</td><td class="snns file grass">sh</td><td class="snnn file grass"><br/></td><td class="snnn file grass"><br/></td><td class="ssnn file grass"><br/></td></tr><tr><td class="snns component yellow">unfold</td><td class="snns plane yellow">term inverse relocation</td><td class="snns file yellow">delift ( ? ⢠? [?,?] â¡ ? )</td><td class="snnn file yellow">delift_lift</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">partial unfold</td><td class="snns file yellow">ltpss ( ? [?,?] â¶* ? )</td><td class="snnn file yellow">ltpss_ldrop</td><td class="snnn file yellow">ltpss_tps</td><td class="ssnn file yellow">ltpss_ltpss</td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">tpss ( ? ⢠? [?,?] â¶* ? )</td><td class="snnn file yellow">tpss_lift</td><td class="snnn file yellow">tpss_tpss</td><td class="ssnn file yellow">tpss_ltps</td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic local env. slicing</td><td class="snns file yellow">ldrops ( â©*[?] ? â¡ ? )</td><td class="snnn file yellow">ldrops_ldrop</td><td class="snnn file yellow">ldrops_ldrops</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">generic term relocation</td><td class="snns file yellow">lifts_vector ( â§*[?] ? â¡ ? )</td><td class="snnn file yellow">lifts_lift_vector</td><td class="snnn file yellow"><br/></td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="nnns plane yellow"><br/></td><td class="snns file yellow">lifts ( â§*[?] ? â¡ ? )</td><td class="snnn file yellow">lifts_lift</td><td class="snnn file yellow">lifts_lifts</td><td class="ssnn file yellow"><br/></td></tr><tr><td class="nnns component yellow"><br/></td><td class="snns plane yellow">support for generic relocation</td><td class="snns file yellow">gr2 ( @ [ ? ] ? â¡ ? )</td><td class="snnn file yellow">gr2_plus ( ? + ? )</td><td class="snnn file yellow">gr2_minus ( ? â ? â¡ ? )</td><td class="ssnn file yellow">gr2_gr2</td></tr><tr><td class="snns component orange">substitution</td><td class="snns plane orange">parallel substitution</td><td class="snns file orange">ltps ( ? [?,?] ⶠ? )</td><td class="snnn file orange">ltps_ldrop</td><td class="snnn file orange">ltps_tps</td><td class="ssnn file orange">ltps_ltps</td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">tps ( ? ⢠? [?,?] ⶠ? )</td><td class="snnn file orange">tps_lift</td><td class="snnn file orange">tps_tps</td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">global env. slicing</td><td class="snns file orange">gdrop ( â©[?] ? â¡ ? )</td><td class="snnn file orange">gdrop_gdrop</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic local env. slicing</td><td class="snns file orange">ldrop ( â©[?,?] ? â¡ ? )</td><td class="snnn file orange">ldrop_ldrop</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="snns plane orange">basic term relocation</td><td class="snns file orange">lift_vector ( â§[?,?] ? â¡ ? )</td><td class="snnn file orange">lift_lift_vector</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="nnns component orange"><br/></td><td class="nnns plane orange"><br/></td><td class="snns file orange">lift ( â§[?,?] ? â¡ ? )</td><td class="snnn file orange">lift_lift</td><td class="snnn file orange"><br/></td><td class="ssnn file orange"><br/></td></tr><tr><td class="snns component red">grammar</td><td class="snns plane red">local env. ref. for substitution</td><td class="snns file red">lsubs ( ? [?,?] â¼ ? )</td><td class="snnn file red">lsubs_lsubs</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">term hom.</td><td class="snns file red">thom</td><td class="snnn file red">thom_thom</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">closures</td><td class="snns file red">cl_shift ( ? @ ? )</td><td class="snnn file red">cl_weight ( #[?,?] )</td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="snns plane red">internal syntax</td><td class="snns file red">genv</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">lenv</td><td class="snnn file red">lenv_weight ( #[?] )</td><td class="snnn file red">lenv_length ( |?| )</td><td class="ssnn file red"><br/></td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">term</td><td class="snnn file red">term_weight ( #[?] )</td><td class="snnn file red">term_simple ( ð[?] )</td><td class="ssnn file red">term_vector</td></tr><tr><td class="nnns component red"><br/></td><td class="nnns plane red"><br/></td><td class="snns file red">item</td><td class="snnn file red"><br/></td><td class="snnn file red"><br/></td><td class="ssnn file red"><br/></td></tr><tr><td class="nnss component red"><br/></td><td class="snss plane red">external syntax</td><td class="snss file red">aarity</td><td class="snsn file red"><br/></td><td class="snsn file red"><br/></td><td class="sssn file red"><br/></td></tr></tbody></table></div>
<div class="head2">Physical structure of the contribution</div>
<div class="text">The source files are grouped in directories, one for each
component.
</div>
- <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-01-29+01:00</div>
+ <div class="spacer"><img class="rule" alt="[Spacer]" title="lambda_delta rainbow rule" src="http://lambda-delta.info/images/rainbow.png"/></div><div class="spacer"><br/></div><div class="spacer"><a href="http://validator.w3.org/check?uri=referer"><img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue"/></a><a href="http://jigsaw.w3.org/css-validator/check/referer"><img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue"/></a><a href="http://www.w3.org/XML/"><img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambda-delta.info/images/xml_xsl2.png"/></a><a href="http://www.w3.org/Graphics/PNG/"><img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambda-delta.info/images/PNGnow2.png"/></a><a href="http://www.anybrowser.org/campaign/"><img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png"/></a></div><div class="spacer"><br/></div><div class="spacer">Last update: 2012-02-01+01:00</div>
</body>
</html>
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
index 49d4094fe..39fda75de 100644
--- a/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
+++ b/helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
@@ -5,6 +5,23 @@
title = "lambda_delta version 2"
head = "cic:/matita/lambda_delta/Basic_2/ (λδ version 2)"
>
+ <ld:section>Summary of the contribution</ld:section>
+ <ld:body>Here is a numerical acount of the contribution's contents
+ and its timeline.
+ </ld:body>
+ <ld:table name="ld_Basic_2_sum"/>
+ <ld:news date="2012 January 27.">
+ Support for abstract candidates of reducibility closed.
+ </ld:news>
+ <ld:news date="2011 September 21.">
+ Confluence of context-sensitive parallel reduction closed.
+ </ld:news>
+ <ld:news date="2011 September 6.">
+ Confluence of context-free parallel reduction closed.
+ </ld:news>
+ <ld:news date="2011 April 17.">
+ Specification started.
+ </ld:news>
<ld:section>Logical structure of the contribution</ld:section>
<ld:body>The source files are grouped in planes and components
according to the following table.
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl
similarity index 95%
rename from helm/www/lambda_delta/web/home/ld_basic_2.tbl
rename to helm/www/lambda_delta/web/home/ld_basic_2_src.tbl
index 7c65103fb..6c3b47928 100644
--- a/helm/www/lambda_delta/web/home/ld_basic_2.tbl
+++ b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl
@@ -73,7 +73,7 @@ table {
}
]
[ { "context-free normal forms" * } {
- [ "twhnf" "tnf" "tnf_trf" * ]
+ [ "twhnf ( ððð[?] )" "tnf ( ð[?] )" "tnf_tif" * ]
}
]
[ { "context-free reduction" * } {
@@ -82,7 +82,7 @@ table {
}
]
[ { "context-free reducible forms" * } {
- [ "trf" * ]
+ [ "trf ( ð[?] )" "tif ( ð[?] )" * ]
}
]
}
@@ -172,7 +172,7 @@ table {
[ { "internal syntax" * } {
[ "genv" * ]
[ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ]
- [ "term" "term_weight ( #[?] )" "term_simple" "term_vector" * ]
+ [ "term" "term_weight ( #[?] )" "term_simple ( ð[?] )" "term_vector" * ]
[ "item" * ]
}
]
diff --git a/helm/www/lambda_delta/xslt/ld_web_root.xsl b/helm/www/lambda_delta/xslt/ld_web_root.xsl
index 8222e1d94..1375316f8 100644
--- a/helm/www/lambda_delta/xslt/ld_web_root.xsl
+++ b/helm/www/lambda_delta/xslt/ld_web_root.xsl
@@ -20,6 +20,13 @@
</div>
</xsl:template>
+<xsl:template match="ld:news">
+ <ul><li>
+ <span class="date"><xsl:value-of select="@date"/></span>
+ <xsl:apply-templates/>
+ </li></ul>
+</xsl:template>
+
<xsl:template match="ld:table">
<div class="text">
<xsl:call-template name="xhtbl"/>
--
2.39.2