Reimplement the hierarchy related tools in OCaml

The functionalities of the structure hierarchy related tools `hierarchy-diagram`
and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`.
`test_suite/hierarchy_test.v` is deleted. Now make can generate it.

3 files changed, 264 insertions, 233 deletions

diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram
deleted file mode 100755
index e30bb87..0000000
--- a/etc/utils/hierarchy-diagram
+++ /dev/null
@@ -1,154 +0,0 @@
-#!/bin/bash
-
-usage(){
-cat <<EOT >&2
-Usage : hierarchy-diagram [OPTIONS]
-
-Description:
-    hierarchy-diagram is a small utility to draw hierarchy diagrams of
-    mathematical structures.  This utility uses the coercion paths and the
-    canonical projections between <module>.type types (typically in the MathComp
-    library) to draw the diagram.  Indirect edges which can be composed of other
-    edges by transitivity are eliminated automatically for each kind of edges.
-    A diagram appears on the standard output in the DOT format which can be
-    converted to several image formats by Graphviz.
-
-Options:
-    -h, -help:
-        Output a usage message and exit.
-
-    -canonicals (off|on|color):
-        Configure output of edges of canonical projections.  The default value
-        is "on".
-
-    -coercions (off|on|color):
-        Configure output of edges of coercions.  The default value is "off".
-        The value given by this option must be different from that by
-        -canonical soption.
-
-    -R dir coqdir:
-        This option is passed to coqtop: "recursively map physical dir to
-        logical coqdir".
-
-    -lib library:
-        Specify a Coq library used to draw a diagram.  This option can appear
-        repetitively.  If not specified, all.all will be used.
-EOT
-}
-
-raw_coercions=$(tempfile -s .out | sed s/\.out$//)
-raw_canonicals=$(tempfile -s .out | sed s/\.out$//)
-parsed_coercions=$(tempfile)
-parsed_canonicals=$(tempfile)
-opt_raw_inheritances=off
-opt_canonicals=on
-opt_coercions=off
-opt_libs=()
-opt_coqtopargs=()
-
-while [[ $# -gt 0 ]]
-do
-
-case "$1" in
-  -raw-inheritances)
-    opt_raw_inheritances=on
-    shift;
-  ;;
-  -canonicals)
-    opt_canonicals="$2"
-    shift; shift
-  ;;
-  -coercions)
-    opt_coercions="$2"
-    shift; shift
-  ;;
-  -R)
-    opt_coqtopargs+=("-R" "$2" "$3")
-    shift; shift; shift
-  ;;
-  -lib)
-    opt_libs+=("$2")
-    shift; shift
-  ;;
-  -h|-help)
-    usage; exit
-  ;;
-  *)
-    echo "ERROR: invalid option -- $1" >&2
-    echo >&2
-    usage; exit 1
-  ;;
-esac
-
-done
-
-[[ ${#opt_libs[@]} -eq 0 ]] && opt_libs=(all.all)
-
-coqtop -w none ${opt_coqtopargs[@]} >/dev/null 2>&1 <<EOT
-Set Printing Width 4611686018427387903.
-Require Import ${opt_libs[@]}.
-Redirect "$raw_coercions" Print Graph.
-Redirect "$raw_canonicals" Print Canonical Projections.
-EOT
-
-cat $raw_canonicals.out \
-| sed -n 's/^\([a-zA-Z_\.]*\)\.sort <- \([a-zA-Z_\.]*\)\.sort ( \([a-zA-Z_\.]*\)\.\([a-zA-Z_]*\) )$/\1 \2 \3 \4/p' \
-| while read -r from_module to_module proj_module projection; do
-  if [[ $from_module = $proj_module ]] || [[ $to_module = $proj_module ]]; then
-    echo $from_module $to_module $proj_module $projection
-  fi
-done > $parsed_canonicals
-
-cat $raw_coercions.out \
-| sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions
-
-if [[ $opt_raw_inheritances != "off" ]]; then
-
-  cat $parsed_canonicals | sed 's/^\([^ ]*\) \([^ ]*\) .*$/\1\n\2/g' | sort | uniq \
-  | while read -r module; do
-    echo -n "$module "
-    sed -n "s/^\([^ ]*\) $module .*$/\1/p" $parsed_canonicals | sort | xargs
-  done
-
-else
-
-echo "digraph structures {"
-
-if [[ $opt_canonicals != "off" ]]; then
-
-  cat $parsed_canonicals | while read -r from_module to_module proj_module projection; do
-    grep "^$from_module " $parsed_canonicals | ( while read -r _ middle_module _ _; do
-      if grep -q "^$middle_module $to_module " $parsed_canonicals; then
-        exit 1
-      fi
-    done )
-    if [[ "$?" = "0" ]]; then
-      echo -n "\"$to_module\" -> \"$from_module\""
-      [[ $opt_canonicals == "on" ]] || echo -n "[color=$opt_canonicals]"
-      echo ";"
-    fi
-  done
-
-fi
-
-if [[ $opt_coercions != "off" ]]; then
-
-  cat $parsed_coercions | while read -r from_module to_module coercion; do
-    grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do
-      if grep -q "^$middle_module $to_module " $parsed_coercions; then
-        exit 1
-      fi
-    done )
-    if [[ "$?" = "0" ]]; then
-      echo -n "\"$to_module\" -> \"$from_module\""
-      [[ $opt_coercions == "on" ]] || echo -n "[color=$opt_coercions]"
-      echo ";"
-    fi
-  done
-fi
-
-echo "}"
-
-fi
-
-rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals
diff --git a/etc/utils/hierarchy.ml b/etc/utils/hierarchy.ml
new file mode 100644
index 0000000..33d598a
--- /dev/null
+++ b/etc/utils/hierarchy.ml
@@ -0,0 +1,264 @@
+#load "unix.cma";;
+#load "str.cma";;
+
+module MapS = Map.Make(String)
+
+let usage () =
+print_endline
+{|Usage : ocaml hierarchy.ml [OPTIONS]
+
+Description:
+    hierarchy.ml is a small utility to draw a diagram of and verify the
+    hierarchy of mathematical structures.  This utility uses the coercion paths
+    and the canonical projections between <module>.type types (typically in the
+    MathComp library) to draw the diagram.  Indirect edges which can be
+    composed of other edges by transitivity are eliminated automatically for
+    each kind of edges.  A diagram appears on the standard output in the DOT
+    format which can be converted to several image formats by Graphviz.
+
+Options:
+    -h, -help:
+        Output a usage message and exit.
+
+    -verify:
+        Output a proof script to verify the join canonical projections.  The
+        options "-canonicals" and "-coercions" are ignored if "-verify" is
+        given.
+
+    -canonicals (off|on|color):
+        Configure output of edges of canonical projections.  The default value
+        is "on".
+
+    -coercions (off|on|color):
+        Configure output of edges of coercions.  The default value is "off".
+        The value given by this option must be different from that by
+        -canonical soption.
+
+    -R dir coqdir:
+        This option is given to coqtop: "recursively map physical dir to
+        logical coqdir".
+
+    -lib library:
+        Specify a Coq library used to draw a diagram.  This option can appear
+        repetitively.  If not specified, all.all will be used.|}
+;;
+
+let coqtop =
+  match Sys.getenv "COQBIN" with
+    | exception Not_found -> "coqtop"
+    | coqbin ->
+      if coqbin.[String.length coqbin - 1] = '/' then
+        coqbin ^ "coqtop"
+      else
+        coqbin ^ "/coqtop"
+;;
+
+let parse_canonicals file =
+  let lines = ref [] in
+  let ic = open_in file in
+  let re = Str.regexp
+      "^\\([^ ]+\\)\\.sort <- \\([^ ]+\\)\\.sort ( \\([^ ]+\\)\\.\\([^\\. ]+\\) )$" in
+  begin
+    try while true do
+        let line = input_line ic in
+        if Str.string_match re line 0
+        then
+          let to_module = Str.matched_group 1 line in
+          let from_module = Str.matched_group 2 line in
+          let proj_module = Str.matched_group 3 line in
+          if from_module = proj_module || to_module = proj_module then
+            lines := (from_module, to_module,
+                      proj_module ^ "." ^ Str.matched_group 4 line) :: !lines
+      done with End_of_file -> close_in ic
+  end;
+  List.rev !lines
+;;
+
+let parse_coercions file =
+  let lines = ref [] in
+  let ic = open_in file in
+  let re = Str.regexp
+      "^\\[\\([^]]+\\)\\] : \\([^ ]+\\)\\.type >-> \\([^ ]+\\)\\.type$" in
+  begin
+    try while true do
+        let line = input_line ic in
+        if Str.string_match re line 0
+        then
+          lines := (Str.matched_group 3 line, Str.matched_group 2 line,
+                    Str.matched_group 1 line) :: !lines
+      done with End_of_file -> close_in ic
+  end;
+  List.rev !lines
+;;
+
+let map_of_inheritances (inhs : (string * string * string) list) =
+  let rec recur m = function
+    | [] -> m
+    | (from_module, to_module, inh) :: inhs ->
+      recur
+        (MapS.update to_module
+           (function None -> Some MapS.empty | m' -> m')
+           (MapS.update from_module
+              (function
+                | None -> Some (MapS.singleton to_module inh)
+                | Some m' -> Some (MapS.add to_module inh m'))
+              m))
+        inhs
+  in
+  recur MapS.empty inhs
+;;
+
+let is_transitive inhs =
+  let key_subset m m' = MapS.for_all (fun k _ -> MapS.mem k m') m in
+  MapS.for_all
+    (fun kl ml ->
+       MapS.for_all
+         (fun kr _ -> match MapS.find_opt kr inhs with
+              None -> true | Some mr -> key_subset ml mr) ml) inhs
+;;
+
+let minimalize inhs m =
+  let rec recur m k =
+    match MapS.find_first_opt (fun k' -> String.compare k k' < 0) m with
+      | None -> m
+      | Some (k', _) ->
+        try recur (MapS.merge
+                     (fun _ v v' ->
+                        match v, v' with Some _, None -> v | _, _ -> None)
+                     m (MapS.find k' inhs)) k'
+        with Not_found -> recur m k'
+  in
+  recur m ""
+;;
+
+let print_verifier libs inhs =
+  Printf.printf
+{|(** Generated by etc/utils/hierarchy.ml *)
+From mathcomp Require Import %s.
+
+(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *)
+Tactic Notation "check_join"
+       open_constr(t1) open_constr(t2) open_constr(tjoin) :=
+  let rec fillargs t :=
+    lazymatch type of t with
+      | forall _, _ => let t' := open_constr:(t _) in fillargs t'
+      | _ => t
+    end
+  in
+  let t1 := fillargs t1 in
+  let t2 := fillargs t2 in
+  let tjoin := fillargs tjoin in
+  let T1 := open_constr:(_ : t1) in
+  let T2 := open_constr:(_ : t2) in
+  match tt with
+    | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
+    | _ => fail "There is no join of" t1 "and" t2
+  end;
+  let Tjoin :=
+    lazymatch T1 with
+      _ (_ ?Tjoin) => Tjoin | _ ?Tjoin => Tjoin | ?Tjoin => Tjoin
+    end
+  in
+  is_evar Tjoin;
+  let tjoin' := type of Tjoin in
+  lazymatch tjoin' with
+    | tjoin => idtac
+    | _ => fail "The join of" t1 "and" t2 "is" tjoin'
+                "but is expected to be" tjoin
+  end.
+
+Goal False.
+|}
+    (String.concat " " libs);
+  MapS.iter (fun kl ml ->
+      MapS.iter (fun kr mr ->
+          let m =
+            minimalize inhs
+              (MapS.merge
+                 (fun _ v v' ->
+                    match v, v' with Some _, Some _ -> Some () | _, _ -> None)
+                 (MapS.add kl "" ml) (MapS.add kr "" mr))
+          in
+          match MapS.bindings m with
+            | [] -> ()
+            | [kj, ()] ->
+              Printf.printf "check_join %s.type %s.type %s.type.\n" kl kr kj
+            | joins ->
+              failwith
+                (Printf.sprintf
+                   "%s and %s have more than two least common children: %s."
+                   kl kr (String.concat ", " (List.map fst joins)))
+        ) inhs) inhs;
+  Printf.printf "Abort.\n"
+;;
+
+let () =
+  let opt_verify = ref false in
+  let opt_canonicals = ref "on" in
+  let opt_coercions = ref "off" in
+  let opt_libmaps = ref [] in
+  let opt_imports = ref [] in
+  let tmp_coercions = Filename.temp_file "" ".out" in
+  let tmp_canonicals = Filename.temp_file "" ".out" in
+  let rec parse = function
+    | [] -> ()
+    | "-verify" :: rem -> opt_verify := true; parse rem
+    | "-canonicals" :: col :: rem -> opt_canonicals := col; parse rem
+    | "-coercions" :: col :: rem -> opt_coercions := col; parse rem
+    | "-R" :: path :: log :: rem ->
+      opt_libmaps := (path, log) :: !opt_libmaps; parse rem
+    | "-lib" :: lib :: rem -> opt_imports := lib :: !opt_imports; parse rem
+    | "-h" :: _ | "-help" :: _ -> usage (); exit 0
+    | _ -> usage (); exit 1
+  in
+  parse (List.tl (Array.to_list Sys.argv));
+  opt_libmaps := List.rev !opt_libmaps;
+  opt_imports :=
+    if !opt_imports = [] then ["all.all"] else List.rev !opt_imports;
+  (* Interact with coqtop *)
+  begin
+    let (coqtop_out, coqtop_in, _) as coqtop_ch =
+      Unix.open_process_full
+        (Printf.sprintf "%S -w none " coqtop ^
+         String.concat " "
+           (List.map (fun (path, log) -> Printf.sprintf "-R %S %S" path log)
+              !opt_libmaps))
+        [||]
+    in
+    Printf.fprintf coqtop_in {|
+Set Printing Width 4611686018427387903.
+From mathcomp Require Import %s.
+Redirect %S Print Canonical Projections.
+Redirect %S Print Graph.
+|}
+      (String.concat " " !opt_imports)
+      (List.hd (String.split_on_char '.' tmp_canonicals))
+      (List.hd (String.split_on_char '.' tmp_coercions));
+    close_out coqtop_in;
+    try while true do ignore (input_line coqtop_out) done
+      with End_of_file -> ignore (Unix.close_process_full coqtop_ch)
+  end;
+  (* Parsing *)
+  let canonicals = parse_canonicals tmp_canonicals in
+  let coercions = parse_coercions tmp_coercions in
+  (* Output *)
+  if !opt_verify then
+    print_verifier !opt_imports (map_of_inheritances canonicals)
+  else begin
+    let print_graph opt inhs =
+      if opt <> "off" then
+        let attr = if opt = "on" then "" else "color=" ^ opt in
+        MapS.iter
+          (fun k m ->
+             MapS.iter (fun k' _ -> Printf.printf "%S -> %S[%s];\n" k k' attr)
+               (minimalize inhs m))
+          inhs
+    in
+    print_endline "digraph structures {";
+    print_graph !opt_canonicals (map_of_inheritances canonicals);
+    print_graph !opt_coercions (map_of_inheritances coercions);
+    print_endline "}"
+  end;
+  Sys.remove tmp_canonicals;
+  Sys.remove tmp_coercions;
+;;
diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py
deleted file mode 100644
index b0a034c..0000000
--- a/etc/utils/hierarchy_test.py
+++ /dev/null
@@ -1,79 +0,0 @@
-#!/usr/bin/python
-# usage: hiearchy_test.py inputfile
-
-import sys, argparse, collections
-
-def print_hierarchy_test(G, test_cases):
-    print ("(** Generated by etc/utils/hierarchy_test.py *)")
-    print ("From mathcomp Require Import all.")
-
-    print ("""
-(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *)
-Tactic Notation "check_join"
-       open_constr(t1) open_constr(t2) open_constr(tjoin) :=
-  let T1 := open_constr:(_ : t1) in
-  let T2 := open_constr:(_ : t2) in
-  match tt with
-    | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
-    | _ => fail "There is no join of" t1 "and" t2
-  end;
-  let Tjoin :=
-    lazymatch T1 with
-      | _ (_ ?Tjoin) => constr: (Tjoin)
-      | _ ?Tjoin => constr: (Tjoin)
-      | ?Tjoin => constr: (Tjoin)
-    end
-  in
-  is_evar Tjoin;
-  let tjoin' := type of Tjoin in
-  lazymatch tjoin' with
-    | tjoin => lazymatch tjoin with
-                 | tjoin' => idtac
-                 | _ => idtac tjoin'
-               end
-    | _ => fail "The join of" t1 "and" t2 "is" tjoin'
-                "but is expected to be" tjoin
-  end.
-""")
-    for x in G.keys():
-        if x.rfind("Lmod") >= 0 or x.rfind("Splitting") >= 0 or \
-           x.rfind("lgebra") >= 0 or x.rfind("FieldExt") >= 0 or \
-           x.rfind("Vector") >= 0:
-            print ("Local Notation \"" + x + ".type\" := (" + x + ".type _) (only parsing).")
-    print ("")
-    print ("Goal False.")
-    for (x,y,z) in test_cases:
-        print ("check_join " + x + ".type " + y + ".type " + z + ".type.")
-    print ("Abort.")
-
-def compute_least_common_children(G):
-    tests=[]
-    for pa, ch_a in G.items():
-        for pb, ch_b in G.items():
-            ch_c = ({pa} | ch_a) & ({pb} | ch_b) # common children
-            for c in ch_c:
-                ch_c = ch_c - G[c]
-            if len(ch_c) == 1:
-                tests.append((pa, pb, ch_c.pop()))
-            elif 2 <= len(ch_c):
-                print (pa, "and", pb, "have more than two least common children:", ch_c, ".", file=sys.stderr)
-                sys.exit(1)
-    return tests
-
-def main():
-    parser = argparse.ArgumentParser(description='Generate a check .v file \
-                 for mathcomp structure hiearchies')
-    parser.add_argument('graph', metavar='<graph>', nargs=1,
-                        help='a file representing the hierarchy')
-    args = parser.parse_args()
-    G = {}
-    with open(args.graph[0]) as f:
-        for line in f:
-            words = line.split()
-            p = words.pop(0)
-            G[p] = set(words)
-    G = collections.OrderedDict(sorted(G.items()))
-    print_hierarchy_test(G, compute_least_common_children(G))
-
-if __name__ == "__main__":
-    main()