From 7666f9dddfcaca5671dd25d3cd2095481968c7bf Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 4 Feb 2020 00:31:54 +0100
Subject: [PATCH] =?utf8?q?update=20in=20binaries=20for=20=CE=BB=CE=B4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

roles: WIP ...
---
 .../contribs/lambdadelta/bin/roles/Makefile   |  7 ++-
 .../contribs/lambdadelta/bin/roles/roles.css  | 57 +++++++++++++++++++
 .../lambdadelta/bin/roles/rolesEngine.ml      |  4 ++
 .../lambdadelta/bin/roles/rolesEngine.mli     |  5 ++
 .../lambdadelta/bin/roles/rolesUtils.ml       | 20 +++++++
 .../lambdadelta/bin/roles/rolesUtils.mli      |  4 ++
 .../lambdadelta/bin/roles/webEngine.ml        | 25 ++++++++
 7 files changed, 120 insertions(+), 2 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/bin/roles/roles.css

diff --git a/matita/matita/contribs/lambdadelta/bin/roles/Makefile b/matita/matita/contribs/lambdadelta/bin/roles/Makefile
index 779952bac..8c34181a0 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/Makefile
+++ b/matita/matita/contribs/lambdadelta/bin/roles/Makefile
@@ -5,6 +5,9 @@ REQUIRES =
 include ../Makefile.common
 
 test:
-#	@$(MAKE) --no-print-directory -C ../../ www
+	@./roles.native -C ../.. -r -W > roles.html
 
-.PHONY: test
+up-css:
+	@scp roles.css lahar.helm.cs.unibo.it:/projects/helm/public_html/lambdadelta/css/
+
+.PHONY: test up-css
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/roles.css b/matita/matita/contribs/lambdadelta/bin/roles/roles.css
new file mode 100644
index 000000000..768c9afb2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/roles/roles.css
@@ -0,0 +1,57 @@
+@charset "UTF-8";
+
+/* anchors ******************************************************************/
+
+a:link {
+  text-decoration: initial;
+  color: inherit;
+}
+
+/* visited link */
+a:visited {
+  text-decoration: initial;
+  color: inherit;
+}
+
+/* mouse over link */
+a:hover {
+  text-decoration: underline;
+  color: inherit;
+}
+
+/* selected link */
+a:active {
+  text-decoration: underline;
+  color: inherit;
+}
+
+/* layouts ******************************************************************/
+
+.atoms-head {
+}
+
+.count {
+}
+
+.atoms {
+  overflow-x: auto;
+  border-bottom: 0.5em solid white;
+}
+
+.atom {
+  padding: 0.25em 0.5em;
+}
+
+.selected {
+  border: 1pt dotted;
+}
+
+/* colors *******************************************************************/
+
+.object {
+  color: skyblue;
+}
+
+.name {
+  color: darkseagreen;
+}
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
index 285807169..73cca4e66 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.ml
@@ -102,3 +102,7 @@ let write_status () =
 
 let print_status () =
   EO.out_status stdout st
+
+let visit_status before_t each_t after_t before_w each_w after_w =
+  EU.list_visit before_t each_t after_t EU.string_of_obj [1] st.ET.t;
+  EU.list_visit before_w each_w after_w EU.string_of_name [2] st.ET.w
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
index 4ccae9de0..fbaac551a 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesEngine.mli
@@ -26,3 +26,8 @@ val read_status: unit -> unit
 val write_status: unit -> unit
 
 val print_status: unit -> unit
+
+val visit_status:
+  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  unit
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
index 7c779fddf..ae8dc9fe0 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.ml
@@ -74,6 +74,10 @@ let rec list_exists compare = function
     if b <= 0 then b = 0 else
     list_exists compare tl
 
+let rec list_count s c = function
+  | []         -> s, c
+  | (b, _)::tl -> list_count (s + if b then 1 else 0) (succ c) tl
+
 let string_of_version v =
   String.concat "." (List.map string_of_int v)
 
@@ -163,8 +167,24 @@ let new_status = {
   ET.r = []; ET.s = []; ET.t = []; ET.w = [];
 }
 
+let string_of_pointer = string_of_version 
+
 let pointer_of_string = version_of_string
 
+let list_visit before each after string_of p l =
+  let ptr p = string_of_pointer (List.rev p) in
+  let rec aux i = function
+    | []         -> ()
+    | (b, x)::tl ->
+      each (ptr (i::p)) b (string_of x);
+      aux (succ i) tl
+  in
+  let s, c = list_count 0 0 l in
+  let count = Printf.sprintf "%u/%u" s c in
+  before (ptr p) count;
+  aux 0 l;
+  after ()
+
 let string_of_error = function
   | ET.EWrongExt x   ->
     Printf.sprintf "unknown input file type %S" x
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
index 252162e89..6fb3bab57 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
+++ b/matita/matita/contribs/lambdadelta/bin/roles/rolesUtils.mli
@@ -21,6 +21,10 @@ val list_split: (bool * 'b) list -> (bool * 'b) list * (bool * 'b) list
 
 val list_select: 'b option -> (bool * 'b) list -> 'b option
 
+val list_visit:
+  (string -> string -> unit) -> (string -> bool -> string -> unit) -> (unit -> unit) ->
+  ('a -> string) -> RolesTypes.pointer -> (bool * 'a) list -> unit
+
 val string_of_version: RolesTypes.version -> string
 
 val version_of_string: string -> RolesTypes.version
diff --git a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
index 7fc942960..5dcc26e36 100644
--- a/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
+++ b/matita/matita/contribs/lambdadelta/bin/roles/webEngine.ml
@@ -53,6 +53,31 @@ let open_out () =
 let close_out () =
   close_out_html ()
 
+let status_out () =
+  let before_atoms a p count =
+    let c, str =
+      if a then "object", "objects"
+      else "name", "names"
+    in
+    KP.printf "<div class=\"atoms-head %s\">\n" c;
+    KP.printf "<a href=\"\">%s:</a>\n" str;
+    KP.printf "<span class=\"count\">%s</span>\n" count;
+    KP.printf "</div>\n";
+    KP.printf "<div class=\"atoms\"><table><tr>\n"
+  in
+  let each_atom a p b str =
+    let c = if a then "object" else "name" in
+    let s = if b then " selected" else "" in
+    KP.printf "<td class=\"atom %s%s\"><a href=\"\">%s</a></td>\n" c s str
+  in
+  let after_atoms () =
+    KP.printf "</tr></table></div>\n"
+  in
+  EE.visit_status
+    (before_atoms true) (each_atom true) after_atoms
+    (before_atoms false) (each_atom false) after_atoms
+
 let init () =
   open_out ();
+  status_out ();
   close_out ()
-- 
2.39.2