Skip to content

Commit

Permalink
Fixes #270
Browse files Browse the repository at this point in the history
  • Loading branch information
@denismerigoux
denismerigoux committed Nov 15, 2024
1 parent cb7ab5a commit a2431ad
Show file tree
Hide file tree
Showing 2 changed files with 166 additions and 143 deletions.
4 changes: 2 additions & 2 deletions compiler/catala_utils/cli.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,8 +213,8 @@ module Flags = struct
& flag
& info ["no-fail-on-assert"]
~doc:
"Instead of aborting the execution on assertion failure, continues \
as if the assertion had succeeded and reports a warning."
"Instead of reporting an error on assertion failure, reports a \
warning and carry on with the interpretation as usual."

let flags =
let make
Expand Down
305 changes: 164 additions & 141 deletions compiler/shared_ast/interpreter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -804,13 +804,28 @@ let rec evaluate_expr :
match Mark.remove e with
| ELit (LBool true) -> Mark.add m (ELit LUnit)
| ELit (LBool false) ->
Message.warning "Assertion failed:@ %a"
(Print.UserFacing.expr lang)
(partially_evaluate_expr_for_assertion_failure_message ctx lang
(Expr.skip_wrappers e'));
if Global.options.stop_on_error then
raise Runtime.(Error (AssertionFailed, [Expr.pos_to_runtime pos]))
else Mark.add m (ELit LUnit)
else
let partially_evaluated_assertion_failure_expr =
partially_evaluate_expr_for_assertion_failure_message ctx lang
(Expr.skip_wrappers e')
in
(match Mark.remove partially_evaluated_assertion_failure_expr with
| ELit (LBool false) ->
if Global.options.no_fail_on_assert then
Message.warning ~pos "Assertion failed:"
else Message.delayed_error ~kind:Generic () ~pos "Assertion failed:"
| _ ->
if Global.options.no_fail_on_assert then
Message.warning ~pos "Assertion failed:@ %a"
(Print.UserFacing.expr lang)
partially_evaluated_assertion_failure_expr
else
Message.delayed_error ~kind:Generic () ~pos "Assertion failed:@ %a"
(Print.UserFacing.expr lang)
partially_evaluated_assertion_failure_expr);
Mark.add m (ELit LUnit)
| _ ->
Message.error ~pos:(Expr.pos e') "%a" Format.pp_print_text
"Expected a boolean literal for the result of this assertion (should \
Expand Down Expand Up @@ -885,6 +900,8 @@ and partially_evaluate_expr_for_assertion_failure_message :
];
},
Mark.get e )
(* TODO: improve this heuristic, because if the assertion is not [e1 <op> e2],
the error message merely displays [false]... *)
| _ -> evaluate_expr ctx lang e

let evaluate_expr_trace :
Expand Down Expand Up @@ -975,149 +992,155 @@ let delcustom e =

let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let e = Expr.unbox @@ Program.to_expr p s in
let ctx = p.decl_ctx in
match evaluate_expr_safe ctx p.lang (addcustom e) with
| (EAbs { tys = [((TStruct s_in, _) as _targs)]; _ }, mark_e) as e -> begin
(* At this point, the interpreter seeks to execute the scope but does not
have a way to retrieve input values from the command line. [taus] contain
the types of the scope arguments. For [context] arguments, we can provide
an empty thunked term. But for [input] arguments of another type, we
cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
let pos = Expr.mark_pos mark_e in
StructField.Map.map
(fun ty ->
match Mark.remove ty with
| TArrow (ty_in, (TOption _, _)) ->
(* Context args should return an option *)
Expr.make_abs
(List.map (fun _ -> Mark.ghost (Var.make "_")) ty_in)
(Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr
~name:Expr.option_enum mark_e
: (_, _) boxed_gexpr)
ty_in pos
| TTuple ((TArrow (ty_in, (TOption _, _)), _) :: _) ->
(* ... or a closure if closure conversion is enabled *)
Expr.make_tuple
[
Message.with_delayed_errors (fun () ->
let e = Expr.unbox @@ Program.to_expr p s in
let ctx = p.decl_ctx in
match evaluate_expr_safe ctx p.lang (addcustom e) with
| (EAbs { tys = [((TStruct s_in, _) as _targs)]; _ }, mark_e) as e ->
begin
(* At this point, the interpreter seeks to execute the scope but does
not have a way to retrieve input values from the command line. [taus]
contain the types of the scope arguments. For [context] arguments, we
can provide an empty thunked term. But for [input] arguments of
another type, we cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
let pos = Expr.mark_pos mark_e in
StructField.Map.map
(fun ty ->
match Mark.remove ty with
| TArrow (ty_in, (TOption _, _)) ->
(* Context args should return an option *)
Expr.make_abs
(List.map (fun _ -> Mark.ghost (Var.make "_")) ty_in)
(Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr
~name:Expr.option_enum mark_e)
ty_in (Expr.mark_pos mark_e);
Expr.eappop
~op:(Operator.ToClosureEnv, pos)
~args:[Expr.etuple [] mark_e]
~tys:[TClosureEnv, pos]
mark_e;
]
mark_e
| TOption ty ->
Expr.einj ~cons:Expr.none_constr ~name:Expr.option_enum
~e:
(Expr.elit LUnit (Expr.with_ty mark_e (TLit TUnit, Expr.pos e)))
(Expr.with_ty mark_e (TOption ty, Expr.pos e))
| _ ->
Message.error ~pos:(Mark.get ty)
"This scope needs an input argument of type@ %a@ %a"
Print.typ_debug ty Format.pp_print_text
"to be executed. But the Catala built-in interpreter does not \
have a way to retrieve input values from the command line, so \
it cannot execute this scope. Please create another scope that \
provides the input arguments to this one and execute it \
instead.")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[
Expr.estruct ~name:s_in ~fields:application_term
(Expr.map_ty (fun (_, pos) -> TStruct s_in, pos) mark_e);
]
[TStruct s_in, Expr.pos e]
(Expr.pos e)
in
match
Mark.remove (evaluate_expr_safe ctx p.lang (Expr.unbox to_interpret))
with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| exception Runtime.Error (err, rpos) ->
Message.error
~extra_pos:(List.map (fun rp -> "", Expr.runtime_to_pos rp) rpos)
"%a" Format.pp_print_text
(Runtime.error_message err)
| _ ->
Message.error ~pos:(Expr.pos e) ~internal:true "%a" Format.pp_print_text
"The interpretation of the program doesn't yield a struct \
corresponding to the scope variables"
end
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpreter can only interpret terms starting with functions having \
thunked arguments"
~name:Expr.option_enum mark_e
: (_, _) boxed_gexpr)
ty_in pos
| TTuple ((TArrow (ty_in, (TOption _, _)), _) :: _) ->
(* ... or a closure if closure conversion is enabled *)
Expr.make_tuple
[
Expr.make_abs
(List.map (fun _ -> Mark.ghost (Var.make "_")) ty_in)
(Expr.einj ~e:(Expr.elit LUnit mark_e)
~cons:Expr.none_constr ~name:Expr.option_enum mark_e)
ty_in (Expr.mark_pos mark_e);
Expr.eappop
~op:(Operator.ToClosureEnv, pos)
~args:[Expr.etuple [] mark_e]
~tys:[TClosureEnv, pos]
mark_e;
]
mark_e
| TOption ty ->
Expr.einj ~cons:Expr.none_constr ~name:Expr.option_enum
~e:
(Expr.elit LUnit
(Expr.with_ty mark_e (TLit TUnit, Expr.pos e)))
(Expr.with_ty mark_e (TOption ty, Expr.pos e))
| _ ->
Message.error ~pos:(Mark.get ty)
"This scope needs an input argument of type@ %a@ %a"
Print.typ_debug ty Format.pp_print_text
"to be executed. But the Catala built-in interpreter does \
not have a way to retrieve input values from the command \
line, so it cannot execute this scope. Please create \
another scope that provides the input arguments to this one \
and execute it instead.")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[
Expr.estruct ~name:s_in ~fields:application_term
(Expr.map_ty (fun (_, pos) -> TStruct s_in, pos) mark_e);
]
[TStruct s_in, Expr.pos e]
(Expr.pos e)
in
match
Mark.remove (evaluate_expr_safe ctx p.lang (Expr.unbox to_interpret))
with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| exception Runtime.Error (err, rpos) ->
Message.error
~extra_pos:(List.map (fun rp -> "", Expr.runtime_to_pos rp) rpos)
"%a" Format.pp_print_text
(Runtime.error_message err)
| _ ->
Message.error ~pos:(Expr.pos e) ~internal:true "%a"
Format.pp_print_text
"The interpretation of the program doesn't yield a struct \
corresponding to the scope variables"
end
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpreter can only interpret terms starting with functions \
having thunked arguments")

(** {1 API} *)
let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let ctx = p.decl_ctx in
let e = Expr.unbox (Program.to_expr p s) in
match evaluate_expr_safe p.decl_ctx p.lang (addcustom e) with
| (EAbs { tys = [((TStruct s_in, _) as _targs)]; _ }, mark_e) as e -> begin
(* At this point, the interpreter seeks to execute the scope but does not
have a way to retrieve input values from the command line. [taus] contain
the types of the scope arguments. For [context] arguments, we can provide
an empty thunked term. But for [input] arguments of another type, we
cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
StructField.Map.map
(fun ty0 ->
match Mark.remove ty0 with
| TArrow (ty_in, ty_out) ->
Expr.make_abs
(List.map (fun _ -> Mark.ghost (Var.make "_")) ty_in)
(Bindlib.box EEmpty, Expr.with_ty mark_e ty_out)
ty_in (Expr.mark_pos mark_e)
| TDefault _ -> Bindlib.box EEmpty, Expr.with_ty mark_e ty0
| _ ->
Message.error ~pos:(Mark.get ty0) "%a" Format.pp_print_text
"This scope needs input arguments to be executed. But the Catala \
built-in interpreter does not have a way to retrieve input \
values from the command line, so it cannot execute this scope. \
Please create another scope that provides the input arguments \
to this one and execute it instead.")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[
Expr.estruct ~name:s_in ~fields:application_term
(Expr.map_ty (fun (_, pos) -> TStruct s_in, pos) mark_e);
]
[TStruct s_in, Expr.pos e]
(Expr.pos e)
in
match
Mark.remove (evaluate_expr_safe ctx p.lang (Expr.unbox to_interpret))
with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpretation of a program should always yield a struct \
corresponding to the scope variables"
end
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpreter can only interpret terms starting with functions having \
thunked arguments"
Message.with_delayed_errors (fun () ->
let ctx = p.decl_ctx in
let e = Expr.unbox (Program.to_expr p s) in
match evaluate_expr_safe p.decl_ctx p.lang (addcustom e) with
| (EAbs { tys = [((TStruct s_in, _) as _targs)]; _ }, mark_e) as e ->
begin
(* At this point, the interpreter seeks to execute the scope but does
not have a way to retrieve input values from the command line. [taus]
contain the types of the scope arguments. For [context] arguments, we
can provide an empty thunked term. But for [input] arguments of
another type, we cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
StructField.Map.map
(fun ty0 ->
match Mark.remove ty0 with
| TArrow (ty_in, ty_out) ->
Expr.make_abs
(List.map (fun _ -> Mark.ghost (Var.make "_")) ty_in)
(Bindlib.box EEmpty, Expr.with_ty mark_e ty_out)
ty_in (Expr.mark_pos mark_e)
| TDefault _ -> Bindlib.box EEmpty, Expr.with_ty mark_e ty0
| _ ->
Message.error ~pos:(Mark.get ty0) "%a" Format.pp_print_text
"This scope needs input arguments to be executed. But the \
Catala built-in interpreter does not have a way to retrieve \
input values from the command line, so it cannot execute \
this scope. Please create another scope that provides the \
input arguments to this one and execute it instead.")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[
Expr.estruct ~name:s_in ~fields:application_term
(Expr.map_ty (fun (_, pos) -> TStruct s_in, pos) mark_e);
]
[TStruct s_in, Expr.pos e]
(Expr.pos e)
in
match
Mark.remove (evaluate_expr_safe ctx p.lang (Expr.unbox to_interpret))
with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpretation of a program should always yield a struct \
corresponding to the scope variables"
end
| _ ->
Message.error ~pos:(Expr.pos e) "%a" Format.pp_print_text
"The interpreter can only interpret terms starting with functions \
having thunked arguments")

(* Evaluation may introduce intermediate custom terms ([ECustom], pointers to
external functions), straying away from the DCalc and LCalc ASTS. [addcustom]
Expand Down

0 comments on commit a2431ad

Please sign in to comment.