Merge pull request #218 from AltGr/format-strings

Use format strings directly in debug/error/log functions
This commit is contained in:
Denis Merigoux 2022-03-08 15:00:56 +01:00 committed by GitHub
commit 5a186f8cfd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
27 changed files with 1050 additions and 1037 deletions

View File

@ -12,4 +12,4 @@
or implied. See the License for the specific language governing permissions and limitations under
the License. *)
let _ = Clerk_driver.main ()
let () = Clerk_driver.main ()

View File

@ -361,7 +361,7 @@ let collect_all_ninja_build (ninja : ninja) (tested_file : string) (reset_test_o
(string * ninja) option =
let expected_outputs = search_for_expected_outputs tested_file in
if List.length expected_outputs = 0 then (
Cli.debug_print (Format.asprintf "No expected outputs were found for test file %s" tested_file);
Cli.debug_print "No expected outputs were found for test file %s" tested_file;
None)
else
let ninja, test_names =
@ -472,7 +472,7 @@ let run_file (file : string) (catala_exe : string) (catala_opts : string) (scope
String.concat " "
(List.filter (fun s -> s <> "") [ catala_exe; catala_opts; "-s " ^ scope; "Interpret"; file ])
in
Cli.debug_print ("Running: " ^ command);
Cli.debug_print "Running: %s" command;
Sys.command command
(** {1 Driver} *)
@ -483,7 +483,7 @@ let get_catala_files_in_folder (dir : string) : string list =
let f_is_dir =
try Sys.is_directory f
with Sys_error e ->
Printf.sprintf "skipping %s" e |> Cli.warning_print;
Cli.warning_print "skipping %s" e;
false
in
if f_is_dir then
@ -630,24 +630,23 @@ let driver (files_or_folders : string list) (command : string) (catala_exe : str
List.iter
(fun f ->
f
|> Cli.print_with_style [ ANSITerminal.magenta ] "%s"
|> Printf.sprintf "No test case found for %s"
|> Cli.warning_print)
|> Cli.with_style [ ANSITerminal.magenta ] "%s"
|> Cli.warning_print "No test case found for %s")
ctx.all_failed_names;
if 0 = List.compare_lengths ctx.all_failed_names files_or_folders then return_ok
else
try
let out = open_out ninja_output in
Cli.debug_print ("writing " ^ ninja_output ^ "...");
Cli.debug_print "writing %s..." ninja_output;
Nj.format
(Format.formatter_of_out_channel out)
(add_root_test_build ninja ctx.all_file_names ctx.all_test_builds);
close_out out;
let ninja_cmd = "ninja test -f " ^ ninja_output in
Cli.debug_print ("executing '" ^ ninja_cmd ^ "'...");
Cli.debug_print "executing '%s'..." ninja_cmd;
Sys.command ninja_cmd
with Sys_error e ->
e |> Printf.sprintf "can not write in %s" |> Cli.error_print;
Cli.error_print "can not write in %s" e;
return_err)
| "run" -> (
match scope with
@ -662,7 +661,7 @@ let driver (files_or_folders : string list) (command : string) (catala_exe : str
Cli.error_print "Please provide a scope to run with the -s option";
1)
| _ ->
Cli.error_print (Format.asprintf "The command \"%s\" is unknown to clerk." command);
Cli.error_print "The command \"%s\" is unknown to clerk." command;
1
let main () =

View File

@ -33,11 +33,12 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
let apply_div_or_raise_err (div : unit -> A.expr) (op : A.operator Pos.marked) : A.expr =
try div ()
with Division_by_zero ->
Errors.raise_multispanned_error "division by zero at runtime"
Errors.raise_multispanned_error
[
(Some "The division operator:", Pos.get_position op);
(Some "The null denominator:", Pos.get_position (List.nth args 1));
]
"division by zero at runtime"
in
let get_binop_args_pos (args : (A.expr * Pos.t) list) : (string option * Pos.t) list =
[ (None, Pos.get_position (List.nth args 0)); (None, Pos.get_position (List.nth args 1)) ]
@ -47,9 +48,8 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
let apply_cmp_or_raise_err (cmp : unit -> A.expr) (args : (A.expr * Pos.t) list) : A.expr =
try cmp ()
with Runtime.UncomparableDurations ->
Errors.raise_multispanned_error
Errors.raise_multispanned_error (get_binop_args_pos args)
"Cannot compare together durations that cannot be converted to a precise number of days"
(get_binop_args_pos args)
in
Pos.same_pos_as
(match (Pos.unmark op, List.map Pos.unmark args) with
@ -93,9 +93,8 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
(fun _ ->
try A.ELit (LRat Runtime.(d1 /^ d2))
with Runtime.IndivisableDurations ->
Errors.raise_multispanned_error
"Cannot divide durations that cannot be converted to a precise number of days"
(get_binop_args_pos args))
Errors.raise_multispanned_error (get_binop_args_pos args)
"Cannot divide durations that cannot be converted to a precise number of days")
op
| A.Binop (A.Lt KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool Runtime.(i1 <! i2))
| A.Binop (A.Lte KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool Runtime.(i1 <=! i2))
@ -192,9 +191,9 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
| A.ELit (A.LBool b), _ -> b
| _ ->
Errors.raise_spanned_error
(Pos.get_position (List.nth args 0))
"This predicate evaluated to something else than a boolean (should not happen \
if the term was well-typed)"
(Pos.get_position (List.nth args 0)))
if the term was well-typed)")
es)
| A.Binop _, ([ ELit LEmptyError; _ ] | [ _; ELit LEmptyError ]) -> A.ELit LEmptyError
| A.Unop (A.Minus KInt), [ ELit (LInt i) ] -> A.ELit (LInt Runtime.(integer_of_int 0 -! i))
@ -212,48 +211,44 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
if !Cli.trace_flag then (
match entry with
| VarDef _ ->
Cli.log_print
(Format.asprintf "%*s%a %a: %s" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos
(match e' with
(* | Ast.EAbs _ -> Cli.print_with_style [ ANSITerminal.green ] "<function>" *)
| _ ->
let expr_str =
Format.asprintf "%a" (Print.format_expr ctx ~debug:false) (e', Pos.no_pos)
in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
expr_str
in
Cli.print_with_style [ ANSITerminal.green ] "%s" expr_str))
(* TODO: this usage of Format is broken, Formatting requires that all is formatted in
one pass, without going through intermediate "%s" *)
Cli.log_format "%*s%a %a: %s" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos
(match e' with
(* | Ast.EAbs _ -> Cli.with_style [ ANSITerminal.green ] "<function>" *)
| _ ->
let expr_str =
Format.asprintf "%a" (Print.format_expr ctx ~debug:false) (e', Pos.no_pos)
in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
expr_str
in
Cli.with_style [ ANSITerminal.green ] "%s" expr_str)
| PosRecordIfTrueBool -> (
let pos = Pos.get_position op in
match (pos <> Pos.no_pos, e') with
| true, ELit (LBool true) ->
Cli.log_print
(Format.asprintf "%*s%a%s:\n%s" (!log_indent * 2) "" Print.format_log_entry
entry
(Cli.print_with_style [ ANSITerminal.green ] "Definition applied")
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
Format.asprintf "%*s" (!log_indent * 2) "")))
Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) "" Print.format_log_entry entry
(Cli.with_style [ ANSITerminal.green ] "Definition applied")
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
Format.asprintf "%*s" (!log_indent * 2) ""))
| _ -> ())
| BeginCall ->
Cli.log_print
(Format.asprintf "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos);
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos;
log_indent := !log_indent + 1
| EndCall ->
log_indent := !log_indent - 1;
Cli.log_print
(Format.asprintf "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos))
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos)
else ();
e'
| A.Unop _, [ ELit LEmptyError ] -> A.ELit LEmptyError
| _ ->
Errors.raise_multispanned_error
"Operator applied to the wrong arguments\n(should nothappen if the term was well-typed)"
([ (Some "Operator:", Pos.get_position op) ]
@ List.mapi
(fun i arg ->
@ -262,15 +257,15 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
(Print.format_expr ctx ~debug:true)
arg),
Pos.get_position arg ))
args))
args)
"Operator applied to the wrong arguments\n(should not happen if the term was well-typed)")
op
and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.marked =
match Pos.unmark e with
| EVar _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"free variable found at evaluation (should not happen if term was well-typed"
(Pos.get_position e)
| EApp (e1, args) -> (
let e1 = evaluate_expr ctx e1 in
let args = List.map (evaluate_expr ctx) args in
@ -279,18 +274,16 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
if Bindlib.mbinder_arity binder = List.length args then
evaluate_expr ctx (Bindlib.msubst binder (Array.of_list (List.map Pos.unmark args)))
else
Errors.raise_spanned_error
(Format.asprintf "wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder) (List.length args))
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"wrong function call, expected %d arguments, got %d" (Bindlib.mbinder_arity binder)
(List.length args)
| EOp op ->
Pos.same_pos_as (Pos.unmark (evaluate_operator ctx (Pos.same_pos_as op e1) args)) e
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"function has not been reduced to a lambda at evaluation (should not happen if the \
term was well-typed"
(Pos.get_position e))
term was well-typed")
| EAbs _ | ELit _ | EOp _ -> e (* these are values *)
| ETuple (es, s) ->
let new_es = List.map (evaluate_expr ctx) es in
@ -305,27 +298,23 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
| Some s, Some s' when s = s' -> ()
| _ ->
Errors.raise_multispanned_error
[ (None, Pos.get_position e); (None, Pos.get_position e1) ]
"Error during tuple access: not the same structs (should not happen if the term \
was well-typed)"
[ (None, Pos.get_position e); (None, Pos.get_position e1) ]);
was well-typed)");
match List.nth_opt es n with
| Some e' -> e'
| None ->
Errors.raise_spanned_error
(Format.asprintf
"The tuple has %d components but the %i-th element was requested (should not \
happen if the term was well-type)"
(List.length es) n)
(Pos.get_position e1))
Errors.raise_spanned_error (Pos.get_position e1)
"The tuple has %d components but the %i-th element was requested (should not \
happen if the term was well-type)"
(List.length es) n)
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"The expression %a should be a tuple with %d components but is not (should not \
happen if the term was well-typed)"
(Print.format_expr ctx ~debug:true)
e n)
(Pos.get_position e1))
Errors.raise_spanned_error (Pos.get_position e1)
"The expression %a should be a tuple with %d components but is not (should not happen \
if the term was well-typed)"
(Print.format_expr ctx ~debug:true)
e n)
| EInj (e1, n, en, ts) ->
let e1' = evaluate_expr ctx e1 in
if is_empty_error e1' then Pos.same_pos_as (A.ELit LEmptyError) e
@ -336,25 +325,23 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
| A.EInj (e1, n, e_name', _) ->
if e_name <> e_name' then
Errors.raise_multispanned_error
[ (None, Pos.get_position e); (None, Pos.get_position e1) ]
"Error during match: two different enums found (should not happend if the term was \
well-typed)"
[ (None, Pos.get_position e); (None, Pos.get_position e1) ];
well-typed)";
let es_n =
match List.nth_opt es n with
| Some es_n -> es_n
| None ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"sum type index error (should not happend if the term was well-typed)"
(Pos.get_position e)
in
let new_e = Pos.same_pos_as (A.EApp (es_n, [ e1 ])) e in
evaluate_expr ctx new_e
| A.ELit A.LEmptyError -> Pos.same_pos_as (A.ELit A.LEmptyError) e
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e1)
"Expected a term having a sum type as an argument to a match (should not happend if \
the term was well-typed"
(Pos.get_position e1))
the term was well-typed")
| EDefault (exceptions, just, cons) -> (
let exceptions = List.map (evaluate_expr ctx) exceptions in
let empty_count = List.length (List.filter is_empty_error exceptions) in
@ -366,29 +353,27 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
| ELit (LBool true) -> evaluate_expr ctx cons
| ELit (LBool false) -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"Default justification has not been reduced to a boolean at evaluation (should not \
happen if the term was well-typed"
(Pos.get_position e))
happen if the term was well-typed")
| 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions
| _ ->
Errors.raise_multispanned_error
"There is a conflict between multiple validd consequences for assigning the same \
variable."
(List.map
(fun except ->
(Some "This consequence has a valid justification:", Pos.get_position except))
(List.filter (fun sub -> not (is_empty_error sub)) exceptions)))
(List.filter (fun sub -> not (is_empty_error sub)) exceptions))
"There is a conflict between multiple validd consequences for assigning the same \
variable.")
| EIfThenElse (cond, et, ef) -> (
match Pos.unmark (evaluate_expr ctx cond) with
| ELit (LBool true) -> evaluate_expr ctx et
| ELit (LBool false) -> evaluate_expr ctx ef
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position cond)
"Expected a boolean literal for the result of this condition (should not happen if the \
term was well-typed)"
(Pos.get_position cond))
term was well-typed)")
| EArray es ->
let new_es = List.map (evaluate_expr ctx) es in
if List.exists is_empty_error new_es then Pos.same_pos_as (A.ELit LEmptyError) e
@ -396,10 +381,9 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
| ErrorOnEmpty e' ->
let e' = evaluate_expr ctx e' in
if Pos.unmark e' = A.ELit LEmptyError then
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"This variable evaluated to an empty term (no rule that defined it applied in this \
situation)"
(Pos.get_position e)
else e'
| EAssert e' -> (
match Pos.unmark (evaluate_expr ctx e') with
@ -407,21 +391,17 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
| ELit (LBool false) -> (
match Pos.unmark e' with
| EApp ((Ast.EOp (Binop op), pos_op), [ ((ELit _, _) as e1); ((ELit _, _) as e2) ]) ->
Errors.raise_spanned_error
(Format.asprintf "Assertion failed: %a %a %a"
(Print.format_expr ctx ~debug:false)
e1 Print.format_binop (op, pos_op)
(Print.format_expr ctx ~debug:false)
e2)
(Pos.get_position e')
| _ ->
Errors.raise_spanned_error (Format.asprintf "Assertion failed") (Pos.get_position e'))
Errors.raise_spanned_error (Pos.get_position e') "Assertion failed: %a %a %a"
(Print.format_expr ctx ~debug:false)
e1 Print.format_binop (op, pos_op)
(Print.format_expr ctx ~debug:false)
e2
| _ -> Errors.raise_spanned_error (Pos.get_position e') "Assertion failed")
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e')
"Expected a boolean literal for the result of this assertion (should not happen if the \
term was well-typed)"
(Pos.get_position e'))
term was well-typed)")
(** {1 API} *)
@ -442,11 +422,9 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
in
List.map2 (fun arg var -> (var, arg)) args s_out_fields
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"The interpretation of a program should always yield a struct corresponding to the \
scope variables"
(Pos.get_position e))
scope variables")
| _ ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position e)
"The interpreter can only interpret terms starting with functions having thunked arguments"
(Pos.get_position e)

View File

@ -156,10 +156,10 @@ let format_ternop (fmt : Format.formatter) (op : ternop Pos.marked) : unit =
let format_log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
Format.fprintf fmt "@<2>%s"
(match entry with
| VarDef _ -> Utils.Cli.print_with_style [ ANSITerminal.blue ] ""
| BeginCall -> Utils.Cli.print_with_style [ ANSITerminal.yellow ] ""
| EndCall -> Utils.Cli.print_with_style [ ANSITerminal.yellow ] ""
| PosRecordIfTrueBool -> Utils.Cli.print_with_style [ ANSITerminal.green ] "")
| VarDef _ -> Utils.Cli.with_style [ ANSITerminal.blue ] ""
| BeginCall -> Utils.Cli.with_style [ ANSITerminal.yellow ] ""
| EndCall -> Utils.Cli.with_style [ ANSITerminal.yellow ] ""
| PosRecordIfTrueBool -> Utils.Cli.with_style [ ANSITerminal.green ] "")
let format_unop (fmt : Format.formatter) (op : unop Pos.marked) : unit =
Format.fprintf fmt "%s"

View File

@ -78,27 +78,27 @@ let rec unify (ctx : Ast.decl_ctx) (t1 : typ Pos.marked UnionFind.elem)
(* TODO: if we get weird error messages, then it means that we should use the persistent version
of the union-find data structure. *)
let t1_s =
Cli.print_with_style [ ANSITerminal.yellow ] "%s"
Cli.with_style [ ANSITerminal.yellow ] "%s"
(Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
(Format.asprintf "%a" (format_typ ctx) t1))
in
let t2_s =
Cli.print_with_style [ ANSITerminal.yellow ] "%s"
Cli.with_style [ ANSITerminal.yellow ] "%s"
(Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
(Format.asprintf "%a" (format_typ ctx) t2))
in
Errors.raise_multispanned_error
(Format.asprintf "Error during typechecking, incompatible types:\n%a %s\n%a %s"
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
"-->" t1_s
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
"-->" t2_s)
[
(Some (Format.asprintf "Type %s coming from expression:" t1_s), t1_pos);
(Some (Format.asprintf "Type %s coming from expression:" t2_s), t2_pos);
]
"Error during typechecking, incompatible types:\n%a %s\n%a %s"
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
"-->" t1_s
(Cli.format_with_style [ ANSITerminal.blue; ANSITerminal.Bold ])
"-->" t2_s
in
let repr =
match (t1_repr, t2_repr) with
@ -180,7 +180,7 @@ let op_type (op : A.operator Pos.marked) : typ Pos.marked UnionFind.elem =
| A.Unop A.GetYear -> arr dat it
| A.Unop A.IntToRat -> arr it rt
| Binop (Mult (KDate | KDuration)) | Binop (Div KDate) | Unop (Minus KDate) ->
Errors.raise_spanned_error "This operator is not available!" pos
Errors.raise_spanned_error pos "This operator is not available!"
let rec ast_to_typ (ty : A.typ) : typ =
match ty with
@ -223,8 +223,8 @@ let rec typecheck_expr_bottom_up (ctx : Ast.decl_ctx) (env : env) (e : A.expr Po
match A.VarMap.find_opt (Pos.unmark v) env with
| Some t -> t
| None ->
Errors.raise_spanned_error "Variable not found in the current context"
(Pos.get_position e))
Errors.raise_spanned_error (Pos.get_position e)
"Variable not found in the current context")
| ELit (LBool _) -> UnionFind.make (Pos.same_pos_as (TLit TBool) e)
| ELit (LInt _) -> UnionFind.make (Pos.same_pos_as (TLit TInt) e)
| ELit (LRat _) -> UnionFind.make (Pos.same_pos_as (TLit TRat) e)
@ -244,22 +244,18 @@ let rec typecheck_expr_bottom_up (ctx : Ast.decl_ctx) (env : env) (e : A.expr Po
match List.nth_opt typs n with
| Some t' -> t'
| None ->
Errors.raise_spanned_error
(Format.asprintf
"Expression should have a tuple type with at least %d elements but only has %d" n
(List.length typs))
(Pos.get_position e1))
Errors.raise_spanned_error (Pos.get_position e1)
"Expression should have a tuple type with at least %d elements but only has %d" n
(List.length typs))
| EInj (e1, n, e_name, ts) ->
let ts = List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts in
let ts_n =
match List.nth_opt ts n with
| Some ts_n -> ts_n
| None ->
Errors.raise_spanned_error
(Format.asprintf
"Expression should have a sum type with at least %d cases but only has %d" n
(List.length ts))
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"Expression should have a sum type with at least %d cases but only has %d" n
(List.length ts)
in
typecheck_expr_top_down ctx env e1 ts_n;
UnionFind.make (Pos.same_pos_as (TEnum (ts, e_name)) e)
@ -293,10 +289,9 @@ let rec typecheck_expr_bottom_up (ctx : Ast.decl_ctx) (env : env) (e : A.expr Po
xstaus
(typecheck_expr_bottom_up ctx env body)
else
Errors.raise_spanned_error
(Format.asprintf "function has %d variables but was supplied %d types"
(Array.length xs) (List.length taus))
pos_binder
Errors.raise_spanned_error pos_binder
"function has %d variables but was supplied %d types" (Array.length xs)
(List.length taus)
| EApp (e1, args) ->
let t_args = List.map (typecheck_expr_bottom_up ctx env) args in
let t_ret = UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e) in
@ -352,8 +347,8 @@ and typecheck_expr_top_down (ctx : Ast.decl_ctx) (env : env) (e : A.expr Pos.mar
match A.VarMap.find_opt (Pos.unmark v) env with
| Some tau' -> ignore (unify ctx tau tau')
| None ->
Errors.raise_spanned_error "Variable not found in the current context"
(Pos.get_position e))
Errors.raise_spanned_error (Pos.get_position e)
"Variable not found in the current context")
| ELit (LBool _) -> unify ctx tau (UnionFind.make (Pos.same_pos_as (TLit TBool) e))
| ELit (LInt _) -> unify ctx tau (UnionFind.make (Pos.same_pos_as (TLit TInt) e))
| ELit (LRat _) -> unify ctx tau (UnionFind.make (Pos.same_pos_as (TLit TRat) e))
@ -374,22 +369,18 @@ and typecheck_expr_top_down (ctx : Ast.decl_ctx) (env : env) (e : A.expr Pos.mar
match List.nth_opt typs n with
| Some t1n -> unify ctx t1n tau
| None ->
Errors.raise_spanned_error
(Format.asprintf
"Expression should have a tuple type with at least %d elements but only has %d" n
(List.length typs))
(Pos.get_position e1))
Errors.raise_spanned_error (Pos.get_position e1)
"Expression should have a tuple type with at least %d elements but only has %d" n
(List.length typs))
| EInj (e1, n, e_name, ts) ->
let ts = List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts in
let ts_n =
match List.nth_opt ts n with
| Some ts_n -> ts_n
| None ->
Errors.raise_spanned_error
(Format.asprintf
"Expression should have a sum type with at least %d cases but only has %d" n
(List.length ts))
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"Expression should have a sum type with at least %d cases but only has %d" n
(List.length ts)
in
typecheck_expr_top_down ctx env e1 ts_n;
unify ctx (UnionFind.make (Pos.same_pos_as (TEnum (ts, e_name)) e)) tau
@ -424,10 +415,9 @@ and typecheck_expr_top_down (ctx : Ast.decl_ctx) (env : env) (e : A.expr Pos.mar
in
unify ctx t_func tau
else
Errors.raise_spanned_error
(Format.asprintf "function has %d variables but was supplied %d types" (Array.length xs)
(List.length t_args))
pos_binder
Errors.raise_spanned_error pos_binder
"function has %d variables but was supplied %d types" (Array.length xs)
(List.length t_args)
| EApp (e1, args) ->
let t_args = List.map (typecheck_expr_bottom_up ctx env) args in
let te1 = typecheck_expr_bottom_up ctx env e1 in

View File

@ -89,38 +89,40 @@ let check_for_cycle (scope : Ast.scope) (g : ScopeDependencies.t) : unit =
let sccs = SCC.scc_list g in
if List.length sccs < ScopeDependencies.nb_vertex g then
let scc = List.find (fun scc -> List.length scc > 1) sccs in
Errors.raise_multispanned_error
(Format.asprintf "Cyclic dependency detected between variables of scope %a!"
Scopelang.Ast.ScopeName.format_t scope.scope_uid)
(List.flatten
(List.map
(fun v ->
let var_str, var_info =
match v with
| Vertex.Var (v, None) ->
(Format.asprintf "%a" Ast.ScopeVar.format_t v, Ast.ScopeVar.get_info v)
| Vertex.Var (v, Some sv) ->
( Format.asprintf "%a.%a" Ast.ScopeVar.format_t v Ast.StateName.format_t sv,
Ast.StateName.get_info sv )
| Vertex.SubScope v ->
( Format.asprintf "%a" Scopelang.Ast.SubScopeName.format_t v,
Scopelang.Ast.SubScopeName.get_info v )
in
let succs = ScopeDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str =
match succ with
| Vertex.Var (v, None) -> Format.asprintf "%a" Ast.ScopeVar.format_t v
| Vertex.Var (v, Some sv) ->
Format.asprintf "%a.%a" Ast.ScopeVar.format_t v Ast.StateName.format_t sv
| Vertex.SubScope v -> Format.asprintf "%a" Scopelang.Ast.SubScopeName.format_t v
in
[
(Some ("Cycle variable " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle variable " ^ succ_str ^ ":"),
edge_pos );
])
scc))
let spans =
List.flatten
(List.map
(fun v ->
let var_str, var_info =
match v with
| Vertex.Var (v, None) ->
(Format.asprintf "%a" Ast.ScopeVar.format_t v, Ast.ScopeVar.get_info v)
| Vertex.Var (v, Some sv) ->
( Format.asprintf "%a.%a" Ast.ScopeVar.format_t v Ast.StateName.format_t sv,
Ast.StateName.get_info sv )
| Vertex.SubScope v ->
( Format.asprintf "%a" Scopelang.Ast.SubScopeName.format_t v,
Scopelang.Ast.SubScopeName.get_info v )
in
let succs = ScopeDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str =
match succ with
| Vertex.Var (v, None) -> Format.asprintf "%a" Ast.ScopeVar.format_t v
| Vertex.Var (v, Some sv) ->
Format.asprintf "%a.%a" Ast.ScopeVar.format_t v Ast.StateName.format_t sv
| Vertex.SubScope v -> Format.asprintf "%a" Scopelang.Ast.SubScopeName.format_t v
in
[
(Some ("Cycle variable " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle variable " ^ succ_str ^ ":"),
edge_pos );
])
scc)
in
Errors.raise_multispanned_error spans
"Cyclic dependency detected between variables of scope %a!" Scopelang.Ast.ScopeName.format_t
scope.scope_uid
(** Builds the dependency graph of a particular scope *)
let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
@ -155,12 +157,10 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
(* simple case *)
if v_used = v_defined && s_used = s_defined then
(* variable definitions cannot be recursive *)
Errors.raise_spanned_error
(Format.asprintf
"The variable %a is used in one of its definitions, but recursion is \
forbidden in Catala"
Ast.ScopeDef.format_t def_key)
fv_def_pos
Errors.raise_spanned_error fv_def_pos
"The variable %a is used in one of its definitions, but recursion is forbidden \
in Catala"
Ast.ScopeDef.format_t def_key
else
let edge =
ScopeDependencies.E.create
@ -181,12 +181,10 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
(* here we are defining the input of a scope with the output of another subscope *)
if used = defined then
(* subscopes are not recursive functions *)
Errors.raise_spanned_error
(Format.asprintf
"The subscope %a is used when defining one of its inputs, but recursion is \
forbidden in Catala"
Scopelang.Ast.SubScopeName.format_t defined)
fv_def_pos
Errors.raise_spanned_error fv_def_pos
"The subscope %a is used when defining one of its inputs, but recursion is \
forbidden in Catala"
Scopelang.Ast.SubScopeName.format_t defined
else
let edge =
ScopeDependencies.E.create (Vertex.SubScope used) fv_def_pos
@ -246,21 +244,23 @@ let build_exceptions_graph (def : Ast.rule Ast.RuleMap.t) (def_info : Ast.ScopeD
if Ast.RuleSet.equal rule_set1 rule_set2 then ()
else if Ast.RuleSet.disjoint rule_set1 rule_set2 then ()
else
Errors.raise_multispanned_error
"Definitions or rules grouped by different labels overlap, whereas these groups \
shoule be disjoint"
(List.of_seq
(Seq.map
(fun rule ->
( Some "Rule or definition from the first group:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleSet.to_seq rule_set1))
let spans =
List.of_seq
(Seq.map
(fun rule ->
( Some "Rule or definition from the first group:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleSet.to_seq rule_set1))
@ List.of_seq
(Seq.map
(fun rule ->
( Some "Rule or definition from the second group:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleSet.to_seq rule_set2))))
(Ast.RuleSet.to_seq rule_set2))
in
Errors.raise_multispanned_error spans
"Definitions or rules grouped by different labels overlap, whereas these groups \
shoule be disjoint")
all_rule_sets_pointed_to_by_exceptions)
all_rule_sets_pointed_to_by_exceptions;
(* Then we add the exception graph vertices by taking all those sets of rules pointed to by
@ -292,7 +292,7 @@ let build_exceptions_graph (def : Ast.rule Ast.RuleMap.t) (def_info : Ast.ScopeD
if Ast.RuleSet.is_empty exception_to_ruleset then g (* we don't add an edge*)
else if ExceptionsDependencies.mem_vertex g exception_to_ruleset then
if exception_to_ruleset = Ast.RuleSet.singleton rule_name then
Errors.raise_spanned_error "Cannot define rule as an exception to itself" pos
Errors.raise_spanned_error pos "Cannot define rule as an exception to itself"
else
let edge =
ExceptionsDependencies.E.create (Ast.RuleSet.singleton rule_name) pos
@ -300,12 +300,10 @@ let build_exceptions_graph (def : Ast.rule Ast.RuleMap.t) (def_info : Ast.ScopeD
in
ExceptionsDependencies.add_edge_e g edge
else
Errors.raise_spanned_error
(Format.asprintf
"This rule has been declared as an exception to an incorrect label: this label is \
not attached to a definition of \"%a\""
Ast.ScopeDef.format_t def_info)
pos)
Errors.raise_spanned_error pos
"This rule has been declared as an exception to an incorrect label: this label is not \
attached to a definition of \"%a\""
Ast.ScopeDef.format_t def_info)
def g
in
g
@ -316,25 +314,26 @@ let check_for_exception_cycle (g : ExceptionsDependencies.t) : unit =
let sccs = ExceptionsSCC.scc_list g in
if List.length sccs < ExceptionsDependencies.nb_vertex g then
let scc = List.find (fun scc -> List.length scc > 1) sccs in
Errors.raise_multispanned_error
(Format.asprintf "Cyclic dependency detected between exceptions!")
(List.flatten
(List.map
(fun (vs : Ast.RuleSet.t) ->
let v = Ast.RuleSet.choose vs in
let var_str, var_info =
(Format.asprintf "%a" Ast.RuleName.format_t v, Ast.RuleName.get_info v)
in
let succs = ExceptionsDependencies.succ_e g vs in
let _, edge_pos, _ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
[
( Some
("Cyclic exception for definition of variable \"" ^ var_str
^ "\", declared here:"),
Pos.get_position var_info );
( Some
("Used here in the definition of another cyclic exception for defining \""
^ var_str ^ "\":"),
edge_pos );
])
scc))
let spans =
List.flatten
(List.map
(fun (vs : Ast.RuleSet.t) ->
let v = Ast.RuleSet.choose vs in
let var_str, var_info =
(Format.asprintf "%a" Ast.RuleName.format_t v, Ast.RuleName.get_info v)
in
let succs = ExceptionsDependencies.succ_e g vs in
let _, edge_pos, _ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
[
( Some
("Cyclic exception for definition of variable \"" ^ var_str
^ "\", declared here:"),
Pos.get_position var_info );
( Some
("Used here in the definition of another cyclic exception for defining \""
^ var_str ^ "\":"),
edge_pos );
])
scc)
in
Errors.raise_multispanned_error spans "Cyclic dependency detected between exceptions!"

View File

@ -268,25 +268,24 @@ let translate_def (ctx : ctx) (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.Ru
match Pos.unmark typ with
| Scopelang.Ast.TArrow (t_param, _) -> Some t_param
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"The definitions of %a are function but its type, %a, is not a function type"
Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ)
(Pos.get_position typ)
Errors.raise_spanned_error (Pos.get_position typ)
"The definitions of %a are function but its type, %a, is not a function type"
Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ
else if (not is_def_func) && all_rules_not_func then None
else
Errors.raise_multispanned_error
"some definitions of the same variable are functions while others aren't"
(List.map
(fun (_, r) ->
( Some "This definition is a function:",
Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
(Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def))
let spans =
List.map
(fun (_, r) ->
(Some "This definition is a function:", Pos.get_position (Bindlib.unbox r.Ast.rule_cons)))
(Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def))
@ List.map
(fun (_, r) ->
( Some "This definition is not a function:",
Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
(Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def)))
(Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def))
in
Errors.raise_multispanned_error spans
"some definitions of the same variable are functions while others aren't"
in
let top_list = def_map_to_tree def_info def in
let top_value =
@ -350,13 +349,13 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
| OnlyInput when not (Ast.RuleMap.is_empty var_def) ->
(* If the variable is tagged as input, then it shall not be redefined. *)
Errors.raise_multispanned_error
"It is impossible to give a definition to a scope variable tagged as input."
((Some "Incriminated variable:", Pos.get_position (Ast.ScopeVar.get_info var))
:: List.map
(fun (rule, _) ->
( Some "Incriminated variable definition:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleMap.bindings var_def))
"It is impossible to give a definition to a scope variable tagged as input."
| OnlyInput -> [] (* we do not provide any definition for an input-only variable *)
| _ ->
let expr_def =
@ -417,8 +416,6 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
(match Pos.unmark scope_def.Ast.scope_def_io.io_input with
| Scopelang.Ast.NoInput ->
Errors.raise_multispanned_error
"It is impossible to give a definition to a subscope variable not \
tagged as input or context."
((Some "Incriminated subscope:", Ast.ScopeDef.get_position def_key)
:: ( Some "Incriminated variable:",
Pos.get_position (Ast.ScopeVar.get_info sub_scope_var) )
@ -427,17 +424,19 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
( Some "Incriminated subscope variable definition:",
Pos.get_position (Ast.RuleName.get_info rule) ))
(Ast.RuleMap.bindings def))
"It is impossible to give a definition to a subscope variable not \
tagged as input or context."
| OnlyInput when Ast.RuleMap.is_empty def && not is_cond ->
(* If the subscope variable is tagged as input, then it shall be
defined. *)
Errors.raise_multispanned_error
"This subscope variable is a mandatory input but no definition was \
provided."
[
(Some "Incriminated subscope:", Ast.ScopeDef.get_position def_key);
( Some "Incriminated variable:",
Pos.get_position (Ast.ScopeVar.get_info sub_scope_var) );
]
"This subscope variable is a mandatory input but no definition was \
provided."
| _ -> ());
(* Now that all is good, we can proceed with translating this redefinition
to a proper Scopelang term. *)

View File

@ -49,17 +49,15 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
let ext = Filename.extension !filename in
if ext = "" then
Errors.raise_error
(Printf.sprintf
"No file extension found for the file '%s'. (Try to add one or to specify the -l \
flag)"
!filename);
"No file extension found for the file '%s'. (Try to add one or to specify the -l \
flag)"
!filename;
try List.assoc ext extensions with Not_found -> ext)
in
let language =
try List.assoc l languages
with Not_found ->
Errors.raise_error
(Printf.sprintf "The selected language (%s) is not supported by Catala" l)
Errors.raise_error "The selected language (%s) is not supported by Catala" l
in
Cli.locale_lang := language;
let backend =
@ -76,9 +74,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
else if backend = "typecheck" then Cli.Typecheck
else if backend = "lcalc" then Cli.Lcalc
else if backend = "scalc" then Cli.Scalc
else
Errors.raise_error
(Printf.sprintf "The selected backend (%s) is not supported by Catala" backend)
else Errors.raise_error "The selected backend (%s) is not supported by Catala" backend
in
let prgm = Surface.Parser_driver.parse_top_level_file source_file language in
let prgm = Surface.Fill_positions.fill_pos_with_legislative_info prgm in
@ -96,7 +92,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
| Some f -> f
| None -> Filename.remove_extension source_file ^ ".d"
in
Cli.debug_print (Format.asprintf "Writing list of dependencies to %s..." output_file);
Cli.debug_print "Writing list of dependencies to %s..." output_file;
let oc = open_out output_file in
Printf.fprintf oc "%s:\\\n%s\n%s:"
(String.concat "\\\n"
@ -115,12 +111,11 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
Errors.raise_error
"The literate programming backends do not work if the input is not a file"
in
Cli.debug_print
(Printf.sprintf "Weaving literate program into %s"
(match backend with
| Cli.Latex -> "LaTeX"
| Cli.Html -> "HTML"
| _ -> assert false (* should not happen *)));
Cli.debug_print "Weaving literate program into %s"
(match backend with
| Cli.Latex -> "LaTeX"
| Cli.Html -> "HTML"
| _ -> assert false (* should not happen *));
let output_file =
match output_file with
| Some f -> f
@ -138,7 +133,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
| _ -> assert false
(* should not happen *)
in
Cli.debug_print (Printf.sprintf "Writing to %s" output_file);
Cli.debug_print "Writing to %s" output_file;
let fmt = Format.formatter_of_out_channel oc in
if wrap_weaved_output then
match backend with
@ -161,13 +156,10 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
| None, _ ->
snd
(try Desugared.Ast.IdentMap.choose ctxt.scope_idmap
with Not_found ->
Errors.raise_error (Printf.sprintf "There isn't any scope inside the program."))
with Not_found -> Errors.raise_error "There isn't any scope inside the program.")
| Some name, _ -> (
match Desugared.Ast.IdentMap.find_opt name ctxt.scope_idmap with
| None ->
Errors.raise_error
(Printf.sprintf "There is no scope \"%s\" inside the program." name)
| None -> Errors.raise_error "There is no scope \"%s\" inside the program." name
| Some uid -> uid)
in
Cli.debug_print "Desugaring...";
@ -244,15 +236,13 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
List.sort (fun ((v1, _), _) ((v2, _), _) -> String.compare v1 v2) results
in
Cli.debug_print "End of interpretation";
Cli.result_print
(Format.asprintf "Computation successful!%s"
(if List.length results > 0 then " Results:" else ""));
Cli.result_print "Computation successful!%s"
(if List.length results > 0 then " Results:" else "");
List.iter
(fun ((var, _), result) ->
Cli.result_print
(Format.asprintf "@[<hov 2>%s@ =@ %a@]" var
(Dcalc.Print.format_expr prgm.decl_ctx)
result))
Cli.result_format "@[<hov 2>%s@ =@ %a@]" var
(Dcalc.Print.format_expr prgm.decl_ctx)
result)
results;
0
| Cli.OCaml | Cli.Python | Cli.Lcalc | Cli.Scalc ->
@ -306,7 +296,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(match backend with
| Cli.OCaml ->
let output_file = new_output_file ".ml" in
Cli.debug_print (Printf.sprintf "Writing to %s..." output_file);
Cli.debug_print "Writing to %s..." output_file;
let oc = open_out output_file in
let fmt = Format.formatter_of_out_channel oc in
Cli.debug_print "Compiling program into OCaml...";
@ -342,7 +332,7 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
end;
let output_file = new_output_file ".py" in
Cli.debug_print "Compiling program into Python...";
Cli.debug_print (Printf.sprintf "Writing to %s..." output_file);
Cli.debug_print "Writing to %s..." output_file;
let oc = open_out output_file in
let fmt = Format.formatter_of_out_channel oc in
Scalc.To_python.format_program fmt prgm type_ordering;
@ -353,10 +343,10 @@ let driver (source_file : Pos.input_file) (debug : bool) (unstyled : bool)
(* should not happen *))
with
| Errors.StructuredError (msg, pos) ->
Cli.error_print (Errors.print_structured_error msg pos);
Cli.error_print "%s" (Errors.print_structured_error msg pos);
-1
| Sys_error msg ->
Cli.error_print ("System error: " ^ msg);
Cli.error_print "System error: %s" msg;
-1
let main () =

View File

@ -69,12 +69,10 @@ let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
pp_ctx ctx |> Cli.debug_print in *)
try D.VarMap.find n ctx.vars
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf
"Internal Error: Variable %a was not found in the current environment. Additional \
informations : %s."
Dcalc.Print.format_var n info)
Pos.no_pos
Errors.raise_spanned_error Pos.no_pos
"Internal Error: Variable %a was not found in the current environment. Additional \
informations : %s."
Dcalc.Print.format_var n info
(** [add_var pos var is_pure ctx] add to the context [ctx] the Dcalc variable var, creating a unique
corresponding variable in Lcalc, with the corresponding expression, and the boolean is_pure. It
@ -117,16 +115,16 @@ let translate_lit (l : D.lit) (pos : Pos.t) : A.lit =
| D.LDate d -> A.LDate d
| D.LDuration d -> A.LDuration d
| D.LEmptyError ->
Errors.raise_spanned_error
"Internal Error: An empty error was found in a place that shouldn't be possible." pos
Errors.raise_spanned_error pos
"Internal Error: An empty error was found in a place that shouldn't be possible."
(** [c = disjoint_union_maps cs] Compute the disjoint union of multiple maps. Raises an internal
error if there is two identicals keys in differnts parts. *)
let disjoint_union_maps (pos : Pos.t) (cs : 'a A.VarMap.t list) : 'a A.VarMap.t =
let disjoint_union =
A.VarMap.union (fun _ _ _ ->
Errors.raise_spanned_error
"Internal Error: Two supposed to be disjoints maps have one shared key." pos)
Errors.raise_spanned_error pos
"Internal Error: Two supposed to be disjoints maps have one shared key.")
in
List.fold_left disjoint_union A.VarMap.empty cs
@ -159,8 +157,8 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Pos.marked) :
replace it" Dcalc.Print.format_var v Print.format_var v'; *)
(A.make_var (v', pos), A.VarMap.singleton v' (D.EVar (v, pos_v), p))
else
Errors.raise_spanned_error
"Internal error: an pure variable was found in an unpure environment." pos
Errors.raise_spanned_error pos
"Internal error: an pure variable was found in an unpure environment."
| D.EDefault (_exceptions, _just, _cons) ->
let v' = A.Var.make ("default_term", pos) in
(A.make_var (v', pos), A.VarMap.singleton v' e)
@ -318,8 +316,8 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Pos.marked) :
(A.make_var (x, pos_hoist)))
pos_hoist [ (D.TAny, pos_hoist) ] pos_hoist)
| _ ->
Errors.raise_spanned_error
"Internal Error: An term was found in a position where it should not be" pos_hoist
Errors.raise_spanned_error pos_hoist
"Internal Error: An term was found in a position where it should not be"
in
(* [ match {{ c' }} with | None -> None | Some {{ v }} -> {{ acc }} end ] *)
@ -367,13 +365,11 @@ let rec translate_scope_let (ctx : ctx) (lets : scope_lets) =
(translate_scope_let ctx' next)
| ScopeLet
{ scope_let_kind = SubScopeVarDefinition; scope_let_pos = pos; scope_let_expr = expr; _ } ->
Errors.raise_spanned_error
(Format.asprintf
"Internal Error: found an SubScopeVarDefinition that does not satisfy the invariants \
when translating Dcalc to Lcalc without exceptions: @[<hov 2>%a@]"
(Dcalc.Print.format_expr ctx.decl_ctx)
expr)
pos
Errors.raise_spanned_error pos
"Internal Error: found an SubScopeVarDefinition that does not satisfy the invariants when \
translating Dcalc to Lcalc without exceptions: @[<hov 2>%a@]"
(Dcalc.Print.format_expr ctx.decl_ctx)
expr
| ScopeLet
{
scope_let_kind = kind;

View File

@ -22,20 +22,16 @@ let find_struct (s : D.StructName.t) (ctx : D.decl_ctx) :
try D.StructMap.find s ctx.D.ctx_structs
with Not_found ->
let s_name, pos = D.StructName.get_info s in
Errors.raise_spanned_error
(Format.asprintf "Internal Error: Structure %s was not found in the current environment."
s_name)
pos
Errors.raise_spanned_error pos
"Internal Error: Structure %s was not found in the current environment." s_name
let find_enum (en : D.EnumName.t) (ctx : D.decl_ctx) : (D.EnumConstructor.t * D.typ Pos.marked) list
=
try D.EnumMap.find en ctx.D.ctx_enums
with Not_found ->
let en_name, pos = D.EnumName.get_info en in
Errors.raise_spanned_error
(Format.asprintf "Internal Error: Enumeration %s was not found in the current environment."
en_name)
pos
Errors.raise_spanned_error pos
"Internal Error: Enumeration %s was not found in the current environment." en_name
let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit =
match Pos.unmark l with
@ -101,9 +97,8 @@ let format_unop (fmt : Format.formatter) (op : Dcalc.Ast.unop Pos.marked) : unit
| Minus k -> Format.fprintf fmt "~-%a" format_op_kind k
| Not -> Format.fprintf fmt "%s" "not"
| Log (_entry, _infos) ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position op)
"Internal error: a log operator has not been caught by the expression match"
(Pos.get_position op)
| Length -> Format.fprintf fmt "%s" "array_length"
| IntToRat -> Format.fprintf fmt "%s" "decimal_of_integer"
| GetDay -> Format.fprintf fmt "%s" "day_of_month_of_date"
@ -177,9 +172,8 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Pos.marked) : u
| TEnum ([ t ], e) when D.EnumName.compare e Ast.option_enum = 0 ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t format_enum_name e
| TEnum (_, e) when D.EnumName.compare e Ast.option_enum = 0 ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position typ)
"Internal Error: found an typing parameter for an eoption type of the wrong lenght."
(Pos.get_position typ)
| TEnum (_ts, e) -> Format.fprintf fmt "%a" format_enum_name e
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a ->@ %a@]" format_typ_with_parens t1 format_typ_with_parens t2

View File

@ -33,9 +33,8 @@ let pre_html (s : string) =
(** Raise an error if pygments cannot be found *)
let raise_failed_pygments (command : string) (error_code : int) : 'a =
Errors.raise_error
(Printf.sprintf "Weaving to HTML failed: pygmentize command \"%s\" returned with error code %d"
command error_code)
Errors.raise_error "Weaving to HTML failed: pygmentize command \"%s\" returned with error code %d"
command error_code
(** Partial application allowing to remove first code lines of [<td class="code">] and
[<td class="linenos">] generated HTML. Basically, remove all code block first lines. *)
@ -99,7 +98,7 @@ let wrap_html (source_files : string list) (language : Cli.backend_lang) (fmt :
(** Performs syntax highlighting on a piece of code by using Pygments and the special Catala lexer. *)
let pygmentize_code (c : string Pos.marked) (language : C.backend_lang) : string =
C.debug_print (Printf.sprintf "Pygmenting the code chunk %s" (Pos.to_string (Pos.get_position c)));
C.debug_print "Pygmenting the code chunk %s" (Pos.to_string (Pos.get_position c));
let temp_file_in = Filename.temp_file "catala_html_pygments" "in" in
let temp_file_out = Filename.temp_file "catala_html_pygments" "out" in
let oc = open_out temp_file_in in

View File

@ -55,11 +55,10 @@ let build_program_dep_graph (prgm : Ast.program) : SDependencies.t =
| Ast.Call (subscope, subindex) ->
if subscope = scope_name then
Errors.raise_spanned_error
(Format.asprintf
"The scope %a is calling into itself as a subscope, which is forbidden \
since Catala does not provide recursion"
Ast.ScopeName.format_t scope.Ast.scope_decl_name)
(Pos.get_position (Ast.ScopeName.get_info scope.Ast.scope_decl_name))
"The scope %a is calling into itself as a subscope, which is forbidden since \
Catala does not provide recursion"
Ast.ScopeName.format_t scope.Ast.scope_decl_name
else
Ast.ScopeMap.add subscope
(Pos.get_position (Ast.SubScopeName.get_info subindex))
@ -78,22 +77,24 @@ let check_for_cycle_in_scope (g : SDependencies.t) : unit =
let sccs = SSCC.scc_list g in
if List.length sccs < SDependencies.nb_vertex g then
let scc = List.find (fun scc -> List.length scc > 1) sccs in
Errors.raise_multispanned_error "Cyclic dependency detected between scopes!"
(List.flatten
(List.map
(fun v ->
let var_str, var_info =
(Format.asprintf "%a" Ast.ScopeName.format_t v, Ast.ScopeName.get_info v)
in
let succs = SDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str = Format.asprintf "%a" Ast.ScopeName.format_t succ in
[
(Some ("Cycle variable " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle variable " ^ succ_str ^ ":"),
edge_pos );
])
scc))
let spans =
List.flatten
(List.map
(fun v ->
let var_str, var_info =
(Format.asprintf "%a" Ast.ScopeName.format_t v, Ast.ScopeName.get_info v)
in
let succs = SDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str = Format.asprintf "%a" Ast.ScopeName.format_t succ in
[
(Some ("Cycle variable " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle variable " ^ succ_str ^ ":"),
edge_pos );
])
scc)
in
Errors.raise_multispanned_error spans "Cyclic dependency detected between scopes!"
let get_scope_ordering (g : SDependencies.t) : Ast.ScopeName.t list =
List.rev (STopologicalTraversal.fold (fun sd acc -> sd :: acc) g [])
@ -162,12 +163,10 @@ let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : TDepend
TVertexSet.fold
(fun used g ->
if TVertex.equal used def then
Errors.raise_spanned_error
(Format.asprintf
"The type %a is defined using itself, which is forbidden since Catala does \
not provide recursive types"
TVertex.format_t used)
(Pos.get_position typ)
Errors.raise_spanned_error (Pos.get_position typ)
"The type %a is defined using itself, which is forbidden since Catala does not \
provide recursive types"
TVertex.format_t used
else
let edge = TDependencies.E.create used (Pos.get_position typ) def in
TDependencies.add_edge_e g edge)
@ -186,12 +185,10 @@ let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : TDepend
TVertexSet.fold
(fun used g ->
if TVertex.equal used def then
Errors.raise_spanned_error
(Format.asprintf
"The type %a is defined using itself, which is forbidden since Catala does \
not provide recursive types"
TVertex.format_t used)
(Pos.get_position typ)
Errors.raise_spanned_error (Pos.get_position typ)
"The type %a is defined using itself, which is forbidden since Catala does not \
provide recursive types"
TVertex.format_t used
else
let edge = TDependencies.E.create used (Pos.get_position typ) def in
TDependencies.add_edge_e g edge)
@ -207,20 +204,20 @@ let check_type_cycles (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : TVerte
let sccs = TSCC.scc_list g in
(if List.length sccs < TDependencies.nb_vertex g then
let scc = List.find (fun scc -> List.length scc > 1) sccs in
Errors.raise_multispanned_error "Cyclic dependency detected between types!"
(List.flatten
(List.map
(fun v ->
let var_str, var_info =
(Format.asprintf "%a" TVertex.format_t v, TVertex.get_info v)
in
let succs = TDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str = Format.asprintf "%a" TVertex.format_t succ in
[
(Some ("Cycle type " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle type " ^ succ_str ^ ":"),
edge_pos );
])
scc)));
let spans =
List.flatten
(List.map
(fun v ->
let var_str, var_info = (Format.asprintf "%a" TVertex.format_t v, TVertex.get_info v) in
let succs = TDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str = Format.asprintf "%a" TVertex.format_t succ in
[
(Some ("Cycle type " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle type " ^ succ_str ^ ":"),
edge_pos );
])
scc)
in
Errors.raise_multispanned_error spans "Cyclic dependency detected between types!");
List.rev (TTopologicalTraversal.fold (fun v acc -> v :: acc) g [])

View File

@ -112,15 +112,14 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Po
struct_sig ([], e_fields)
in
if Ast.StructFieldMap.cardinal remaining_e_fields > 0 then
Errors.raise_spanned_error
(Format.asprintf "The fields \"%a\" do not belong to the structure %a"
Ast.StructName.format_t struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
(fun fmt (field_name, _) ->
Format.fprintf fmt "%a" Ast.StructFieldName.format_t field_name))
(Ast.StructFieldMap.bindings remaining_e_fields))
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"The fields \"%a\" do not belong to the structure %a" Ast.StructName.format_t
struct_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
(fun fmt (field_name, _) ->
Format.fprintf fmt "%a" Ast.StructFieldName.format_t field_name))
(Ast.StructFieldMap.bindings remaining_e_fields)
else
Bindlib.box_apply
(fun d_fields -> Dcalc.Ast.ETuple (d_fields, Some struct_name))
@ -130,10 +129,9 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Po
let _, field_index =
try List.assoc field_name (List.mapi (fun i (x, y) -> (x, (y, i))) struct_sig)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "The field \"%a\" does not belong to the structure %a"
Ast.StructFieldName.format_t field_name Ast.StructName.format_t struct_name)
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"The field \"%a\" does not belong to the structure %a" Ast.StructFieldName.format_t
field_name Ast.StructName.format_t struct_name
in
let e1 = translate_expr ctx e1 in
Bindlib.box_apply
@ -149,10 +147,9 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Po
let _, constructor_index =
try List.assoc constructor (List.mapi (fun i (x, y) -> (x, (y, i))) enum_sig)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "The constructor \"%a\" does not belong to the enum %a"
Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name)
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"The constructor \"%a\" does not belong to the enum %a" Ast.EnumConstructor.format_t
constructor Ast.EnumName.format_t enum_name
in
let e1 = translate_expr ctx e1 in
Bindlib.box_apply
@ -171,26 +168,23 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Po
let case_e =
try Ast.EnumConstructorMap.find constructor e_cases
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf
"The constructor %a of enum %a is missing from this pattern matching"
Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name)
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"The constructor %a of enum %a is missing from this pattern matching"
Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name
in
let case_d = translate_expr ctx case_e in
(case_d :: d_cases, Ast.EnumConstructorMap.remove constructor e_cases))
enum_sig ([], cases)
in
if Ast.EnumConstructorMap.cardinal remaining_e_cases > 0 then
Errors.raise_spanned_error
(Format.asprintf "Patter matching is incomplete for enum %a: missing cases %a"
Ast.EnumName.format_t enum_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
(fun fmt (case_name, _) ->
Format.fprintf fmt "%a" Ast.EnumConstructor.format_t case_name))
(Ast.EnumConstructorMap.bindings remaining_e_cases))
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"Patter matching is incomplete for enum %a: missing cases %a" Ast.EnumName.format_t
enum_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
(fun fmt (case_name, _) ->
Format.fprintf fmt "%a" Ast.EnumConstructor.format_t case_name))
(Ast.EnumConstructorMap.bindings remaining_e_cases)
else
let e1 = translate_expr ctx e1 in
Bindlib.box_apply2
@ -273,18 +267,17 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Po
Bindlib.box_var v
with Not_found ->
Errors.raise_multispanned_error
(Format.asprintf
"The variable %a.%a cannot be used here, as it is not part subscope %a's results. \
Maybe you forgot to qualify it as an output?"
Ast.SubScopeName.format_t (Pos.unmark s) Ast.ScopeVar.format_t (Pos.unmark a)
Ast.SubScopeName.format_t (Pos.unmark s))
[
(Some "Incriminated variable usage:", Pos.get_position e);
( Some "Incriminated subscope variable declaration:",
Pos.get_position (Ast.ScopeVar.get_info (Pos.unmark a)) );
( Some "Incriminated subscope declaration:",
Pos.get_position (Ast.SubScopeName.get_info (Pos.unmark s)) );
])
]
"The variable %a.%a cannot be used here, as it is not part subscope %a's results. \
Maybe you forgot to qualify it as an output?"
Ast.SubScopeName.format_t (Pos.unmark s) Ast.ScopeVar.format_t (Pos.unmark a)
Ast.SubScopeName.format_t (Pos.unmark s))
| EIfThenElse (cond, et, ef) ->
Bindlib.box_apply3
(fun c t f -> Dcalc.Ast.EIfThenElse (c, t, f))

View File

@ -63,29 +63,25 @@ let disambiguate_constructor (ctxt : Name_resolution.context)
match constructor with
| [ c ] -> c
| _ ->
Errors.raise_spanned_error "The deep pattern matching syntactic sugar is not yet supported"
pos
Errors.raise_spanned_error pos
"The deep pattern matching syntactic sugar is not yet supported"
in
let possible_c_uids =
try Desugared.Ast.IdentMap.find (Pos.unmark constructor) ctxt.constructor_idmap
with Not_found ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position constructor)
"The name of this constructor has not been defined before, maybe it is a typo?"
(Pos.get_position constructor)
in
match enum with
| None ->
if Scopelang.Ast.EnumMap.cardinal possible_c_uids > 1 then
Errors.raise_spanned_error
(Format.asprintf
"This constructor name is ambiguous, it can belong to %a. Disambiguate it by \
prefixing it with the enum name."
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
(fun fmt (s_name, _) ->
Format.fprintf fmt "%a" Scopelang.Ast.EnumName.format_t s_name))
(Scopelang.Ast.EnumMap.bindings possible_c_uids))
(Pos.get_position constructor);
Errors.raise_spanned_error (Pos.get_position constructor)
"This constructor name is ambiguous, it can belong to %a. Disambiguate it by prefixing \
it with the enum name."
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
(fun fmt (s_name, _) -> Format.fprintf fmt "%a" Scopelang.Ast.EnumName.format_t s_name))
(Scopelang.Ast.EnumMap.bindings possible_c_uids);
Scopelang.Ast.EnumMap.choose possible_c_uids
| Some enum -> (
try
@ -95,14 +91,11 @@ let disambiguate_constructor (ctxt : Name_resolution.context)
let c_uid = Scopelang.Ast.EnumMap.find e_uid possible_c_uids in
(e_uid, c_uid)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Enum %s does not contain case %s" (Pos.unmark enum)
(Pos.unmark constructor))
pos
Errors.raise_spanned_error pos "Enum %s does not contain case %s" (Pos.unmark enum)
(Pos.unmark constructor)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Enum %s has not been defined before" (Pos.unmark enum))
(Pos.get_position enum))
Errors.raise_spanned_error (Pos.get_position enum) "Enum %s has not been defined before"
(Pos.unmark enum))
(** Usage: [translate_expr scope ctxt expr]
@ -203,17 +196,17 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
Desugared.Ast.ELit
(Dcalc.Ast.LDuration (Runtime.duration_of_numbers 0 0 (Runtime.integer_to_int i)))
| LNumber ((Dec (_, _), _), Some ((Year | Month | Day), _)) ->
Errors.raise_spanned_error
"Impossible to specify decimal amounts of days, months or years" pos
Errors.raise_spanned_error pos
"Impossible to specify decimal amounts of days, months or years"
| LDate date ->
if Pos.unmark date.literal_date_month > 12 then
Errors.raise_spanned_error
"There is an error in this date: the month number is bigger than 12"
(Pos.get_position date.literal_date_month);
(Pos.get_position date.literal_date_month)
"There is an error in this date: the month number is bigger than 12";
if Pos.unmark date.literal_date_day > 31 then
Errors.raise_spanned_error
"There is an error in this date: the day number is bigger than 31"
(Pos.get_position date.literal_date_day);
(Pos.get_position date.literal_date_day)
"There is an error in this date: the day number is bigger than 31";
Desugared.Ast.ELit
(Dcalc.Ast.LDate
(try
@ -222,10 +215,9 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
(Pos.unmark date.literal_date_month)
(Pos.unmark date.literal_date_day)
with Runtime.ImpossibleDate ->
Errors.raise_spanned_error
Errors.raise_spanned_error pos
"There is an error in this date, it does not correspond to a correct \
calendar day"
pos))
calendar day"))
in
Bindlib.box (untyped_term, pos)
| Ident x -> (
@ -253,10 +245,9 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
| Some inside_def_state ->
if Desugared.Ast.StateName.compare inside_def_state (List.hd states) = 0
then
Errors.raise_spanned_error
Errors.raise_spanned_error pos
"It is impossible to refer to the variable you are defining when \
defining its first state."
pos
else
(* Tricky: we have to retrieve in the list the previous state with
respect to the state that we are defining. *)
@ -300,23 +291,21 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
let x_possible_structs =
try Desugared.Ast.IdentMap.find (Pos.unmark x) ctxt.field_idmap
with Not_found ->
Errors.raise_spanned_error "Unknown subscope or struct field name"
(Pos.get_position x)
Errors.raise_spanned_error (Pos.get_position x)
"Unknown subscope or struct field name"
in
match c with
| None ->
(* No constructor name was specified *)
if Scopelang.Ast.StructMap.cardinal x_possible_structs > 1 then
Errors.raise_spanned_error
(Format.asprintf
"This struct field name is ambiguous, it can belong to %a. Disambiguate it by \
prefixing it with the struct name."
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
(fun fmt (s_name, _) ->
Format.fprintf fmt "%a" Scopelang.Ast.StructName.format_t s_name))
(Scopelang.Ast.StructMap.bindings x_possible_structs))
(Pos.get_position x)
Errors.raise_spanned_error (Pos.get_position x)
"This struct field name is ambiguous, it can belong to %a. Disambiguate it by \
prefixing it with the struct name."
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
(fun fmt (s_name, _) ->
Format.fprintf fmt "%a" Scopelang.Ast.StructName.format_t s_name))
(Scopelang.Ast.StructMap.bindings x_possible_structs)
else
let s_uid, f_uid = Scopelang.Ast.StructMap.choose x_possible_structs in
Bindlib.box_apply (fun e -> (Desugared.Ast.EStructAccess (e, f_uid, s_uid), pos)) e
@ -329,14 +318,11 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
(fun e -> (Desugared.Ast.EStructAccess (e, f_uid, c_uid), pos))
e
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Struct %s does not contain field %s" (Pos.unmark c_name)
(Pos.unmark x))
pos
Errors.raise_spanned_error pos "Struct %s does not contain field %s"
(Pos.unmark c_name) (Pos.unmark x)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Struct %s has not been defined before" (Pos.unmark c_name))
(Pos.get_position c_name))))
Errors.raise_spanned_error (Pos.get_position c_name)
"Struct %s has not been defined before" (Pos.unmark c_name))))
| FunCall (f, arg) ->
Bindlib.box_apply2
(fun f arg -> (Desugared.Ast.EApp (f, [ arg ]), pos))
@ -345,9 +331,10 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
let s_uid =
try Desugared.Ast.IdentMap.find (Pos.unmark s_name) ctxt.struct_idmap
with Not_found ->
Errors.raise_spanned_error "This identifier should refer to a struct name"
(Pos.get_position s_name)
Errors.raise_spanned_error (Pos.get_position s_name)
"This identifier should refer to a struct name"
in
let s_fields =
List.fold_left
(fun s_fields (f_name, f_e) ->
@ -356,18 +343,16 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
Scopelang.Ast.StructMap.find s_uid
(Desugared.Ast.IdentMap.find (Pos.unmark f_name) ctxt.field_idmap)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "This identifier should refer to a field of struct %s"
(Pos.unmark s_name))
(Pos.get_position f_name)
Errors.raise_spanned_error (Pos.get_position f_name)
"This identifier should refer to a field of struct %s" (Pos.unmark s_name)
in
(match Scopelang.Ast.StructFieldMap.find_opt f_uid s_fields with
| None -> ()
| Some e_field ->
Errors.raise_multispanned_error
(Format.asprintf "The field %a has been defined twice:"
Scopelang.Ast.StructFieldName.format_t f_uid)
[ (None, Pos.get_position f_e); (None, Pos.get_position (Bindlib.unbox e_field)) ]);
[ (None, Pos.get_position f_e); (None, Pos.get_position (Bindlib.unbox e_field)) ]
"The field %a has been defined twice:" Scopelang.Ast.StructFieldName.format_t
f_uid);
let f_e = translate_expr scope inside_definition_of ctxt f_e in
Scopelang.Ast.StructFieldMap.add f_uid f_e s_fields)
Scopelang.Ast.StructFieldMap.empty fields
@ -376,11 +361,9 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
Scopelang.Ast.StructFieldMap.iter
(fun expected_f _ ->
if not (Scopelang.Ast.StructFieldMap.mem expected_f s_fields) then
Errors.raise_spanned_error
(Format.asprintf "Missing field for structure %a: \"%a\""
Scopelang.Ast.StructName.format_t s_uid Scopelang.Ast.StructFieldName.format_t
expected_f)
pos)
Errors.raise_spanned_error pos "Missing field for structure %a: \"%a\""
Scopelang.Ast.StructName.format_t s_uid Scopelang.Ast.StructFieldName.format_t
expected_f)
expected_s_fields;
Bindlib.box_apply
@ -390,26 +373,24 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
let possible_c_uids =
try Desugared.Ast.IdentMap.find (Pos.unmark constructor) ctxt.constructor_idmap
with Not_found ->
Errors.raise_spanned_error
Errors.raise_spanned_error (Pos.get_position constructor)
"The name of this constructor has not been defined before, maybe it is a typo?"
(Pos.get_position constructor)
in
match enum with
| None ->
if
(* No constructor name was specified *)
Scopelang.Ast.EnumMap.cardinal possible_c_uids > 1
then
Errors.raise_spanned_error
(Format.asprintf
"This constructor name is ambiguous, it can belong to %a. Desambiguate it by \
prefixing it with the enum name."
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
(fun fmt (s_name, _) ->
Format.fprintf fmt "%a" Scopelang.Ast.EnumName.format_t s_name))
(Scopelang.Ast.EnumMap.bindings possible_c_uids))
(Pos.get_position constructor)
Errors.raise_spanned_error (Pos.get_position constructor)
"This constructor name is ambiguous, it can belong to %a. Desambiguate it by \
prefixing it with the enum name."
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
(fun fmt (s_name, _) ->
Format.fprintf fmt "%a" Scopelang.Ast.EnumName.format_t s_name))
(Scopelang.Ast.EnumMap.bindings possible_c_uids)
else
let e_uid, c_uid = Scopelang.Ast.EnumMap.choose possible_c_uids in
let payload = Option.map (translate_expr scope inside_definition_of ctxt) payload in
@ -441,14 +422,11 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
pos ))
(Bindlib.box_opt payload)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Enum %s does not contain case %s" (Pos.unmark enum)
(Pos.unmark constructor))
pos
Errors.raise_spanned_error pos "Enum %s does not contain case %s" (Pos.unmark enum)
(Pos.unmark constructor)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Enum %s has not been defined before" (Pos.unmark enum))
(Pos.get_position enum)))
Errors.raise_spanned_error (Pos.get_position enum) "Enum %s has not been defined before"
(Pos.unmark enum)))
| MatchWith (e1, (cases, _cases_pos)) ->
let e1 = translate_expr scope inside_definition_of ctxt e1 in
let cases_d, e_uid =
@ -462,9 +440,8 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
(match snd (Pos.unmark pattern) with
| None -> ()
| Some binding ->
Errors.print_spanned_warning
"This binding will be ignored (remove it to suppress warning)"
(Pos.get_position binding));
Errors.format_spanned_warning (Pos.get_position binding)
"This binding will be ignored (remove it to suppress warning)");
let enum_uid, c_uid =
disambiguate_constructor ctxt (fst (Pos.unmark pattern)) (Pos.get_position pattern)
in
@ -524,11 +501,10 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
| Ast.Duration -> Dcalc.Ast.KDuration
| Ast.Date -> Dcalc.Ast.KDate
| _ ->
Errors.raise_spanned_error
(Format.asprintf "It is impossible to compute the arg-%s of two values of type %a"
(if max_or_min then "max" else "min")
Print.format_primitive_typ pred_typ)
pos
Errors.raise_spanned_error pos
"It is impossible to compute the arg-%s of two values of type %a"
(if max_or_min then "max" else "min")
Print.format_primitive_typ pred_typ
in
let cmp_op = if max_or_min then Dcalc.Ast.Gt op_kind else Dcalc.Ast.Lt op_kind in
let f_pred =
@ -602,10 +578,8 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
( Desugared.Ast.ELit (Dcalc.Ast.LDuration (Runtime.duration_of_numbers 0 0 0)),
Pos.get_position op' )
| Ast.Aggregate (Ast.AggregateSum t) ->
Errors.raise_spanned_error
(Format.asprintf "It is impossible to sum two values of type %a together"
Print.format_primitive_typ t)
pos
Errors.raise_spanned_error pos "It is impossible to sum two values of type %a together"
Print.format_primitive_typ t
| Ast.Aggregate (Ast.AggregateExtremum (_, _, init)) -> rec_helper init
| Ast.Aggregate Ast.AggregateCount ->
Bindlib.box
@ -661,11 +635,10 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
| Ast.Duration -> (Dcalc.Ast.KDuration, (Scopelang.Ast.TLit TDuration, pos))
| Ast.Date -> (Dcalc.Ast.KDate, (Scopelang.Ast.TLit TDate, pos))
| _ ->
Errors.raise_spanned_error
(Format.asprintf "It is impossible to compute the %s of two values of type %a"
(if max_or_min then "max" else "min")
Print.format_primitive_typ t)
pos
Errors.raise_spanned_error pos
"It is impossible to compute the %s of two values of type %a"
(if max_or_min then "max" else "min")
Print.format_primitive_typ t
in
let cmp_op = if max_or_min then Dcalc.Ast.Gt op_kind else Dcalc.Ast.Lt op_kind in
make_extr_body cmp_op typ
@ -814,22 +787,21 @@ and disambiguate_match_and_build_expression (scope : Scopelang.Ast.ScopeName.t)
if e_uid = e_uid' then e_uid
else
Errors.raise_spanned_error
(Format.asprintf
"This case matches a constructor of enumeration %a but previous case were \
matching constructors of enumeration %a"
Scopelang.Ast.EnumName.format_t e_uid Scopelang.Ast.EnumName.format_t e_uid')
(Pos.get_position case.Ast.match_case_pattern)
"This case matches a constructor of enumeration %a but previous case were \
matching constructors of enumeration %a"
Scopelang.Ast.EnumName.format_t e_uid Scopelang.Ast.EnumName.format_t e_uid'
in
(match Scopelang.Ast.EnumConstructorMap.find_opt c_uid cases_d with
| None -> ()
| Some e_case ->
Errors.raise_multispanned_error
(Format.asprintf "The constructor %a has been matched twice:"
Scopelang.Ast.EnumConstructor.format_t c_uid)
[
(None, Pos.get_position case.match_case_expr);
(None, Pos.get_position (Bindlib.unbox e_case));
]);
]
"The constructor %a has been matched twice:" Scopelang.Ast.EnumConstructor.format_t
c_uid);
let ctxt, (param_var, param_pos) = create_var binding in
let case_body = translate_expr scope inside_definition_of ctxt case.Ast.match_case_expr in
let e_binder = Bindlib.bind_mvar (Array.of_list [ param_var ]) case_body in
@ -838,19 +810,19 @@ and disambiguate_match_and_build_expression (scope : Scopelang.Ast.ScopeName.t)
| Ast.WildCard match_case_expr -> (
let nb_cases = List.length cases in
let raise_wildcard_not_last_case_err () =
Errors.raise_multispanned_error "Wildcard must be the last match case"
Errors.raise_multispanned_error
[
(Some "Not ending wildcard:", case_pos);
(Some "Next reachable case:", curr_index + 1 |> List.nth cases |> Pos.get_position);
]
"Wildcard must be the last match case"
in
match e_uid with
| None ->
if 1 = nb_cases then
Errors.raise_spanned_error
Errors.raise_spanned_error case_pos
"Couldn't infer the enumeration name from lonely wildcard (wildcard cannot be used \
as single match case)"
case_pos
else raise_wildcard_not_last_case_err ()
| Some e_uid ->
if curr_index < nb_cases - 1 then raise_wildcard_not_last_case_err ();
@ -862,12 +834,10 @@ and disambiguate_match_and_build_expression (scope : Scopelang.Ast.ScopeName.t)
| None -> Some c_uid)
in
if Scopelang.Ast.EnumConstructorMap.is_empty missing_constructors then
Errors.print_spanned_warning
(Format.asprintf
"Unreachable match case, all constructors of the enumeration %a are already \
specified"
Scopelang.Ast.EnumName.format_t e_uid)
case_pos;
Errors.format_spanned_warning case_pos
"Unreachable match case, all constructors of the enumeration %a are already \
specified"
Scopelang.Ast.EnumName.format_t e_uid;
(* The current used strategy is to replace the wildcard branch:
match foo with
| Case1 x -> x
@ -943,12 +913,12 @@ let process_default (ctxt : Name_resolution.context) (scope : Scopelang.Ast.Scop
| Scopelang.Ast.TArrow (t_in, _), Some param_uid -> Some (Pos.unmark param_uid, t_in)
| Scopelang.Ast.TArrow _, None ->
Errors.raise_spanned_error
"This definition has a function type but the parameter is missing"
(Pos.get_position (Bindlib.unbox cons))
"This definition has a function type but the parameter is missing"
| _, Some _ ->
Errors.raise_spanned_error
"This definition has a parameter but its type is not a function"
(Pos.get_position (Bindlib.unbox cons))
"This definition has a parameter but its type is not a function"
| _ -> None);
rule_exception_to_rules = exception_to_rules;
rule_id;
@ -993,10 +963,9 @@ let process_def (precond : Desugared.Ast.expr Pos.marked Bindlib.box option)
( Desugared.Ast.LabelMap.find label_id scope_def.scope_def_label_groups,
Pos.get_position def.Ast.definition_name )
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Unknown label for the scope variable %a: \"%s\""
Desugared.Ast.ScopeDef.format_t def_key (Pos.unmark label))
(Pos.get_position label))
Errors.raise_spanned_error (Pos.get_position label)
"Unknown label for the scope variable %a: \"%s\"" Desugared.Ast.ScopeDef.format_t
def_key (Pos.unmark label))
in
let scope_def =
{
@ -1091,13 +1060,13 @@ let check_unlabeled_exception (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_r
| Ast.UnlabeledException -> (
match scope_def_ctxt.default_exception_rulename with
| None ->
Errors.raise_spanned_error "This exception does not have a corresponding definition"
(Pos.get_position item)
Errors.raise_spanned_error (Pos.get_position item)
"This exception does not have a corresponding definition"
| Some (Ambiguous pos) ->
Errors.raise_multispanned_error
"This exception can refer to several definitions. Try using labels to disambiguate"
([ (Some "Ambiguous exception", Pos.get_position item) ]
@ List.map (fun p -> (Some "Candidate definition", p)) pos)
"This exception can refer to several definitions. Try using labels to disambiguate"
| Some (Unique _) -> ()))
| _ -> ()

View File

@ -51,9 +51,8 @@ let update_acc (lexbuf : lexbuf) : unit = Buffer.add_string code_buffer (Utf8.le
(** Error-generating helper *)
let raise_lexer_error (loc : Pos.t) (token : string) =
Errors.raise_spanned_error
(Printf.sprintf "Parsing error after token \"%s\": what comes after is unknown" token)
loc
Errors.raise_spanned_error loc "Parsing error after token \"%s\": what comes after is unknown"
token
(** Associative list matching each punctuation string part of the Catala syntax with its {!module:
Surface.Parser} token. Same for all the input languages (English, French, etc.) *)

View File

@ -82,16 +82,14 @@ type context = {
(** Temporary function raising an error message saying that a feature is not supported yet *)
let raise_unsupported_feature (msg : string) (pos : Pos.t) =
Errors.raise_spanned_error (Printf.sprintf "Unsupported feature: %s" msg) pos
Errors.raise_spanned_error pos "Unsupported feature: %s" msg
(** Function to call whenever an identifier used somewhere has not been declared in the program
previously *)
let raise_unknown_identifier (msg : string) (ident : ident Pos.marked) =
Errors.raise_spanned_error
(Printf.sprintf "\"%s\": unknown identifier %s"
(Utils.Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Pos.unmark ident))
msg)
(Pos.get_position ident)
Errors.raise_spanned_error (Pos.get_position ident) "\"%s\": unknown identifier %s"
(Utils.Cli.with_style [ ANSITerminal.yellow ] "%s" (Pos.unmark ident))
msg
(** Gets the type associated to an uid *)
let get_var_typ (ctxt : context) (uid : Desugared.Ast.ScopeVar.t) : typ Pos.marked =
@ -171,13 +169,13 @@ let process_subscope_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
match Desugared.Ast.IdentMap.find_opt subscope scope_ctxt.sub_scopes_idmap with
| Some use ->
Errors.raise_multispanned_error
(Format.asprintf "Subscope name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
subscope)
[
(Some "first use", Pos.get_position (Scopelang.Ast.SubScopeName.get_info use));
(Some "second use", s_pos);
]
"Subscope name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
subscope
| None ->
let sub_scope_uid = Scopelang.Ast.SubScopeName.fresh (name, name_pos) in
let original_subscope_uid =
@ -226,11 +224,10 @@ let rec process_base_typ (ctxt : context) ((typ, typ_pos) : Ast.base_typ Pos.mar
match Desugared.Ast.IdentMap.find_opt ident ctxt.enum_idmap with
| Some e_uid -> (Scopelang.Ast.TEnum e_uid, typ_pos)
| None ->
Errors.raise_spanned_error
(Format.asprintf "Unknown type \"%a\", not a struct or enum previously declared"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
ident)
typ_pos)))
Errors.raise_spanned_error typ_pos
"Unknown type \"%a\", not a struct or enum previously declared"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
ident)))
(** Process a type (function or not) *)
let process_type (ctxt : context) ((typ, typ_pos) : Ast.typ Pos.marked) :
@ -252,13 +249,13 @@ let process_data_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
match Desugared.Ast.IdentMap.find_opt name scope_ctxt.var_idmap with
| Some use ->
Errors.raise_multispanned_error
(Format.asprintf "var name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
name)
[
(Some "first use", Pos.get_position (Desugared.Ast.ScopeVar.get_info use));
(Some "second use", pos);
]
"var name \"%a\" already used"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
name
| None ->
let uid = Desugared.Ast.ScopeVar.fresh (name, pos) in
let scope_ctxt =
@ -393,10 +390,10 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context =
let process_name_item (ctxt : context) (item : Ast.code_item Pos.marked) : context =
let raise_already_defined_error (use : Uid.MarkedString.info) name pos msg =
Errors.raise_multispanned_error
(Format.asprintf "%s name \"%a\" already defined" msg
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
name)
[ (Some "First definition:", Pos.get_position use); (Some "Second definition:", pos) ]
"%s name \"%a\" already defined" msg
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
name
in
match Pos.unmark item with
| ScopeDecl decl -> (
@ -486,25 +483,24 @@ let get_def_key (name : Ast.qident) (state : Ast.ident Pos.marked option)
try Some (Desugared.Ast.IdentMap.find (Pos.unmark state) var_sig.var_sig_states_idmap)
with Not_found ->
Errors.raise_multispanned_error
(Format.asprintf "This identifier is not a state declared for variable %a."
Desugared.Ast.ScopeVar.format_t x_uid)
[
(None, Pos.get_position state);
( Some "Variable declaration:",
Pos.get_position (Desugared.Ast.ScopeVar.get_info x_uid) );
])
]
"This identifier is not a state declared for variable %a."
Desugared.Ast.ScopeVar.format_t x_uid)
| None ->
if not (Desugared.Ast.IdentMap.is_empty var_sig.var_sig_states_idmap) then
Errors.raise_multispanned_error
(Format.asprintf
"This definition does not indicate which state has to be considered for \
variable %a."
Desugared.Ast.ScopeVar.format_t x_uid)
[
(None, Pos.get_position x);
( Some "Variable declaration:",
Pos.get_position (Desugared.Ast.ScopeVar.get_info x_uid) );
]
"This definition does not indicate which state has to be considered for variable \
%a."
Desugared.Ast.ScopeVar.format_t x_uid
else None )
| [ y; x ] ->
let subscope_uid : Scopelang.Ast.SubScopeName.t = get_subscope_uid scope_uid ctxt y in
@ -513,7 +509,7 @@ let get_def_key (name : Ast.qident) (state : Ast.ident Pos.marked option)
in
let x_uid = get_var_uid subscope_real_uid ctxt x in
Desugared.Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid)
| _ -> Errors.raise_spanned_error "Structs are not handled yet" default_pos
| _ -> Errors.raise_spanned_error default_pos "Structs are not handled yet"
let process_definition (ctxt : context) (s_name : Scopelang.Ast.ScopeName.t) (d : Ast.definition) :
context =
@ -647,10 +643,10 @@ let process_scope_use (ctxt : context) (suse : Ast.scope_use) : context =
try Desugared.Ast.IdentMap.find (Pos.unmark suse.Ast.scope_use_name) ctxt.scope_idmap
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "\"%a\": this scope has not been declared anywhere, is it a typo?"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Pos.unmark suse.Ast.scope_use_name))
(Pos.get_position suse.Ast.scope_use_name)
"\"%a\": this scope has not been declared anywhere, is it a typo?"
(Utils.Cli.format_with_style [ ANSITerminal.yellow ])
(Pos.unmark suse.Ast.scope_use_name)
in
List.fold_left (process_scope_use_item s_name) ctxt suse.Ast.scope_use_items

