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
|
#compdef why3
##
## zsh completion for why3
## generated by ocompl
##
##
##
##
typeset -A opt_args
typeset -a last_theories
local state line cmd ret=1
local last_file tmp last_theorie
##
_arguments -s -S \
'(- *)'{-h,--help}'[Brief help message]' \
'-'"[Read the input file from stdin]"\
'*-T'"[<theory> Select <theory> in the input file or in the library]:<theory>:->theories"\
'*--theory'"[same as -T]:<theory>:->theories"\
'*-G'"[<goal> Select <goal> in the last selected theory]:<goal>:->goals"\
'*--goal'"[same as -G]:<goal>:->goals"\
'-C'"[<file> Read configuration from <file>]:Configuration File:_files -g '*.conf'"\
'--config'"[same as -C]:Configuration File:_files -g '*.conf'"\
"(-L --library -I)"'-L'"[<dir> Add <dir> to the library search path]:Mlpost lib path:_files -/ "\
"(-L --library -I)"'--library'"[same as -L]:Mlpost lib path:_files -/ "\
"(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/ "\
"(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:->provers"\
"(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:->provers"\
'*-M'"[<meta_name>=<string> Add a meta option to each tasks]:<meta_name>=<meta_arg>:->metas"\
"(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
"(-F --format)"'--format'"[same as -F]:<input format>:"\
"(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
"(-t --timelimit)"'--timelimit'"[same as -t]:<timeout s>:"\
"(-m --memlimit)"'-m'"[<MiB> Set the prover\'s memory limit (default: no limit)]:<memory limit M>:"\
"(-m --memlimit)"'--memlimit'"[same as -m]:<memory limit M>:"\
"(-D --driver -P -prover)"'-D'"[<file> Specify a prover\'s driver (conflicts with -P)]:Prover\'s driver:_files -g '*.drv'"\
"(-D --driver -P -prover)"'--driver'"[same as -D]:Prover\'s driver:_files -g '*.drv'"\
"(-o --output)"'-o'"[<dir> Print the selected goals to separate files in <dir>]:directory output:_files -/ "\
"(-o --output)"'--output'"[same as -o]:directory output:_files -/ "\
'--print-theory'"[Print the selected theories]"\
'--print-namespace'"[Print the namespaces of selected theories]"\
"(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--parse-only'"[Stop after parsing]"\
"(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--type-only'"[Stop after type checking]"\
'--debug'"[Set the debug flag]"\
'*-a'"[<transformation> Add a transformation to apply to the task]:<transformation>:->transforms"\
'*--apply-transform'"[same as -a]:<transformation>:->transforms"\
"*:The why3 file:->files"\
&& return 0
cmd=$service
last_file=$line[-1]
tmp=$opt_args[-T]
last_theories=(${(s<:>)tmp})
last_theory=$last_theories[-1]
case $state in
transforms)
_message "<transformations>";
compadd $($cmd show transformations | grep -e '^ [^ ]');
return 0
;;
provers)
_message "<provers>";
compadd $($cmd config list-provers | sed -n -e 's/^\([^ ]\+\).*/\1/p' | uniq);
return 0
;;
metas)
_message "<metas>";
METAS="$($cmd show metas |
grep -e '^[^ ]\+\( (flag)\)\?\( \[string\]\)\?$' |
sed -e 's/ (flag)//;s/ \[string\]/=/')";
METAS=(${(f)METAS});
compadd $METAS;
return 0
;;
theories)
tmp=$($cmd --print-namespace $last_file 2> /dev/null);
if [[ $? = 0 ]]; then
_message "<theories of $last_file>";
compadd $(echo $tmp |grep "^[a-zA-Z]" | cut -d- -f 1);
return 0
else
_message "<invalid file $last_file>";
return 1
fi;;
goals)
tmp=$($cmd --print-namespace $last_file -T $last_theory 2> /dev/null);
if [[ $? = 0 ]]; then
_message "<goals of $last_theory>";
compadd $(echo $tmp |grep -e "-goal" | sed "s/[^-]*-goal //");
return 0
else
_message "<invalid file or theory>";
return 1
fi;;
files)
case $cmd in
why3)
_files -g '*.{why,mlw}';
return 0;
;;
*)
_message "absurd";
return 1;
esac;;
*)
return 1
esac
#_why3 "$@"
|
