remove logs from the no_partial_evaluation invariant

removed error_on_empty when functions
This commit is contained in:
adelaett 2023-02-20 15:48:56 +01:00
parent b5f3621302
commit 75dc978fa9
4 changed files with 25 additions and 13 deletions

View File

@ -486,9 +486,15 @@ let debug_format (format : ('a, Format.formatter, unit) format) =
let error_print (format : ('a, out_channel, unit) format) =
Printf.eprintf ("%s" ^^ format ^^ "\n%!") (error_marker ())
let error_format (format : ('a, Format.formatter, unit) format) =
Format.eprintf ("%s" ^^ format ^^ "\n%!") (error_marker ())
let warning_print (format : ('a, out_channel, unit) format) =
Printf.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())
let warning_format (format : ('a, Format.formatter, unit) format) =
Format.printf ("%s" ^^ format ^^ "\n%!") (warning_marker ())
let result_print (format : ('a, out_channel, unit) format) =
Printf.printf ("%s" ^^ format ^^ "\n%!") (result_marker ())

View File

@ -142,11 +142,13 @@ 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 : ('a, out_channel, unit) format -> 'a
val debug_format : ('a, Format.formatter, unit) format -> 'a
val debug_print : ('a, out_channel, unit) format -> 'a
val error_format : ('a, Format.formatter, unit) format -> 'a
val error_print : ('a, out_channel, unit) format -> 'a
val warning_print : ('a, out_channel, unit) format -> 'a
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
val log_print : ('a, out_channel, unit) format -> 'a
val result_format : ('a, Format.formatter, unit) format -> 'a
val result_print : ('a, out_channel, unit) format -> 'a
val warning_format : ('a, Format.formatter, unit) format -> 'a
val warning_print : ('a, out_channel, unit) format -> 'a

View File

@ -580,16 +580,16 @@ let translate_rule
let a_var = Var.make (Marked.unmark a_name) in
let new_e = translate_expr ctx e in
let a_expr = Expr.make_var a_var (pos_mark var_def_pos) in
let is_func =
match Marked.unmark tau with TArrow _ -> true | _ -> false
in
let merged_expr =
match Marked.unmark a_io.io_input with
| OnlyInput -> failwith "should not happen"
(* scopelang should not contain any definitions of input only variables *)
| Reentrant ->
merge_defaults
~is_func:
(match Marked.unmark tau with TArrow _ -> true | _ -> false)
a_expr new_e
| NoInput -> Expr.eerroronempty new_e (pos_mark_as a_name)
| Reentrant -> merge_defaults ~is_func a_expr new_e
| NoInput ->
if is_func then new_e else Expr.eerroronempty new_e (pos_mark_as a_name)
in
let merged_expr =
tag_with_log_entry merged_expr

View File

@ -23,6 +23,9 @@ let invariant_no_partial_evaluation () : string * invariant_expr =
( __FUNCTION__,
fun e ->
match Marked.unmark e with
| EApp { f = EOp { op = Op.Log _; _ }, _; _ } ->
(* logs are differents. *)
Some true
| EApp _ -> begin
match Marked.unmark (Expr.ty e) with
| TArrow _ -> Some false
@ -57,9 +60,10 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) =
match inv e with
| None -> true
| Some false ->
Cli.error_print "%s Invariant failed %s."
Cli.error_format "%s failed in %s.\n\n %a" name
(Pos.to_string_short (Expr.pos e))
name;
(Print.expr ~debug:true p.decl_ctx)
e;
incr total;
false
| Some true ->