From: Ferruccio Guidi Date: Sat, 1 Dec 2012 17:01:11 +0000 (+0000) Subject: planned dehyphenation of lambdadelta eventually took place! X-Git-Tag: make_still_working~1427 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2a5e0b799cd6aae5d920c67a5ddc9d9888cf7e80 planned dehyphenation of lambdadelta eventually took place! --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html new file mode 100644 index 000000000..ec1ba2de0 --- /dev/null +++ b/helm/www/lambdadelta/BTM.html @@ -0,0 +1,25 @@ + + + + + + + + + + BTM + + + + + +
[lambdadelta home]
cic:/matita/BTM/
[Spacer]
+
Character classes
+
This table shows how the first 45 positive integers + are distributed in the four classes. +
+
classcontents














p
147101316192225283134374043
q
5111517232933354145




s
268141820242632384244


t
39122127303639






+ +
[Spacer]

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

Last update: 2012-12-01T17:55:33+01:00
+ + diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile new file mode 100644 index 000000000..388070cd0 --- /dev/null +++ b/helm/www/lambdadelta/Makefile @@ -0,0 +1,98 @@ +H=@ + +TAGS = www up \ + lint-xml index lddl install-xml \ + test-html html install-html \ + install-jed install-bib \ + +LDDLURL = http://lambdadelta.info/static/lddl + +ETCDIR = etc +DOWNDIR = download +XSLTDIR = xslt +XMLDIR = xml +HTMLDIR = $(HOME)/public_html/lddl +JEDDIR = $(HOME)/mps/jed +BIBDIR = $(HOME)/texmf/bibtex/bib +XHTBLDIR = bin/xhtbl + +REMOTE = helm.cs.unibo.it +RDIR = /projects/helm/public_html/lambdadelta +RXMLDIR = $(REMOTE):$(RDIR)/xml +RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl + +SLS = helena.sl automath.sl +BIB = lambdadelta.bib + +XMLS = brg_si/grundlagen/l/not.ld.xml \ + brg_si/grundlagen/l/et.ld.xml \ + brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + brg_si/grundlagen/l/e/pairis1.ld.xml \ + brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ + crg_si/grundlagen/l/not.ld.xml \ + crg_si/grundlagen/l/et.ld.xml \ + crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + crg_si/grundlagen/l/e/pairis1.ld.xml \ + crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ + brg_si/grundlagen/ccs.ldc.xml + +XMLLINT = xmllint --noout +XSLT = xsltproc + +all: www + +lint-xml: $(XMLS:%=$(XMLDIR)/%) + @echo XMLLINT --valid + $(H)$(XMLLINT) --valid $^ + +$(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index: + @echo " GENERATE INDEXES" + $(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt + $(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh + +lddl: $(ETCDIR)/exclude.txt index + @echo " GENERATE lddl.tar.bz2" + $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) + +install-xml: $(XMLDIR)/index.txt + @echo " INSTALL xml" + $(H)scp -r $< $(XMLDIR)/brg_si/ $(XMLDIR)/crg_si/ $(RXMLDIR) + +test-html: + @$(MAKE) --no-print-directory $(XMLS:%.xml=%) + +html: $(ETCDIR)/make_html.sh + @echo " MAKE */*.ld" + $(H). $< + +install-html: $(ETCDIR)/make_html.sh + @echo " INSTALL html" + $(H)scp -r $(HTMLDIR)/* $(RHTMLDIR) + +install-jed: $(SLS:%=$(JEDDIR)/%) + @echo " INSTALL $(SLS)" + $(H)scp $^ $(DOWNDIR) + +install-bib: $(BIB:%=$(BIBDIR)/%) + @echo " INSTALL $(BIB)" + $(H)scp $< $(DOWNDIR) + $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt) + +www: + $(H)$(MAKE) --no-print-directory -C $(XHTBLDIR) www + +up: + @echo " UPDATE $(REMOTE):$(RDIR)" + $(H)ssh $(REMOTE) "svn up $(RDIR)" + +%.ld: BASEURL = --stringparam baseurl $(LDDLURL) + +%.ld: + @echo " XSLT $@" + $(H)mkdir -p $(HTMLDIR)/$(@D) + $(H)$(XSLT) -o $(HTMLDIR)/$@.html $(BASEURL) $(XSLTDIR)/lddl.xsl $(XMLDIR)/$@.xml + +%.ldc: + @echo " SKIP $@" + +.PHONY: $(TAGS) diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html new file mode 100644 index 000000000..80c3d45b0 --- /dev/null +++ b/helm/www/lambdadelta/apps_2.html @@ -0,0 +1,62 @@ + + + + + + + + + + applications of lambdadelta version 2 + + + + + +
[lambdadelta home]
cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)
[Spacer]
+
Contents of the Specification
+
This specification comprises a collection of checked + applications of λδ version 2. + In particular it contains the components below. +
+ + + +
Summary of the Specification
+
Here is a numerical acount of the specification's contents + and its timeline. +
+
categoryobjects




sizesfiles5bytes13143

propositionstheorems4lemmas1total5
conceptsdeclared3defined10total13
+ + + + +
Logical Structure of the Specification
+
The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). +
+
componentplanefiles
MLTT1genv_primitivejudgement
functionalreduction and type machinertmrtm_step ( ? ⇨ ? )

unfoldlift ( ↑[?,?] ? )subst ( [?←?] ? )
+ +
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-12-01T17:55:33+01:00
+ + diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html new file mode 100644 index 000000000..8019b44f8 --- /dev/null +++ b/helm/www/lambdadelta/basic_2.html @@ -0,0 +1,88 @@ + + + + + + + + + + lambdadelta version 2 + + + + + +
[lambdadelta home]
cic:/matita/lambdadelta/basic_2/ (λδ version 2)
[Spacer]
+
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}local typed abstraction *Γ ⊢ +λWⓐV→βno#i

local typed declaration **Γ ⊢ -λWⓐV→βno#i

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

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

local definition **Γ ⊢ -δVnolocal →δno#i

global definition ***Γ ⊢ 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




sizesfiles226characters427252

propositionstheorems82lemmas981total1063
conceptsdeclared43defined76total119
+ + + + + + + + + + + + +
Logical Structure of the Specification
+
The source files are grouped in planes and components + according to the following table. + A notation file covering the whole specification is provided. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). +
+
componentplanefiles



dynamic typingstratified native validitysnv ( ⦃?,?⦄ ⊩ ? :[?] )snv_lift snv_aaa snv_ssta


equivalencefocalized equivalencelfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )lfpcs_aaa lfpcs_lfprs lfpcs_lfpcs




fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )fpcs_aaa fpcs_cpcs fpcs_fprs fpcs_fpcs



local env. ref. for context-sensitive equivalencelsubse ( ? ⊢•⊑[?] ? )lsubse_ldrop lsubse_ssta lsubse_cpcs



context-sensitive equivalencecpcs ( ? ⊢ ? ⬌* ? )cpcs_ltpss cpcs_delift cpcs_aaa cpcs_ltpr cpcs_cprs cpcs_cpcs


conversionfocalized conversionlfpc ( ⦃?⦄ ⬌ ⦃?⦄ )lfpc_lfpc




fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )fpc_fpc



context-sensitive conversioncpc ( ? ⊢ ? ⬌ ? )cpc_cpc


computationextended computationxprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )xprs_lift xprs_aaa xpr_lsubss xprs_cprs xprs_xprs



weakly normalizing computationcpe ( ? ⊢ ➡* 𝐍⦃?⦄ )cpe_cpe



strongly normalizing computationcsn_vector ( ? ⊢ ⬊* ? )csn_cpr_vector csn_tstc_vector csn_aaa




csn ( ? ⊢ ⬊* ? )csn_alt ( ? ⊢ ⬊⬊* ? )csn_lift csn_cpr csn_lfpr


focalized computationlfprs ( ⦃?⦄ ➡* ⦃?⦄ )lfprs_aaa lfprs_cprs lfprs_lfprs




fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )fprs_aaa fprs_fprs



context-sensitive computationcprs (? ⊢ ? ➡* ?)cprs_lift cprs_delift cprs_aaa cprs_ltpr cprs_lfpr cprs_cprs cprs_lfprs cprs_tstc cprs_tstc_vector



context-free computationltprs ( ? ➡* ? )ltprs_alt ( ? ➡➡* ? )ltprs_ldrop ltprs_ltprs



tprs ( ? ➡* ?)tprs_lift tprs_tprs



local env. ref. for abstract candidates of reducibilitylsubc ( ? ⊑[?] ? )lsubc_ldrop lsubc_ldrops lsubc_lsuba



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

reducibilityextended reductionxpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )xpr_lift xpr_aaa xpr_lsubss



context-sensitive focalized reductioncfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )cnfpr_ltpss cfpr_aaa cfpr_cpr cfpr_cfpr



context-free focalized reductionlfpr ( ⦃?⦄ ➡ ⦃?⦄ )lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )lfpr_aaa lfpr_cpr lfpr_fpr lfpr_lfpr



fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )fpr_cpr fpr_fpr



context-sensitive normal formscnf ( ? ⊢ 𝐍⦃?⦄ )cnf_lift cnf_cif



context-sensitive reductioncpr ( ? ⊢ ? ➡ ? )cpr_lift cpr_tpss cpr_ltpss cpr_delift cpr_aaa cpr_ltpr cpr_cpr



context-sensitive reducible formscrf ( ? ⊢ 𝐑⦃?⦄ )crf_appendcif ( ? ⊢ 𝐈⦃?⦄ )cif_append

context-free normal formsthnf ( 𝐇𝐍⦃?⦄ )




context-free reductionltpr ( ? ➡ ? )ltpr_ldrop ltpr_tps ltpr_ltpss_dx ltpr_ltpss_sn ltpr_aaa ltpr_ltpr




tpr ( ? ➡ ? )tpr_lift tpr_tps tpr_tpss tpr_delift tpr_tpr


unwind



static typinglocal env. ref. for stratified static type assignmentlsubss ( ? •⊑[?] ? )lsubss_ldrop lsubss_ssta lsubss_lsubss



stratified static type assignmentssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )ssta_lift ssta_ltpss_dx ssta_ltpss_sn ssta_aaa ssta_ssta



local env. ref. for atomic arity assignmentlsuba ( ? ⁝⊑ ? )lsuba_ldrop lsuba_aaa lsuba_lsuba



atomic arity assignmentaaa ( ? ⊢ ? ⁝ ? )aaa_lift aaa_lifts aaa_ltpss_dx aaa_ltpss_sn aaa_aaa



parametersshsd


unfoldbasic local env. thinningthin ( ? ▼*[?,?] ≡ ? )thin_ldrop thin_delift



