Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove Util.failwith #872

Merged
merged 2 commits into from
Oct 12, 2023
Merged

Remove Util.failwith #872

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1e9a1ec
Using specific exceptions to unsupported features and unifying use of…
Stevendeo Oct 12, 2023
97b701f
Poetry
Stevendeo Oct 12, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/bin/common/solving_loop.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -530,7 +530,7 @@ let main () =
| Simple name -> name
| _ ->
let loc = DStd.Loc.loc file_loc loc in
Util.failwith "%a: internal error: goal name should be simple"
Fmt.failwith "%a: internal error: goal name should be simple"
DStd.Loc.fmt loc
in
let contents =
Expand All @@ -539,7 +539,7 @@ let main () =
| `Solve ([], [t]) -> `Goal t
| _ ->
let loc = DStd.Loc.loc file_loc loc in
Util.failwith "%a: internal error: unknown statement"
Fmt.failwith "%a: internal error: unknown statement"
DStd.Loc.fmt loc
in
let stmt = { Typer_Pipe.id; contents; loc ; attrs } in
Expand Down
64 changes: 31 additions & 33 deletions src/lib/frontend/d_cnf.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,11 @@ module DT = DE.Ty
module Id = DStd.Id
module B = DStd.Builtin

let unsupported msg =
Format.kasprintf
(fun str -> Errors.(run_error (Unsupported_feature str)))
msg
Copy link
Collaborator

@Halbaroth Halbaroth Oct 12, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess we can use Fmt.kstr here :)? Besides we can move the function in Utils.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Errors depends on Util unfortunately, but I can use Fmt


module Shared = struct
(* Shared constants to avoid allocations*)

Expand All @@ -62,7 +67,7 @@ let get_basename = function
| DStd.Path.Local { name; }
| Absolute { name; path = []; } -> name
| Absolute { name; path; } ->
Util.failwith
Fmt.failwith
"Expected an empty path to the basename: \"%s\" but got: [%a]."
name (fun fmt l ->
match l with
Expand Down Expand Up @@ -91,7 +96,7 @@ module Cache = struct
match find_sy ind with
| Sy.Var v -> v
| sym ->
Util.failwith
Fmt.failwith
"Internal error: Expected to find a variable symbol,\
instead found (%a)"
Sy.print sym
Expand Down Expand Up @@ -477,7 +482,7 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty =
if update then
Cache.store_tyvl ~is_var tyvl;
aux ty
| _ -> Util.failwith "Unsupported Type %a" DE.Ty.print dty
| _ -> unsupported "Type %a" DE.Ty.print dty

and handle_ty_app ?(update = false) ty_c l =
(* Applies the substitutions in [tysubsts] to each encountered type
Expand Down Expand Up @@ -550,7 +555,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
let pty = dty_to_ty id_ty in
(pn, pty) :: acc
| _ ->
Util.failwith
Fmt.failwith
"Unexpected null label for some field of the record type %a"
DE.Ty.Const.print ty_c

Expand Down Expand Up @@ -647,7 +652,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
let pty = dty_to_ty id_ty in
(pn, pty) :: acc
| _ ->
Util.failwith
Fmt.failwith
"Unexpected null label for some field of the record type %a"
DE.Ty.Const.print ty_c
) [] dstrs
Expand Down Expand Up @@ -766,7 +771,7 @@ let handle_patt_var name (DE.{ term_descr; _ } as term) =
v, n, ty

| _ ->
Util.failwith
Fmt.failwith
"Expected a variable in a case match but got %a"
DE.Term.print term

Expand All @@ -791,7 +796,7 @@ let mk_pattern DE.{ term_descr; _ } =
| _ -> assert false
) [] dstrs
| _ ->
Util.failwith
Fmt.failwith
"Expected a constructor for an algebraic data type but got\
something else for the definition of: %a"
DE.Ty.Const.print adt
Expand Down Expand Up @@ -826,8 +831,7 @@ let mk_pattern DE.{ term_descr; _ } =
let arith_ty = function
| `Int -> Ty.Tint
| `Real -> Ty.Treal
| `Rat ->
Util.failwith "rationals are not currently supported"
| `Rat -> unsupported "rationals"

