CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 00:41:05 +03:00
Code Issues Projects Releases Wiki Activity

Fix bug

Browse Source
This commit is contained in:
Denis Merigoux 2022-03-17 17:52:26 +01:00
parent a7bdc0a114
commit 6722cf9647
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
1 changed files with 73 additions and 69 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
compiler/verification/conditions.ml
View File

@ -303,77 +303,81 @@ let generate_verification_conditions
verification_condition list =
List.fold_left
(fun acc (s_name, _s_var, s_body) ->
match s with
| Some s when Dcalc.Ast.ScopeName.compare s s_name = 0 ->
let ctx = { decl = p.decl_ctx; input_vars = [] } in
let acc, _ =
List.fold_left
(fun (acc, ctx) s_let ->
match s_let.scope_let_kind with
| DestructuringInputStruct ->
( acc,
let is_selected_scope =
match s with
| Some s when Dcalc.Ast.ScopeName.compare s s_name = 0 -> true
| None -> true
| _ -> false
in
if is_selected_scope then
let ctx = { decl = p.decl_ctx; input_vars = [] } in
let acc, _ =
List.fold_left
(fun (acc, ctx) s_let ->
match s_let.scope_let_kind with
| DestructuringInputStruct ->
( acc,
{
ctx with
input_vars =
Pos.unmark s_let.scope_let_var :: ctx.input_vars;
} )
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never
evaluate to emptyError nor conflictError. But for subscope
variable definitions, what we're really doing is adding
exceptions to something defined in the subscope so we just
ought to verify only that the exceptions overlap. *)
let e =
match_and_ignore_outer_reentrant_default ctx
(Bindlib.unbox s_let.scope_let_expr)
in
let vc_confl, vc_confl_typs =
generate_vs_must_not_return_confict ctx e
in
let vc_confl =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr p.decl_ctx vc_confl)
else vc_confl
in
let vc_list =
[
{
ctx with
input_vars =
Pos.unmark s_let.scope_let_var :: ctx.input_vars;
} )
| ScopeVarDefinition | SubScopeVarDefinition ->
(* For scope variables, we should check both that they never
evaluate to emptyError nor conflictError. But for
subscope variable definitions, what we're really doing is
adding exceptions to something defined in the subscope so
we just ought to verify only that the exceptions
overlap. *)
let e =
match_and_ignore_outer_reentrant_default ctx
(Bindlib.unbox s_let.scope_let_expr)
in
let vc_confl, vc_confl_typs =
generate_vs_must_not_return_confict ctx e
in
let vc_confl =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr p.decl_ctx vc_confl)
else vc_confl
in
let vc_list =
[
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
vc_kind = NoOverlappingExceptions;
vc_free_vars_typ = vc_confl_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
};
]
in
let vc_list =
match s_let.scope_let_kind with
| ScopeVarDefinition ->
let vc_empty, vc_empty_typs =
generate_vc_must_not_return_empty ctx e
in
let vc_empty =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr p.decl_ctx vc_empty)
else vc_empty
in
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_confl) e;
vc_kind = NoOverlappingExceptions;
vc_free_vars_typ = vc_confl_typs;
vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e;
vc_kind = NoEmptyError;
vc_free_vars_typ = vc_empty_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
};
]
in
let vc_list =
match s_let.scope_let_kind with
| ScopeVarDefinition ->
let vc_empty, vc_empty_typs =
generate_vc_must_not_return_empty ctx e
in
let vc_empty =
if !Cli.optimize_flag then
Bindlib.unbox
(Optimizations.optimize_expr p.decl_ctx vc_empty)
else vc_empty
in
{
vc_guard = Pos.same_pos_as (Pos.unmark vc_empty) e;
vc_kind = NoEmptyError;
vc_free_vars_typ = vc_empty_typs;
vc_scope = s_name;
vc_variable = s_let.scope_let_var;
}
:: vc_list
| _ -> vc_list
in
(vc_list @ acc, ctx)
| _ -> (acc, ctx))
(acc, ctx) s_body.scope_body_lets
in
acc
| Some _ | None -> acc)
}
:: vc_list
| _ -> vc_list
in
(vc_list @ acc, ctx)
| _ -> (acc, ctx))
(acc, ctx) s_body.scope_body_lets
in
acc
else acc)
[] p.scopes