From 427efd63045c98ec6381c0c044108ded870111fc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi 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 @@
[lambda_delta home]
cic:/matita/lambda_delta/Basic_2/ (λδ version 2)
[Spacer]
+
Summary of the contribution
+
Here is a numerical acount of the contribution's contents + and its timeline. +
+
categoryobjects


propositionstheorems39lemmas333
conceptsdeclared33defined46
+ + Support for abstract candidates of reducibility closed. + + + Confluence of context-sensitive parallel reduction closed. + + + Confluence of context-free parallel reduction closed. + + + Specification started. +
Logical structure of the contribution
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.
-
componentplanefiles


functionalreduction and type machinertmrtm_step ( ? ⇨ ? )


unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )

examples




native typing
nty


conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )


computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa

context-sensitive computationcprs (? ⊢ ? ➡* ?)



local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba

support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnftnftnf_trf

context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf


static typingstatic type assignmentstysty_liftsty_sty

local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba

atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_aaa

parameterssh


unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift


partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss


tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops

generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector



lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts

support for generic relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop


basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop


basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector



lift ( ⇧[?,?] ? ≡ ? )lift_lift

grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs


term hom.thomthom_thom


closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )


internal syntaxgenv




lenvlenv_weight ( #[?] )lenv_length ( |?| )


termterm_weight ( #[?] )term_simpleterm_vector


item



external syntaxaarity


+
componentplanefiles


functionalreduction and type machinertmrtm_step ( ? ⇨ ? )


unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )

examples




native typing
nty


conversioncontext-sensitive conversioncpcs ( ? ⊢ ? ⬌* ? )


computationstrongly normalizing computationcsn ( ⬇* ? )csn_crcsn_aaa

context-sensitive computationcprs (? ⊢ ? ➡* ?)



local env. ref. for abstract candidates of reducibilitylsubc ( ? [?] ⊑ ? )lsubc_ldroplsubc_ldropslsubc_lsuba

support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa
reducibilitycontext-sensitive reductionlcpr ( ? ⊢ ➡ ? )




cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltprcpr_cpr

context-free normal formstwhnf ( 𝐖𝐇𝐍[?] )tnf ( 𝐍[?] )tnf_tif

context-free reductionltpr ( ? ➡ ? )ltpr_ldrop



tpr ( ? ➡ ? )tpr_lifttpr_tpsstpr_tpr

context-free reducible formstrf ( 𝐑[?] )tif ( 𝐈[?] )

static typingstatic type assignmentstysty_liftsty_sty

local env. ref. for atomic arity assignmentlsuba ( ? ÷⊑ ? )lsuba_ldroplsuba_aaalsuba_lsuba

atomic arity assignmentaaa ( ? ⊢ ? ÷ ? )aaa_liftaaa_liftsaaa_aaa

parameterssh


unfoldterm inverse relocationdelift ( ? ⊢ ? [?,?] ≡ ? )delift_lift


partial unfoldltpss ( ? [?,?] ▶* ? )ltpss_ldropltpss_tpsltpss_ltpss


tpss ( ? ⊢ ? [?,?] ▶* ? )tpss_lifttpss_tpsstpss_ltps

generic local env. slicingldrops ( ⇩*[?] ? ≡ ? )ldrops_ldropldrops_ldrops

generic term relocationlifts_vector ( ⇧*[?] ? ≡ ? )lifts_lift_vector



lifts ( ⇧*[?] ? ≡ ? )lifts_liftlifts_lifts

support for generic relocationgr2 ( @ [ ? ] ? ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutionltps ( ? [?,?] ▶ ? )ltps_ldropltps_tpsltps_ltps


tps ( ? ⊢ ? [?,?] ▶ ? )tps_lifttps_tps

global env. slicinggdrop ( ⇩[?] ? ≡ ? )gdrop_gdrop


basic local env. slicingldrop ( ⇩[?,?] ? ≡ ? )ldrop_ldrop


basic term relocationlift_vector ( ⇧[?,?] ? ≡ ? )lift_lift_vector



lift ( ⇧[?,?] ? ≡ ? )lift_lift

grammarlocal env. ref. for substitutionlsubs ( ? [?,?] ≼ ? )lsubs_lsubs


term hom.thomthom_thom


closurescl_shift ( ? @ ? )cl_weight ( #[?,?] )


internal syntaxgenv




lenvlenv_weight ( #[?] )lenv_length ( |?| )


termterm_weight ( #[?] )term_simple ( 𝐒[?] )term_vector


item



external syntaxaarity


Physical structure of the contribution
The source files are grouped in directories, one for each component.
-
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-01-29+01:00
+
[Spacer]

[Valid XHTML 1.1][Valid CSS level 2][Generated from XML via XSL][PNG used here][Viewable with any browser]

Last update: 2012-02-01+01:00
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)" > + Summary of the contribution + Here is a numerical acount of the contribution's contents + and its timeline. + + + + Support for abstract candidates of reducibility closed. + + + Confluence of context-sensitive parallel reduction closed. + + + Confluence of context-free parallel reduction closed. + + + Specification started. + Logical structure of the contribution 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 @@ + +
  • + + +
+ +
-- 2.39.2