From 2aa295aa37f8fb274f7b640f7627078d9435cefa Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 6 Jul 2014 18:40:20 +0000 Subject: [PATCH] - xhtbl: we added the real concatenation of cells (without added spaces) - web site: we added a page for each version of \lambda\delta --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 2 +- helm/www/lambdadelta/bin/xhtbl/textLexer.mll | 1 + helm/www/lambdadelta/bin/xhtbl/textParser.mly | 7 +- .../www/lambdadelta/bin/xhtbl/textUnparser.ml | 2 +- helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml | 2 +- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/index.html | 10 +- helm/www/lambdadelta/version_1.html | 136 ++++++++++++++++++ helm/www/lambdadelta/version_2.html | 93 ++++++++++++ .../lambdadelta/web/home/version_1.ldw.xml | 62 ++++++++ .../lambdadelta/web/home/version_2.ldw.xml | 23 +++ helm/www/lambdadelta/web/home/versions.tbl | 5 +- helm/www/lambdadelta/xslt/ld_web_root.xsl | 36 +++-- 15 files changed, 362 insertions(+), 23 deletions(-) create mode 100644 helm/www/lambdadelta/version_1.html create mode 100644 helm/www/lambdadelta/version_2.html create mode 100644 helm/www/lambdadelta/web/home/version_1.ldw.xml create mode 100644 helm/www/lambdadelta/web/home/version_2.ldw.xml diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 46a625930..c3c16c3cb 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 06 Jul 2014 17:03:50 +0200
+
Last update: Sun, 06 Jul 2014 20:28:30 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 93b2272a4..9fc581eb9 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sun, 06 Jul 2014 17:03:50 +0200
+
Last update: Sun, 06 Jul 2014 20:28:30 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index e4bebe63d..3511fbfb0 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1300,6 +1300,6 @@

-
Last update: Sun, 06 Jul 2014 17:03:50 +0200
+
Last update: Sun, 06 Jul 2014 20:28:30 +0200
diff --git a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll index aa8f42fe4..4b06e4c40 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll +++ b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll @@ -22,6 +22,7 @@ rule token = parse | "[" { out "["; TP.OB } | "]" { out "]"; TP.CB } | "*" { out "*"; TP.SR } + | "^" { out "^"; TP.CF } | "+" { out "+"; TP.PS } | "(" { out "("; TP.OP } | ")" { out ")"; TP.CP } diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly index 3dba122d0..587395988 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly +++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly @@ -20,7 +20,7 @@ let mk_string_atom s rs = %token NUM %token TEXT -%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS OP CP AT EOF +%token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS CF OP CP AT EOF %start script %type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script @@ -45,8 +45,9 @@ text: ; texts: - | text { [$1] } - | text PS texts { $1 :: $3 } + | text { [$1] } + | text PS texts { $1 :: T.Plain " " :: $3 } + | text CF texts { $1 :: $3 } ; key: diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml index ece6949d9..339a9aeec 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml @@ -50,7 +50,7 @@ let text = function | T.Link (false, uri, s) -> P.sprintf "@@(\"%s\" \"%s\")" uri s let key = function - | T.Text sl -> S.concat " + " (L.map text sl) + | T.Text sl -> S.concat " ^ " (L.map text sl) | T.Glue None -> "*" | T.Glue (Some i) -> P.sprintf "%u" i diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml index 603c7f1be..e46682c3f 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml @@ -30,7 +30,7 @@ let text baseuri ext = function P.sprintf "%s" uri s let key cell = - if cell.M.ck = [] then "
" else S.concat " " (L.map (text cell.M.cu cell.M.cx) 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/ground_2.html b/helm/www/lambdadelta/ground_2.html index 9b799f060..e79359b0d 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -234,6 +234,6 @@

-
Last update: Sun, 06 Jul 2014 17:03:50 +0200
+
Last update: Sun, 06 Jul 2014 20:28:30 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 0fb9ca8e2..cd48d35d4 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -79,7 +79,9 @@ 2 - basic_2 + + basic_2 + Matita 0.99.2 @@ -90,7 +92,9 @@ 1 - basic_1 + + basic_1 + Coq 7.3.1 @@ -139,6 +143,6 @@

-
Last update: Sun, 06 Jul 2014 17:03:50 +0200
+
Last update: Sun, 06 Jul 2014 20:28:30 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html new file mode 100644 index 000000000..5bf4e0abd --- /dev/null +++ b/helm/www/lambdadelta/version_1.html @@ -0,0 +1,136 @@ + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ version 1
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + +
+ foreword + + news + + documentation + + implementation +
+
+ +
Formats [spacer] +
+
+ The formal specification of λδ version 1 + is available in the following formats: + + + +
+ +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 06 Jul 2014 20:36:00 +0200
+ + diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html new file mode 100644 index 000000000..27030b1f7 --- /dev/null +++ b/helm/www/lambdadelta/version_2.html @@ -0,0 +1,93 @@ + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ version 2
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + +
+ foreword + + news + + documentation + + implementation +
+
+ +
Formats [spacer] +
+
+ The formal specification of λδ version 2 + is available in the following formats: + +
+ +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 06 Jul 2014 20:36:00 +0200
+ + diff --git a/helm/www/lambdadelta/web/home/version_1.ldw.xml b/helm/www/lambdadelta/web/home/version_1.ldw.xml new file mode 100644 index 000000000..4c7542189 --- /dev/null +++ b/helm/www/lambdadelta/web/home/version_1.ldw.xml @@ -0,0 +1,62 @@ + + + + + + Formats + + The formal specification of λδ version 1 + is available in the following formats: + + lambdadelta_1 for Coq 7.3.1 + (revised ). + Source scripts. + BibTeX entry + + + lambdadelta_1 for Matita 0.5" + (revised ). + Static HTML pages generated by the HELM rendering engine. + + + + Confluence of reduction + (Church-Rosser property). + + + + Correctness of types. + + + + Uniqueness of types up to conversion. + + + + Subject reduction of the type assignment. + + + + Strong normalization of the typed terms. + + + + Decidability of the type inference problem. + + + + + + lambdadelta_1 for Matita 0.5" + (revised ). + HELM directory. + + + + +