inverse basic term relocationdelift ( ? ⊢ ? ▼*[?,?] ≡ ? )delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )delift_lift delift_tpss delift_ltpss delift_delift


partial unfoldltpss_sn ( ? ⊢ ▶*[?,?] ? )ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )ltpss_sn_ldrop ltpss_sn_tps ltpss_sn_tpss ltpss_sn_ltpss_sn



ltpss_dx ( ? ▶*[?,?] ? )ltpss_dx_ldrop ltpss_dx_tps ltpss_dx_tpss ltpss_dx_ltpss_dx




tpss ( ? ⊢ ? ▶*[?,?] ? )tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )tpss_lifttpss_tpss

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



iterated restricted structural predecessor for closuresfrsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )frsups_frsups




frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )frsupp_frsupp



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




lifts ( ⇧*[?] ? ≡ ? )lifts_lift lifts_lifts



support for generic relocationgr2 ( @⦃?,?⦄ ≡ ? )gr2_plus ( ? + ? )gr2_minus ( ? ▭ ? ≡ ? )gr2_gr2
substitutionparallel substitutiontps ( ? ⊢ ? ▶[?,?] ? )tps_lift tps_tps



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



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



local env. ref. for substitutionlsubs ( ? ≼[?,?] ? )(lsubs_lsubs)lsubs_sfr ( ≽[?,?] ? )


restricted structural predecessor for closuresfrsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )




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




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


grammarsame head term formtshf ( ? ≈ ? )(tshf_tshf)



same top term constructortstc ( ? ≃ ? )tstc_tstc tstc_vector



