From 7583b9007c3ed23720d26a522f0d822722a11e2a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 3 Apr 2019 12:42:50 +0200 Subject: least common childen --- etc/utils/hierarchy_test.py | 69 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 53 insertions(+), 16 deletions(-) (limited to 'etc/utils') diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py index 79e065c..b3c4dc1 100644 --- a/etc/utils/hierarchy_test.py +++ b/etc/utils/hierarchy_test.py @@ -4,34 +4,71 @@ import pygraphviz as pgv import sys, argparse -def children(G,n): - res = set() - new = set([n]) - while new != set(): - p = new.pop() - res.add(p) - new.update(set(G.successors(p)).difference(res)) +def children(G,r): + res = [] + new = list([r]) + while new != []: + n = new.pop() + # replace with a correct implementation of a topological sort + ns = set(G.successors(n)) + resp = list(filter(lambda x: x not in ns, res)) + resn = list(filter(lambda x: x in ns, res)) + res = resp + [n] + resn + new=(list(ns.difference(set(res))))+new return res -def common_children(G): +def least_common_children(G): result = set() for x in G.nodes(): for y in G.nodes(): - if x < y and children(G,x).intersection(children(G,y)) != set(): - result.add((x,y)) + if x < y: + z = next((n for n in children(G,x) if n in children(G,y)),None) + if z != None: + result.add((x,y,z)) return result -def print_common_children_coq_check(G): - print("(** Generated by etc/utils/hierarchy_test.py *)") - print("From mathcomp Require Import all.") +def print_least_common_children_coq_check(G): + 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 f1 := open_constr:(id : t1 -> Type) in + let f2 := open_constr:(id : t2 -> Type) in + let T1 := open_constr:(_ : t1) in + let T2 := open_constr:(_ : t2) in + match tt with + | _ => unify (f1 T1) (f2 T2) + | _ => fail "There is no join of" t1 "and" t2 + end; + let Tjoin := + lazymatch T1 with + | _ ?Tjoin => constr: (Tjoin) + | ?Tjoin => constr: (Tjoin) + end + in + 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.nodes(): 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 _).") print ("") - for (x, y) in common_children(G): - print ("Goal False. have := erefl : (_ : " + x + ".type) = (_ : " + y + ".type) :> Type. Abort.") + print ("Goal False.") + for (x, y,z) in least_common_children(G): + print ("check_join " + x + ".type " + y + ".type " + z + ".type.") + print ("Abort.") def main(): parser = argparse.ArgumentParser(description='Generate a check .v file \ @@ -39,7 +76,7 @@ def main(): parser.add_argument('dotfile', metavar='', nargs=1, help='a dotfile representing the hierarchy') args = parser.parse_args() - print_common_children_coq_check(pgv.AGraph(args.dotfile[0])) + print_least_common_children_coq_check(pgv.AGraph(args.dotfile[0])) if __name__ == "__main__": main() -- cgit v1.2.3 From a348deb229074be37ff31fd892a7d8835a49b566 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 5 Apr 2019 19:11:55 +0200 Subject: New test cases generation: corrent implementation of least common children Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an intermediate file for `hierarchy_test.py`. So the typical usage is: $ python3.5 etc/utils/hierarchy_test.py \ <(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \ > mathcomp/test_suite/hierarchy_test.v --- etc/utils/hierarchy-diagram | 38 ++++++++++++++++++------- etc/utils/hierarchy_test.py | 67 ++++++++++++++++++++++----------------------- 2 files changed, 60 insertions(+), 45 deletions(-) (limited to 'etc/utils') diff --git a/etc/utils/hierarchy-diagram b/etc/utils/hierarchy-diagram index 845ecfa..e30bb87 100755 --- a/etc/utils/hierarchy-diagram +++ b/etc/utils/hierarchy-diagram @@ -40,6 +40,7 @@ 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=() @@ -49,6 +50,10 @@ while [[ $# -gt 0 ]] do case "$1" in + -raw-inheritances) + opt_raw_inheritances=on + shift; + ;; -canonicals) opt_canonicals="$2" shift; shift @@ -86,18 +91,31 @@ 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 $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 $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 @@ -114,8 +132,6 @@ if [[ $opt_canonicals != "off" ]]; then fi if [[ $opt_coercions != "off" ]]; then - cat $raw_coercions.out \ - | sed -n 's/^\[\([^]]*\)\] : \([a-zA-Z_\.]*\)\.type >-> \([a-zA-Z_\.]*\)\.type$/\2 \3 \1/p' > $parsed_coercions cat $parsed_coercions | while read -r from_module to_module coercion; do grep "^$from_module " $parsed_coercions | ( while read -r _ middle_module _; do @@ -133,4 +149,6 @@ fi echo "}" +fi + rm $raw_coercions.out $raw_canonicals.out $parsed_coercions $parsed_canonicals diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py index b3c4dc1..b0a034c 100644 --- a/etc/utils/hierarchy_test.py +++ b/etc/utils/hierarchy_test.py @@ -1,33 +1,9 @@ #!/usr/bin/python # usage: hiearchy_test.py inputfile -import pygraphviz as pgv -import sys, argparse +import sys, argparse, collections -def children(G,r): - res = [] - new = list([r]) - while new != []: - n = new.pop() - # replace with a correct implementation of a topological sort - ns = set(G.successors(n)) - resp = list(filter(lambda x: x not in ns, res)) - resn = list(filter(lambda x: x in ns, res)) - res = resp + [n] + resn - new=(list(ns.difference(set(res))))+new - return res - -def least_common_children(G): - result = set() - for x in G.nodes(): - for y in G.nodes(): - if x < y: - z = next((n for n in children(G,x) if n in children(G,y)),None) - if z != None: - result.add((x,y,z)) - return result - -def print_least_common_children_coq_check(G): +def print_hierarchy_test(G, test_cases): print ("(** Generated by etc/utils/hierarchy_test.py *)") print ("From mathcomp Require Import all.") @@ -35,20 +11,20 @@ def print_least_common_children_coq_check(G): (* `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 f1 := open_constr:(id : t1 -> Type) in - let f2 := open_constr:(id : t2 -> Type) in let T1 := open_constr:(_ : t1) in let T2 := open_constr:(_ : t2) in match tt with - | _ => unify (f1 T1) (f2 T2) + | _ => 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 @@ -59,24 +35,45 @@ Tactic Notation "check_join" "but is expected to be" tjoin end. """) - for x in G.nodes(): + 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 _).") + print ("Local Notation \"" + x + ".type\" := (" + x + ".type _) (only parsing).") print ("") print ("Goal False.") - for (x, y,z) in least_common_children(G): + 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('dotfile', metavar='', nargs=1, - help='a dotfile representing the hierarchy') + parser.add_argument('graph', metavar='', nargs=1, + help='a file representing the hierarchy') args = parser.parse_args() - print_least_common_children_coq_check(pgv.AGraph(args.dotfile[0])) + 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() -- cgit v1.2.3