Fix handling of embedded context through modules

Exceptions raised by the interpreter from within the native modules were not
handled correctly.
This commit is contained in:
Louis Gesbert 2023-12-07 15:09:18 +01:00
parent 509ce9788a
commit a988ad473b

View File

@ -537,7 +537,8 @@ and val_to_runtime :
| [] ->
let args = List.rev acc in
val_to_runtime eval_expr ctx tret
(eval_expr ctx (EApp { f = v; args }, m))
(try eval_expr ctx (EApp { f = v; args }, m)
with CatalaException EmptyError -> raise Runtime.EmptyError)
| targ :: targs ->
Obj.repr (fun x ->
curry (runtime_to_val eval_expr ctx m targ x :: acc) targs)