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
|
#!/bin/bash
COQSRC=../../coq
if [ $# -gt 0 ]; then
COQSRC=$1
fi
PLUGINSRC=../../src
if [ $# -gt 1 ]; then
PLUGINSRC=$2
fi
THEORIES=$COQSRC
GENDEP=$( dirname "${BASH_SOURCE[0]}")/gendep.py
echo "COQSRC = $COQSRC"
echo "PLUGINSRC = $PLUGINSRC"
echo "GENDEP = $GENDEP"
ARGS=$(find $THEORIES -name "Rdef*.v" | sed 's/^.*coq\///')
ARGS="$ARGS $(find $THEORIES -name "Classical_Prop.v" | sed 's/^.*coq\///')"
modules=$(find $THEORIES -name '*.d' -exec cat '{}' ';' | grep '\.vo[^:]*: ' | python $GENDEP $ARGS)
tmp="/tmp/stdlib.tmp.v"
prefix="stdlib_R"
makefile="Makefile.gen"
for x in $modules; do
if [[ $x == *-* ]]; then
echo "Parametricity Module $(echo $x | sed 's/-.*$//') as $(echo $x | sed 's/^.*-//')." >> $tmp
else
echo "Parametricity Module $x." >> $tmp
fi
done
test -f $tmp || exit
split -l 15 -d $tmp $prefix --additional-suffix=.v
rm -f $tmp
cat > $makefile << EOF
COQBIN := $COQSRC/bin/
PLUGINSRC := $PLUGINSRC
OPTIONS := -I \$(PLUGINSRC)
.PHONY: coq clean
SRCS=\$(wildcard *.v)
OBJS=\$(SRCS:.v=.vo)
all: \$(OBJS)
%.vo: %.v
\$(COQBIN)coqc \$(OPTIONS) \$<
Parametricity.vo: Parametricity.v
clean:
rm -f *.vo *.glob
EOF
first="$(printf "$prefix%02d" 0)"
sed -i "1iRequire Parametricity.\nRequire Import $(echo $modules | sed 's/-[a-Z]*[0-9]*_R//g').\n(* Ignoring the following modules : $ARGS. *)" $first.v
echo "$first.vo : $first.v Parametricity.vo" >> $makefile
for x in $(seq 0 100); do
y=$(($x + 1))
prev="$(printf "$prefix%02d" $x)"
file="$(printf "$prefix%02d" $y)"
if [ -f "$file.v" ]; then
sed -i "1iRequire $prev." $file.v
echo "$file.vo : $file.v $prev.vo" >> $makefile
fi
done
|