closurescl_shift ( ? @@ ? )cl_weight ( #{?,?} )



internal syntaxgenv





lenvlenv_weight ( #{?} )lenv_length ( |?| )lenv_append ( ? @@ ? )lenv_px lenv_px_bi


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-12-01T17:55:33+01:00
+ + diff --git a/helm/www/lambdadelta/bin/a.ml b/helm/www/lambdadelta/bin/a.ml new file mode 100644 index 000000000..4f310c873 --- /dev/null +++ b/helm/www/lambdadelta/bin/a.ml @@ -0,0 +1,17 @@ +let f = "0123456789abcdef" + +let r, g, b = 1.0, 0.5, 0.0 + +let h = 1. /. 2. + +let mk_h x = x +. (1. -. x) *. h + +let rr, gg, bb = mk_h r, mk_h g, mk_h b + +let mk_f x = + let x = int_of_float x in + print_char f.[x / 16]; print_char f.[x mod 16] + +let _ = + mk_f (rr *. 255.); mk_f (gg *. 255.); mk_f (bb *. 255.); + print_newline () diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile b/helm/www/lambdadelta/bin/xhtbl/Makefile new file mode 100644 index 000000000..9e9db85db --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/Makefile @@ -0,0 +1,36 @@ +EXEC = xhtbl +VERSION=0.1.1 + +REQUIRES = str + +YACCFLAGS = -v + +include Makefile.common + +XSLT = xsltproc +XHTBL = ./xhtbl.native + +LDURL = http://lambdadelta.info/ +XSLDIR = ../../xslt/ +SRCDIR = ../../web/home/ +ETCDIR = ../../etc/ +HOMEDIR = ../../ +TBLDIRS = $(SRCDIR) $(ETCDIR) + +LDWS = $(shell find $(SRCDIR) -name "*.ldw.xml") +TBLS = $(shell find -L $(TBLDIRS) -name "*.tbl") +XSLS = xhtbl.xsl $(patsubst %.tbl, %.xsl, $(notdir $(TBLS))) +HTMLS = $(patsubst %.ldw.xml, $(HOMEDIR)%.html, $(notdir $(LDWS))) +LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl + +$(HOMEDIR)%.html: BASEURL = --stringparam baseurl $(LDURL) + +www: $(HTMLS) + +$(XSLS:%=$(XSLDIR)%): $(TBLS) $(XHTBL) + @echo " XHTBL *.tbl" + $(H)$(XHTBL) -O $(XSLDIR) $(TBLS) + +$(HOMEDIR)%.html: $(SRCDIR)%.ldw.xml $(XSLS:%=$(XSLDIR)%) $(LDWEB:%=$(XSLDIR)%) + @echo " XSLT $(notdir $<)" + $(H)$(XSLT) -o $@ $(BASEURL) $(XSLDIR)ld_web.xsl $< diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile.common b/helm/www/lambdadelta/bin/xhtbl/Makefile.common new file mode 100644 index 000000000..bf944971b --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/Makefile.common @@ -0,0 +1,27 @@ +H=@ + +include ../../etc/Makefile.defs + +DIST=$(EXEC)---$(VERSION) +DATE=$(shell date +%y%m%d) + +OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) + +all: $(EXEC).native + +$(EXEC).native: $(wildcard *.ml) $(wildcard *.mli) $(wildcard *.mly) $(wildcard *.mll) + @echo " OCAMLBUILD $(EXEC).native" + $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" -yaccflags "$(YACCFLAGS)" $(EXEC).native + +clean: + ocamlbuild -clean + rm -rf $(DIST) $(DIST).tgz + +dist: + mkdir -p $(DIST)/Sources + cp ReadMe $(DIST) + cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources + cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) + tar -cvzf $(DIST).tgz $(DIST) diff --git a/helm/www/lambdadelta/bin/xhtbl/css.ml b/helm/www/lambdadelta/bin/xhtbl/css.ml new file mode 100644 index 000000000..82a41e91c --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/css.ml @@ -0,0 +1,20 @@ +module L = List + +module T = Table + +(* true for a row specification *) +type atom = T.css * bool * int option * int option + +type atoms = atom list + +let get_css a y x = + let map y x (c, b, x1, x2) = match b, x1, x2 with + | _ , None, None -> c + | false, None, Some c2 -> if x <= c2 then c else [] + | false, Some c1, None -> if x >= c1 then c else [] + | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else [] + | true , None, Some r2 -> if y <= r2 then c else [] + | true , Some r1, None -> if y >= r1 then c else [] + | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else [] + in + L.concat (L.map (map y x) a) diff --git a/helm/www/lambdadelta/bin/xhtbl/fold.ml b/helm/www/lambdadelta/bin/xhtbl/fold.ml new file mode 100644 index 000000000..752b06d77 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/fold.ml @@ -0,0 +1,25 @@ +module T = Table + +type 'a fold_cb = { + open_table : 'a -> T.table -> 'a; + close_table: 'a -> T.table -> 'a; + map_key : 'a -> T.key -> 'a; + open_line : bool -> 'a -> 'a; + close_line : bool -> 'a -> 'a; + open_entry : bool -> 'a -> 'a; + close_entry: bool -> 'a -> 'a -> 'a; +} + +let map h g f a b = h a (g (f a) b) + +let rec fold_table cb a t = + let a = cb.open_table a t in + let a = fold_entry cb a t.T.te in + cb.close_table a t + +and fold_entry cb a = function + | T.Key k -> cb.map_key a k + | T.Line (r, ts) -> + let a = cb.open_line r a in + let a = List.fold_left (map (cb.close_entry r) (fold_table cb) (cb.open_entry r)) a ts in + cb.close_line r a diff --git a/helm/www/lambdadelta/bin/xhtbl/matrix.ml b/helm/www/lambdadelta/bin/xhtbl/matrix.ml new file mode 100644 index 000000000..4769a5457 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/matrix.ml @@ -0,0 +1,52 @@ +module A = Array + +module T = Table + +type cell = { + ck: string list; (* contents *) + cc: T.css; (* css classes *) + cb: T.border; (* border *) +} + +type matrix = { + r: int; (* rows *) + c: int; (* columns *) + m: cell array array; (* matrix *) +} + +let empty = { + ck = []; cc = []; cb = T.border false; +} + +let make ts = { + r = ts.T.rf; c = ts.T.cf; + m = A.make_matrix ts.T.rf ts.T.cf empty; +} + +let set_key m y x kl = + m.m.(y).(x) <- {m.m.(y).(x) with ck = kl} + +let set_css m y x c = + m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc} + +let set_west m y x b = + let c = m.m.(y).(x) in + let cb = {c.cb with T.w = c.cb.T.w || b.T.w} in + m.m.(y).(x) <- {c with cb = cb} + +let set_north m y x b = + let c = m.m.(y).(x) in + let cb = {c.cb with T.n = c.cb.T.n || b.T.n} in + m.m.(y).(x) <- {c with cb = cb} + +let set_east m y x b = + if x < pred m.c then set_west m y (succ x) {b with T.w = b.T.e} else + let c = m.m.(y).(x) in + let cb = {c.cb with T.e = c.cb.T.e || b.T.e} in + m.m.(y).(x) <- {c with cb = cb} + +let set_south m y x b = + if y < pred m.r then set_north m (succ y) x {b with T.n = b.T.s} else + let c = m.m.(y).(x) in + let cb = {c.cb with T.s = c.cb.T.s || b.T.s} in + m.m.(y).(x) <- {c with cb = cb} diff --git a/helm/www/lambdadelta/bin/xhtbl/options.ml b/helm/www/lambdadelta/bin/xhtbl/options.ml new file mode 100644 index 000000000..ce1c88867 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/options.ml @@ -0,0 +1,34 @@ +let output_dir_default = "" + +let debug_lexer_default = false + +let debug_pass_default = false + +let pass_default = false + +let output_dir = ref output_dir_default + +let debug_lexer = ref debug_lexer_default + +let d0 = ref debug_pass_default + +let d1 = ref debug_pass_default + +let d2 = ref debug_pass_default + +let e1 = ref debug_pass_default + +let e2 = ref debug_pass_default + +let p0 = ref pass_default + +let p1 = ref pass_default + +let p2 = ref pass_default + +let clear () = + output_dir := output_dir_default; + debug_lexer := debug_lexer_default; + d0 := debug_pass_default; d1 := debug_pass_default; d2 := debug_pass_default; + e1 := debug_pass_default; e2 := debug_pass_default; + p0 := pass_default; p1 := pass_default; p2 := pass_default diff --git a/helm/www/lambdadelta/bin/xhtbl/pass1.ml b/helm/www/lambdadelta/bin/xhtbl/pass1.ml new file mode 100644 index 000000000..1c53e7d6f --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/pass1.ml @@ -0,0 +1,86 @@ +module L = List + +module T = Table +module F = Fold + +type status = { + ts: T.size; (* current dimensions *) + tc: T.css; (* current class *) +} + +let empty = { + ts = T.no_size; tc = []; +} + +let init b ts = + if b then + {ts with T.ri = max_int; T.ci = 0} + else + {ts with T.ri = 0; T.ci = max_int} + +let combine b ts1 ts2 = + if b then + {ts1 with + T.rf = max ts1.T.rf ts2.T.rf; T.ri = min ts1.T.ri ts2.T.ri; + T.cf = ts1.T.cf + ts2.T.cf; T.ci = ts1.T.ci + ts2.T.ci; + } + else + {ts1 with + T.cf = max ts1.T.cf ts2.T.cf; T.ci = min ts1.T.ci ts2.T.ci; + T.rf = ts1.T.rf + ts2.T.rf; T.ri = ts1.T.ri + ts2.T.ri; + } + +let deinit ts = {ts with + T.ri = if ts.T.ri = max_int then 0 else ts.T.ri; + T.ci = if ts.T.ci = max_int then 0 else ts.T.ci; +} + +(****************************************************************************) + +let open_table st t = + t.T.tc <- t.T.tc @ st.tc; + {st with tc = t.T.tc} + +let close_table st t = + t.T.ts <- st.ts; st + +let map_key st k = + let ts = match k, st.ts.T.p with + | T.Text _ , _ -> + {st.ts with T.rf = 1; T.cf = 1; T.ri = 0; T.ci = 0} + | T.Glue None , _ -> + {st.ts with T.rf = 0; T.cf = 0; T.ri = 1; T.ci = 1} + | T.Glue Some g, Some false -> + {st.ts with T.rf = g; T.cf = 0; T.ri = 0; T.ci = 1} + | T.Glue Some g, Some true -> + {st.ts with T.rf = 0; T.cf = g; T.ri = 1; T.ci = 0} + | T.Glue Some g, None -> + {st.ts with T.rf = g; T.cf = g; T.ri = 0; T.ci = 0} + in + {st with ts = ts} + +let open_line b st = + let ts = init b st.ts in + let ts = {ts with T.rf = 0; T.cf = 0} in + {st with ts = ts} + +let open_entry b st = + let ts = {st.ts with T.p = Some b} in + {st with ts = ts} + +let close_entry b st sst = + {st with ts = combine b st.ts sst.ts} + +let close_line b st = + {st with ts = deinit st.ts} + +let cb = { + F.open_table = open_table; F.close_table = close_table; + F.open_line = open_line; F.close_line = close_line; + F.open_entry = open_entry; F.close_entry = close_entry; + F.map_key = map_key; +} + +let process t = + let st = F.fold_table cb empty t in + st.ts diff --git a/helm/www/lambdadelta/bin/xhtbl/pass2.ml b/helm/www/lambdadelta/bin/xhtbl/pass2.ml new file mode 100644 index 000000000..68cc7ba99 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/pass2.ml @@ -0,0 +1,139 @@ +module O = Options +module T = Table +module M = Matrix +module F = Fold + +type status = { + ts: T.size; (* current dimensions *) + tm: M.matrix; (* current matrix *) +} + +let initial t m = { + ts = {t.T.ts with T.ri = 0; T.ci = 0}; + tm = m; +} + +let resize b sts tts = + if b then begin (* parent is a row *) + if tts.T.rf < sts.T.rf && tts.T.ri = 0 then + failwith "underful column"; + {tts with T.rf = sts.T.rf; T.cf = tts.T.cf + sts.T.ci * tts.T.ci} + end else begin (* parent is a column *) + if tts.T.cf < sts.T.cf && tts.T.ci = 0 then + failwith "underful row"; + {tts with T.cf = sts.T.cf; T.rf = tts.T.rf + sts.T.ri * tts.T.ri} + end + +let fill b sts tts = + if b then (* parent is a row *) + {sts with T.ri = + let rf, ri = sts.T.rf - tts.T.rf, tts.T.ri in + if ri = 0 then 0 else + if rf mod ri = 0 then rf / ri else + failwith "fracted column" + } + else (* parent is a column *) + {sts with T.ci = + let cf, ci = sts.T.cf - tts.T.cf, tts.T.ci in + if ci = 0 then 0 else + if cf mod ci = 0 then cf / ci else + failwith "fracted row" + } + +let place b sts tts = + if b then (* parent is a row *) + {sts with T.x = sts.T.x + tts.T.cf} + else (* parent is a column *) + {sts with T.y = sts.T.y + tts.T.rf} + +let set_key st t = match t.T.te with + | T.Key (T.Text sl) -> M.set_key st.tm t.T.ts.T.y t.T.ts.T.x sl + | _ -> () + +let set_css st t = + let rec aux y x = + if y >= t.T.ts.T.rf then () else + if x >= t.T.ts.T.cf then aux (succ y) 0 else begin + M.set_css st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc; + aux y (succ x) + end + in + match t.T.te with + | T.Key _ -> aux 0 0 + | _ -> () + +let set_borders st t = + let rec aux_we y = + if y >= t.T.ts.T.rf then () else begin + M.set_west st.tm (t.T.ts.T.y + y) t.T.ts.T.x t.T.tb; + if t.T.ts.T.cf > 0 then + M.set_east st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + pred t.T.ts.T.cf) t.T.tb; + aux_we (succ y) + end + in + let rec aux_ns x = + if x >= t.T.ts.T.cf then () else begin + M.set_north st.tm t.T.ts.T.y (t.T.ts.T.x + x) t.T.tb; + if t.T.ts.T.rf > 0 then + M.set_south st.tm (t.T.ts.T.y + pred t.T.ts.T.rf) (t.T.ts.T.x + x) t.T.tb; + aux_ns (succ x) + end + in + match t.T.te with + | T.Line (true, _) -> aux_we 0; aux_ns 0 + | _ -> () + +let print st t = + if !O.e2 then + Printf.printf "#%u: (%u+%u, %u+%u) - (%u+%u, %u+%u)\n" + t.T.ti + t.T.ts.T.rf t.T.ts.T.ri + t.T.ts.T.cf t.T.ts.T.ci + st.ts.T.rf st.ts.T.ri + st.ts.T.cf st.ts.T.ci + +(****************************************************************************) + +let open_table st t = + print st t; + let ts = match t.T.ts.T.p with + | None -> + let ts = fill false st.ts t.T.ts in + let ts = fill true ts t.T.ts in + t.T.ts <- resize false st.ts t.T.ts; + t.T.ts <- resize true st.ts t.T.ts; + ts + | Some b -> + let ts = fill b st.ts t.T.ts in + t.T.ts <- resize b st.ts t.T.ts; + ts + in + t.T.ts <- {t.T.ts with T.ri = 0; T.ci = 0; T.x = st.ts.T.x; T.y = st.ts.T.y}; + let ts = {ts with T.rf = t.T.ts.T.rf; T.cf = t.T.ts.T.cf} in + let st = {st with ts = ts} in + print st t; st + +let close_table st t = + set_key st t; set_css st t; set_borders st t; st + +let map_key st k = st + +let open_line b st = st + +let open_entry b st = st + +let close_entry b st sst = + let ts = place b st.ts sst.ts in + {st with ts = ts} + +let close_line b st = st + +let cb = { + F.open_table = open_table; F.close_table = close_table; + F.open_line = open_line; F.close_line = close_line; + F.open_entry = open_entry; F.close_entry = close_entry; + F.map_key = map_key; +} + +let process t m = + let _ = F.fold_table cb (initial t m) t in () diff --git a/helm/www/lambdadelta/bin/xhtbl/pass3.ml b/helm/www/lambdadelta/bin/xhtbl/pass3.ml new file mode 100644 index 000000000..4513828b5 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/pass3.ml @@ -0,0 +1,23 @@ +module A = Array + +module M = Matrix +module C = Css + +type status = { + m: M.matrix; + a: C.atoms; +} + +let initial a m = { + m = m; a = a; +} + +let process_cell st y x c = + M.set_css st.m y x (C.get_css st.a y x) + +let process_row st y row = + A.iteri (process_cell st y) row + +let process css matrix = + let st = initial css matrix in + A.iteri (process_row st) matrix.M.m diff --git a/helm/www/lambdadelta/bin/xhtbl/table.ml b/helm/www/lambdadelta/bin/xhtbl/table.ml new file mode 100644 index 000000000..e363cd434 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/table.ml @@ -0,0 +1,54 @@ +type css = string list + +type size = { + y : int; (* first row *) + x : int; (* first column *) + rf: int; (* finite rows *) + cf: int; (* finite columns *) + ri: int; (* infinite rows *) + ci: int; (* infinite columns *) + p : bool option; (* parent kind *) +} + +type border = { + n: bool; (* north *) + s: bool; (* south *) + e: bool; (* east *) + w: bool; (* west *) +} + +type key = Text of string list + | Glue of int option + +type table = { + mutable tc: css; (* css classes *) + mutable ts: size; (* dimension *) + tb: border; (* border *) + te: entry; (* contents *) + ti: int; (* table identifier *) +} + +and entry = Key of key + | Line of bool * table list (* true for a row *) + +let id = + let current = ref 0 in + fun () -> incr current; !current + +let no_size = { + y = 0; x = 0; rf = 0; cf = 0; ri = 0; ci = 0; p = None; +} + +let border b = { + n = b; s = b; e = b; w = b; +} + +let mk_key k tc = { + ts = no_size; tb = border false; te = Key k; tc = tc; + ti = id (); +} + +let mk_line b tl tc = { + ts = no_size; tb = border b; te = Line (b, tl); tc = tc; + ti = id (); +} diff --git a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll new file mode 100644 index 000000000..7557e7bb8 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll @@ -0,0 +1,35 @@ +{ + module S = String + module O = Options + module TP = TextParser + + let trim s = S.sub s 1 (S.length s - 2) + + let out s = if !O.debug_lexer then prerr_endline s +} + +let SPC = ['\r' '\n' '\t' ' ']+ +let QT = '"' +let STR = QT [^'"']* QT +let NUM = ['0'-'9']+ + +rule token = parse + | SPC { token lexbuf } + | STR as s { out s; TP.TEXT (trim s) } + | NUM as s { out s; TP.NUM (int_of_string s) } + | "{" { out "{"; TP.OC } + | "}" { out "}"; TP.CC } + | "[" { out "["; TP.OB } + | "]" { out "]"; TP.CB } + | "*" { out "*"; TP.SR } + | "+" { out "+"; TP.PS } + | "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/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly new file mode 100644 index 000000000..333d3421f --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly @@ -0,0 +1,95 @@ +%{ + +module S = Str +module L = List +module T = Table + +let split s = + S.split (S.regexp "[ \r\n\t]+") s + +let mk_atom s rs = + let map c (b, (x1, x2)) = c, b, x1, x2 in + L.map (map (split s)) rs + +%} + +%token NUM +%token TEXT +%token NAME TABLE CSS SR OC CC OB CB PS EOF + +%start script +%type <(string * Table.table * Css.atoms) list> script + +%% + +text: + | TEXT { $1 } + +texts: + | text { [$1] } + | text PS texts { $1 :: $3 } +; + +key: + | texts { T.Text $1 } + | SR { T.Glue None } + | NUM { T.Glue (Some $1) } +; + +css: + | { [] } + | CSS TEXT { split $2 } +; + +table: + | css key { T.mk_key $2 $1 } + | css OC tables CC { T.mk_line false $3 $1 } + | css OB tables CB { T.mk_line true $3 $1 } +; + +tables: + | { [] } + | table tables { $1 :: $2 } +; + +name: + | { "" } + | NAME TEXT { $2 } +; + +interval: + | NUM { Some $1, Some $1 } + | SR { None, None } + | NUM NUM { Some $1, Some $2 } + | NUM SR { Some $1, None } + | SR NUM { None, Some $2 } + | SR SR { None, None } +; + +range: + | OB interval CB { true, $2 } + | OC interval CC { false, $2 } +; + +ranges: + | { [] } + | range ranges { $1 :: $2 } +; + +atom: + | CSS TEXT ranges { mk_atom $2 $3 } +; + +atoms: + | { [] } + | atom atoms { $1 @ $2 } +; + +directive: + | name TABLE table atoms { $1, $3, $4 } +; + +script: + | EOF { [] } + | directive script { $1 :: $2 } +; diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml new file mode 100644 index 000000000..54995e96b --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml @@ -0,0 +1,91 @@ +module L = List +module P = Printf +module S = String + +module T = Table +module F = Fold + +type status = { + i: int; (* indentation *) + out: string -> unit; (* output function *) +} + +let home = { + i = 0; out = print_string +} + +let indent st = + S.make st.i ' ' + +let add st = {st with i = st.i + 3} + +let sub st = {st with i = st.i - 3} + +let parent = function + | None -> "key" + | Some false -> "col" + | Some true -> "row" + +let size ts = + P.sprintf "(%u, %u); (%u+%u, %u+%u); %s" + ts.T.y ts.T.x ts.T.rf ts.T.ri ts.T.cf ts.T.ci (parent ts.T.p) + +let border tb = + let str = S.make 4 ' ' in + if tb.T.w then str.[0] <- 'W'; + if tb.T.n then str.[1] <- 'N'; + if tb.T.e then str.[2] <- 'E'; + if tb.T.s then str.[3] <- 'S'; + str + +let css tc = + P.sprintf "\"%s\"" (S.concat " " tc) + +let key = function + | T.Text sl -> + let map s = P.sprintf "\"%s\"" s in + S.concat " + " (L.map map sl) + | T.Glue None -> "*" + | T.Glue (Some i) -> P.sprintf "%u" i + +let entry = function + | false -> "column" + | true -> "row" + +(****************************************************************************) + +let open_table st t = + let str = + P.sprintf "%s[{#%u: %s; %s; %s}\n" + (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) + in + st.out str; add st + +let close_table st t = + let st = sub st in + let str = P.sprintf "%s]\n" (indent st) in + st.out str; st + +let map_key st k = + let str = P.sprintf "%s%s\n" (indent st) (key k) in + st.out str; st + +let open_line b st = + let str = P.sprintf "%s%s\n" (indent st) (entry b) in + st.out str; st + +let close_line b st = st + +let open_entry b st = st + +let close_entry b st sst = st + +let cb = { + F.open_table = open_table; F.close_table = close_table; + F.open_line = open_line; F.close_line = close_line; + F.open_entry = open_entry; F.close_entry = close_entry; + F.map_key = map_key; +} + +let debug t = + let _ = F.fold_table cb home t in () diff --git a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml new file mode 100644 index 000000000..cf4d818b6 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml @@ -0,0 +1,76 @@ +module A = Arg +module F = Filename +module L = List + +module O = Options +module TP = TextParser +module TL = TextLexer +module TU = TextUnparser +module P1 = Pass1 +module P2 = Pass2 +module P3 = Pass3 +module M = Matrix +module XU = XmlUnparser + +let help = "" +let help_L = "" +let help_O = "" +let help_X = "" +let help_d0 = "" +let help_d1 = "" +let help_d2 = "" +let help_e1 = "" +let help_e2 = "" +let help_p0 = "" +let help_p1 = "" +let help_p2 = "" + +let hook = "xhtbl" + +let includes, tables = ref [], ref [] + +let set_output_dir s = O.output_dir := s + +let process_directive och bname (name, table, css) = + tables := name :: !tables; + if !O.d0 then TU.debug table; + if not !O.p0 then begin + let size = P1.process table in + if !O.d1 then TU.debug table; + if not !O.p1 then begin + let matrix = M.make size in + let _ = P2.process table matrix in + if !O.d2 then TU.debug table; + if not !O.p2 then P3.process css matrix; + let name = if name = "" then bname else name in + XU.output och name matrix + end + end + +let process_file fname = + let bname = F.chop_extension (F.basename fname) in + let ich = open_in fname in + let lexbuf = Lexing.from_channel ich in + let ds = TP.script TL.token lexbuf in + close_in ich; includes := bname :: !includes; + let och = XU.open_out true bname in + L.iter (process_directive och bname) ds; + XU.close_out och + +let main () = + A.parse [ + "-L", A.Set O.debug_lexer, help_L; + "-O", A.String set_output_dir, help_O; + "-X", A.Unit O.clear, help_X; + "-d0", A.Set O.d0, help_d0; + "-d1", A.Set O.d1, help_d1; + "-d2", A.Set O.d2, help_d2; + "-e1", A.Set O.e1, help_e1; + "-e2", A.Set O.e2, help_e2; + "-p0", A.Set O.p0, help_p0; + "-p1", A.Set O.p1, help_p1; + "-p2", A.Set O.p2, help_p2; + ] process_file help; + XU.write_hook hook !includes !tables + +let _ = main () diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml new file mode 100644 index 000000000..3583c2f75 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml @@ -0,0 +1,82 @@ +module A = Array +module F = Filename +module L = List +module P = Printf +module S = String + +module O = Options +module T = Table +module M = Matrix + +let i = 0 + +let myself = F.basename (Sys.argv.(0)) + +let msg = P.sprintf "This file was generated by %s, do not edit" myself + +let border cell = + let str = S.make 4 'n' in + if cell.M.cb.T.n then str.[0] <- 's'; + if cell.M.cb.T.e then str.[1] <- 's'; + if cell.M.cb.T.s then str.[2] <- 's'; + if cell.M.cb.T.w then str.[3] <- 's'; + str :: cell.M.cc + +let key cell = + if cell.M.ck = [] then "
" else S.concat " " cell.M.ck + +let ind i = S.make (2 * i) ' ' + +let out_cell och cell = + let cc = border cell in + P.fprintf och "%s%s\n" + (ind (i+4)) (S.concat " " cc) (key cell) + +let out_row och row = + P.fprintf och "%s\n" (ind (i+3)); + A.iter (out_cell och) row; + P.fprintf och "%s\n" (ind (i+3)) + +(****************************************************************************) + +let open_out html name = + let fname = F.concat !O.output_dir (P.sprintf "%s.xsl" name) in + let och = open_out fname in + P.fprintf och "\n\n"; + P.fprintf och "\n\n" msg; + P.fprintf och "\n\n"; + och + +let output och name matrix = + P.fprintf och "\n" name; + P.fprintf och "%s\n" (ind (i+1)); + P.fprintf och "%s\n" (ind (i+2)); + A.iter (out_row och) matrix.M.m; + P.fprintf och "%s\n" (ind (i+2)); + P.fprintf och "%s
\n" (ind (i+1)); + P.fprintf och "\n\n" + +let close_out och = + P.fprintf och "\n"; + close_out och + +let map_incs och name = + P.fprintf och "\n" name + +let map_tbls och name = + P.fprintf och "%s\n" (ind (i+2)) name; + P.fprintf och "%s\n" (ind (i+3)) name; + P.fprintf och "%s\n" (ind (i+2)) + +let write_hook name incs tbls = + let och = open_out false name in + L.iter (map_incs och) incs; + P.fprintf och "\n\n" name; + P.fprintf och "%s\n" (ind (i+1)); + L.iter (map_tbls och) tbls; + P.fprintf och "%s\n" (ind (i+1)); + P.fprintf och "\n\n"; + close_out och diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css new file mode 100644 index 000000000..9e7c3fc08 --- /dev/null +++ b/helm/www/lambdadelta/css/ld_web.css @@ -0,0 +1,121 @@ +@charset "UTF-8"; + +/* general ******************************************************************/ + +body { + background: rgb(255, 255, 255); + color: rgb(0, 0, 0); + margin: 2.5%; +} + +a:link, a:visited { + text-decoration: underline; +} + +a:active, a:hover, a:focus { + background: rgb(192, 192, 192); +} + +/* blocks *******************************************************************/ + +div.spacer { + text-align: center; +} + +div.head1 { + margin: 0.5em 0; + text-align: center; + font-weight: bold; + font-size: xx-large; +} + +div.head2 { + margin: 0.5em 0; + text-align: left; + font-weight: bold; + font-size: x-large; +} + +div.text { + margin: 1em 0; + text-align: left; +} + +span.date { + font-weight: bold; +} + +/* inline decorations *******************************************************/ + +img.icon32 { + border: 0; + width: 32px; + height: 32px; +} + +img.rule { + border: 0; + height: 4px; + width: 100%; +} + +img.w3c { + margin: 0 0.5em; + border: 0; + width: 88px; + height: 32px; /* this should be 31px */ +} + +/* background colors ********************************************************/ + +.grey { + background-color:#dfdfdf; /* + 7/8 */ +} + +.wine { + background-color:#ffbfdf; /* + 3/4 */ +} + +.magenta { + background-color:#ffccff; /* + 4/5 */ +} + +.prune { + background-color:#e5ccff; /* + 4/5 */ +} + +.blue { + background-color:#ccccff; /* + 4/5 */ +} + +.sky { + background-color:#bfdfff; /* + 3/4 */ +} + +.cyan { + background-color:#bfffff; /* + 3/4 */ +} + +.water { + background-color:#ccffe5; /* + 4/5 */ +} + +.green { + background-color:#bfffbf; /* + 3/4 */ +} + +.grass { + background-color:#dfffbf; /* + 3/4 */ +} + +.yellow { + background-color:#ffffbf; /* + 3/4 */ +} + +.orange { + background-color:#ffdfbf; /* + 3/4 */ +} + +.red { + background-color:#ffbfbf; /* + 3/4 */ +} diff --git a/helm/www/lambdadelta/css/lddl.css b/helm/www/lambdadelta/css/lddl.css new file mode 100644 index 000000000..41a635d45 --- /dev/null +++ b/helm/www/lambdadelta/css/lddl.css @@ -0,0 +1,43 @@ +@charset "UTF-8"; + +/* terms ********************************************************************/ + +.separator { + background: rgb(255, 255, 255); + color: rgb(0, 0, 0); +} + +.sort { + background: rgb(255, 255, 255); + color: rgb(128, 0, 255); +} + +.lref { + background: rgb(255, 255, 255); + color: rgb(0, 0, 0); +} + +.gref { + background: rgb(255, 255, 255); + color: rgb(0, 0, 255); +} + +.appl { + background: rgb(255, 255, 255); + color: rgb(0, 0, 0); +} + +.cast { + background: rgb(255, 255, 255); + color: rgb(255, 0, 0); +} + +.local { + background: rgb(255, 255, 255); + color: rgb(0, 160, 0); +} + +.global { + background: rgb(255, 255, 255); + color: rgb(0, 0, 0); +} diff --git a/helm/www/lambdadelta/css/xhtbl.css b/helm/www/lambdadelta/css/xhtbl.css new file mode 100644 index 000000000..f58db47c3 --- /dev/null +++ b/helm/www/lambdadelta/css/xhtbl.css @@ -0,0 +1,108 @@ +@charset "UTF-8"; + +/* positioning **************************************************************/ + +table { + margin-left: auto; + margin-right: auto; + width: 100%; +} + +td { + border-color:#000000; + border-width:1px; + color:#000000; +} + +/* content types ************************************************************/ + +.text { + font-style: normal; +} + +.component { + font-style: italic; + text-transform: capitalize; +} + +.plane { + font-style: italic; + text-transform: lowercase; +} + +.file { + font-style: normal; + text-transform: lowercase; +} + +.number { + text-align: right; + font-style: italic; + text-transform: lowercase; +} + +/* cell borders *************************************************************/ + +td.nnnn { + border-style:none none none none; +} + +td.nnns { + border-style:none none none solid; +} + +td.nnsn { + border-style:none none solid none; +} + +td.nnss { + border-style:none none solid solid; +} + +td.nsnn { + border-style:none solid none none; +} + +td.nsns { + border-style:none solid none solid; +} + +td.nssn { + border-style:none solid solid none; +} + +td.nsss { + border-style:none solid solid solid; +} + +td.snnn { + border-style:solid none none none; +} + +td.snns { + border-style:solid none none solid; +} + +td.snsn { + border-style:solid none solid none; +} + +td.snss { + border-style:solid none solid solid; +} + +td.ssnn { + border-style:solid solid none none; +} + +td.ssns { + border-style:solid solid none solid; +} + +td.sssn { + border-style:solid solid solid none; +} + +td.ssss { + border-style:solid solid solid solid; +} diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html new file mode 100644 index 000000000..3f24ef43c --- /dev/null +++ b/helm/www/lambdadelta/documentation.html @@ -0,0 +1,355 @@ + + + + + lambdadelta home page + + + + + +
+
+ [Crux Logo] +

The Formal System λδ (lambdadelta)
+

+

Towards the unification of terms, types, environments and + contexts

+ [Separator]
+ + + + + + + +
+ + +
    +
  • Papers
    • +
+ + 		+

Documentation [Butterfly]

+ Currently the main + source of + information on λδ (version 1) is Resource + 1.1 below.
+ A summary of + basic λδ (version + 1) is found in Resource + 1.5 + below.
+

[Basic + lambdadelta Logo] Basic λδ version 2 (in + progress):

+ + + + + + + + + + + + + + + + + + + +
2.1.
+ 		F. + Guidi: An + Efficient + Validation Procedure for the Formal System λδ + (2010-07). + In CiE 2010 + Local Proceedings. + University of Azores, CMATI Booklet, pp. 204-213. + BibTeX entry.
+
+
2.2.
+ 		F. +Guidi: + + + + + + + + + + + + Landau's + "Grundlagen der Analysis" from Automath to + lambdadelta (2009-09). + University of + Bologna, technical report UBLCS-2009-16. BibTeX entry.
+
+
2.3.
+ 		F. + Guidi: An + Efficient + Validation Procedure for the Formal System λδ + (2010-07). + Presentation + at + CiE + 2010 + (slides).
+
+
2.4.
+ 		F. + Guidi: A + Validator + for the Formal System λδ (revised 2010-02). + Presentation + at + the + University + of + Bologna + (slides).
+

[Basic + lambdadelta Logo] Basic λδ version 1 + (dismissed):

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
1.1.
+ 		F. +Guidi: + The Formal System + λδ (2009-10). In ACM ToCL 11(1), + Article + No. 5 (accepted + 2008-07). + CoRR + identifier cs/0611040 + [v10] (revised 2008-09). + BibTeX + entry.
+
+
1.2.
+ 		F. + Guidi: Lambda + Types on the Lambda Calculus with + Abbreviations (2007-06). + In CiE 2007 + Local Proceedings. + University + of + Siena, + technical + report + 487, + p. + 387 + (abstract + of + a + presentation). BibTeX + entry.
+
+
1.3.
+ 		F. + Guidi: Lambda Types on + the Lambda Calculus with + Abbreviations (2006-11). + University + of + Bologna, + technical + report + UBLCS-2006-25. BibTeX + entry.
+
+
1.4.
+ 		F. + Guidi: Lambda + Types + on + the + Lambda + Calculus + with + Abbreviations: + a + Certified + Specification (2006-01). + University of + Bologna, technical report UBLCS-2006-01. BibTeX entry.
+
+
1.5.
+ 		F. + Guidi: The + Formal + System lambdadelta + (2008-10). + Presentation at + "Advances in Constructive Topology and Logical + Foundations" (slides).
+
+
1.6.
+ 		F. + Guidi: Towards + the Unification of Terms, Types + and Contexts (2008-03). + Presentation + at + Types + 2008 + (slides).
+
+
1.7.
+ 		F. + Guidi: Lambda + Types on the Lambda Calculus with + Abbreviations (2007-06). + Presentation + at + CiE + 2007 + (slides).
+
+
1.8.
+ 		F. + Guidi: Lambda + Tipi sul Lambda Calcolo con + Abbreviazioni (2007-01). + Presentation + at + the + University + of + Padova + (slides in + Italian).
+
+
1.9.
+ 		F. +Guidi: + Lambda Tipi sul + Lambda Calcolo con + Abbreviazioni: una Specifica Certificata + (2005-12). + Presentation at + the University of Bologna (slides in + Italian).
+
+
+
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+ Last update 2012-12-01 by Ferruccio + Guidi
+
+ + diff --git a/helm/www/lambdadelta/download/automath.sl b/helm/www/lambdadelta/download/automath.sl new file mode 100644 index 000000000..d28950a36 --- /dev/null +++ b/helm/www/lambdadelta/download/automath.sl @@ -0,0 +1,27 @@ +$1 = "Automath"; + +create_syntax_table ($1); + +define_syntax ("{","}",'%', $1); % comments +define_syntax ("#","",'%', $1); % comments +define_syntax ("%","",'%', $1); % comments +define_syntax ("([<", ")]>", '(', $1); % brackets +define_syntax ('"', '"', $1); % strings +define_syntax ("a-zA-Z_0-9`'", 'w', $1); % words +define_syntax (":+-=*@~,;.?", '+', $1); % operators + + +() = define_keywords_n ($1, "EBPN_E", 2, 0); +() = define_keywords_n ($1, "'_E''eb''pn'PRIMPROPTYPE", 4, 0); +() = define_keywords_n ($1, "'prim''prop''type'", 6, 0); + +define Automath_mode () +{ + variable kmap = "Automath"; + + set_mode(kmap, 0x04); + use_syntax_table (kmap); + runhooks("Automath_mode_hook"); +} + +add_mode_for_extension ("Automath", "aut"); diff --git a/helm/www/lambdadelta/download/cie_2007.pdf b/helm/www/lambdadelta/download/cie_2007.pdf new file mode 100644 index 000000000..d369a8bc3 Binary files /dev/null and b/helm/www/lambdadelta/download/cie_2007.pdf differ diff --git a/helm/www/lambdadelta/download/cie_2010.pdf b/helm/www/lambdadelta/download/cie_2010.pdf new file mode 100644 index 000000000..8afbebb26 Binary files /dev/null and b/helm/www/lambdadelta/download/cie_2010.pdf differ diff --git a/helm/www/lambdadelta/download/helena.sl b/helm/www/lambdadelta/download/helena.sl new file mode 100644 index 000000000..fc8b1903e --- /dev/null +++ b/helm/www/lambdadelta/download/helena.sl @@ -0,0 +1,28 @@ +$1 = "Helena"; + +create_syntax_table ($1); + +define_syntax ("\\*","*\\",'%', $1); % comments +define_syntax ("([{<", ")]}>", '(', $1); % brackets +define_syntax ('"', '"', $1); % strings +define_syntax ("\\a-zA-Z_0-9", 'w', $1); % words + +set_syntax_flags ($1, 4); + +() = define_keywords_n ($1, "\\ax\\th", 3, 0); +() = define_keywords_n ($1, "\\def", 4, 0); +() = define_keywords_n ($1, "\\cong\\decl\\open", 5, 0); +() = define_keywords_n ($1, "\\close\\graph\\sorts", 6, 0); +() = define_keywords_n ($1, "\\require", 8, 0); +() = define_keywords_n ($1, "\\generate", 9, 0); + +define helena_mode () +{ + variable kmap = "Helena"; + + set_mode(kmap, 0x04); + use_syntax_table (kmap); + runhooks("helena_mode_hook"); +} + +add_mode_for_extension ("helena", "hln"); diff --git a/helm/www/lambdadelta/download/helena_0.8.0.tar.gz b/helm/www/lambdadelta/download/helena_0.8.0.tar.gz new file mode 100644 index 000000000..ef78bc46b Binary files /dev/null and b/helm/www/lambdadelta/download/helena_0.8.0.tar.gz differ diff --git a/helm/www/lambdadelta/download/helena_0.8.1.tar.gz b/helm/www/lambdadelta/download/helena_0.8.1.tar.gz new file mode 100644 index 000000000..c02f7bc14 Binary files /dev/null and b/helm/www/lambdadelta/download/helena_0.8.1.tar.gz differ diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib new file mode 100644 index 000000000..f6df7f861 --- /dev/null +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -0,0 +1,78 @@ +@incollection{lambdadelta7, + author="F. {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", + publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores", + address="Ponta Delgada, Portugal", + editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", + booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", + pages="204-213", + year="2010", + month="July" +} + +@techreport{lambdadelta6, + author="F. {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2009-16", + year="2009", + month="September" +} + +@article{lambdadelta5, + author="F. {Guidi}", + title="{The Formal System $\lambda\delta$}", + publisher="ACM", + address="New York, NY, USA", + journal="Transactions on Computational Logic", + volume="11", + number="1", + year="2009", + month="October", + pages="Article No. 5" +} + +@incollection{lambdadelta4, + author="F. {Guidi}", + title="{Lambda Types on the Lambda Calculus with Abbreviations}", + publisher="Universit\`a di Siena", + address="Siena, Italy", + editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", + booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", + pages="387-387", + year="2007", + month="June" +} + +@techreport{lambdadelta3, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-25", + year="2006", + month="November" +} + +@techreport{lambdadelta2, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-01", + year="2006", + month="January" +} + +@misc{lambdadelta1, + author="F. {Guidi}", + title="{lambda\_delta\_1}", + howpublished="Formal specification with the proof assistant Coq 7.3.1", + year="2007", + month="January", + note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}" +} diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt new file mode 100644 index 000000000..f6df7f861 --- /dev/null +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -0,0 +1,78 @@ +@incollection{lambdadelta7, + author="F. {Guidi}", + title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", + publisher="Centre for Applied Mathematics and Information Technology, Department of Mathematics, University of Azores", + address="Ponta Delgada, Portugal", + editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", + booktitle="Local Proceedings of 6th Conference on Computability in Europe (CiE 2010)", + pages="204-213", + year="2010", + month="July" +} + +@techreport{lambdadelta6, + author="F. {Guidi}", + title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2009-16", + year="2009", + month="September" +} + +@article{lambdadelta5, + author="F. {Guidi}", + title="{The Formal System $\lambda\delta$}", + publisher="ACM", + address="New York, NY, USA", + journal="Transactions on Computational Logic", + volume="11", + number="1", + year="2009", + month="October", + pages="Article No. 5" +} + +@incollection{lambdadelta4, + author="F. {Guidi}", + title="{Lambda Types on the Lambda Calculus with Abbreviations}", + publisher="Universit\`a di Siena", + address="Siena, Italy", + editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", + booktitle="Local Proceedings of 3rd Conference on Computability in Europe (CiE 2007) Technical Report 487", + pages="387-387", + year="2007", + month="June" +} + +@techreport{lambdadelta3, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-25", + year="2006", + month="November" +} + +@techreport{lambdadelta2, + author="F. {Guidi}", + title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", + type="Technical Report", + institution="University of Bologna", + address="Bologna, Italy", + number="UBLCS 2006-01", + year="2006", + month="January" +} + +@misc{lambdadelta1, + author="F. {Guidi}", + title="{lambda\_delta\_1}", + howpublished="Formal specification with the proof assistant Coq 7.3.1", + year="2007", + month="January", + note="Available at the lambda\_delta Web site: {http://lambda-delta.info/}" +} diff --git a/helm/www/lambdadelta/download/lambdadelta_1.tar.gz b/helm/www/lambdadelta/download/lambdadelta_1.tar.gz new file mode 100644 index 000000000..89e3231ec Binary files /dev/null and b/helm/www/lambdadelta/download/lambdadelta_1.tar.gz differ diff --git a/helm/www/lambdadelta/download/ld_talk_1s.pdf b/helm/www/lambdadelta/download/ld_talk_1s.pdf new file mode 100644 index 000000000..3f523b092 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_1s.pdf differ diff --git a/helm/www/lambdadelta/download/ld_talk_2s.pdf b/helm/www/lambdadelta/download/ld_talk_2s.pdf new file mode 100644 index 000000000..f7a3c9464 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_2s.pdf differ diff --git a/helm/www/lambdadelta/download/ld_talk_3s.pdf b/helm/www/lambdadelta/download/ld_talk_3s.pdf new file mode 100644 index 000000000..c3e18f6d6 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_3s.pdf differ diff --git a/helm/www/lambdadelta/download/ld_talk_4s.pdf b/helm/www/lambdadelta/download/ld_talk_4s.pdf new file mode 100644 index 000000000..6552c2140 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_4s.pdf differ diff --git a/helm/www/lambdadelta/download/ld_talk_5s.pdf b/helm/www/lambdadelta/download/ld_talk_5s.pdf new file mode 100644 index 000000000..b7051c919 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_5s.pdf differ diff --git a/helm/www/lambdadelta/download/ld_talk_6s.pdf b/helm/www/lambdadelta/download/ld_talk_6s.pdf new file mode 100644 index 000000000..04fcec20f Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_6s.pdf differ diff --git a/helm/www/lambdadelta/download/ld_talk_7s.pdf b/helm/www/lambdadelta/download/ld_talk_7s.pdf new file mode 100644 index 000000000..754547c91 Binary files /dev/null and b/helm/www/lambdadelta/download/ld_talk_7s.pdf differ diff --git a/helm/www/lambdadelta/download/lddl.tar.bz2 b/helm/www/lambdadelta/download/lddl.tar.bz2 new file mode 100644 index 000000000..0f3262388 Binary files /dev/null and b/helm/www/lambdadelta/download/lddl.tar.bz2 differ diff --git a/helm/www/lambdadelta/images/PNGnow2.png b/helm/www/lambdadelta/images/PNGnow2.png new file mode 100644 index 000000000..dc25983fb Binary files /dev/null and b/helm/www/lambdadelta/images/PNGnow2.png differ diff --git a/helm/www/lambdadelta/images/b3.png b/helm/www/lambdadelta/images/b3.png new file mode 100644 index 000000000..3ed538923 Binary files /dev/null and b/helm/www/lambdadelta/images/b3.png differ diff --git a/helm/www/lambdadelta/images/b4.png b/helm/www/lambdadelta/images/b4.png new file mode 100644 index 000000000..ccfd1a99a Binary files /dev/null and b/helm/www/lambdadelta/images/b4.png differ diff --git a/helm/www/lambdadelta/images/b5.png b/helm/www/lambdadelta/images/b5.png new file mode 100644 index 000000000..30cace1d1 Binary files /dev/null and b/helm/www/lambdadelta/images/b5.png differ diff --git a/helm/www/lambdadelta/images/b9.png b/helm/www/lambdadelta/images/b9.png new file mode 100644 index 000000000..0de559867 Binary files /dev/null and b/helm/www/lambdadelta/images/b9.png differ diff --git a/helm/www/lambdadelta/images/basic_32.png b/helm/www/lambdadelta/images/basic_32.png new file mode 100644 index 000000000..350f6bcb0 Binary files /dev/null and b/helm/www/lambdadelta/images/basic_32.png differ diff --git a/helm/www/lambdadelta/images/crux_16.ico b/helm/www/lambdadelta/images/crux_16.ico new file mode 100644 index 000000000..b4e63327a Binary files /dev/null and b/helm/www/lambdadelta/images/crux_16.ico differ diff --git a/helm/www/lambdadelta/images/crux_177.png b/helm/www/lambdadelta/images/crux_177.png new file mode 100644 index 000000000..38b643264 Binary files /dev/null and b/helm/www/lambdadelta/images/crux_177.png differ diff --git a/helm/www/lambdadelta/images/crux_177.xcf b/helm/www/lambdadelta/images/crux_177.xcf new file mode 100644 index 000000000..685256637 Binary files /dev/null and b/helm/www/lambdadelta/images/crux_177.xcf differ diff --git a/helm/www/lambdadelta/images/crux_32.png b/helm/www/lambdadelta/images/crux_32.png new file mode 100644 index 000000000..465bf19f2 Binary files /dev/null and b/helm/www/lambdadelta/images/crux_32.png differ diff --git a/helm/www/lambdadelta/images/globe_trans.png b/helm/www/lambdadelta/images/globe_trans.png new file mode 100644 index 000000000..463b0be80 Binary files /dev/null and b/helm/www/lambdadelta/images/globe_trans.png differ diff --git a/helm/www/lambdadelta/images/helena_32.png b/helm/www/lambdadelta/images/helena_32.png new file mode 100644 index 000000000..4a065aefe Binary files /dev/null and b/helm/www/lambdadelta/images/helena_32.png differ diff --git a/helm/www/lambdadelta/images/helena_label.png b/helm/www/lambdadelta/images/helena_label.png new file mode 100644 index 000000000..55487ab99 Binary files /dev/null and b/helm/www/lambdadelta/images/helena_label.png differ diff --git a/helm/www/lambdadelta/images/rainbow.png b/helm/www/lambdadelta/images/rainbow.png new file mode 100644 index 000000000..45925baa7 Binary files /dev/null and b/helm/www/lambdadelta/images/rainbow.png differ diff --git a/helm/www/lambdadelta/images/xml_xsl2.png b/helm/www/lambdadelta/images/xml_xsl2.png new file mode 100644 index 000000000..00d82967b Binary files /dev/null and b/helm/www/lambdadelta/images/xml_xsl2.png differ diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html new file mode 100644 index 000000000..7785bbf75 --- /dev/null +++ b/helm/www/lambdadelta/implementation.html @@ -0,0 +1,325 @@ + + + + + lambdadelta home page + + + + + +
+
+ [Crux Logo] +

The Formal System λδ (lambdadelta)
+

+

Towards the unification of terms, types, environments and + contexts

+ [Separator]
+ + + + + + + +
+ + + +
    +
  • Resources
    +
    • +
+ 		+

Computer-checked formal + specifications [Butterfly]

+ Resource + 1 below provides for the statically generated natural language + representation of + λδ meta-theory (faster rendering w.r.t. resource 2 below).
+ Resource 2 below + provides + for the dynamically generated natural + language representation of + λδ meta-theory (powered by the HELM + rendering engine).
+ Remarkably, λδ was born and developed in the digital + format of resource 3 + below, which is not the + formal counterpart of some informal material previously + written on + paper (as it happens for most currently digitalized + Mathematics).
+
    +
  1. F. Guidi: lambdadelta + (revised 2011-09). + Formal + specification for Matita 0.5 + (HTML pages generated + by the HELM + rendering engine)
    + Here are the most relevant theorems proved in the + formal specification: + +
    2. +
  2. F. Guidi: lambdadelta + (revised 2011-09). + Formal + specification for Matita 0.5 (HELM directory).
    +
    +
    3. +
  3. F. Guidi: lambdadelta_1 + (revised 2011-09). +Formal + specification for Coq + 7.3.1 + (source + proof scripts). BibTeX entry.
    +
    4. +
+

Tools [Butterfly]

+ [Crux Logo] The λδ + Digital + Library + (LDDL) is part of HELM + and contains a set of + resources expressed in λδ.
+
    +
  • Contents: + Landau's "Grundlagen + der Analysis" (from + Jutting's specification in Automath).
    +
    • +
+ + +
+ [Helena Logo] Helena + is a λδ + processor, + implemented in Caml + as a part of + the HELM software, + meant for + testing the stable features of the calculus as well as the + unstable + ones.
+ The processor source code is available in the directory /trunk/helm/software/helena/ + of the HELM + Svn + repository. The Svn revisions containing the stable + versions + of  Helena are indicated below.
+
    +
  • Version 0.8.2. + In + progress.
    +
    • +
+
    +
  • Version 0.8.1 + (2010-11). + Exploits a subset of "complete_rg" λδ as the + intermediate language. + Features importation from ".hln" files containing λδ + textual syntax. + The overall validation speed of the "Grundlagen + der + Analysis" increases of 22% with respect to + version 0.8.0. [Svn + revision: 11032] (archived + source code) + +
    • +
+
    +
  • Version 0.8.0 (2009-09). + Supports + "basic_rg" λδ with naive implementation of + impredicative sort + inclusion. Features + importation from Automath + and exportation to XML. + [Svn + revision: 10304] (archived + source code)
    +
      +
    • 2009-09. + Jutting's specification of Landau's "Grundlagen + der + Analysis" enters λδ Digital Library.
      +
      • +
    • 2009-06. + Jutting's specification of Landau's "Grundlagen + der + Analysis" is + successfully processed, enabling sort inclusion.
      • +
    +
    • +
+

Other resources [Butterfly]

+ +
    +
  • A Jed mode + for + editing ".hln" files (containing λδ textual syntax): helena.sl + (revised 2010-11).
    • +
+ +
    +
  • A logo for λδ: crux_177.png + (revised 2012-09).
    +
    • +
+
+
+ [Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+ Last update 2012-12-01 by Ferruccio + Guidi
+
+ + diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html new file mode 100644 index 000000000..fc46d7254 --- /dev/null +++ b/helm/www/lambdadelta/index.html @@ -0,0 +1,179 @@ + + + + + lambdadelta home page + + + + + +
+
+[Crux Logo] +

The Formal System λδ (lambdadelta)
+

+

Towards the unification of terms, types, environments and contexts

+[Separator]
+ + + + + + + +
+
    +
  • Foreword
    • +
+ + + + 		+

Foreword [Butterfly]

+The formal system λδ +(lambdadelta) is a typed lambda calculus that pursues the static and +dynamic unification of terms, types, environments and contexts while +enjoying a well-conceived meta-theory, which includes the commonly +desired properties.
+
+λδ takes some features from the calculi of the Automath family and +some from the pure type systems, but it differs from both in that it +does not include the Π construction while it provides for an +abbreviation mechanism at the level of terms.
+
+λδ features explicit type annotations, which are borrowed from +realistic type checker implementations and with which type checking is +reduced to type inference.
+
+The reduction steps of λδ include β-contraction, δ-expansion, +ζ-contraction and θ-swap. On the other hand, +η-contraction is not included.
+
+The meta-theory of λδ includes important properties such as the +confluence of reduction, the correctness of types, the +uniqueness of types up to conversion, the subject reduction of the type +assignment, the strong normalization of the typed terms. The +decidability of type inference and of type checking come as corollaries.
+
+λδ features uniformly dependent types and a predicative abstraction +mechanism, so the calculus can serve as a formal specification language +for the type theories that need a predicative foundation. λδ is +expected to have the expressive power of λ→.
+
+λδ comes in several versions listed in the following table, which +includes the major milestones:
+
+ + + + + + + + + + + + + + + + + + + + + + + + +
Version
+ 		Name
+ 		Started
+ 		Released
+ 		Dismissed
+
2
+ 		basic_2
+ 		April +2011
+ 		planned +in +2013
+ 		not +planned yet
+
1
+ 		basic_1
+ 		May +2004
+ 		November +2006
+ 		May +2008
+
+
+

Notice +for +the +Internet +Explorer +user [Butterfly]

+To view this site +correctly, please select a font with Unicode +support. +For example Lucida Sans Unicode +(it should be already installed on your system). +To change the current font follow: "Tools" +menu +→ "Internet +Options" entry → "General" tab → "Fonts" button.
+
+
+[Valid HTML 4.01 Transitional] [Use Any Browser Here] [PNG Used Here]
+
+Last update 2012-12-01 by Ferruccio +Guidi
+
+ + diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html new file mode 100644 index 000000000..7d581cbb7 --- /dev/null +++ b/helm/www/lambdadelta/news.html @@ -0,0 +1,259 @@ + + + + + lambdadelta home page + + + + + +

+[Crux Logo] +

The Formal System λδ (lambdadelta)
+

+

Towards the unification of terms, types, environments and contexts

+[Separator]
+ + + + + + + +
+ +
    +
  • News
    • +
+ + + 		+

News [Butterfly]

+
    +
  • September 2011. The +denomination "lambdadelta" changes to "lambdadelta". +
      +
    • The character "-" is reserved in λδ textual syntax +(recognized by Helena 0.8.1). +
      • +
    • Eventually, the occurrences of the character "-" will +be replaced by "_" in all λδ-related identifiers.
      • +
    • In particular, this refactoring involves file names and +path names.
      • +
    • The permanent λδ URL is sheduled to become http://lambdadelta.info on +December 2012.
      +
      • +
    +
    • +
+
    +
  • April 2011. The +specification of λδ version 2 and related topics is restarted in Matita 0.5. +
      +
    • Here is a page about the +topics related to the specification (Applications).
      • +
    • Here is a page about the +specification (Core).
      • +
    +
    • +
+ +
    +
  • November 2010. Helena 0.8.1 is released.
    +
    • +
+ + + +
    +
  • September 2008. +This site is online.
    +
    • +
+ + + + +
    +
  • May 2008. The +specification of λδ version 1 is closed.
    +
    • +
+
    +
  • March 2008. The +specification of λδ version 2 is started with Coq 7.3.1 (false start).
    • +
+ + + + + +

Visibility [Butterfly]

+
    +
  • February 2012. The Google search for formal system lambda delta gives +5 resources about λδ in the first 6 results.
    +
    • +
+
    +
  • February 2012. The Yahoo search formal system lambda delta gives +this site as the first result.
    • +
+
+
+[Valid HTML 4.01 Transitional] [Use Any + Browser Here] [PNG Used Here]
+
+Last update 2012-12-01 by Ferruccio + +Guidi
+
+ + diff --git a/helm/www/lambdadelta/web/home/BTM.ldw.xml b/helm/www/lambdadelta/web/home/BTM.ldw.xml new file mode 100644 index 000000000..63f49585e --- /dev/null +++ b/helm/www/lambdadelta/web/home/BTM.ldw.xml @@ -0,0 +1,15 @@ + + + +
Character classes
+ This table shows how the first 45 positive integers + are distributed in the four classes. + + + +
+ diff --git a/helm/www/lambdadelta/web/home/apps_2.ldw.xml b/helm/www/lambdadelta/web/home/apps_2.ldw.xml new file mode 100644 index 000000000..6b108c960 --- /dev/null +++ b/helm/www/lambdadelta/web/home/apps_2.ldw.xml @@ -0,0 +1,52 @@ + + + +
Contents of the Specification
+ This specification comprises a collection of checked + applications of λδ version 2. + In particular it contains the components below. + + + Martin-Löf's Type Theory with one universe + using λδ as theory of expressions. + + + The validation algorithm for λδ as implemented in + Helena 0.8. + + +
Summary of the Specification
+ Here is a numerical acount of the specification's contents + and its timeline. + +
+ + The Applications directory is started. + + + The Functional component is started + inside the specification of λδ version 2. + + + The MLTT1 component is started. + + +
Logical Structure of the Specification
+ The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each component. + +
+ diff --git a/helm/www/lambdadelta/web/home/apps_2_src.tbl b/helm/www/lambdadelta/web/home/apps_2_src.tbl new file mode 100644 index 000000000..d5508e3d6 --- /dev/null +++ b/helm/www/lambdadelta/web/home/apps_2_src.tbl @@ -0,0 +1,38 @@ +name "apps_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "orange" + [ { "MLTT1" * } { + [ { "" * } { + [ "genv_primitive" "judgement" * ] + } + ] + } + ] + class "red" + [ { "functional" * } { + [ { "reduction and type machine" * } { + [ "rtm" "rtm_step ( ? ⇨ ? )" * ] + } + ] + [ { "unfold" * } { + [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] + } + ] + } + ] +} + +class "component" { 0 } + +class "plane" { 1 } + +class "file" { 2 * } diff --git a/helm/www/lambdadelta/web/home/basic_2.ldw.xml b/helm/www/lambdadelta/web/home/basic_2.ldw.xml new file mode 100644 index 000000000..9159f0411 --- /dev/null +++ b/helm/www/lambdadelta/web/home/basic_2.ldw.xml @@ -0,0 +1,78 @@ + + + +
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. + +
+ + Context-sensitive subject equivalence + for native type assignment. + + + Closure of extended context-sensitive computation + for native validity. + + + Extended context-sensitive strong normalization + for simply typed terms. + + + Confluence for context-free parallel reduction on closures. + + + Term binders polarized to control ζ reduction. + + + Context-sensitive subject equivalence + for atomic arity assignment + (anniversary milestone). + + + Context-sensitive strong normalization + for simply typed terms. + + + Support for abstract candidates of reducibility. + + + Confluence for context-sensitive parallel reduction on terms. + + + Confluence for context-free parallel reduction on terms. + + + Specification starts. + + +
Logical Structure of the Specification
+ The source files are grouped in planes and components + according to the following table. + A notation file covering the whole specification is provided. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each component. + +
+ diff --git a/helm/www/lambdadelta/web/home/basic_2_blk.tbl b/helm/www/lambdadelta/web/home/basic_2_blk.tbl new file mode 100644 index 000000000..ed50adf79 --- /dev/null +++ b/helm/www/lambdadelta/web/home/basic_2_blk.tbl @@ -0,0 +1,52 @@ +name "basic_2_blk" + +table { + class "grey" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "wine" [ + [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ] + [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] + ] + class "magenta" [ + [ "local typed declaration **" ] [ "Γ ⊢ -λW" ] + [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] + ] + class "prune" [ + [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ] + [ "no" ] [ "no" ] [ "no" ] [ "$p" ] + ] + class "blue" [ + [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ] + [ "no" ] [ "no" ] [ "yes" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "sky" [ + [ "local abbreviation *" ] [ "Γ ⊢ +δV" ] + [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ] + ] + class "cyan" [ + [ "local definition **" ] [ "Γ ⊢ -δV" ] + [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ] + ] + class "water" [ + [ "global definition ***" ] [ "Γ ⊢ pδV" ] + [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ] + ] + } ] + [ { "no" * } { + class "green" [ + [ "sort ****" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "text" { 0 } { 2 * } + +class "plane" { 1 } diff --git a/helm/www/lambdadelta/web/home/basic_2_src.tbl b/helm/www/lambdadelta/web/home/basic_2_src.tbl new file mode 100644 index 000000000..28aacba87 --- /dev/null +++ b/helm/www/lambdadelta/web/home/basic_2_src.tbl @@ -0,0 +1,304 @@ +name "basic_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] +(* + class "wine" + [ { "examples" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] + class "magenta" + [ { "higher order dynamic typing" * } { + [ { "higher order native type assignment" * } { + [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + } + ] + } + ] +*) + class "prune" + [ { "dynamic typing" * } { +(* + [ { "local env. ref. for native type assignment" * } { + [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ] + } + ] + [ { "native type assignment" * } { + [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ] + } + ] +*) + [ { "stratified native validity" * } { + [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" + "snv_ssta" * ] + } + ] + } + ] + class "blue" + [ { "equivalence" * } { + [ { "focalized equivalence" * } { + [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ] + [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ] + } + ] + [ { "local env. ref. for context-sensitive equivalence" * } { + [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ] + } + ] + [ { "context-sensitive equivalence" * } { + [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ] + } + ] + } + ] + class "sky" + [ { "conversion" * } { + [ { "focalized conversion" * } { + [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ] + [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ] + } + ] + [ { "context-sensitive conversion" * } { + [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] + } + ] + } + ] + class "cyan" + [ { "computation" * } { +(* + [ { "hyper computation" * } { + [ "ysteps ( ? ⊢ ⦃?,?⦄ •⭃*[g] ⦃?,?⦄ )" "ysteps_csups" * ] + [ "yprs ( ? ⊢ ⦃?,?⦄ •⥸*[g] ⦃?,?⦄ )" "yprs_csups" + "yprs_xprs" + "yprs_yprs" * ] + } + ] +*) + [ { "extended computation" * } { + [ "xprs ( ⦃?,?⦄ ⊢ ? •➡*[?] ? )" "xprs_lift" + "xprs_aaa" + "xpr_lsubss" + "xprs_cprs" + "xprs_xprs" * ] + } + ] + [ { "weakly normalizing computation" * } { + [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ] + } + ] + [ { "strongly normalizing computation" * } { + [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" + "csn_tstc_vector" + "csn_aaa" * ] + [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ] + } + ] + [ { "focalized computation" * } { + [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_cprs" + "lfprs_lfprs" * ] + [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] + } + ] + [ { "context-sensitive computation" * } { + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ] + } + ] + [ { "context-free computation" * } { + [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" + "ltprs_ltprs" * ] + [ "tprs ( ? ➡* ?)" "tprs_lift" + "tprs_tprs" * ] + } + ] + [ { "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 "water" + [ { "reducibility" * } { +(* + [ { "hyper reduction" * } { + [ "ypr ( ? ⊢ ⦃?,?⦄ •⥸[g] ⦃?,?⦄ )" * ] + } + ] +*) + [ { "extended reduction" * } { + [ "xpr ( ⦃?,?⦄ ⊢ ? •➡[?] ? )" "xpr_lift" + "xpr_aaa" + "xpr_lsubss" * ] + } + ] + [ { "context-sensitive focalized reduction" * } { + [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ] + } + ] + [ { "context-free focalized reduction" * } { + [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" "lfpr_aaa" + "lfpr_cpr" + "lfpr_fpr" + "lfpr_lfpr" * ] + [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ] + } + ] + [ { "context-sensitive normal forms" * } { + [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ] + } + ] + [ { "context-sensitive reduction" * } { + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ] + } + ] + [ { "context-sensitive reducible forms" * } { + [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ] + } + ] + [ { "context-free normal forms" * } { + [ "thnf ( 𝐇𝐍⦃?⦄ )" * ] + } + ] + [ { "context-free reduction" * } { + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ] + [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ] + } + ] + } + ] + class "green" + [ { "unwind" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] +(* + [ { "stratified unwind" * } { + [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" "sstas_ltpss" "sstas_sstas" * ] + } + ] +*) + class "grass" + [ { "static typing" * } { + [ { "local env. ref. for stratified static type assignment" * } { + [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ] + } + ] + [ { "stratified static type assignment" * } { + [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ] + } + ] + [ { "local env. ref. for atomic arity assignment" * } { + [ "lsuba ( ? ⁝⊑ ? )" "lsuba_ldrop" + "lsuba_aaa" + "lsuba_lsuba" * ] + } + ] + [ { "atomic arity assignment" * } { + [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_ltpss_dx" + "aaa_ltpss_sn" + "aaa_aaa" * ] + } + ] + [ { "parameters" * } { + [ "sh" "sd" * ] + } + ] + } + ] + class "yellow" + [ { "unfold" * } { + [ { "basic local env. thinning" * } { + [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ] + } + ] + [ { "inverse basic term relocation" * } { + [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ] + } + ] + [ { "partial unfold" * } { + [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ] + [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ] + [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ] + } + ] + [ { "generic local env. slicing" * } { + [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] + } + ] + [ { "iterated restricted structural predecessor for closures" * } { + [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ] + [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ] + } + ] + [ { "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" * } { + [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ] + } + ] + [ { "global env. slicing" * } { + [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] + } + ] + [ { "basic local env. slicing" * } { + [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_sfr" + "ldrop_ldrop" * ] + } + ] + [ { "local env. ref. for substitution" * } { + [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ] + } + ] + [ { "restricted structural predecessor for closures" * } { + [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ] + } + ] + [ { "basic term relocation" * } { + [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] + [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "same head term form" * } { + [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ] + } + ] + [ { "same top term constructor" * } { + [ "tstc ( ? ≃ ? )" "tstc_tstc" + "tstc_vector" * ] + } + ] + [ { "closures" * } { + [ "cl_shift ( ? @@ ? )" "cl_weight ( #{?,?} )" * ] + } + ] + [ { "internal syntax" * } { + [ "genv" * ] + [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_bi" * ] + [ "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/lambdadelta/xml/ld.dtd b/helm/www/lambdadelta/xml/ld.dtd new file mode 100644 index 000000000..369f8c400 --- /dev/null +++ b/helm/www/lambdadelta/xml/ld.dtd @@ -0,0 +1,140 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/helm/www/lambdadelta/xslt/ld_web.xsl b/helm/www/lambdadelta/xslt/ld_web.xsl new file mode 100644 index 000000000..288973806 --- /dev/null +++ b/helm/www/lambdadelta/xslt/ld_web.xsl @@ -0,0 +1,21 @@ + + + + + + + + + + + + + diff --git a/helm/www/lambdadelta/xslt/ld_web_library.xsl b/helm/www/lambdadelta/xslt/ld_web_library.xsl new file mode 100644 index 000000000..a90d005a1 --- /dev/null +++ b/helm/www/lambdadelta/xslt/ld_web_library.xsl @@ -0,0 +1,90 @@ + + + + + +
+ + [lambdadelta home] + +
+ + + +
+ [Spacer] +
+ + + + + [Valid XHTML 1.1] + + + + + + [Valid CSS level 2] + + + + + + [Generated from XML via XSL] + + + + + + [PNG used here] + + + + + + [Viewable with any browser] + + + + + + [Powered by Helena lambdadelta processor] + + + + diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl new file mode 100644 index 000000000..7c0afb538 --- /dev/null +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -0,0 +1,92 @@ + + + + + +
+ +
+ + + +
+ +
+ + + + + + + + + +
  • + + +
+ + + +
+ +
+ + + + +

+
+ + + + + + +
+

+
+ + +
+ + + + + + + + + + + + + + <xsl:value-of select="@title"/> + + + + + + +
+ + + + + + diff --git a/helm/www/lambdadelta/xslt/lddl.xsl b/helm/www/lambdadelta/xslt/lddl.xsl new file mode 100644 index 000000000..2711cff96 --- /dev/null +++ b/helm/www/lambdadelta/xslt/lddl.xsl @@ -0,0 +1,33 @@ + + + + + + + + + + + + + + + + diff --git a/helm/www/lambdadelta/xslt/lddl_entity.xsl b/helm/www/lambdadelta/xslt/lddl_entity.xsl new file mode 100644 index 000000000..99f699d9b --- /dev/null +++ b/helm/www/lambdadelta/xslt/lddl_entity.xsl @@ -0,0 +1,62 @@ + + + + + + + + + + +
+ + + + + + + + + + + + + + +
+
+ + + + +
+
+ +
+ + + + + Declaration + + + + + + Definition + + + + diff --git a/helm/www/lambdadelta/xslt/lddl_library.xsl b/helm/www/lambdadelta/xslt/lddl_library.xsl new file mode 100644 index 000000000..e69468a9d --- /dev/null +++ b/helm/www/lambdadelta/xslt/lddl_library.xsl @@ -0,0 +1,284 @@ + + + + + + + + + + + + , + + + + / + + + + + + + + + .​ + + + + ( + + + + ) + + + + [ + + + + ] + + + + < + + + + > + + + + : + + + + = + + + + " + + + + Informal description: + + + + Validation parameters: + + + + sort hierarchy = + + + + kernel options = + + + + + + + + + + + + + &Pi; + + + + &Pi; + + + &lambda; + + + &lambda; + &infin; + + + &lambda; + + + + + + + + + &delta; + + + + + + &chi; + + + + + + + + + + + + + + + + + + + + + .html + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + &lambda;&delta; Digital Library (LDDL) + + + diff --git a/helm/www/lambdadelta/xslt/lddl_root.xsl b/helm/www/lambdadelta/xslt/lddl_root.xsl new file mode 100644 index 000000000..ba2dd9028 --- /dev/null +++ b/helm/www/lambdadelta/xslt/lddl_root.xsl @@ -0,0 +1,114 @@ + + + + + + + + + + + + + + + + lambdadelta digital library (LDDL) + + + + +
+ + [lambdadelta home] +
+
+ +
+
+ [Spacer] +
+ +
+ + [Valid XHTML 1.1] + + [Valid CSS level 2] + + [Generated from XML via XSL] + + [Powered by Helena lambdadelta processor] + + [PNG used here] + + [Viewable with any browser] +
+ + + + + +
+ + + + + + + + + + + +
+ + + diff --git a/helm/www/lambdadelta/xslt/lddl_term.xsl b/helm/www/lambdadelta/xslt/lddl_term.xsl new file mode 100644 index 000000000..d2cb461a3 --- /dev/null +++ b/helm/www/lambdadelta/xslt/lddl_term.xsl @@ -0,0 +1,97 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +