-
Notifications
You must be signed in to change notification settings - Fork 6
Expand file tree
/
Copy pathconfig
More file actions
executable file
·169 lines (148 loc) · 4.23 KB
/
config
File metadata and controls
executable file
·169 lines (148 loc) · 4.23 KB
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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
#!/bin/sh
if test -z "$HOL2DK_DIR"
then
echo "HOL2DK_DIR is not set"
exit 1
fi
if test -z "$HOLLIGHT_DIR"
then
echo "HOLLIGHT_DIR is not set"
exit 1
fi
usage() {
cat <<__EOF__
usage: `basename $0` \$hollight_file.ml \$root_path [rocq_file_or_module] ... [\$mapping.mk] [\$mapping.lp]
arguments:
\$hollight_file.ml: path to an ml file relative to \$HOLLIGHT_DIR
\$root_path: name of the generated library
rocq_file_or_module: rocq module that needs to be imported in generated files
\$mapping.mk: dependencies of vo files given in arguments
\$mapping.lp: mappings between lambdapi and rocq
effect in the current directory:
- create a file CONFIG containing the command used to create links
- create a file BASE containing the base name of \$hollight_file.ml
- create a file ROOT_PATH containing \$root_path
- create a file lambdapi.pkg
- create a file _CoqProject
- create a file MAPPING containing \$mapping.lp
- create a file REQUIRING containing the list of Rocq module names that need to be imported (in the same order as they are given in the command)
- create a file VOFILES containing the list of Rocq module names corresponding to the Rocq files given in arguments with file extension ".vo"
- add links to \$file.mk, the Rocq files given in argument and other files in \$HOL2DK_DIR and \$HOLLIGHT_DIR for translating and checking the proofs of \$hollight_file.ml
__EOF__
}
error() {
echo error: $1
echo
usage
exit 1
}
parse_args() {
if test $# -ne 0; then
case $1 in
*.lp)
if test -z "$mapping"
then
mapping=$1
shift
parse_args $*
else
error 'too many lp files'
fi;;
*.ml)
if test -z "$hollight_file"
then
hollight_file=$1
shift
parse_args $*
else
error 'too many ml files'
fi;;
*.mk)
if test -z "$mk_file"
then
mk_file=$1
shift
parse_args $*
else
error 'too many make files'
fi;;
*.v)
if test -z "$root_path"
then
error 'the root_path must be given before Rocq files'
else
rocq_files="$rocq_files $1"
vo_files="$vo_files `basename $1`o"
requiring="$requiring $root_path.`basename $1 .v`"
shift
parse_args $*
fi;;
*)
if test -z "$root_path"
then
root_path=$1
else
requiring="$requiring $1"
fi
shift
parse_args $*;;
esac
fi
}
parse_args $*
if test -z "$root_path"
then
error 'missing root_path'
fi
echo create CONFIG ...
echo '#!/bin/sh' > CONFIG
echo hol2dk config $* >> CONFIG
chmod a+x CONFIG
echo create BASE ...
echo `basename $hollight_file .ml` > BASE
echo create ROOT_PATH ...
echo $root_path > ROOT_PATH
echo create lambdapi.pkg ...
echo "package_name = $root_path" > lambdapi.pkg
echo "root_path = $root_path" >> lambdapi.pkg
echo create _CoqProject ...
echo "-R . $root_path ." > _CoqProject
echo create MAPPING ...
if test -z "$mapping"
then
touch mapping.lp
mapping=mapping.lp
fi
echo $mapping > MAPPING
echo create REQUIRING ...
echo $requiring > REQUIRING
echo create VOFILES ...
echo $vo_files > VOFILES
if test -z "$mk_file"
then
echo create deps.mk ...
echo $vo_files: > deps.mk
else
echo ln -f -s $mk_file deps.mk
ln -f -s $mk_file deps.mk
fi
for f in $rocq_files
do
echo cp -f $f .
cp -f $f .
done
for f in theory_hol.dk theory_hol.lp
do
echo cp -f $HOL2DK_DIR/$f .
cp -f $HOL2DK_DIR/$f .
done
for f in Makefile BIG_FILES part.mk spec.mk
do
echo ln -f -s $HOL2DK_DIR/$f
ln -f -s $HOL2DK_DIR/$f
done
for ext in prf nbp sig thm pos use
do
echo ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
ln -f -s $HOLLIGHT_DIR/${hollight_file%.ml}.$ext
done