Nicer error message

This commit is contained in:
Denis Merigoux 2023-06-15 17:47:58 +02:00
parent ed2891c761
commit 3d3e735402
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3

View File

@ -147,7 +147,13 @@ let rec evaluate_operator
in
let err () =
Messages.raise_multispanned_error
([Some "Operator:", pos]
([
( Some
(Format.asprintf "Operator (value %a):"
(Print.operator ~debug:true)
op),
pos );
]
@ List.mapi
(fun i arg ->
( Some
@ -324,6 +330,13 @@ let rec evaluate_operator
ELit (LBool (o_eq_dat_dat x y))
| Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_eq_dur_dur x y))
| HandleDefault, _ ->
Messages.raise_internal_error
"The interpreter is trying to evaluate the \"handle_default\" operator, \
which is the leftover from the dcalc->lcalc compilation pass. This \
indicates that you are trying to interpret the lcalc without having \
activating --avoid_exceptions. This interpretation is not implemented, \
just try to interpret the dcalc (with \"Interpret\") instead."
| HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> (
let valid_exceptions =
ListLabels.filter exps ~f:(function
@ -331,7 +344,6 @@ let rec evaluate_operator
EnumConstructor.equal cons Expr.some_constr
| _ -> err ())
in
match valid_exceptions with
| [] -> (
match
@ -376,8 +388,7 @@ let rec evaluate_operator
| Lte_mon_mon | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat
| Gt_mon_mon | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat
| Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleDefault | HandleDefaultOpt
),
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleDefaultOpt ),
_ ) ->
err ()