aboutsummaryrefslogtreecommitdiff
path: root/etc/utils
diff options
context:
space:
mode:
Diffstat (limited to 'etc/utils')
-rw-r--r--etc/utils/builddoc_lib.sh146
-rw-r--r--etc/utils/dependtodot.ml343
2 files changed, 489 insertions, 0 deletions
diff --git a/etc/utils/builddoc_lib.sh b/etc/utils/builddoc_lib.sh
new file mode 100644
index 0000000..89d1911
--- /dev/null
+++ b/etc/utils/builddoc_lib.sh
@@ -0,0 +1,146 @@
+
+mangle_sources() {
+# pre processing, mainly comments
+for f in $@; do
+
+
+sed -r -e '
+ # We remove comments inside proofs
+ /^Proof.$/,/^Qed./s/\(\*[^*](([^(]|\([^*]){1,}?[^^])\*+\)//g;
+ ' $f |
+
+sed -r -e '
+ # read the whole file into the pattern space
+ # :a is the label, N glues the current line; b branches
+ # to a if not EOF
+ :a; N; $!ba;
+ # remove all starred lines
+ s/\(\*{5,}?\)//g;
+
+ # remove *)\n(*
+ s/\*+\)\n\(\*+/\n/g;
+
+ # double star not too short comments, that are left
+ # as singly starred comments, like (*a.3*)
+ s/\n\(\*+(([^(]|\([^*]){5,}?[^^])\*+\)/\n(**\ \1\ **)/g;
+
+ # restore hide
+ s/\(\*+[ ]*begin hide[ ]*\*+\)/\(\* begin hide \*\)/g;
+ s/\(\*+[ ]*end hide[ ]*\*+\)/\(\* end hide \*\)/g;
+ ' |
+
+sed -r -e '
+ # since ranges apply to lines only we create lines
+ s/\(\*\*/\n(**\n/g;
+ s/\*\*\)/\n**)\n/g;
+ ' |
+
+sed -r -e '
+ # quote sharp, percent and dollar on comment blocks
+ # hiding underscore
+ /\(\*\*/,/\*\*\)/s/#/##/g;
+ /\(\*\*/,/\*\*\)/s/%/%%/g;
+ /\(\*\*/,/\*\*\)/s/\$/$$/g;
+ /\(\*\*/,/\*\*\)/s/\[/#[#/g;
+ /\(\*\*/,/\*\*\)/s/]/#]#/g;
+ /\(\*\*/,/\*\*\)/s/\_/#\_#/g;
+
+ # the lexer glues sharp with other symbols
+ /\(\*\*/,/\*\*\)/s/([^A-Za-z0-9 ])#\[#/\1 #[#/g;
+ /\(\*\*/,/\*\*\)/s/([^A-Za-z0-9 ])#]#/\1 #]#/g;
+ ' |
+
+sed -r -e '
+ # we glue comment lines back together
+ :a; N; $!ba;
+ s/\n\(\*\*\n/(**/g;
+ s/\n\*\*\)\n/**)/g;
+ ' > $f.tmp
+ mv $f.tmp $f
+done
+}
+
+build_doc() {
+rm -rf html
+mkdir html
+coqdoc -t "$TITLE" -g --utf8 $COQDOCOPTS \
+ --parse-comments \
+ --multi-index $@ -d html
+
+# graph
+coqdep -noglob $COQOPTS $@ > depend
+sed -i -e 's/ [^ ]*\.cmxs//g' -e 's/ [^ ]*\.cm.//g' depend
+ocamlc -o $MAKEDOT/makedot -pp camlp5o $MAKEDOT/dependtodot.ml
+$MAKEDOT/makedot depend
+mv *.dot theories.dot || true
+$MANGLEDOT theories.dot
+dot -Tpng -o html/depend.png -Tcmapx -o html/depend.map theories.dot
+dot -Tsvg -o html/depend.svg theories.dot
+
+# post processing
+for f in html/*.html; do sed -r -i -e '
+ # read the whole file into the pattern space
+ # :a is the label, N glues the current line; b branches
+ # to a if not EOF
+ :a; N; $!ba;
+
+ #Add the favicon
+ s/^<\/head>/<link rel="icon" type="image\/png" href="favicon.png" \/>\n<\/head>/mg;
+
+ # add the Joint Center logo
+ s/<h1([^>]*?)>/<h1\1><img src="jc.png" alt="(Joint Center)"\/>/g;
+
+ # extra blank line
+ s/<div\ class="doc">\n/<div class="doc">/g;
+
+ # weird underscore
+ s/ /_/g;
+
+ # putting back underscore
+ s/#\_#/\_/g;
+
+
+ # abundance of <br/>
+ s/\n<br\/> <br\/>//g;
+ ' $f
+done
+
+mv html/index.html html/index_lib.html
+cat >html/index.html <<EOT
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
+<link rel="icon" type="image/png" href="favicon.png" />
+<title>$TITLE</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1><img src="jc.png" alt="(Joint Center)"/>
+$TITLE Documentation</h1>
+<hr/>
+<img class="graph" src="depend.png" usemap="#theories" />
+EOT
+cat html/depend.map >> html/index.html
+cat >>html/index.html <<EOT
+<hr/>
+<center><a href="index_lib.html">
+Library index
+</a></center>
+</div>
+</div>
+</body>
+</html>
+EOT
+
+}
diff --git a/etc/utils/dependtodot.ml b/etc/utils/dependtodot.ml
new file mode 100644
index 0000000..1ea350f
--- /dev/null
+++ b/etc/utils/dependtodot.ml
@@ -0,0 +1,343 @@
+(* Loic Pottier, projet CROAP, INRIA Sophia Antipolis, April 1998. *)
+(* Laurent Théry , INRIA Sophia Antipolis, April 2007 *)
+
+(* Convert a dependencies file, in makefile form, into a graph in a file readable by dot.
+
+The function dependtodot takes as input the dependencies file, and create a file with the same name suffixed by ".dot", readable by dot.
+
+*)
+
+let nodecol="#dbc3b6";; (* #add8ff *)
+let edgecol="#676767";; (* #ff0000 *)
+
+(* parameters to draw edges and nodes *)
+let vnode x =
+ "l(\"" ^ x
+ ^ "\",n(\"\",[a(\"COLOR\",\""^ nodecol ^"\"),a(\"OBJECT\",\"" ^ x ^ "\")],"
+;;
+
+let wstring x = "\""^x^"\""
+;;
+
+let vnoder x = "r(\"" ^ x ^ "\")"
+;;
+
+let vedge =
+ "e(\"\",[a(\"_DIR\",\"inverse\"),a(\"EDGEPATTERN\",\"solid\"),a(\"EDGECOLOR\",\"" ^ edgecol ^ "\")],"
+;;
+
+let listdv l = match l with
+ [] -> "[]"
+ |x::l -> let rec listdvr l = match l with
+ [] -> ""
+ |y::l -> "," ^ y ^ (listdvr l)
+ in "[" ^ x ^ (listdvr l) ^ "]"
+;;
+
+let rec visit ht hte x s =
+ Hashtbl.add ht x x;
+ try let le=Hashtbl.find hte x in
+ let rec visit_edge ls le =
+ match le with
+ [] -> ls
+ |b::l ->
+ try let _ =Hashtbl.find ht b in
+ (visit_edge (ls@[vedge ^ (vnoder b) ^ ")"]) l)
+ with Not_found ->
+ (visit_edge (ls@[vedge ^ (visit ht hte b s) ^ ")"]) l)
+ in s ^ (vnode x) ^ (listdv (visit_edge [] le)) ^ "))"
+ with Not_found -> s ^ (vnode x) ^ "[]))"
+;;
+
+(* cloture transitive *)
+
+let rec merge_list a b = match a with
+ [] -> b
+ |x::a -> if (List.mem x b)
+ then (merge_list a b)
+ else x::(merge_list a b)
+;;
+
+let ht_graph g =
+ let ht =Hashtbl.create 50 in
+ let rec fill g = match g with
+ [] -> ()
+ |(a,lb)::g -> Hashtbl.add ht a lb; fill g
+ in fill g;
+ ht
+;;
+
+let trans_clos1 g =
+ let ht =ht_graph g in
+ List.map (fun (a,lb) ->
+ (a,(let l = ref lb in
+ let rec addlb lb = match lb with
+ [] -> ()
+ |b::lb -> (try l:=(merge_list (Hashtbl.find ht b) !l)
+ with Not_found -> ()); addlb lb
+ in addlb lb;
+ !l))) g
+;;
+
+let rec transitive_closure g =
+ let g1=trans_clos1 g in
+ if g1=g then g else (transitive_closure g1)
+;;
+
+(*
+let g=["A",["B"];
+ "B",["C"];
+ "C",["D"];
+ "D",["E"];
+ "E",["A"]];;
+transitive_closure g;;
+*)
+
+(* enlever les arcs de transitivite *)
+
+let remove_trans g =
+ let ht = ht_graph (transitive_closure g) in
+ List.map (fun (a,lb) ->
+ (a,(let l=ref [] in
+ (let rec sel l2 = match l2 with
+ [] -> ()
+ |b::l2 -> (let r=ref false in
+ (let rec testlb l3 = match l3 with
+ [] -> ()
+ |c::l3 -> if (not (b=a)) &&(not(b=c)) && (not (a=c)) &&
+ (try (List.mem b (Hashtbl.find ht c))
+ with Not_found -> false)
+ then r:=true
+ else ();
+ testlb l3
+ in testlb lb);
+ if (!r=false)
+ then l:=b::!l
+ else ());
+ sel l2
+ in sel lb);
+ !l))) g
+;;
+
+(*
+let g1=["Le", ["C";"Lt";"B"; "Plus"];
+ "Lt", ["A";"Plus"]];;
+
+let g=["A",["B";"C";"D";"E"];
+ "B",["C"];
+ "C",["D"];
+ "D",["E"]];;
+remove_trans g;;
+
+*)
+let dot g name file=
+ let chan_out = open_out (file^".dot") in
+ output_string chan_out "digraph ";
+ output_string chan_out name;
+ output_string chan_out " {\n";
+ output_string chan_out " bgcolor=transparent;\n";
+ output_string chan_out " splines=true;\n";
+ output_string chan_out " nodesep=1;\n";
+ output_string chan_out " node [fontsize=18, shape=rect, color=\"#dbc3b6\", style=filled];\n";
+ List.iter (fun (x,y) ->
+ output_string chan_out " ";
+ output_string chan_out (wstring x);
+ output_string chan_out " [URL=\"./";
+ output_string chan_out x;
+ output_string chan_out ".html\"]\n";
+ List.iter (fun y ->
+ output_string chan_out " ";
+ output_string chan_out (wstring x);
+ output_string chan_out " -> ";
+ output_string chan_out (wstring y);
+ output_string chan_out ";\n") y) g;
+ flush chan_out;
+ output_string chan_out "}";
+ close_out chan_out
+;;
+
+(*
+example: a complete 5-graph,
+
+let g=["A",["B";"C";"D";"E"];
+ "B",["A";"C";"D";"E"];
+ "C",["A";"B";"D";"E"];
+ "D",["A";"B";"C";"E"];
+ "E",["A";"B";"C";"D"]];;
+
+daVinci g "g2";;
+
+the file is then g2.daVinci
+
+*)
+(***********************************************************************)
+open Genlex;;
+
+(* change OP april 28 *)
+(*
+this parsing produce a pair where the first member is a paire (file,Directory)
+and the second is a list of pairs (file,Directory).
+from this we can compute the files graph dependency and also the directory graph dependency
+*)
+
+let lexer = make_lexer [":";".";"/";"-"];;
+
+let rec parse_dep = parser
+ [< a=parse_name; 'Kwd ".";'Ident b; _=parse_until_colon;
+ _=parse_name ;'Kwd "."; 'Ident d;n=parse_rem >] -> (a,n)
+and parse_rem = parser
+ [< a=parse_name;'Kwd ".";'Ident b;n=parse_rem >] -> a::n
+ | [<>]->[]
+and parse_until_colon = parser
+ [< 'Kwd ":" >] -> ()
+ | [< 'Kwd _; _=parse_until_colon >] -> ()
+ | [< 'Int _; _=parse_until_colon >] -> ()
+ | [< 'Ident _; _=parse_until_colon >] -> ()
+
+and parse_name = parser
+ [<'Kwd "/";a=parse_ident; b=parse_name_rem a "" >]-> a::b
+ |[<a=parse_ident; b=parse_name_rem a "" >]-> a::b
+ and parse_name2 k = parser
+ [<d=parse_ident; b=parse_name_rem d k >]-> d::b
+ and parse_name_rem a b= parser
+ [<'Kwd "/";c=parse_name2 a >]-> c
+ | [<>]->[]
+
+and parse_ident = parser
+ [<'Ident a; b=parse_ident_rem a "" >]-> a ^ b
+ |[<'Int a; b=parse_ident_rem (string_of_int a) "" >]-> (string_of_int a) ^ b
+ and parse_ident2 k = parser
+ [<'Ident d; b=parse_ident_rem d k >]-> d ^ b
+ |[<'Int d; b=parse_ident_rem (string_of_int d) k >]-> (string_of_int d) ^ b
+ and parse_ident_rem a b= parser
+ [<'Kwd "-";c=parse_ident2 a >]-> "-" ^ c
+ | [<>]-> ""
+;;
+
+(*
+parse_name(lexer(Stream.of_string "u/sanglier/0/croap/pottier/Coq/Dist/contrib/Rocq/ALGEBRA/CATEGORY_THEORY/NT/YONEDA_LEMMA/NatFun.vo: "));;
+parse_ident(lexer(Stream.of_string "ARITH-OMEGA-ggg-2.vo:"));; PROBLEME
+*)
+
+(* reads the depend file *)
+let read_depend file=
+ let st =open_in file in
+ let lr =ref [] in
+ let rec other() =
+ (try
+ let d=parse_dep(lexer(Stream.of_string (input_line st))) in
+ lr:=d::(!lr);
+ other()
+ with _ ->[])
+ in (let _ = other() in ());
+ !lr;;
+
+(* graph of a directory (given by a path) *)
+let rec is_prefix p q = match p with
+ [] -> true
+ |a::p -> match q with [] -> false
+ |b::q -> if a=b then (is_prefix p q) else false
+;;
+
+let rec after_prefix p q = match p with
+ [] ->(match q with
+ [] -> "unknown"
+ |a::_ -> a)
+ |a::p -> match q with [] -> "unknown"
+ |b::q -> (after_prefix p q)
+;;
+
+let rec proj_graph p g = match g with
+ [] -> []
+ |(q,l)::g -> if (is_prefix p q)
+ then let rec proj_edges l = match l with
+ [] -> []
+ |r::l -> if (is_prefix p r)
+ then (after_prefix p r)::(proj_edges l)
+ else (proj_edges l)
+ in ((after_prefix p q),(proj_edges l))
+ ::(proj_graph p g)
+ else (proj_graph p g)
+
+;;
+
+let rec start_path p = match p with
+ [] ->[]
+ |a::p -> match p with
+ [] ->[]
+ |b::q -> a::(start_path p)
+;;
+
+
+(* the list of all the paths and subpaths in g *)
+let all_path g =
+ let ht =Hashtbl.create 50 in
+ let add_path p = Hashtbl.remove ht p;Hashtbl.add ht p true in
+ let rec add_subpath p = match p with
+ [] ->()
+ |_ -> add_path p; add_subpath (start_path p) in
+ let rec all_path g = match g with
+ [] -> ()
+ |(q,l)::g -> add_subpath (start_path q);
+ let rec all_pathl l = match l with
+ [] -> ()
+ |a::l -> add_subpath (start_path a);
+ all_pathl l
+ in all_pathl l;
+ all_path g
+ in all_path g;
+ let lp=ref [] in
+ Hashtbl.iter (fun x y -> lp:=x::!lp) ht;
+ !lp
+;;
+
+
+(*
+let g=read_depend "depend";;
+proj_graph ["theories"] g;;
+*)
+
+let rec endpath p = match p with
+ [] ->""
+ |a::p -> match p with
+ [] ->a
+ |_ -> endpath p
+;;
+
+let rec fpath p = match p with
+ [] ->""
+ |a::p -> a ^ "/" ^ (fpath p)
+;;
+
+let rec spath p = match p with
+ [] -> ""
+ |a::p -> match p with
+ [] ->a
+ |b::q -> a ^ "/" ^ (spath p)
+;;
+
+(* creates graphs for all paths *)
+
+
+let dependtodot file=
+ let g =(read_depend file) in
+ let lp1 = all_path g in
+ let lp = (if lp1=[] then [[]] else lp1) in
+ let rec ddv lp = match lp with
+ [] -> ()
+ |p::lp -> let name = (let f = (endpath p) in
+ if f="" then file else f) in
+ let filep = (let f = (spath p) in
+ if f="" then file else f) in
+ dot (remove_trans (proj_graph p g))
+ name filep;
+ ddv lp
+ in ddv lp
+
+;;
+let _ =
+ if (Array.length Sys.argv) == 2 then
+ dependtodot Sys.argv.(1)
+ else print_string "makedot depend";
+ print_newline()
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:20:32 +0000