CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

correct typo in vc generation for conflict error

Browse Source 
add some debug in comments
This commit is contained in:
Alain 2022-01-10 17:29:53 +01:00
parent baa435d2c5
commit 0c2dbdddd1
1 changed files with 13 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
compiler/verification/conditions.ml
View File

@ -132,7 +132,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Pos.marked) : ex
conjunction (List.map (generate_vs_must_not_return_confict ctx) (f::args)) (Pos.get_position e)
| EIfThenElse (e1, e2, e3) ->
conjunction (List.map (generate_vs_must_not_return_confict ctx) [e1; e2; e3]) (Pos.get_position e)
| ELit _ | EOp _ -> Pos.same_pos_as (ELit (LBool false)) e
| EVar _ | ELit _ | EOp _ -> Pos.same_pos_as (ELit (LBool true)) e
| EDefault (exceptions, just, cons) ->
(* <e1 ... en | ejust :- econs > never returns conflict if and only if:
@ -153,13 +153,23 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : expr Pos.marked) : ex
)
(Pos.get_position e)
in
conjunction (quadratic :: (List.map (generate_vs_must_not_return_confict ctx) (just :: cons :: exceptions))) (Pos.get_position e)
let others = (List.map (generate_vs_must_not_return_confict ctx) (just :: cons :: exceptions)) in
let out = conjunction (quadratic :: others) (Pos.get_position e) in
(* let _ = Cli.debug_print
(Format.asprintf ">>> Conflict, Input:@\n%a@\nQuadratic:@\n%a@\nOthers:@\n%a@\nOutput:@\n%a"
(Print.format_expr ctx.decl) e
(Print.format_expr ctx.decl) (Bindlib.unbox (Optimizations.optimize_expr quadratic))
(Print.format_expr ctx.decl) (Bindlib.unbox (Optimizations.optimize_expr (conjunction others (Pos.get_position e))))
(Print.format_expr ctx.decl) (Bindlib.unbox (Optimizations.optimize_expr out))) in *)
out
| _ -> assert false
in
out