(* Parse a semantic bound [x `b` y] and returns a tuple [(sort, lb, ub)] where:

Expand All @@ -850,7 +854,7 @@ let parse_semantic_bound ?(loc = Loc.dummy) ~var b x y =
| B.Gt t -> `Gt, t
| B.Geq t -> `Ge, t
| _ ->
Util.failwith
Fmt.failwith
"%aInternal error: invalid semantic bound"
Loc.report loc
in
Expand All @@ -861,7 +865,7 @@ let parse_semantic_bound ?(loc = Loc.dummy) ~var b x y =
Sy.ValBnd (Numbers.Q.from_string s)
| Var v -> Sy.VarBnd (Cache.find_var v)
| _ ->
Util.failwith
Fmt.failwith
"%aInternal error: invalid semantic bound"
Loc.report loc
in
Expand Down Expand Up @@ -966,8 +970,7 @@ let rec mk_expr
let sy = Sy.Op (Sy.Constr (Hstring.make name)) in
E.mk_term sy [] ty

| _ ->
Util.failwith "Unsupported constant term %a" DE.Term.print term
| _ -> unsupported "Constant term %a" DE.Term.print term
end

| Var ({ id_ty; _ } as ty_v) ->
Expand Down Expand Up @@ -1015,13 +1018,13 @@ let rec mk_expr
in
E.mk_term sy [e] ty
| _ ->
Util.failwith
Fmt.failwith
"Adt Destructor error: Can't find %dth field of %dth \
case of the type %a."
field case DE.Ty.Const.print adt
end
| None | Some Abstract ->
Util.failwith
Fmt.failwith
"Can't find the adt %a to which the destructor %a belongs"
DE.Ty.Const.print adt DE.Term.print app_term
end
Expand Down Expand Up @@ -1069,7 +1072,7 @@ let rec mk_expr
| [] -> None
| [ var, value ] -> Some (var, value)
| _ ->
Util.failwith
Fmt.failwith
"%asemantic trigger should have at most one bound variable"
Loc.report loc
in
Expand All @@ -1088,7 +1091,7 @@ let rec mk_expr
match E.type_info t with
| Tbitv m ->
if m <= i then
Util.failwith
Fmt.failwith
"%alength of bitvector extraction exceeds the length\
of its argument."
Loc.report loc
Expand Down Expand Up @@ -1347,7 +1350,7 @@ let rec mk_expr
let l = List.map (fun t -> aux_mk_expr t) args in
E.mk_term (Sy.Op Sy.Record) l ty
| _ ->
Util.failwith
Fmt.failwith
"Constructor error: %a does not belong to a record nor an\
algebraic data type"
DE.Term.print app_term
Expand All @@ -1356,9 +1359,7 @@ let rec mk_expr
| B.Coercion, [ x ] ->
begin match DT.view (DE.Term.ty x), DT.view term_ty with
| `Int, `Real -> op Real_of_int
| _ ->
Util.failwith "Unsupported coercion: %a"
DE.Term.print term
| _ -> unsupported "coercion: %a" DE.Term.print term
end
| Float, _ -> op Float
| Integer_round, _ -> op Integer_round
Expand All @@ -1379,9 +1380,7 @@ let rec mk_expr
| Not_theory_constant, _ -> op Not_theory_constant
| Is_theory_constant, _ -> op Is_theory_constant
| Linear_dependency, _ -> op Linear_dependency

| _, _ ->
Util.failwith "Unsupported Application Term %a" DE.Term.print term
| _, _ -> unsupported "Application Term %a" DE.Term.print term
end

| Match (t, pats) ->
Expand Down Expand Up @@ -1494,8 +1493,7 @@ let rec mk_expr
end
in
mk name loc binders triggers qbody ~toplevel ~decl_kind

| _ -> Util.failwith "Unsupported Term %a" DE.Term.print term
| _ -> unsupported "Term %a" DE.Term.print term
in
match DStd.Tag.get root_tags DE.Tags.named with
| Some s ->
Expand All @@ -1509,7 +1507,7 @@ let rec mk_expr
match destruct_app t with
| Some (cst, args) -> cst, args
| None ->
Util.failwith
Fmt.failwith
"invalid semantic trigger: %a"
DE.Term.print t
in
Expand All @@ -1526,7 +1524,7 @@ let rec mk_expr
let e2 = aux_mk_expr y in
E.mk_term sy [e2] Ty.Tbool
| _ ->
Util.failwith
Fmt.failwith
"%aMaps_to: expected a variable but got: %a"
Loc.report loc DE.Term.print x
end
Expand Down Expand Up @@ -1570,12 +1568,12 @@ let rec mk_expr
in
E.mk_term (Sy.mk_in lb ub) [aux_mk_expr main_expr] Ty.Tbool
| _ ->
Util.failwith "%aInvalid semantic trigger: %a"
Fmt.failwith "%aInvalid semantic trigger: %a"
Loc.report loc DE.Term.print t
end

| _ ->
Util.failwith "%aInvalid semantic trigger: %a"
Fmt.failwith "%aInvalid semantic trigger: %a"
Loc.report loc DE.Term.print t

in aux_mk_expr ~toplevel dt
Expand Down Expand Up @@ -1867,7 +1865,7 @@ let make dloc_file acc stmt =
let name = match name.name with
| Simple name -> name
| _ ->
Util.failwith
Fmt.failwith
"Internal error: invalid theory extension: %a"
print name
in
Expand All @@ -1879,7 +1877,7 @@ let make dloc_file acc stmt =
Errors.typing_error (ThExtError name) aloc
end
| _ ->
Util.failwith
Fmt.failwith
"Internal error: invalid base theory name: %a"
print extends
in
Expand All @@ -1890,7 +1888,7 @@ let make dloc_file acc stmt =
| [] -> None
| [name, extends] -> Some (name, extends)
| _ ->
Util.failwith
Fmt.failwith
"%a: Internal error: multiple theories."
DStd.Loc.fmt dloc
in
Expand Down
2 changes: 1 addition & 1 deletion src/lib/reasoners/records.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -257,7 +257,7 @@ module Shostak (X : ALIEN) = struct
let record = is_mine (Record (flds, tyr)) in
record, (left_abs_xe2, record) :: acc
| ty ->
Util.failwith
Fmt.failwith
"Not a record type: `%a" Ty.print_full ty
in
let abs_access = normalize (Access (field, embed abs_right_xe, ty)) in
Expand Down
6 changes: 3 additions & 3 deletions src/lib/structures/expr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -704,12 +704,12 @@ let print_list fmt = print_list_sep "," fmt
let lit_view t =
let { f; xs; ty; _ } = t in
if ty != Ty.Tbool then
Util.failwith "Calling lit_view on a non boolean expression %a"
Fmt.failwith "Calling lit_view on a non boolean expression %a"
print t
else
match f with
| Sy.Form _ ->
Util.failwith "Calling lit_view on a formula %a" print t
Fmt.failwith "Calling lit_view on a formula %a" print t
| Sy.Lit lit ->
begin match lit, xs with
| (Sy.L_eq | Sy.L_neg_eq), ([] | [_]) -> assert false
Expand All @@ -726,7 +726,7 @@ let lit_view t =
let form_view t =
let { f; xs; bind; _ } = t in
if t.ty != Ty.Tbool then
Util.failwith "Term %a is not a formula" print t
Fmt.failwith "Term %a is not a formula" print t
else
match f, xs, bind with
| Sy.Form (Sy.F_Unit _), [a;b], _ -> Unit (a, b)
Expand Down
2 changes: 0 additions & 2 deletions src/lib/util/util.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,5 @@ let rec print_list_pp ~sep ~pp fmt = function
Format.fprintf fmt "%a %a" pp x sep ();
print_list_pp ~sep ~pp fmt l

let failwith msg = Format.kasprintf failwith msg

let internal_error msg =
Format.kasprintf (fun s -> raise (Internal_error s)) msg
2 changes: 0 additions & 2 deletions src/lib/util/util.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,4 @@ val print_list_pp:
pp:(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a list -> unit

val failwith: ('a, Format.formatter, unit, 'b) format4 -> 'a

val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a
Loading