View File

@ -466,8 +466,8 @@ ident:
match Localisation.lex_builtin i with
| Some _ ->
Errors.raise_spanned_error
(Printf.sprintf "Reserved builtin name")
(Pos.from_lpos $sloc)
"Reserved builtin name"
| None ->
(i, Pos.from_lpos $sloc)
}

View File

@ -98,14 +98,14 @@ let syntax_hints_style = [ ANSITerminal.yellow ]
let raise_parser_error (error_loc : Pos.t) (last_good_loc : Pos.t option) (token : string)
(msg : string) : 'a =
Errors.raise_multispanned_error
(Printf.sprintf "Syntax error at token %s\n%s"
(Cli.print_with_style syntax_hints_style "\"%s\"" token)
msg)
((Some "Error token:", error_loc)
::
(match last_good_loc with
| None -> []
| Some last_good_loc -> [ (Some "Last good token:", last_good_loc) ]))
"Syntax error at token %a\n%s"
(Cli.format_with_style syntax_hints_style)
(Printf.sprintf "\"%s\"" token) msg
module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
include Parser.Make (LocalisedLexer)
@ -163,18 +163,17 @@ module ParserAux (LocalisedLexer : Lexer_common.LocalisedLexer) = struct
(Printf.sprintf "did you mean %s?"
(String.concat ", or maybe "
(List.map
(fun (ts, _) -> Cli.print_with_style syntax_hints_style "\"%s\"" ts)
(fun (ts, _) -> Cli.with_style syntax_hints_style "\"%s\"" ts)
similar_acceptable_tokens)))
in
(* The parser has suspended itself because of a syntax error. Stop. *)
let custom_menhir_message =
match Parser_errors.message (state env) with
| exception Not_found ->
"Message: " ^ Cli.print_with_style syntax_hints_style "%s" "unexpected token"
"Message: " ^ Cli.with_style syntax_hints_style "%s" "unexpected token"
| msg ->
"Message: "
^ Cli.print_with_style syntax_hints_style "%s"
(String.trim (String.uncapitalize_ascii msg))
^ Cli.with_style syntax_hints_style "%s" (String.trim (String.uncapitalize_ascii msg))
in
let msg =
match similar_token_msg with
@ -237,15 +236,14 @@ let localised_parser : Cli.backend_lang -> lexbuf -> Ast.source_file = function
(** Parses a single source file *)
let rec parse_source_file (source_file : Pos.input_file) (language : Cli.backend_lang) : Ast.program
=
Cli.debug_print
(Printf.sprintf "Parsing %s" (match source_file with FileName s | Contents s -> s));
Cli.debug_print "Parsing %s" (match source_file with FileName s | Contents s -> s);
let lexbuf, input =
match source_file with
| FileName source_file -> (
try
let input = open_in source_file in
(Sedlexing.Utf8.from_channel input, Some input)
with Sys_error msg -> Errors.raise_error msg)
with Sys_error msg -> Errors.raise_error "%s" msg)
| Contents contents -> (Sedlexing.Utf8.from_string contents, None)
in
let source_file_name = match source_file with FileName s -> s | Contents _ -> "stdin" in

