@@ -179,21 +179,21 @@ run_interpret() {
179
179
-c SCHEDULE " $cSCHEDULE " text -c MODE " $cMODE " text --initializer ' initKevmCell' \
180
180
--output-file " $output " " $@ " \
181
181
|| exit_status=" $? "
182
- if [[ " $exit_status " != ' 0' ]]; then
182
+ if [[ " $unparse " == ' true ' ]] && [[ " $ exit_status" != ' 0' ]]; then
183
183
k-bin-to-text " $output " " $output_text "
184
184
cat " $output_text "
185
- exit " $exit_status "
186
185
fi
186
+ exit " $exit_status "
187
187
;;
188
188
189
189
llvm) run_kast kore > " $kast "
190
190
if $debug ; then debugger=" gdb --args" ; fi
191
191
$debugger " $interpreter " " $kast " -1 " $output_text " " $@ " \
192
192
|| exit_status=" $? "
193
- if [[ " $exit_status " != ' 0' ]]; then
193
+ if [[ " $unparse " == ' true ' ]] && [[ " $ exit_status" != ' 0' ]]; then
194
194
cat " $output_text " | " $0 " kast --backend " $backend " - pretty --input " $output_format " --sort GeneratedTopCell
195
- exit " $exit_status "
196
195
fi
196
+ exit " $exit_status "
197
197
;;
198
198
199
199
* ) fatal " Bad backend for interpreter: '$backend '"
@@ -208,17 +208,17 @@ run_command="$1" ; shift
208
208
209
209
if [[ " $run_command " == ' help' ]] || [[ " $run_command " == ' --help' ]] ; then
210
210
echo "
211
- usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*
212
- $0 interpret [--backend (ocaml|llvm)] [--debug] <pgm> <interpreter arg>*
213
- $0 kast [--backend (ocaml|java|llvm|haskell|web3)] <pgm> <output format> <K arg>*
214
- $0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
215
- $0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
216
- $0 web3 [--debug|--dump] <port>
217
- $0 web3-ganache [--debug|--dump] <port>
218
- $0 web3-send <port> <web3 method> <web3 params>
219
- $0 klab-run <pgm> <K arg>*
220
- $0 klab-prove <spec> <K arg>* -m <def_module>
221
- $0 klab-view <spec>
211
+ usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*
212
+ $0 interpret [--backend (ocaml|llvm)] [--debug|--no-unparse] <pgm> <interpreter arg>*
213
+ $0 kast [--backend (ocaml|java|llvm|haskell|web3)] <pgm> <output format> <K arg>*
214
+ $0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
215
+ $0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
216
+ $0 web3 [--debug|--dump] <port>
217
+ $0 web3-ganache [--debug|--dump] <port>
218
+ $0 web3-send <port> <web3 method> <web3 params>
219
+ $0 klab-run <pgm> <K arg>*
220
+ $0 klab-prove <spec> <K arg>* -m <def_module>
221
+ $0 klab-view <spec>
222
222
223
223
$0 [help|--help|version|--version]
224
224
265
265
backend=" llvm"
266
266
debug=false
267
267
dump=false
268
+ unparse=true
268
269
[[ ! " $run_command " == ' prove' ]] || backend=' java'
269
270
[[ ! " $run_command " =~ klab* ]] || backend=' java'
270
271
[[ ! " $run_command " =~ web3* ]] || backend=' llvm'
271
272
while [[ $# -gt 0 ]]; do
272
- arg=" $1 "
273
- case $arg in
274
- --backend)
275
- backend=" $2 "
276
- shift 2
277
- ;;
278
- --debug)
279
- debug=true
280
- shift
281
- ;;
282
- --dump)
283
- dump=true
284
- shift
285
- ;;
286
- * )
287
- break
288
- ;;
289
- esac
273
+ arg=" $1 "
274
+ case $arg in
275
+ --backend) backend=" $2 " ; shift 2 ;;
276
+ --debug) debug=true ; shift ;;
277
+ --dump) dump=true ; shift ;;
278
+ --no-unparse) unparse=false ; shift ;;
279
+ * ) break ;;
280
+ esac
290
281
done
291
282
backend_dir=" $defn_dir /$backend "
292
283
[[ ! " $backend " == " ocaml" ]] || eval $( ${OPAM:- opam} config env)
0 commit comments