]> matita.cs.unibo.it Git - helm.git/commitdiff
we added summary and timeline to the Basic_2 page
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 1 Feb 2012 15:49:09 +0000 (15:49 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 1 Feb 2012 15:49:09 +0000 (15:49 +0000)
helm/www/lambda_delta/bin/xhtbl/Makefile
helm/www/lambda_delta/css/ld_web.css
helm/www/lambda_delta/css/xhtbl.css
helm/www/lambda_delta/ld_basic_2.html
helm/www/lambda_delta/web/home/ld_basic_2.ldw.xml
helm/www/lambda_delta/web/home/ld_basic_2.tbl [deleted file]
helm/www/lambda_delta/web/home/ld_basic_2_src.tbl [new file with mode: 0644]
helm/www/lambda_delta/xslt/ld_web_root.xsl

index 289c0cecd9f1f3ad5c936001d70a2d67cbc91aea..3cf252d5c118d8195efc1cd17b12d13eae837f7e 100644 (file)
@@ -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 $<"
index e553c3a3af9ca5c23b4a64222a3e6f03dc210631..9e7c3fc08fb76116394dad032eb996dc884ea03d 100644 (file)
@@ -41,6 +41,10 @@ div.text {
    text-align: left;
 }
 
+span.date {
+   font-weight: bold;
+}
+
 /* inline decorations *******************************************************/
 
 img.icon32 {
index 7c90c511d7c43b45bb70917f6660ceb7e2410627..7bc0a30d87c9130ed14b902403d79e50fb2e0b14 100644 (file)
@@ -31,6 +31,12 @@ td {
   text-transform: lowercase;
 }
 
+.number {
+  text-align: right; 
+  font-style: italic;
+  text-transform: lowercase;
+}
+
 /* cell borders *************************************************************/
 
 td.nnnn {
index ad5d7e51e1fe2066db03353066dac6f60376ef0d..da3068b9315087f86b6f1124f3df44e3d489513f 100644 (file)
     <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>
index 49d4094fe873663398dc3e96fec30f2388f6c695..39fda75ded49e99961f521cd029d08ecc48887d9 100644 (file)
@@ -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.tbl
deleted file mode 100644 (file)
index 7c65103..0000000
+++ /dev/null
@@ -1,191 +0,0 @@
-name "ld_basic_2_src"
-
-table {
-   class "grey"
-   [ { "component" * } {
-        [ { "plane" * } { 
-             [ "files" * ]
-         }
-        ]
-     }
-   ]
-   class "prune"
-   [ { "functional" * } {
-        [ { "reduction and type machine" * } { 
-             [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
-         }
-        ]
-        [ { "unfold" * } { 
-             [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
-         }
-        ]
-     }
-   ]
-   class "blue"
-   [ { "examples" * } {
-        [ { "" * } {
-            [ "" * ]
-         }
-        ]
-     }
-   ]
-   class "sky"
-   [ { "native typing" * } {
-        [ { "" * } {
-            [ "nty" * ]
-         }
-        ]
-     }
-   ]
-   class "cyan"
-   [ { "conversion" * } {
-        [ { "context-sensitive conversion" * } {
-            [ "cpcs ( ? ⊢ ? ⬌* ? )" * ]
-         }
-        ]
-     }
-   ]
-   class "water"
-   [ { "computation" * } {
-        [ { "strongly normalizing computation" * } {
-            [ "csn ( ⬇* ? )" "csn_cr" "csn_aaa" * ]
-         }
-        ]
-        [ { "context-sensitive computation" * } {
-            [ "cprs (? ⊢ ? ➡* ?)" * ]
-         }
-        ]
-        [ { "local env. ref. for abstract candidates of reducibility" * } {
-            [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ]
-         }
-        ]
-        [ { "support for abstract computation properties" * } {
-            [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ]
-          }
-       ]
-     }
-   ]
-   class "green"
-   [ { "reducibility" * } {
-        [ { "context-sensitive reduction" * } {
-            [ "lcpr ( ? ⊢ ➡ ? )" * ]
-            [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
-         }
-        ]
-        [ { "context-free normal forms" * } {
-            [ "twhnf" "tnf" "tnf_trf" * ]
-          }
-       ]
-        [ { "context-free reduction" * } {
-            [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" * ]
-            [ "tpr ( ? ➡ ? )"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
-          }
-       ]
-        [ { "context-free reducible forms" * } {
-            [ "trf" * ]
-          }
-       ]
-     }
-   ]
-   class "grass"
-   [ { "static typing" * } {
-        [ { "static type assignment" * } {
-            [ "sty" "sty_lift" "sty_sty" * ]
-          }
-       ]
-        [ { "local env. ref. for atomic arity assignment" * } {
-            [ "lsuba ( ? ÷⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ]
-         }
-        ]
-        [ { "atomic arity assignment" * } {
-            [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_aaa" * ]
-         }
-        ]
-        [ { "parameters" * } {
-             [ "sh" * ]
-          }
-        ]
-     }
-   ]
-   class "yellow"
-   [ { "unfold" * } {
-        [ { "term inverse relocation" * } {
-            [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ]
-          }
-       ]
-       [ { "partial unfold" * } {
-             [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
-            [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
-          }
-       ]
-       [ { "generic local env. slicing" * } { 
-            [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ]
-          }
-       ]
-       [ { "generic term relocation" * } {
-            [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
-            [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ] 
-          }
-       ]
-       [ { "support for generic relocation" * } { 
-            [ "gr2 ( @ [ ? ] ? ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
-          }
-       ]
-     }
-   ]
-   class "orange"   
-   [ { "substitution" * } { 
-        [ { "parallel substitution" * } {
-             [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
-            [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ]
-          }
-       ]
-       [ { "global env. slicing" * } {
-             [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
-          }
-       ]
-       [ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ]
-          }
-       ]
-        [ { "basic term relocation" * } {
-            [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
-             [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
-          }
-        ]
-     }
-   ]
-   class "red"   
-   [ { "grammar" * } {
-        [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
-          }
-       ]
-       [ { "term hom." * } {
-             [ "thom" "thom_thom" * ]
-          }
-       ]
-       [ { "closures" * } {
-             [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ]
-          }
-       ]
-        [ { "internal syntax" * } {
-             [ "genv" * ]
-            [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ]
-             [ "term" "term_weight ( #[?] )" "term_simple" "term_vector" * ]
-            [ "item" * ]
-         }
-       ] 
-        [ { "external syntax" * } {
-             [ "aarity" * ]
-         }
-       ] 
-     }
-   ]
-}
-
-class "component" { 0 }
-
-class "plane" { 1 }
-
-class "file" { 2 * }
diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl
new file mode 100644 (file)
index 0000000..6c3b479
--- /dev/null
@@ -0,0 +1,191 @@
+name "ld_basic_2_src"
+
+table {
+   class "grey"
+   [ { "component" * } {
+        [ { "plane" * } { 
+             [ "files" * ]
+         }
+        ]
+     }
+   ]
+   class "prune"
+   [ { "functional" * } {
+        [ { "reduction and type machine" * } { 
+             [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+         }
+        ]
+        [ { "unfold" * } { 
+             [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
+         }
+        ]
+     }
+   ]
+   class "blue"
+   [ { "examples" * } {
+        [ { "" * } {
+            [ "" * ]
+         }
+        ]
+     }
+   ]
+   class "sky"
+   [ { "native typing" * } {
+        [ { "" * } {
+            [ "nty" * ]
+         }
+        ]
+     }
+   ]
+   class "cyan"
+   [ { "conversion" * } {
+        [ { "context-sensitive conversion" * } {
+            [ "cpcs ( ? ⊢ ? ⬌* ? )" * ]
+         }
+        ]
+     }
+   ]
+   class "water"
+   [ { "computation" * } {
+        [ { "strongly normalizing computation" * } {
+            [ "csn ( ⬇* ? )" "csn_cr" "csn_aaa" * ]
+         }
+        ]
+        [ { "context-sensitive computation" * } {
+            [ "cprs (? ⊢ ? ➡* ?)" * ]
+         }
+        ]
+        [ { "local env. ref. for abstract candidates of reducibility" * } {
+            [ "lsubc ( ? [?] ⊑ ? )" "lsubc_ldrop" "lsubc_ldrops" "lsubc_lsuba" * ]
+         }
+        ]
+        [ { "support for abstract computation properties" * } {
+            [ "acp" "acp_cr ( ⦃?,?⦄ ϵ 〚?〛 )" "acp_aaa" * ]
+          }
+       ]
+     }
+   ]
+   class "green"
+   [ { "reducibility" * } {
+        [ { "context-sensitive reduction" * } {
+            [ "lcpr ( ? ⊢ ➡ ? )" * ]
+            [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpr" "cpr_cpr" * ]
+         }
+        ]
+        [ { "context-free normal forms" * } {
+            [ "twhnf ( 𝐖𝐇𝐍[?] )" "tnf ( 𝐍[?] )" "tnf_tif" * ]
+          }
+       ]
+        [ { "context-free reduction" * } {
+            [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" * ]
+            [ "tpr ( ? ➡ ? )"  "tpr_lift" "tpr_tpss" "tpr_tpr" * ]
+          }
+       ]
+        [ { "context-free reducible forms" * } {
+            [ "trf ( 𝐑[?] )" "tif ( 𝐈[?] )" * ]
+          }
+       ]
+     }
+   ]
+   class "grass"
+   [ { "static typing" * } {
+        [ { "static type assignment" * } {
+            [ "sty" "sty_lift" "sty_sty" * ]
+          }
+       ]
+        [ { "local env. ref. for atomic arity assignment" * } {
+            [ "lsuba ( ? ÷⊑ ? )" "lsuba_ldrop" "lsuba_aaa" "lsuba_lsuba" * ]
+         }
+        ]
+        [ { "atomic arity assignment" * } {
+            [ "aaa ( ? ⊢ ? ÷ ? )" "aaa_lift" "aaa_lifts" "aaa_aaa" * ]
+         }
+        ]
+        [ { "parameters" * } {
+             [ "sh" * ]
+          }
+        ]
+     }
+   ]
+   class "yellow"
+   [ { "unfold" * } {
+        [ { "term inverse relocation" * } {
+            [ "delift ( ? ⊢ ? [?,?] ≡ ? )" "delift_lift" * ]
+          }
+       ]
+       [ { "partial unfold" * } {
+             [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_ltpss" * ] 
+            [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_lift" "tpss_tpss" "tpss_ltps" * ]
+          }
+       ]
+       [ { "generic local env. slicing" * } { 
+            [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" "ldrops_ldrops" * ]
+          }
+       ]
+       [ { "generic term relocation" * } {
+            [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
+            [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" "lifts_lifts" * ] 
+          }
+       ]
+       [ { "support for generic relocation" * } { 
+            [ "gr2 ( @ [ ? ] ? ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
+          }
+       ]
+     }
+   ]
+   class "orange"   
+   [ { "substitution" * } { 
+        [ { "parallel substitution" * } {
+             [ "ltps ( ? [?,?] ▶ ? )" "ltps_ldrop" "ltps_tps" "ltps_ltps" * ]
+            [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ]
+          }
+       ]
+       [ { "global env. slicing" * } {
+             [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
+          }
+       ]
+       [ { "basic local env. slicing" * } {
+             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ]
+          }
+       ]
+        [ { "basic term relocation" * } {
+            [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
+             [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
+          }
+        ]
+     }
+   ]
+   class "red"   
+   [ { "grammar" * } {
+        [ { "local env. ref. for substitution" * } {
+             [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
+          }
+       ]
+       [ { "term hom." * } {
+             [ "thom" "thom_thom" * ]
+          }
+       ]
+       [ { "closures" * } {
+             [ "cl_shift ( ? @ ? )" "cl_weight ( #[?,?] )" * ]
+          }
+       ]
+        [ { "internal syntax" * } {
+             [ "genv" * ]
+            [ "lenv" "lenv_weight ( #[?] )" "lenv_length ( |?| )" * ]
+             [ "term" "term_weight ( #[?] )" "term_simple ( 𝐒[?] )" "term_vector" * ]
+            [ "item" * ]
+         }
+       ] 
+        [ { "external syntax" * } {
+             [ "aarity" * ]
+         }
+       ] 
+     }
+   ]
+}
+
+class "component" { 0 }
+
+class "plane" { 1 }
+
+class "file" { 2 * }
index 8222e1d941fdc8a58cd3a8fc982b054eac922ded..1375316f8f29e9cd05c8880d1d1aa572ef7efd2a 100644 (file)
    </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"/>