View File

@ -206,7 +206,7 @@ let info =
let time : float ref = ref (Unix.gettimeofday ())
let print_with_style (styles : ANSITerminal.style list) (str : ('a, unit, string) format) =
let with_style (styles : ANSITerminal.style list) (str : ('a, unit, string) format) =
if !style_flag then ANSITerminal.sprintf styles str else Printf.sprintf str
let format_with_style (styles : ANSITerminal.style list) fmt (str : string) =
@ -221,24 +221,24 @@ let time_marker () =
let delta = (new_time -. old_time) *. 1000. in
if delta > 50. then
Printf.printf "%s"
(print_with_style [ ANSITerminal.Bold; ANSITerminal.black ] "[TIME] %.0f ms\n" delta)
(with_style [ ANSITerminal.Bold; ANSITerminal.black ] "[TIME] %.0f ms\n" delta)
(** Prints [\[DEBUG\]] in purple on the terminal standard output *)
let debug_marker () =
time_marker ();
print_with_style [ ANSITerminal.Bold; ANSITerminal.magenta ] "[DEBUG] "
with_style [ ANSITerminal.Bold; ANSITerminal.magenta ] "[DEBUG] "
(** Prints [\[ERROR\]] in red on the terminal error output *)
let error_marker () = print_with_style [ ANSITerminal.Bold; ANSITerminal.red ] "[ERROR] "
let error_marker () = with_style [ ANSITerminal.Bold; ANSITerminal.red ] "[ERROR] "
(** Prints [\[WARNING\]] in yellow on the terminal standard output *)
let warning_marker () = print_with_style [ ANSITerminal.Bold; ANSITerminal.yellow ] "[WARNING] "
let warning_marker () = with_style [ ANSITerminal.Bold; ANSITerminal.yellow ] "[WARNING] "
(** Prints [\[RESULT\]] in green on the terminal standard output *)
let result_marker () = print_with_style [ ANSITerminal.Bold; ANSITerminal.green ] "[RESULT] "
let result_marker () = with_style [ ANSITerminal.Bold; ANSITerminal.green ] "[RESULT] "
(** Prints [\[LOG\]] in red on the terminal error output *)
let log_marker () = print_with_style [ ANSITerminal.Bold; ANSITerminal.black ] "[LOG] "
let log_marker () = with_style [ ANSITerminal.Bold; ANSITerminal.black ] "[LOG] "
(**{2 Printers}*)
@ -265,29 +265,28 @@ let add_prefix_to_each_line (s : string) (prefix : int -> string) =
(fun _ -> "\n")
(String.split_on_char '\n' s)
let debug_print (s : string) =
if !debug_flag then begin
Printf.printf "%s\n" (debug_marker () ^ s);
flush stdout;
flush stdout
end
let debug_print (format : ('a, out_channel, unit) format) =
if !debug_flag then Printf.printf ("%s" ^^ format ^^ "\n%!") (debug_marker ())
else Printf.ifprintf stdout format
let error_print (s : string) =
Printf.eprintf "%s\n" (error_marker () ^ s);
flush stderr;
flush stderr
let debug_format (format : ('a, Format.formatter, unit) format) =
if !debug_flag then Format.printf ("%s@[<hov>" ^^ format ^^ "@]@.") (debug_marker ())
else Format.ifprintf Format.std_formatter format
let warning_print (s : string) =
Printf.printf "%s\n" (warning_marker () ^ s);
flush stdout;
flush stdout
let error_print (format : ('a, out_channel, unit) format) =
Printf.eprintf ("%s" ^^ format ^^ "\n%!") (error_marker ())
let result_print (s : string) =
Printf.printf "%s\n" (result_marker () ^ s);
flush stdout;
flush stdout
let warning_print (format : ('a, out_channel, unit) format) =
Printf.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())
let log_print (s : string) =
Printf.printf "%s\n" (log_marker () ^ s);
flush stdout;
flush stdout
let result_print (format : ('a, out_channel, unit) format) =
Printf.printf ("%s" ^^ format ^^ "\n%!") (result_marker ())
let result_format (format : ('a, Format.formatter, unit) format) =
Format.printf ("%s" ^^ format ^^ "\n%!") (result_marker ())
let log_print (format : ('a, out_channel, unit) format) =
Printf.printf ("%s" ^^ format ^^ "\n%!") (log_marker ())
let log_format (format : ('a, Format.formatter, unit) format) =
Format.printf ("%s@[<hov>" ^^ format ^^ "@]@.") (log_marker ())

View File

@ -104,7 +104,7 @@ val info : Cmdliner.Term.info
(**{2 Markers}*)
val print_with_style : ANSITerminal.style list -> ('a, unit, string) format -> 'a
val with_style : ANSITerminal.style list -> ('a, unit, string) format -> 'a
val format_with_style : ANSITerminal.style list -> Format.formatter -> string -> unit
@ -128,12 +128,18 @@ val concat_with_line_depending_prefix_and_suffix :
val add_prefix_to_each_line : string -> (int -> string) -> string
(** The int argument of the prefix corresponds to the line number, starting at 0 *)
val debug_print : string -> unit
val debug_print : ('a, out_channel, unit) format -> 'a
val error_print : string -> unit
val debug_format : ('a, Format.formatter, unit) format -> 'a
val warning_print : string -> unit
val error_print : ('a, out_channel, unit) format -> 'a
val result_print : string -> unit
val warning_print : ('a, out_channel, unit) format -> 'a
val log_print : string -> unit
val result_print : ('a, out_channel, unit) format -> 'a
val result_format : ('a, Format.formatter, unit) format -> 'a
val log_print : ('a, out_channel, unit) format -> 'a
val log_format : ('a, Format.formatter, unit) format -> 'a

View File

@ -34,20 +34,20 @@ let print_structured_error (msg : string) (pos : (string option * Pos.t) list) :
(** {1 Error exception and printing} *)
let raise_spanned_error (msg : string) ?(span_msg : string option) (span : Pos.t) : 'a =
raise (StructuredError (msg, [ (span_msg, span) ]))
let raise_spanned_error ?(span_msg : string option) (span : Pos.t) format =
Format.kasprintf (fun msg -> raise (StructuredError (msg, [ (span_msg, span) ]))) format
let raise_multispanned_error (msg : string) (spans : (string option * Pos.t) list) =
raise (StructuredError (msg, spans))
let raise_multispanned_error (spans : (string option * Pos.t) list) format =
Format.kasprintf (fun msg -> raise (StructuredError (msg, spans))) format
let raise_error (msg : string) : 'a = raise (StructuredError (msg, []))
let raise_error format = Format.kasprintf (fun msg -> raise (StructuredError (msg, []))) format
(** {1 Warning printing}*)
let print_multispanned_warning (msg : string) (pos : (string option * Pos.t) list) : unit =
Cli.warning_print (print_structured_error msg pos)
let format_multispanned_warning (pos : (string option * Pos.t) list) format =
Format.kasprintf (fun msg -> Cli.warning_print "%s" (print_structured_error msg pos)) format
let print_spanned_warning (msg : string) ?(span_msg : string option) (span : Pos.t) : unit =
print_multispanned_warning msg [ (span_msg, span) ]
let format_spanned_warning ?(span_msg : string option) (span : Pos.t) format =
format_multispanned_warning [ (span_msg, span) ] format
let print_warning (msg : string) : unit = print_multispanned_warning msg []
let format_warning format = format_multispanned_warning [] format

View File

@ -25,16 +25,19 @@ val print_structured_error : string -> (string option * Pos.t) list -> string
(** {1 Error exception and printing} *)
val raise_spanned_error : string -> ?span_msg:string -> Pos.t -> 'a
val raise_spanned_error :
?span_msg:string -> Pos.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val raise_multispanned_error : string -> (string option * Pos.t) list -> 'a
val raise_multispanned_error :
(string option * Pos.t) list -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val raise_error : string -> 'a
val raise_error : ('a, Format.formatter, unit, 'b) format4 -> 'a
(** {1 Warning printing}*)
val print_multispanned_warning : string -> (string option * Pos.t) list -> unit
val format_multispanned_warning :
(string option * Pos.t) list -> ('a, Format.formatter, unit) format -> 'a
val print_spanned_warning : string -> ?span_msg:string -> Pos.t -> unit
val format_spanned_warning : ?span_msg:string -> Pos.t -> ('a, Format.formatter, unit) format -> 'a
val print_warning : string -> unit
val format_warning : ('a, Format.formatter, unit) format -> 'a

View File

@ -105,18 +105,18 @@ let retrieve_loc_text (pos : t) : string =
"\n"
^
if line_no = sline && line_no = eline then
Cli.print_with_style error_indicator_style "%*s"
Cli.with_style error_indicator_style "%*s"
(get_end_column pos - 1)
(String.make (max (get_end_column pos - get_start_column pos) 0) '^')
else if line_no = sline && line_no <> eline then
Cli.print_with_style error_indicator_style "%*s"
Cli.with_style error_indicator_style "%*s"
(String.length line - 1)
(String.make (max (String.length line - get_start_column pos) 0) '^')
else if line_no <> sline && line_no <> eline then
Cli.print_with_style error_indicator_style "%*s%s" line_indent ""
Cli.with_style error_indicator_style "%*s%s" line_indent ""
(String.make (max (String.length line - line_indent) 0) '^')
else if line_no <> sline && line_no = eline then
Cli.print_with_style error_indicator_style "%*s%*s" line_indent ""
Cli.with_style error_indicator_style "%*s%*s" line_indent ""
(get_end_column pos - 1 - line_indent)
(String.make (max (get_end_column pos - line_indent) 0) '^')
else assert false (* should not happen *)
@ -141,7 +141,7 @@ let retrieve_loc_text (pos : t) : string =
pos.law_pos)
in
(match oc with None -> () | Some oc -> close_in oc);
Cli.print_with_style blue_style "%*s--> %s\n%s\n%s" spaces "" filename
Cli.with_style blue_style "%*s--> %s\n%s\n%s" spaces "" filename
(Cli.add_prefix_to_each_line
(Printf.sprintf "\n%s" (String.concat "\n" pos_lines))
(fun i ->
@ -150,21 +150,21 @@ let retrieve_loc_text (pos : t) : string =
cur_line >= sline
&& cur_line <= sline + (2 * (eline - sline))
&& cur_line mod 2 = sline mod 2
then Cli.print_with_style blue_style "%*d | " spaces (sline + ((cur_line - sline) / 2))
then Cli.with_style blue_style "%*d | " spaces (sline + ((cur_line - sline) / 2))
else if cur_line >= sline - include_extra_count && cur_line < sline then
Cli.print_with_style blue_style "%*d | " spaces cur_line
Cli.with_style blue_style "%*d | " spaces cur_line
else if
cur_line <= sline + (2 * (eline - sline)) + 1 + include_extra_count
&& cur_line > sline + (2 * (eline - sline)) + 1
then Cli.print_with_style blue_style "%*d | " spaces (cur_line - (eline - sline + 1))
else Cli.print_with_style blue_style "%*s | " spaces ""))
then Cli.with_style blue_style "%*d | " spaces (cur_line - (eline - sline + 1))
else Cli.with_style blue_style "%*s | " spaces ""))
(Cli.add_prefix_to_each_line
(Printf.sprintf "%s"
(String.concat "\n"
(List.map (fun l -> Cli.print_with_style blue_style "%s" l) legal_pos_lines)))
(List.map (fun l -> Cli.with_style blue_style "%s" l) legal_pos_lines)))
(fun i ->
if i = 0 then Cli.print_with_style blue_style "%*s + " (spaces + (2 * i)) ""
else Cli.print_with_style blue_style "%*s+-+ " (spaces + (2 * i) - 1) ""))
if i = 0 then Cli.with_style blue_style "%*s + " (spaces + (2 * i)) ""
else Cli.with_style blue_style "%*s+-+ " (spaces + (2 * i) - 1) ""))
with Sys_error _ -> "Location:" ^ to_string pos
type 'a marked = 'a * t

View File

@ -80,26 +80,21 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : expr Pos.marked) :
match Pos.unmark body with
| EApp ((EOp (Unop (Log _)), _), [ arg ]) -> arg
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"Internal error: this expression does not have the structure expected by the VC \
generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e)
(Pos.get_position e))
Errors.raise_spanned_error (Pos.get_position e)
"Internal error: this expression does not have the structure expected by the VC \
generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e)
| ErrorOnEmpty (EApp ((EOp (Unop (Log _)), _), [ d ]), _)
| EApp ((EOp (Unop (Log _)), _), [ (ErrorOnEmpty d, _) ]) ->
d (* input subscope variables and non-input scope variable *)
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"Internal error: this expression does not have the structure expected by the VC \
generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e)
(Pos.get_position e)
Errors.raise_spanned_error (Pos.get_position e)
"Internal error: this expression does not have the structure expected by the VC generator:\n\
%a"
(Print.format_expr ~debug:true ctx.decl)
e
(** {1 Verification conditions generator}*)

View File

@ -84,12 +84,12 @@ module MakeBackendIO (B : Backend) = struct
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable never returns an empty error"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s No two exceptions to ever overlap for this variable"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
@ -99,13 +99,13 @@ module MakeBackendIO (B : Backend) = struct
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable might return an empty error:\n%s"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s At least two exceptions overlap for this variable:\n%s"
(Cli.print_with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
(Pos.retrieve_loc_text (Pos.get_position vc.vc_variable))
@ -137,26 +137,22 @@ module MakeBackendIO (B : Backend) = struct
(vc : Conditions.verification_condition * vc_encoding_result) : unit =
let vc, z3_vc = vc in
Cli.debug_print
(Format.asprintf "For this variable:\n%s\n"
(Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard)));
Cli.debug_print
(Format.asprintf "This verification condition was generated for %s:@\n%a"
(Cli.print_with_style [ ANSITerminal.yellow ] "%s"
(match vc.vc_kind with
| Conditions.NoEmptyError -> "the variable definition never to return an empty error"
| NoOverlappingExceptions -> "no two exceptions to ever overlap"))
(Dcalc.Print.format_expr decl_ctx)
vc.vc_guard);
Cli.debug_print "For this variable:\n%s\n"
(Pos.retrieve_loc_text (Pos.get_position vc.Conditions.vc_guard));
Cli.debug_format "This verification condition was generated for %a:@\n%a"
(Cli.format_with_style [ ANSITerminal.yellow ])
(match vc.vc_kind with
| Conditions.NoEmptyError -> "the variable definition never to return an empty error"
| NoOverlappingExceptions -> "no two exceptions to ever overlap")
(Dcalc.Print.format_expr decl_ctx)
vc.vc_guard;
match z3_vc with
| Success (encoding, backend_ctx) -> (
Cli.debug_print
(Format.asprintf "The translation to Z3 is the following:@\n%s"
(B.print_encoding encoding));
Cli.debug_print "The translation to Z3 is the following:@\n%s" (B.print_encoding encoding);
match B.solve_vc_encoding backend_ctx encoding with
| ProvenTrue -> Cli.result_print (print_positive_result vc)
| ProvenFalse model -> Cli.error_print (print_negative_result vc backend_ctx model)
| ProvenTrue -> Cli.result_print "%s" (print_positive_result vc)
| ProvenFalse model -> Cli.error_print "%s" (print_negative_result vc backend_ctx model)
| Unknown -> failwith "The solver failed at proving or disproving the VC")
| Fail msg -> Cli.error_print (Format.asprintf "The translation to Z3 failed:@\n%s" msg)
| Fail msg -> Cli.error_print "The translation to Z3 failed:@\n%s" msg
end

View File

@ -188,8 +188,8 @@ let print_model (ctx : context) (model : Model.model) : string =
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(Cli.with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(print_z3model_expr ctx (VarMap.find v ctx.ctx_var) e)
else
(* Declaration d is a function *)
@ -201,8 +201,8 @@ let print_model (ctx : context) (model : Model.model) : string =
let symbol_name = Symbol.to_string (FuncDecl.get_name d) in
let v = StringMap.find symbol_name ctx.ctx_z3vars in
Format.fprintf fmt "%s %s : %s"
(Cli.print_with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.print_with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(Cli.with_style [ ANSITerminal.blue ] "%s" "-->")
(Cli.with_style [ ANSITerminal.yellow ] "%s" (Bindlib.name_of v))
(* TODO: Model of a Z3 function should be pretty-printed *)
(Model.FuncInterp.to_string f)))
decls
@ -611,7 +611,7 @@ module Backend = struct
let translate_expr (ctx : backend_context) (e : Dcalc.Ast.expr Pos.marked) = translate_expr ctx e
let init_backend () = Cli.debug_print (Format.asprintf "Running Z3 version %s" Version.to_string)
let init_backend () = Cli.debug_print "Running Z3 version %s" Version.to_string
let make_context (decl_ctx : decl_ctx) (free_vars_typ : typ Pos.marked VarMap.t) : backend_context
=

File diff suppressed because it is too large Load Diff