1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
#!/bin/sh
# auto bench for why
pgm=$1
option=$2
coqc="coqc -I ../lib/coq"
pvstc () {
context=`dirname $1`
theory=`basename $1`
cd $context
echo "(typecheck "'"'$theory'"'")" > pvstc.el
pvs -q -batch -l pvstc.el
cd ..
}
provers () {
file=$1
base=$2
dir=`dirname $1`
# running Coq
if ! $coqc "$base"_why.v > /dev/null 2>&1; then
echo "coq FAILED"
$coqc "$base"_why.v
exit 1
fi
# if ! $coqc -I $dir "$base"_valid.v > /dev/null 2>&1; then
# echo "coq validation FAILED"
# $coqc -I $dir "$base"_valid.v
# exit 1
# fi
echo -n "coq ok... "
# running PVS
if ! $pgm --pvs $f > /dev/null 2>&1; then
echo "pvs generation FAILED"
$pgm --pvs $f
exit 1
fi
if test "$option" = "pvs"; then
if ! pvstc "$base"_why > /dev/null 2>&1; then
echo "pvs typecheck FAILED"
pvs -q -v 3 -batch -l pvstc.el
exit 1
fi
echo "pvs ok"
else
echo
fi
}
good_tc () {
for f in $1/*.mlw; do
echo -n " "$f"... "
base=$1/`basename $f .mlw`
# running Why
if ! $pgm --type-only $f > /dev/null 2>&1; then
echo "why FAILED"
$pgm --type-only $f
exit 1
fi
echo "why ok... "
done
}
good_ml () {
for f in $1/*.mlw; do
echo -n " "$f"... "
base=$1/`basename $f .mlw`
# running Why
if ! $pgm --coq-@COQVER@ $f > /dev/null 2>&1; then
echo "why FAILED"
$pgm --coq-@COQVER@ $f
exit 1
fi
echo -n "why ok... "
provers $f $base
# echo -n "coq ok..."
# $pgm --ocaml --ocaml-ext $f > $base.ml 2>/dev/null
# if ocamlc -c $base.ml > /dev/null 2>&1; then
# echo "ocaml ok"
# else
# echo "ocaml FAILED"
# fi
done
}
bads () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgm $2 $f > /dev/null 2>&1; then
echo "$pgm $2 $f"
echo "FAILED!"
exit 1
else
echo "ok"
fi
done
}
# 1. Syntax
echo "=== Checking parsing errors ==="
bads bad/syntax --parse-only
echo ""
# 2. Typing
echo "=== Checking typing errors ==="
bads bad/typing --type-only
echo ""
# 2. Other
echo "=== Checking other errors ==="
bads bad/other
echo ""
# 3. benchmark
echo "=== Type-checking good files ==="
good_tc provers
echo ""
echo "=== Checking good files ==="
good_ml good
echo ""
|
