This commit is contained in:
Denis Merigoux 2023-09-19 14:48:21 +02:00
parent 7bad9aa20e
commit ea838ed6af
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3

View File

@ -752,6 +752,11 @@ and partially_evaluate_expr_for_assertion_failure_message :
type d e. type d e.
decl_ctx -> ((d, e, yes) astk, 't) gexpr -> ((d, e, yes) astk, 't) gexpr = decl_ctx -> ((d, e, yes) astk, 't) gexpr -> ((d, e, yes) astk, 't) gexpr =
fun ctx e -> fun ctx e ->
(* Here we want to print an expression that explains why an assertion has
failed. Since assertions have type [bool] and are usually constructed with
comparisons and logical operators, we leave those unevaluated at the top of
the AST while evaluating everything below. This makes for a good error
message. *)
match Mark.remove e with match Mark.remove e with
| EApp { f = EOp ({ op = op_kind; _ } as op), m; args = [e1; e2] } | EApp { f = EOp ({ op = op_kind; _ } as op), m; args = [e1; e2] }
when match op_kind with when match op_kind with