@@ -179,21 +179,21 @@ run_interpret() {
179179 -c SCHEDULE " $cSCHEDULE " text -c MODE " $cMODE " text --initializer ' initKevmCell' \
180180 --output-file " $output " " $@ " \
181181 || exit_status=" $? "
182- if [[ " $exit_status " != ' 0' ]]; then
182+ if [[ " $unparse " == ' true ' ]] && [[ " $ exit_status" != ' 0' ]]; then
183183 k-bin-to-text " $output " " $output_text "
184184 cat " $output_text "
185- exit " $exit_status "
186185 fi
186+ exit " $exit_status "
187187 ;;
188188
189189 llvm) run_kast kore > " $kast "
190190 if $debug ; then debugger=" gdb --args" ; fi
191191 $debugger " $interpreter " " $kast " -1 " $output_text " " $@ " \
192192 || exit_status=" $? "
193- if [[ " $exit_status " != ' 0' ]]; then
193+ if [[ " $unparse " == ' true ' ]] && [[ " $ exit_status" != ' 0' ]]; then
194194 cat " $output_text " | " $0 " kast --backend " $backend " - pretty --input " $output_format " --sort GeneratedTopCell
195- exit " $exit_status "
196195 fi
196+ exit " $exit_status "
197197 ;;
198198
199199 * ) fatal " Bad backend for interpreter: '$backend '"
@@ -208,17 +208,17 @@ run_command="$1" ; shift
208208
209209if [[ " $run_command " == ' help' ]] || [[ " $run_command " == ' --help' ]] ; then
210210 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>
222222
223223 $0 [help|--help|version|--version]
224224
265265backend=" llvm"
266266debug=false
267267dump=false
268+ unparse=true
268269[[ ! " $run_command " == ' prove' ]] || backend=' java'
269270[[ ! " $run_command " =~ klab* ]] || backend=' java'
270271[[ ! " $run_command " =~ web3* ]] || backend=' llvm'
271272while [[ $# -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
290281done
291282backend_dir=" $defn_dir /$backend "
292283[[ ! " $backend " == " ocaml" ]] || eval $( ${OPAM:- opam} config env)
0 commit comments