From c0d87c3cdf879f61aa53e91f43580e9815ae7190 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 6 Jul 2014 14:41:50 +0000 Subject: [PATCH] - xhtbl: support for relative links added - web site: now the "forword" page is generated --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/Makefile | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 2 +- helm/www/lambdadelta/bin/xhtbl/attr.ml | 20 ++ helm/www/lambdadelta/bin/xhtbl/css.ml | 20 -- helm/www/lambdadelta/bin/xhtbl/matrix.ml | 13 +- helm/www/lambdadelta/bin/xhtbl/options.ml | 5 + helm/www/lambdadelta/bin/xhtbl/pass1.ml | 8 +- helm/www/lambdadelta/bin/xhtbl/pass2.ml | 6 +- helm/www/lambdadelta/bin/xhtbl/pass3.ml | 28 +- helm/www/lambdadelta/bin/xhtbl/table.ml | 20 +- helm/www/lambdadelta/bin/xhtbl/textLexer.mll | 5 +- helm/www/lambdadelta/bin/xhtbl/textParser.mly | 68 +++-- .../www/lambdadelta/bin/xhtbl/textUnparser.ml | 12 +- helm/www/lambdadelta/bin/xhtbl/xhtbl.ml | 10 +- helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml | 11 +- helm/www/lambdadelta/css/ld_web.css | 12 +- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/index.html | 259 +++++++++--------- .../home/{index2.ldw.xml => index.ldw.xml} | 0 helm/www/lambdadelta/web/home/sitemap.tbl | 10 +- 22 files changed, 302 insertions(+), 215 deletions(-) create mode 100644 helm/www/lambdadelta/bin/xhtbl/attr.ml delete mode 100644 helm/www/lambdadelta/bin/xhtbl/css.ml rename helm/www/lambdadelta/web/home/{index2.ldw.xml => index.ldw.xml} (100%) diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index c78a0d430..fb86723f5 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -224,6 +224,6 @@

-
Last update: Sat, 05 Jul 2014 12:39:48 +0200
+
Last update: Sun, 06 Jul 2014 16:29:26 +0200
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 3533cb02e..c88300d95 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -81,7 +81,7 @@ ifeq ($(MAKECMDGOALS), www) $(XSLS): $(TBLS) $(XHTBL) @echo " XHTBL *.tbl" - $(H)$(XHTBL) -O $(XSLTDIR) $(TBLS) + $(H)$(XHTBL) -b $(LDURL) -O $(XSLTDIR) $(TBLS) $(foreach LDW,$(LDWS),$(eval $(call HTML_TEMPLATE,$(LDW),$(notdir $(LDW:%.ldw.xml=%))))) endif diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 96f58a97b..3cb582ae7 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -195,6 +195,6 @@

-
Last update: Sat, 05 Jul 2014 12:39:48 +0200
+
Last update: Sun, 06 Jul 2014 16:29:26 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index a8588e72b..071ad9091 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1303,6 +1303,6 @@

