From 4cd0faedb102c866719990bc1e61b099db0ea39d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 27 Nov 2013 21:47:16 +0000
Subject: [PATCH] web page for ground_2 and bugfixed statistics generation in
 the Makefile

---
 matita/matita/contribs/lambdadelta/Makefile   | 24 ++++++------
 .../lambdadelta/ground_2/web/ground_2.ldw.xml | 38 +++++++++++++++++++
 .../lambdadelta/ground_2/web/ground_2_src.tbl | 23 +++++++++++
 3 files changed, 73 insertions(+), 12 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 6eed87bc1..16c000e67 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -118,13 +118,13 @@ define STATS_TEMPLATE
   $$(STT_$(1)): S0  = $$(shell cat $(1)/$(1)_probe.txt)    
   $$(STT_$(1)): S1  = $$(shell cat $(1)/$(1)_mac.txt)
   $$(STT_$(1)): S4  = $$(shell ls $$(MAS_$(1)) | wc -l)
-  $$(STT_$(1)): P1  = $$(shell grep "theorem " $$(MAS_$(1)) | wc -l)
-  $$(STT_$(1)): P2  = $$(shell grep "lemma " $$(MAS_$(1)) | wc -l)
-  $$(STT_$(1)): P3  = $$(shell grep "fact " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): P1  = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): P2  = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): P3  = $$(shell grep "^fact " $$(MAS_$(1)) | wc -l)
   $$(STT_$(1)): P4  = $$(shell grep qed $$(MAS_$(1)) | wc -l)
-  $$(STT_$(1)): C1  = $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l)
-  $$(STT_$(1)): C2  = $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l)
-  $$(STT_$(1)): M1  = $$(shell grep "axiom " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): C1  = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): C2  = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): M1  = $$(shell grep "^axiom " $$(MAS_$(1)) | wc -l)
   $$(STT_$(1)): M2  = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l)
   $$(STT_$(1)): M3  = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l)
 
@@ -180,12 +180,12 @@ define SUMMARY_TEMPLATE
   $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt)  
   $$(SUM_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt)
   $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l)  
-  $$(SUM_$(1)): C1 = $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l)
-  $$(SUM_$(1)): C2 = $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l)
-  $$(SUM_$(1)): C3 = $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l)
-  $$(SUM_$(1)): P1 = $$(shell grep "theorem " $$(MAS_$(1)) | wc -l)
-  $$(SUM_$(1)): P2 = $$(shell grep "lemma " $$(MAS_$(1)) | wc -l)
-  $$(SUM_$(1)): P3 = $$(shell grep "lemma \|theorem " $$(MAS_$(1)) | wc -l)
+  $$(SUM_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l)
+  $$(SUM_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l)
+  $$(SUM_$(1)): C3 = $$(shell grep "^inductive \|^record \|^definition \|^let rec " $$(MAS_$(1)) | wc -l)
+  $$(SUM_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l)
+  $$(SUM_$(1)): P2 = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l)
+  $$(SUM_$(1)): P3 = $$(shell grep "^lemma \|^theorem " $$(MAS_$(1)) | wc -l)
 
   $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt
 	@printf '  SUMMARY $(1)\n'
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
new file mode 100644
index 000000000..f1ea686a1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml
@@ -0,0 +1,38 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+      description = "lambdadelta version 2"
+      title = "lambdadelta version 2"
+      head = "cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)"
+>
+   <section>Summary of the Specification</section>
+   <body>Here is a numerical acount of the specification's contents
+         and its timeline.
+         Nodes are counted according to the "intrinsinc complexity measure"
+         [F. Guidi: "Procedural Representation of CIC Proof Terms"
+         Journal of Automated Reasoning 44(1-2), Springer (February 2010),
+         pp. 53-78].
+   </body>
+   <table name="ground_2_sum"/>
+   <news date="2013 November 27.">
+         Natural numbers with infinity.
+   </news>
+   <news date="2011 August 10.">
+         Specification starts.
+   </news>
+
+   <section>Logical Structure of the Specification</section>
+   <body>The source files are grouped in planes
+         according to the following table.
+         Notation files covering the whole specification are provided.
+         The notation for the relations or functions introduced in each file
+         is shown in parentheses (? are placeholders).
+   </body>
+   <table name="ground_2_src"/>
+
+   <section>Physical Structure of the Specification</section>
+   <body>The source files are grouped in directories,
+         one for each plane.
+   </body>
+   <footer/>
+</page>
diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
new file mode 100644
index 000000000..3eec66de3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -0,0 +1,23 @@
+name "ground_2_src"
+
+table {
+   class "grey"
+   [ { "plane" * } {
+        [ "files" * ]
+     }     
+   ]
+   class "orange"
+   [ { "natural numbers with infinity" * } {
+        [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?&lt;? )" * ]
+     }     
+   ]
+   class "red"
+   [ { "" * } {
+        [ "" * ]
+     }     
+   ]
+}
+
+class "plane" { 0 }
+
+class "file" { 1 * }
-- 
2.39.2