From ce747c4d4c3a087e1f59dca81b7b4962ffa8e02b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 9 Feb 2012 19:51:29 +0000 Subject: [PATCH] - design table for Basic_2 - summary table for Basic_2 and Ground_2 - some additions to the Basic_2 file table - some new cell styles for xhtbl - syntax cor comments added to xhtbl - some improvements in the Makefiles --- helm/www/lambda_delta/Makefile | 3 +- helm/www/lambda_delta/bin/xhtbl/Makefile | 15 ++-- helm/www/lambda_delta/bin/xhtbl/textLexer.mll | 6 ++ helm/www/lambda_delta/css/xhtbl.css | 4 + helm/www/lambda_delta/ld_basic_2.html | 27 +++++-- .../lambda_delta/web/home/ld_basic_2.ldw.xml | 21 ++++- .../lambda_delta/web/home/ld_basic_2_blk.tbl | 45 +++++++++++ .../lambda_delta/web/home/ld_basic_2_src.tbl | 16 ++-- .../www/lambda_delta/xslt/ld_Ground_2_sum.xsl | 38 +++++++++ helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl | 80 +++++++++++++++++++ 10 files changed, 229 insertions(+), 26 deletions(-) create mode 100644 helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl create mode 100644 helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl create mode 100644 helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl diff --git a/helm/www/lambda_delta/Makefile b/helm/www/lambda_delta/Makefile index ae43f1cf4..982c1ff1d 100644 --- a/helm/www/lambda_delta/Makefile +++ b/helm/www/lambda_delta/Makefile @@ -77,8 +77,7 @@ install-bib: $(BIB:%=$(BIBDIR)/%) $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt) www: - @echo " UPDATE HOME PAGES" - $(H)$(MAKE) --no-print-directory -C $(XHTBLDIR) test + $(H)$(MAKE) --no-print-directory -C $(XHTBLDIR) www up: @echo " UPDATE $(REMOTE):$(RDIR)" diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile b/helm/www/lambda_delta/bin/xhtbl/Makefile index ee86004f7..79a056af5 100644 --- a/helm/www/lambda_delta/bin/xhtbl/Makefile +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile @@ -15,19 +15,20 @@ XSLDIR = ../../xslt/ SRCDIR = ../../web/home/ LDSRCDIR = ../../etc/lambda_delta/ HOMEDIR = ../../ +TBLDIRS = $(SRCDIR) $(LDSRCDIR) -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 +TBLS = $(shell find $(TBLDIRS) -name "*.tbl") +XSLS = xhtbl.xsl $(patsubst %.tbl, %.xsl, $(notdir $(TBLS))) +LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl %.html: BASEURL = --stringparam baseurl $(LDURL) -test: $(HOMEDIR)ld_basic_2.html +www: $(HOMEDIR)ld_basic_2.html $(XSLS:%=$(XSLDIR)%): $(TBLS) $(XHTBL) - @echo " XHTBL $(notdir $(TBLS))" + @echo " XHTBL *.tbl" $(H)$(XHTBL) -O $(XSLDIR) $(TBLS) -$(HOMEDIR)ld_basic_2.html: $(SRCDIR)ld_basic_2.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%) - @echo " XSLT $<" +$(HOMEDIR)ld_basic_2.html: $(SRCDIR)ld_basic_2.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%) + @echo " XSLT $(notdir $<)" $(H)$(XSLT) -o $@ $(BASEURL) $(XSLDIR)ld_web.xsl $< diff --git a/helm/www/lambda_delta/bin/xhtbl/textLexer.mll b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll index f1ea9a61a..2ed6742c9 100644 --- a/helm/www/lambda_delta/bin/xhtbl/textLexer.mll +++ b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll @@ -25,4 +25,10 @@ rule token = parse | "name" { out "name"; TP.NAME } | "table" { out "table"; TP.TABLE } | "class" { out "class"; TP.CSS } + | "(*" { block lexbuf; token lexbuf } | eof { TP.EOF } +and block = parse + | "*)" { () } + | "(*" { block lexbuf; block lexbuf } + | STR { block lexbuf } + | _ { block lexbuf } diff --git a/helm/www/lambda_delta/css/xhtbl.css b/helm/www/lambda_delta/css/xhtbl.css index 7bc0a30d8..f58db47c3 100644 --- a/helm/www/lambda_delta/css/xhtbl.css +++ b/helm/www/lambda_delta/css/xhtbl.css @@ -16,6 +16,10 @@ td { /* content types ************************************************************/ +.text { + font-style: normal; +} + .component { font-style: italic; text-transform: capitalize; diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 484bdf19d..95ea6d8e1 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -14,11 +14,22 @@
[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 +
System's Syntax and Behavior
+
This is a summary of the "block structure" + of the System's syntactic items and reductions. +
+
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
+
* In terms only. + ** In terms and local environments only. + *** In global environments only. + **** Sort level k in terms only. +
+ +
Summary of the Specification
+
Here is a numerical acount of the specification's contents and its timeline.
-
categoryobjects


propositionstheorems39lemmas336
conceptsdeclared33defined46
+
categoryobjects


propositionstheorems41lemmas369
conceptsdeclared33defined50
@@ -31,17 +42,19 @@ -
Logical structure of the contribution
+ +
Logical Structure of the Specification
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_tpsscpr_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
+
componentplanefiles



functionalreduction and type machinertmrtm_step ( ? ⇨ ? )



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


examples





native typing
nty



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



computationstrongly normalizing computationcsn ( ⬇* ? )csn_liftcsn_crcsn_aaa

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


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

support for abstract computation propertiesacpacp_cr ( ⦃?,?⦄ ϵ 〚?〛 )acp_aaa

reducibilitycontext-sensitive normal formscnf ( ? ⊢ 𝐍[?] )cnf_lift



context-sensitive reductionlcpr ( ? ⊢ ➡ ? )





cpr ( ? ⊢ ? ➡ ? )cpr_liftcpr_ltpsscpr_ltprcpr_cpr

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


context-free reductionltpr ( ? ➡ ? )ltpr_ldropltpr_tps



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.thom ( ? ≈ ? )thom_thom



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



internal syntaxgenv





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



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


item




external syntaxaarity



+ +
Physical Structure of the Specification
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-02-02+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-09+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 39fda75de..117726fba 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,8 +5,19 @@ 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 + System's Syntax and Behavior + This is a summary of the "block structure" + of the System's syntactic items and reductions. + + + * In terms only. + ** In terms and local environments only. + *** In global environments only. + **** Sort level k in terms only. + + + Summary of the Specification + Here is a numerical acount of the specification's contents and its timeline. @@ -22,14 +33,16 @@ Specification started. - Logical structure of the contribution + + Logical Structure of the Specification 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. - Physical structure of the contribution + + Physical Structure of the Specification The source files are grouped in directories, one for each component. diff --git a/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl b/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl new file mode 100644 index 000000000..8e3ada607 --- /dev/null +++ b/helm/www/lambda_delta/web/home/ld_basic_2_blk.tbl @@ -0,0 +1,45 @@ +name "ld_basic_2_blk" + +table { + class "grey" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "wine" [ + [ "typed abstraction **" ] [ "Γ ⊢ λW" ] + [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] + ] + class "magenta" [ + [ "typed declaration ***" ] [ "Γ ⊢ pλW" ] + [ "no" ] [ "no" ] [ "no" ] [ "$p" ] + ] + class "prune" [ + [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ] + [ "no" ] [ "no" ] [ "yes" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "blue" [ + [ "local abbreviation **" ] [ "Γ ⊢ δV" ] + [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ] + ] + class "sky" [ + [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ] + [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ] + ] + } ] + [ { "no" * } { + class "cyan" [ + [ "sort ****" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "text" { 0 } { 2 * } + +class "plane" { 1 } + 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 index 636c0db74..e8634829f 100644 --- a/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl +++ b/helm/www/lambda_delta/web/home/ld_basic_2_src.tbl @@ -48,11 +48,11 @@ table { class "water" [ { "computation" * } { [ { "strongly normalizing computation" * } { - [ "csn ( ⬇* ? )" "csn_cr" "csn_aaa" * ] + [ "csn ( ⬇* ? )" "csn_lift" "csn_cr" "csn_aaa" * ] } ] [ { "context-sensitive computation" * } { - [ "cprs (? ⊢ ? ➡* ?)" * ] + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lcpr" "cprs_cprs" * ] } ] [ { "local env. ref. for abstract candidates of reducibility" * } { @@ -67,9 +67,13 @@ table { ] class "green" [ { "reducibility" * } { - [ { "context-sensitive reduction" * } { + [ { "context-sensitive normal forms" * } { + [ "cnf ( ? ⊢ 𝐍[?] )" "cnf_lift" * ] + } + ] + [ { "context-sensitive reduction" * } { [ "lcpr ( ? ⊢ ➡ ? )" * ] - [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_tpss" "cpr_ltpr" "cpr_cpr" * ] + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" "cpr_ltpss" "cpr_ltpr" "cpr_cpr" * ] } ] [ { "context-free normal forms" * } { @@ -77,7 +81,7 @@ table { } ] [ { "context-free reduction" * } { - [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" * ] + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" * ] [ "tpr ( ? ➡ ? )" "tpr_lift" "tpr_tpss" "tpr_tpr" * ] } ] @@ -162,7 +166,7 @@ table { } ] [ { "term hom." * } { - [ "thom" "thom_thom" * ] + [ "thom ( ? ≈ ? )" "thom_thom" * ] } ] [ { "closures" * } { diff --git a/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl b/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl new file mode 100644 index 000000000..7477a67ba --- /dev/null +++ b/helm/www/lambda_delta/xslt/ld_Ground_2_sum.xsl @@ -0,0 +1,38 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
categoryobjects


propositionstheorems0lemmas23
conceptsdeclared21defined8
+ + + diff --git a/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl b/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl new file mode 100644 index 000000000..c6ba91d7c --- /dev/null +++ b/helm/www/lambda_delta/xslt/ld_basic_2_blk.xsl @@ -0,0 +1,80 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
domainblockleaderapplicator (with →θ)*reduction→ζ *reference *
{X | Γ ⊢ X : W}typed abstraction **Γ ⊢ λWⓐV→βno#i

typed declaration ***Γ ⊢ pλWnonono$p

native type annotation *Γ ⊢ ⓣWnonoyesno
{X | Γ ⊢ X = V}local abbreviation **Γ ⊢ δVnolocal →δyes#i

global abbreviation ***Γ ⊢ pδVnoglobal →δno$p
nosort ****Γ ⊢ ⋆knononono
+ + + -- 2.39.2