-
Last update: Sat, 05 Jul 2014 12:39:48 +0200
+
Last update: Sun, 06 Jul 2014 16:29:26 +0200
diff --git a/helm/www/lambdadelta/bin/xhtbl/attr.ml b/helm/www/lambdadelta/bin/xhtbl/attr.ml new file mode 100644 index 000000000..36b3d0003 --- /dev/null +++ b/helm/www/lambdadelta/bin/xhtbl/attr.ml @@ -0,0 +1,20 @@ +module L = List + +module T = Table + +(* true for a row specification *) +type 'a atom = 'a * bool * int option * int option + +type 'a atoms = 'a atom list + +let get_attr concat null 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 null + | false, Some c1, None -> if x >= c1 then c else null + | false, Some c1, Some c2 -> if x >= c1 && x <= c2 then c else null + | true , None, Some r2 -> if y <= r2 then c else null + | true , Some r1, None -> if y >= r1 then c else null + | true , Some r1, Some r2 -> if y >= r1 && y <= r2 then c else null + in + concat (L.map (map y x) a) diff --git a/helm/www/lambdadelta/bin/xhtbl/css.ml b/helm/www/lambdadelta/bin/xhtbl/css.ml deleted file mode 100644 index 82a41e91c..000000000 --- a/helm/www/lambdadelta/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/lambdadelta/bin/xhtbl/matrix.ml b/helm/www/lambdadelta/bin/xhtbl/matrix.ml index 86d6f053a..62f6b194e 100644 --- a/helm/www/lambdadelta/bin/xhtbl/matrix.ml +++ b/helm/www/lambdadelta/bin/xhtbl/matrix.ml @@ -1,10 +1,13 @@ module A = Array +module N = Filename module T = Table type cell = { ck: T.text list; (* contents *) cc: T.css; (* css classes *) + cu: T.uri; (* uri *) + cx: T.ext; (* extension *) cb: T.border; (* border *) } @@ -15,7 +18,7 @@ type matrix = { } let empty = { - ck = []; cc = []; cb = T.border false; + ck = []; cc = []; cu = ""; cx = ""; cb = T.border false; } let make ts = { @@ -26,8 +29,12 @@ let make ts = { 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_attrs m y x c u e = + m.m.(y).(x) <- {m.m.(y).(x) with + cc = c @ m.m.(y).(x).cc; + cu = u ^ m.m.(y).(x).cu; + cx = m.m.(y).(x).cx ^ e; + } let set_west m y x b = let c = m.m.(y).(x) in diff --git a/helm/www/lambdadelta/bin/xhtbl/options.ml b/helm/www/lambdadelta/bin/xhtbl/options.ml index ce1c88867..21ebec1d9 100644 --- a/helm/www/lambdadelta/bin/xhtbl/options.ml +++ b/helm/www/lambdadelta/bin/xhtbl/options.ml @@ -1,5 +1,7 @@ let output_dir_default = "" +let baseuri_default = "" + let debug_lexer_default = false let debug_pass_default = false @@ -8,6 +10,8 @@ let pass_default = false let output_dir = ref output_dir_default +let baseuri = ref baseuri_default + let debug_lexer = ref debug_lexer_default let d0 = ref debug_pass_default @@ -28,6 +32,7 @@ let p2 = ref pass_default let clear () = output_dir := output_dir_default; + baseuri := baseuri_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; diff --git a/helm/www/lambdadelta/bin/xhtbl/pass1.ml b/helm/www/lambdadelta/bin/xhtbl/pass1.ml index 1c53e7d6f..bedd9619f 100644 --- a/helm/www/lambdadelta/bin/xhtbl/pass1.ml +++ b/helm/www/lambdadelta/bin/xhtbl/pass1.ml @@ -6,10 +6,12 @@ module F = Fold type status = { ts: T.size; (* current dimensions *) tc: T.css; (* current class *) + tu: T.uri; (* current uri *) + tx: T.ext; (* current extension *) } let empty = { - ts = T.no_size; tc = []; + ts = T.no_size; tc = []; tu = ""; tx = "" } let init b ts = @@ -38,8 +40,8 @@ let deinit ts = {ts with (****************************************************************************) let open_table st t = - t.T.tc <- t.T.tc @ st.tc; - {st with tc = t.T.tc} + t.T.tc <- t.T.tc @ st.tc; t.T.tu <- st.tu ^ t.T.tu; t.T.tx <- st.tx ^ t.T.tx; + {st with tc = t.T.tc; tu = t.T.tu; tx = t.T.tx} let close_table st t = t.T.ts <- st.ts; st diff --git a/helm/www/lambdadelta/bin/xhtbl/pass2.ml b/helm/www/lambdadelta/bin/xhtbl/pass2.ml index 68cc7ba99..2e003ccb3 100644 --- a/helm/www/lambdadelta/bin/xhtbl/pass2.ml +++ b/helm/www/lambdadelta/bin/xhtbl/pass2.ml @@ -50,11 +50,11 @@ 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 set_attrs 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; + M.set_attrs st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc t.T.tu t.T.tx; aux y (succ x) end in @@ -114,7 +114,7 @@ let open_table st t = print st t; st let close_table st t = - set_key st t; set_css st t; set_borders st t; st + set_key st t; set_attrs st t; set_borders st t; st let map_key st k = st diff --git a/helm/www/lambdadelta/bin/xhtbl/pass3.ml b/helm/www/lambdadelta/bin/xhtbl/pass3.ml index 4513828b5..337437709 100644 --- a/helm/www/lambdadelta/bin/xhtbl/pass3.ml +++ b/helm/www/lambdadelta/bin/xhtbl/pass3.ml @@ -1,23 +1,31 @@ -module A = Array +module L = List +module S = String +module V = Array +module T = Table module M = Matrix -module C = Css +module A = Attr type status = { m: M.matrix; - a: C.atoms; + c: T.css A.atoms; + u: T.uri A.atoms; + x: T.ext A.atoms; } -let initial a m = { - m = m; a = a; +let initial c u x m = { + m = m; c = c; u = u; x = x } let process_cell st y x c = - M.set_css st.m y x (C.get_css st.a y x) + M.set_attrs st.m y x + (A.get_attr L.concat [] st.c y x) + (A.get_attr (S.concat "") "" st.u y x) + (A.get_attr (S.concat "") "" st.x y x) let process_row st y row = - A.iteri (process_cell st y) row + V.iteri (process_cell st y) row -let process css matrix = - let st = initial css matrix in - A.iteri (process_row st) matrix.M.m +let process css uri ext matrix = + let st = initial css uri ext matrix in + V.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 index 204df4c90..fe15c94db 100644 --- a/helm/www/lambdadelta/bin/xhtbl/table.ml +++ b/helm/www/lambdadelta/bin/xhtbl/table.ml @@ -1,5 +1,11 @@ type css = string list +type uri = string + +type ext = string + +type absolute = bool + type size = { y : int; (* first row *) x : int; (* first column *) @@ -18,13 +24,15 @@ type border = { } type text = Plain of string - | Link of string * string + | Link of absolute * string * string type key = Text of text list | Glue of int option type table = { mutable tc: css; (* css classes *) + mutable tu: uri; (* uri *) + mutable tx: ext; (* uri extension *) mutable ts: size; (* dimension *) tb: border; (* border *) te: entry; (* contents *) @@ -46,12 +54,14 @@ 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; +let mk_key k tc tu tx = { + ts = no_size; tb = border false; te = Key k; + tc = tc; tu = tu; tx = tx; ti = id (); } -let mk_line b tl tc = { - ts = no_size; tb = border b; te = Line (b, tl); tc = tc; +let mk_line b tl tc tu tx = { + ts = no_size; tb = border b; te = Line (b, tl); + tc = tc; tu = tu; tx = tx; ti = id (); } diff --git a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll index 7efa9035d..aa8f42fe4 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll +++ b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll @@ -26,13 +26,16 @@ rule token = parse | "(" { out "("; TP.OP } | ")" { out ")"; TP.CP } | "@" { out ")"; TP.AT } - | "space" { out "name"; TP.SPACE } + | "space" { out "space"; TP.SPACE } | "name" { out "name"; TP.NAME } | "table" { out "table"; TP.TABLE } | "class" { out "class"; TP.CSS } + | "uri" { out "uri"; TP.URI } + | "ext" { out "ext"; TP.EXT } | eof { TP.EOF } and str = parse | QT { "" } + | "\\\\" { "\\" ^ str lexbuf } | "\\\"" { "\"" ^ str lexbuf } | _ as c { S.make 1 c ^ str lexbuf } and block = parse diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly index 3864bc53c..3dba122d0 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly +++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly @@ -7,18 +7,23 @@ 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 +let mk_css_atom s rs = + let cs = split s in + let map (b, (x1, x2)) = cs, b, x1, x2 in + L.map map rs + +let mk_string_atom s rs = + let map (b, (x1, x2)) = s, b, x1, x2 in + L.map map rs %} %token NUM %token TEXT -%token SPACE NAME TABLE CSS SR OC CC OB CB PS OP CP AT EOF +%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS OP CP AT EOF %start script -%type <(string * string) list * (string * Table.table * Css.atoms) list> script +%type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script %% @@ -32,8 +37,11 @@ spaces: ; text: - | TEXT { T.Plain $1 } - | AT OP TEXT TEXT CP { T.Link ($3, $4) } + | TEXT { T.Plain $1 } + | AT OP TEXT TEXT CP { T.Link (true, $3, $4) } + | AT AT OP TEXT TEXT CP { T.Link (false, $4, $5) } + | AT TEXT { T.Link (true, $2, $2) } + | AT AT TEXT { T.Link (false, $3, $3) } ; texts: @@ -52,10 +60,20 @@ css: | CSS TEXT { split $2 } ; +uri: + | { "" } + | URI TEXT { $2 } +; + +ext: + | { "" } + | EXT TEXT { $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 } + | css uri ext key { T.mk_key $4 $1 $2 $3 } + | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 } + | css uri ext OB tables CB { T.mk_line true $5 $1 $2 $3 } ; tables: @@ -87,17 +105,35 @@ ranges: | range ranges { $1 :: $2 } ; -atom: - | CSS TEXT ranges { mk_atom $2 $3 } +catom: + | CSS TEXT ranges { mk_css_atom $2 $3 } +; + +catoms: + | { [] } + | catom catoms { $1 @ $2 } +; + +uatom: + | URI TEXT ranges { mk_string_atom $2 $3 } +; + +uatoms: + | { [] } + | uatom uatoms { $1 @ $2 } +; + +xatom: + | EXT TEXT ranges { mk_string_atom $2 $3 } ; -atoms: - | { [] } - | atom atoms { $1 @ $2 } +xatoms: + | { [] } + | xatom xatoms { $1 @ $2 } ; directive: - | name TABLE table atoms { $1, $3, $4 } + | name TABLE table catoms uatoms xatoms { $1, $3, $4, $5, $6 } ; directives: diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml index fec699bcb..ece6949d9 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml @@ -41,9 +41,13 @@ let border tb = let css tc = P.sprintf "\"%s\"" (S.concat " " tc) +let uri tu tx = + P.sprintf "@\"%s\" \"%s\"" tu tx + let text = function - | T.Plain s -> P.sprintf "\"%s\"" s - | T.Link (uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s + | T.Plain s -> P.sprintf "\"%s\"" s + | T.Link (true, uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s + | T.Link (false, uri, s) -> P.sprintf "@@(\"%s\" \"%s\")" uri s let key = function | T.Text sl -> S.concat " + " (L.map text sl) @@ -58,8 +62,8 @@ let entry = function 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) + P.sprintf "%s[{#%u: %s; %s; %s; %s}\n" + (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) (uri t.T.tu t.T.tx) in st.out str; add st diff --git a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml index f379185fa..6c5f8b01f 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml @@ -16,6 +16,7 @@ let help = "Usage: xhtbl [ -LX | -O | -d0 | -d1 | -d2 | -e1 | -e2 | -p0 let help_L = " Output lexer tokens" let help_O = " Set this output directory" let help_X = " Clear all options" +let help_b = " Set this base uri for relative links" let help_d0 = " Output table contents after phase zero (parsing)" let help_d1 = " Output table contents after phase one (sizing)" let help_d2 = " Output table contents after phase two (filling)" @@ -29,9 +30,7 @@ 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) = +let process_directive och bname (name, table, css, uri, ext) = tables := name :: !tables; if !O.d0 then TU.debug table; if not !O.p0 then begin @@ -41,7 +40,7 @@ let process_directive och bname (name, table, css) = 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; + if not !O.p2 then P3.process css uri ext matrix; let name = if name = "" then bname else name in XU.output och name matrix end @@ -61,8 +60,9 @@ let process_file fname = let main () = A.parse [ "-L", A.Set O.debug_lexer, help_L; - "-O", A.String set_output_dir, help_O; + "-O", A.String ((:=) O.output_dir), help_O; "-X", A.Unit O.clear, help_X; + "-b", A.String ((:=) O.baseuri), help_b; "-d0", A.Set O.d0, help_d0; "-d1", A.Set O.d1, help_d1; "-d2", A.Set O.d2, help_d2; diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml index f413aa0ef..603c7f1be 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml @@ -22,12 +22,15 @@ let border cell = if cell.M.cb.T.w then str.[3] <- 's'; str :: cell.M.cc -let text = function - | T.Plain s -> s - | T.Link (uri, s) -> P.sprintf "%s" uri s +let text baseuri ext = function + | T.Plain s -> s + | T.Link (true, uri, s) -> P.sprintf "%s" uri s + | T.Link (false, uri, s) -> + let uri = !O.baseuri ^ baseuri ^ uri ^ ext in + P.sprintf "%s" uri s let key cell = - if cell.M.ck = [] then "
" else S.concat " " (L.map text cell.M.ck) + if cell.M.ck = [] then "
" else S.concat " " (L.map (text cell.M.cu cell.M.cx) cell.M.ck) let ind i = S.make (2 * i) ' ' diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index ed3a266f5..150aaf781 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -8,14 +8,20 @@ body { margin: 2.5%; } -a:link, a:visited { +a:link, a:visited, a:hover, a:active, a:focus { text-decoration: underline; color: rgb(0, 0, 0); } -a:active, a:hover, a:focus { +a:hover { background: rgb(192, 192, 192); - color: rgb(0, 0, 0); +} + +/* on newer browsers, disable style modifications for named anchors */ +a[name]:hover { + text-decoration: inherit; + color: inherit; + background: inherit; } /* blocks *******************************************************************/ diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index c5c5b833d..e6f303995 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -237,6 +237,6 @@

-
Last update: Sat, 05 Jul 2014 12:39:48 +0200
+
Last update: Sun, 06 Jul 2014 16:29:26 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 07e98c6a9..ce113aff0 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -1,145 +1,146 @@ - - - - - - λδ 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 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 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:
-
- + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ (\lambda\delta)
+
+ [Spacer] +
+
+
+
+
+
- - - - - + +
Version
+
+ foreword Name
+
+ news Started
+
+ documentation Released
-
Dismissed
+
+ implementation
+ + + +
Foreword [spacer] +
+
+
+ λδ is developed in the context of the + Hypertextual Electronic Library of Mathematics + as a machine-checked digital specification + that is not the formal counterpart of some previously published informal material. +
+
+ λδ comes in several versions listed in the following table, + which includes the major milestones: +
+
+ + - - - - - + + + + + + + - - - + + - - + + + + + + + + + + + +
2
-
basic_2
-
April -2011
-
planned -in -2014
-
not -planned yet
-
versionnamedeveloped withstartedannouncedreleaseddismissed
1
-
basic_1
-
May -2004
+
2basic_2 + Matita 0.99.2 November -2006
-
May -2008
+
April 2011July 2014Planned in 2014Not planned yet
1basic_1 + Coq 7.3.1 May 2004January 2006November 2006May 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 2014-02-24 by Ferruccio -Guidi
-
+ + + +
Notice for the Internet Explorer user [spacer] +
+
+ 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. +
- +
+ [Spacer] +
+
+
+
+ +
+
+
+
Last update: Sun, 06 Jul 2014 16:37:09 +0200
+ + diff --git a/helm/www/lambdadelta/web/home/index2.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml similarity index 100% rename from helm/www/lambdadelta/web/home/index2.ldw.xml rename to helm/www/lambdadelta/web/home/index.ldw.xml diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 78a5a2da0..7e2969bc9 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -2,17 +2,19 @@ name "sitemap" table [ class "sky" { - [ "foreword" * ] + [ @@("index" "foreword") * ] } class "magenta" { - [ "news" * ] + [ @@"news" * ] } class "orange" { - [ "bibliography" * ] + [ @@"documentation" * ] } class "green" { - [ "resources" * ] + [ @@"implementation" * ] } ] class "component" [ 0 ] + +ext ".html" [ 0 ] -- 2.39.2