From: Ferruccio Guidi Date: Sat, 1 Dec 2012 19:37:15 +0000 (+0000) Subject: old lambdadelta home page is dismissed X-Git-Tag: make_still_working~1424 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=207a37632296335aa8db7b22482f91634f74e4e1;p=helm.git old lambdadelta home page is dismissed --- diff --git a/helm/www/lambda_delta/BTM.html b/helm/www/lambda_delta/BTM.html deleted file mode 100644 index d41ec154b..000000000 --- a/helm/www/lambda_delta/BTM.html +++ /dev/null @@ -1,25 +0,0 @@ - - - - - - - - - - BTM - - - - - -
[lambda_delta 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-11-22T16:07:02+01:00
- - diff --git a/helm/www/lambda_delta/Makefile b/helm/www/lambda_delta/Makefile deleted file mode 100644 index 65437a483..000000000 --- a/helm/www/lambda_delta/Makefile +++ /dev/null @@ -1,98 +0,0 @@ -H=@ - -TAGS = www up \ - lint-xml index lddl install-xml \ - test-html html install-html \ - install-jed install-bib \ - -LDDLURL = http://lambda-delta.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/lambda_delta -RXMLDIR = $(REMOTE):$(RDIR)/xml -RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl - -SLS = helena.sl automath.sl -BIB = lambda_delta.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/lambda_delta/apps_2.html b/helm/www/lambda_delta/apps_2.html deleted file mode 100644 index f77bae790..000000000 --- a/helm/www/lambda_delta/apps_2.html +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - - - - - applications of lambda_delta version 2 - - - - - -
[lambda_delta home]
cic:/matita/lambda_delta/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-11-22T16:07:02+01:00
- - diff --git a/helm/www/lambda_delta/basic_2.html b/helm/www/lambda_delta/basic_2.html deleted file mode 100644 index c51e61ef2..000000000 --- a/helm/www/lambda_delta/basic_2.html +++ /dev/null @@ -1,88 +0,0 @@ - - - - - - - - - - lambda_delta version 2 - - - - - -
[lambda_delta home]
cic:/matita/lambda_delta/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-11-22T16:07:02+01:00
- - diff --git a/helm/www/lambda_delta/bin/a.ml b/helm/www/lambda_delta/bin/a.ml deleted file mode 100644 index 4f310c873..000000000 --- a/helm/www/lambda_delta/bin/a.ml +++ /dev/null @@ -1,17 +0,0 @@ -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/lambda_delta/bin/xhtbl/Makefile b/helm/www/lambda_delta/bin/xhtbl/Makefile deleted file mode 100644 index fa9d7b73c..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/Makefile +++ /dev/null @@ -1,36 +0,0 @@ -EXEC = xhtbl -VERSION=0.1.1 - -REQUIRES = str - -YACCFLAGS = -v - -include Makefile.common - -XSLT = xsltproc -XHTBL = ./xhtbl.native - -LDURL = http://lambda-delta.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/lambda_delta/bin/xhtbl/Makefile.common b/helm/www/lambda_delta/bin/xhtbl/Makefile.common deleted file mode 100644 index bf944971b..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/Makefile.common +++ /dev/null @@ -1,27 +0,0 @@ -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/lambda_delta/bin/xhtbl/css.ml b/helm/www/lambda_delta/bin/xhtbl/css.ml deleted file mode 100644 index 82a41e91c..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/css.ml +++ /dev/null @@ -1,20 +0,0 @@ -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/lambda_delta/bin/xhtbl/fold.ml b/helm/www/lambda_delta/bin/xhtbl/fold.ml deleted file mode 100644 index 752b06d77..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/fold.ml +++ /dev/null @@ -1,25 +0,0 @@ -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/lambda_delta/bin/xhtbl/matrix.ml b/helm/www/lambda_delta/bin/xhtbl/matrix.ml deleted file mode 100644 index 4769a5457..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/matrix.ml +++ /dev/null @@ -1,52 +0,0 @@ -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/lambda_delta/bin/xhtbl/options.ml b/helm/www/lambda_delta/bin/xhtbl/options.ml deleted file mode 100644 index ce1c88867..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/options.ml +++ /dev/null @@ -1,34 +0,0 @@ -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/lambda_delta/bin/xhtbl/pass1.ml b/helm/www/lambda_delta/bin/xhtbl/pass1.ml deleted file mode 100644 index 1c53e7d6f..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/pass1.ml +++ /dev/null @@ -1,86 +0,0 @@ -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/lambda_delta/bin/xhtbl/pass2.ml b/helm/www/lambda_delta/bin/xhtbl/pass2.ml deleted file mode 100644 index 68cc7ba99..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/pass2.ml +++ /dev/null @@ -1,139 +0,0 @@ -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/lambda_delta/bin/xhtbl/pass3.ml b/helm/www/lambda_delta/bin/xhtbl/pass3.ml deleted file mode 100644 index 4513828b5..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/pass3.ml +++ /dev/null @@ -1,23 +0,0 @@ -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/lambda_delta/bin/xhtbl/table.ml b/helm/www/lambda_delta/bin/xhtbl/table.ml deleted file mode 100644 index e363cd434..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/table.ml +++ /dev/null @@ -1,54 +0,0 @@ -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/lambda_delta/bin/xhtbl/textLexer.mll b/helm/www/lambda_delta/bin/xhtbl/textLexer.mll deleted file mode 100644 index 7557e7bb8..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/textLexer.mll +++ /dev/null @@ -1,35 +0,0 @@ -{ - 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/lambda_delta/bin/xhtbl/textParser.mly b/helm/www/lambda_delta/bin/xhtbl/textParser.mly deleted file mode 100644 index 333d3421f..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/textParser.mly +++ /dev/null @@ -1,95 +0,0 @@ -%{ - -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/lambda_delta/bin/xhtbl/textUnparser.ml b/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml deleted file mode 100644 index 54995e96b..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/textUnparser.ml +++ /dev/null @@ -1,91 +0,0 @@ -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/lambda_delta/bin/xhtbl/xhtbl.ml b/helm/www/lambda_delta/bin/xhtbl/xhtbl.ml deleted file mode 100644 index cf4d818b6..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/xhtbl.ml +++ /dev/null @@ -1,76 +0,0 @@ -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/lambda_delta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml deleted file mode 100644 index 3583c2f75..000000000 --- a/helm/www/lambda_delta/bin/xhtbl/xmlUnparser.ml +++ /dev/null @@ -1,82 +0,0 @@ -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/lambda_delta/css/ld_web.css b/helm/www/lambda_delta/css/ld_web.css deleted file mode 100644 index 9e7c3fc08..000000000 --- a/helm/www/lambda_delta/css/ld_web.css +++ /dev/null @@ -1,121 +0,0 @@ -@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/lambda_delta/css/lddl.css b/helm/www/lambda_delta/css/lddl.css deleted file mode 100644 index 41a635d45..000000000 --- a/helm/www/lambda_delta/css/lddl.css +++ /dev/null @@ -1,43 +0,0 @@ -@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/lambda_delta/css/xhtbl.css b/helm/www/lambda_delta/css/xhtbl.css deleted file mode 100644 index f58db47c3..000000000 --- a/helm/www/lambda_delta/css/xhtbl.css +++ /dev/null @@ -1,108 +0,0 @@ -@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/lambda_delta/documentation.html b/helm/www/lambda_delta/documentation.html deleted file mode 100644 index 3e6457ba5..000000000 --- a/helm/www/lambda_delta/documentation.html +++ /dev/null @@ -1,355 +0,0 @@ - - - - - lambda_delta home page - - - - - -
-
- [Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

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 - lambda_delta 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 - lambda-delta (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 - lambda_delta 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 lambda-delta - (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-02-24 by Ferruccio - Guidi
-
- - diff --git a/helm/www/lambda_delta/download/automath.sl b/helm/www/lambda_delta/download/automath.sl deleted file mode 100644 index d28950a36..000000000 --- a/helm/www/lambda_delta/download/automath.sl +++ /dev/null @@ -1,27 +0,0 @@ -$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/lambda_delta/download/cie_2007.pdf b/helm/www/lambda_delta/download/cie_2007.pdf deleted file mode 100644 index d369a8bc3..000000000 Binary files a/helm/www/lambda_delta/download/cie_2007.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/cie_2010.pdf b/helm/www/lambda_delta/download/cie_2010.pdf deleted file mode 100644 index 8afbebb26..000000000 Binary files a/helm/www/lambda_delta/download/cie_2010.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/helena.sl b/helm/www/lambda_delta/download/helena.sl deleted file mode 100644 index fc8b1903e..000000000 --- a/helm/www/lambda_delta/download/helena.sl +++ /dev/null @@ -1,28 +0,0 @@ -$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/lambda_delta/download/helena_0.8.0.tar.gz b/helm/www/lambda_delta/download/helena_0.8.0.tar.gz deleted file mode 100644 index ef78bc46b..000000000 Binary files a/helm/www/lambda_delta/download/helena_0.8.0.tar.gz and /dev/null differ diff --git a/helm/www/lambda_delta/download/helena_0.8.1.tar.gz b/helm/www/lambda_delta/download/helena_0.8.1.tar.gz deleted file mode 100644 index c02f7bc14..000000000 Binary files a/helm/www/lambda_delta/download/helena_0.8.1.tar.gz and /dev/null differ diff --git a/helm/www/lambda_delta/download/lambda_delta.bib b/helm/www/lambda_delta/download/lambda_delta.bib deleted file mode 100644 index f6df7f861..000000000 --- a/helm/www/lambda_delta/download/lambda_delta.bib +++ /dev/null @@ -1,78 +0,0 @@ -@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/lambda_delta/download/lambda_delta.txt b/helm/www/lambda_delta/download/lambda_delta.txt deleted file mode 100644 index f6df7f861..000000000 --- a/helm/www/lambda_delta/download/lambda_delta.txt +++ /dev/null @@ -1,78 +0,0 @@ -@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/lambda_delta/download/lambda_delta_1.tar.gz b/helm/www/lambda_delta/download/lambda_delta_1.tar.gz deleted file mode 100644 index d83966597..000000000 Binary files a/helm/www/lambda_delta/download/lambda_delta_1.tar.gz and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_1s.pdf b/helm/www/lambda_delta/download/ld_talk_1s.pdf deleted file mode 100644 index 3f523b092..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_1s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_2s.pdf b/helm/www/lambda_delta/download/ld_talk_2s.pdf deleted file mode 100644 index f7a3c9464..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_2s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_3s.pdf b/helm/www/lambda_delta/download/ld_talk_3s.pdf deleted file mode 100644 index c3e18f6d6..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_3s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_4s.pdf b/helm/www/lambda_delta/download/ld_talk_4s.pdf deleted file mode 100644 index 6552c2140..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_4s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_5s.pdf b/helm/www/lambda_delta/download/ld_talk_5s.pdf deleted file mode 100644 index b7051c919..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_5s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_6s.pdf b/helm/www/lambda_delta/download/ld_talk_6s.pdf deleted file mode 100644 index 04fcec20f..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_6s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/ld_talk_7s.pdf b/helm/www/lambda_delta/download/ld_talk_7s.pdf deleted file mode 100644 index 754547c91..000000000 Binary files a/helm/www/lambda_delta/download/ld_talk_7s.pdf and /dev/null differ diff --git a/helm/www/lambda_delta/download/lddl.tar.bz2 b/helm/www/lambda_delta/download/lddl.tar.bz2 deleted file mode 100644 index 0f3262388..000000000 Binary files a/helm/www/lambda_delta/download/lddl.tar.bz2 and /dev/null differ diff --git a/helm/www/lambda_delta/images/PNGnow2.png b/helm/www/lambda_delta/images/PNGnow2.png deleted file mode 100644 index dc25983fb..000000000 Binary files a/helm/www/lambda_delta/images/PNGnow2.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/b3.png b/helm/www/lambda_delta/images/b3.png deleted file mode 100644 index 3ed538923..000000000 Binary files a/helm/www/lambda_delta/images/b3.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/b4.png b/helm/www/lambda_delta/images/b4.png deleted file mode 100644 index ccfd1a99a..000000000 Binary files a/helm/www/lambda_delta/images/b4.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/b5.png b/helm/www/lambda_delta/images/b5.png deleted file mode 100644 index 30cace1d1..000000000 Binary files a/helm/www/lambda_delta/images/b5.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/b9.png b/helm/www/lambda_delta/images/b9.png deleted file mode 100644 index 0de559867..000000000 Binary files a/helm/www/lambda_delta/images/b9.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/basic_32.png b/helm/www/lambda_delta/images/basic_32.png deleted file mode 100644 index 350f6bcb0..000000000 Binary files a/helm/www/lambda_delta/images/basic_32.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/crux_16.ico b/helm/www/lambda_delta/images/crux_16.ico deleted file mode 100644 index b4e63327a..000000000 Binary files a/helm/www/lambda_delta/images/crux_16.ico and /dev/null differ diff --git a/helm/www/lambda_delta/images/crux_177.png b/helm/www/lambda_delta/images/crux_177.png deleted file mode 100644 index 38b643264..000000000 Binary files a/helm/www/lambda_delta/images/crux_177.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/crux_177.xcf b/helm/www/lambda_delta/images/crux_177.xcf deleted file mode 100644 index 685256637..000000000 Binary files a/helm/www/lambda_delta/images/crux_177.xcf and /dev/null differ diff --git a/helm/www/lambda_delta/images/crux_32.png b/helm/www/lambda_delta/images/crux_32.png deleted file mode 100644 index 465bf19f2..000000000 Binary files a/helm/www/lambda_delta/images/crux_32.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/globe_trans.png b/helm/www/lambda_delta/images/globe_trans.png deleted file mode 100644 index 463b0be80..000000000 Binary files a/helm/www/lambda_delta/images/globe_trans.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/helena_32.png b/helm/www/lambda_delta/images/helena_32.png deleted file mode 100644 index 4a065aefe..000000000 Binary files a/helm/www/lambda_delta/images/helena_32.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/helena_label.png b/helm/www/lambda_delta/images/helena_label.png deleted file mode 100644 index 55487ab99..000000000 Binary files a/helm/www/lambda_delta/images/helena_label.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/rainbow.png b/helm/www/lambda_delta/images/rainbow.png deleted file mode 100644 index 45925baa7..000000000 Binary files a/helm/www/lambda_delta/images/rainbow.png and /dev/null differ diff --git a/helm/www/lambda_delta/images/xml_xsl2.png b/helm/www/lambda_delta/images/xml_xsl2.png deleted file mode 100644 index 00d82967b..000000000 Binary files a/helm/www/lambda_delta/images/xml_xsl2.png and /dev/null differ diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html deleted file mode 100644 index 598daae78..000000000 --- a/helm/www/lambda_delta/implementation.html +++ /dev/null @@ -1,325 +0,0 @@ - - - - - lambda_delta home page - - - - - -
-
- [Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

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: lambda_delta - (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: lambda_delta - (revised 2011-09). - Formal - specification for Matita 0.5 (HELM directory).
    -
    -
    3. -
  3. F. Guidi: lambda_delta_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-10-16 by Ferruccio - Guidi
-
- - diff --git a/helm/www/lambda_delta/index.html b/helm/www/lambda_delta/index.html deleted file mode 100644 index 6e7492e4e..000000000 --- a/helm/www/lambda_delta/index.html +++ /dev/null @@ -1,179 +0,0 @@ - - - - - lambda_delta home page - - - - - -
-
-[Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
-
    -
  • Foreword
    • -
- - - - 		-

Foreword [Butterfly]

-The formal system λδ -(lambda_delta) 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-11-20 by Ferruccio -Guidi
-
- - diff --git a/helm/www/lambda_delta/news.html b/helm/www/lambda_delta/news.html deleted file mode 100644 index 74a213109..000000000 --- a/helm/www/lambda_delta/news.html +++ /dev/null @@ -1,259 +0,0 @@ - - - - - lambda_delta home page - - - - - -

-[Crux Logo] -

The Formal System λδ (lambda_delta)
-

-

Towards the unification of terms, types, environments and contexts

-[Separator]
- - - - - - - -
- -
    -
  • News
    • -
- - - 		-

News [Butterfly]

-
    -
  • September 2011. The -denomination "lambda-delta" changes to "lambda_delta". -
      -
    • 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://lambda_delta.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-11-20 by Ferruccio - -Guidi
-
- - diff --git a/helm/www/lambda_delta/web/home/BTM.ldw.xml b/helm/www/lambda_delta/web/home/BTM.ldw.xml deleted file mode 100644 index 141113108..000000000 --- a/helm/www/lambda_delta/web/home/BTM.ldw.xml +++ /dev/null @@ -1,15 +0,0 @@ - - - -
Character classes
- This table shows how the first 45 positive integers - are distributed in the four classes. - - - -
- diff --git a/helm/www/lambda_delta/web/home/apps_2.ldw.xml b/helm/www/lambda_delta/web/home/apps_2.ldw.xml deleted file mode 100644 index 2d15c0bf7..000000000 --- a/helm/www/lambda_delta/web/home/apps_2.ldw.xml +++ /dev/null @@ -1,52 +0,0 @@ - - - -
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/lambda_delta/web/home/apps_2_src.tbl b/helm/www/lambda_delta/web/home/apps_2_src.tbl deleted file mode 100644 index d5508e3d6..000000000 --- a/helm/www/lambda_delta/web/home/apps_2_src.tbl +++ /dev/null @@ -1,38 +0,0 @@ -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/lambda_delta/web/home/basic_2.ldw.xml b/helm/www/lambda_delta/web/home/basic_2.ldw.xml deleted file mode 100644 index 86b431c6e..000000000 --- a/helm/www/lambda_delta/web/home/basic_2.ldw.xml +++ /dev/null @@ -1,78 +0,0 @@ - - - -
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/lambda_delta/web/home/basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl deleted file mode 100644 index ed50adf79..000000000 --- a/helm/www/lambda_delta/web/home/basic_2_blk.tbl +++ /dev/null @@ -1,52 +0,0 @@ -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/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl deleted file mode 100644 index 28aacba87..000000000 --- a/helm/www/lambda_delta/web/home/basic_2_src.tbl +++ /dev/null @@ -1,304 +0,0 @@ -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/lambda_delta/xml/ld.dtd b/helm/www/lambda_delta/xml/ld.dtd deleted file mode 100644 index 4c9046a27..000000000 --- a/helm/www/lambda_delta/xml/ld.dtd +++ /dev/null @@ -1,140 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/helm/www/lambda_delta/xslt/ld_web.xsl b/helm/www/lambda_delta/xslt/ld_web.xsl deleted file mode 100644 index 288973806..000000000 --- a/helm/www/lambda_delta/xslt/ld_web.xsl +++ /dev/null @@ -1,21 +0,0 @@ - - - - - - - - - - - - - diff --git a/helm/www/lambda_delta/xslt/ld_web_library.xsl b/helm/www/lambda_delta/xslt/ld_web_library.xsl deleted file mode 100644 index a100e5bd9..000000000 --- a/helm/www/lambda_delta/xslt/ld_web_library.xsl +++ /dev/null @@ -1,90 +0,0 @@ - - - - - -
- - [lambda_delta 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 lambda_delta processor] - - - - diff --git a/helm/www/lambda_delta/xslt/ld_web_root.xsl b/helm/www/lambda_delta/xslt/ld_web_root.xsl deleted file mode 100644 index 991f32058..000000000 --- a/helm/www/lambda_delta/xslt/ld_web_root.xsl +++ /dev/null @@ -1,92 +0,0 @@ - - - - - -
- -
- - - -
- -
- - - - - - - - - -
  • - - -
- - - -
- -
- - - - -

-
- - - - - - -
-

-
- - -
- - - - - - - - - - - - - - <xsl:value-of select="@title"/> - - - - - - -
- - - - - - diff --git a/helm/www/lambda_delta/xslt/lddl.xsl b/helm/www/lambda_delta/xslt/lddl.xsl deleted file mode 100644 index 2711cff96..000000000 --- a/helm/www/lambda_delta/xslt/lddl.xsl +++ /dev/null @@ -1,33 +0,0 @@ - - - - - - - - - - - - - - - - diff --git a/helm/www/lambda_delta/xslt/lddl_entity.xsl b/helm/www/lambda_delta/xslt/lddl_entity.xsl deleted file mode 100644 index f9fca428f..000000000 --- a/helm/www/lambda_delta/xslt/lddl_entity.xsl +++ /dev/null @@ -1,62 +0,0 @@ - - - - - - - - - - -
- - - - - - - - - - - - - - -
-
- - - - -
-
- -
- - - - - Declaration - - - - - - Definition - - - - diff --git a/helm/www/lambda_delta/xslt/lddl_library.xsl b/helm/www/lambda_delta/xslt/lddl_library.xsl deleted file mode 100644 index 8af7006a3..000000000 --- a/helm/www/lambda_delta/xslt/lddl_library.xsl +++ /dev/null @@ -1,284 +0,0 @@ - - - - - - - - - - - - , - - - - / - - - - + - - - - .​ - - - - ( - - - - ) - - - - [ - - - - ] - - - - < - - - - > - - - - : - - - - = - - - - " - - - - 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/lambda_delta/xslt/lddl_root.xsl b/helm/www/lambda_delta/xslt/lddl_root.xsl deleted file mode 100644 index 251b9cee8..000000000 --- a/helm/www/lambda_delta/xslt/lddl_root.xsl +++ /dev/null @@ -1,114 +0,0 @@ - - - - - - - - - - - - - - - - lambda_delta digital library (LDDL) - - - - -
- - [lambda_delta home] -
-
- -
-
- [Spacer] -
- -
- - [Valid XHTML 1.1] - - [Valid CSS level 2] - - [Generated from XML via XSL] - - [Powered by Helena lambda_delta processor] - - [PNG used here] - - [Viewable with any browser] -
- - - - - -
- - - - - - - - - - - -
- - - diff --git a/helm/www/lambda_delta/xslt/lddl_term.xsl b/helm/www/lambda_delta/xslt/lddl_term.xsl deleted file mode 100644 index b11a02b64..000000000 --- a/helm/www/lambda_delta/xslt/lddl_term.xsl +++ /dev/null @@ -1,97 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -