diff options
Diffstat (limited to 'etc/utils')
| -rwxr-xr-x | etc/utils/hierarchy-diagram | 154 | ||||
| -rw-r--r-- | etc/utils/hierarchy.ml | 264 | ||||
| -rw-r--r-- | etc/utils/hierarchy_test.py | 79 |
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() |