From 8d2348d1d93b24ffa7dfda9e0f0d860837e71b93 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 24 Mar 2022 17:15:22 +0100 Subject: [PATCH 01/10] [Z3 encoding] Add support for Duration type and operators --- compiler/verification/z3backend.real.ml | 48 +++++-------------------- 1 file changed, 9 insertions(+), 39 deletions(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 532602b5..5f5254c3 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -153,9 +153,7 @@ let rec print_z3model_expr (ctx : context) (ty : typ Pos.marked) (e : Expr.expr) 1900. We pretty-print it as the actual date *) (* TODO: Use differnt dates conventions depending on the language ? *) | TDate -> nb_days_to_date (int_of_string (Expr.to_string e)) - | TDuration -> - failwith - "[Z3 model]: Pretty-printing of duration literals not supported" + | TDuration -> Format.asprintf "%s days" (Expr.to_string e) in match Pos.unmark ty with @@ -261,7 +259,7 @@ let translate_typ_lit (ctx : context) (t : typ_lit) : Sort.sort = (* Dates are encoded as integers, corresponding to the number of days since Jan 1, 1900 *) | TDate -> Arithmetic.Integer.mk_sort ctx.ctx_z3 - | TDuration -> failwith "[Z3 encoding] TDuration type not supported" + | TDuration -> Arithmetic.Integer.mk_sort ctx.ctx_z3 (** [translate_typ] returns the Z3 sort correponding to the Catala type [t] **) let rec translate_typ (ctx : context) (t : typ) : context * Sort.sort = @@ -524,54 +522,26 @@ let rec translate_op | And -> (ctx, Boolean.mk_and ctx.ctx_z3 [ e1; e2 ]) | Or -> (ctx, Boolean.mk_or ctx.ctx_z3 [ e1; e2 ]) | Xor -> (ctx, Boolean.mk_xor ctx.ctx_z3 e1 e2) - | Add KInt | Add KRat | Add KMoney -> + | Add KInt | Add KRat | Add KMoney | Add KDate | Add KDuration -> (ctx, Arithmetic.mk_add ctx.ctx_z3 [ e1; e2 ]) - | Add _ -> - failwith - "[Z3 encoding] application of non-integer binary operator Add \ - not supported" - | Sub KInt | Sub KRat | Sub KMoney -> + | Sub KInt | Sub KRat | Sub KMoney | Sub KDate | Sub KDuration -> (ctx, Arithmetic.mk_sub ctx.ctx_z3 [ e1; e2 ]) - | Sub _ -> - failwith - "[Z3 encoding] application of non-integer binary operator Sub \ - not supported" - | Mult KInt | Mult KRat | Mult KMoney -> + | Mult KInt | Mult KRat | Mult KMoney | Mult KDate | Mult KDuration -> (ctx, Arithmetic.mk_mul ctx.ctx_z3 [ e1; e2 ]) - | Mult _ -> - failwith - "[Z3 encoding] application of non-integer binary operator Mult \ - not supported" | Div KInt | Div KRat | Div KMoney -> (ctx, Arithmetic.mk_div ctx.ctx_z3 e1 e2) | Div _ -> failwith "[Z3 encoding] application of non-integer binary operator Div \ not supported" - | Lt KInt | Lt KRat | Lt KMoney | Lt KDate -> + | Lt KInt | Lt KRat | Lt KMoney | Lt KDate | Lt KDuration -> (ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2) - | Lt _ -> - failwith - "[Z3 encoding] application of non-integer or money binary \ - operator Lt not supported" - | Lte KInt | Lte KRat | Lte KMoney | Lte KDate -> + | Lte KInt | Lte KRat | Lte KMoney | Lte KDate | Lte KDuration -> (ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2) - | Lte _ -> - failwith - "[Z3 encoding] application of non-integer or money binary \ - operator Lte not supported" - | Gt KInt | Gt KRat | Gt KMoney | Gt KDate -> + | Gt KInt | Gt KRat | Gt KMoney | Gt KDate | Gt KDuration -> (ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2) - | Gt _ -> - failwith - "[Z3 encoding] application of non-integer or money binary \ - operator Gt not supported" - | Gte KInt | Gte KRat | Gte KMoney | Gte KDate -> + | Gte KInt | Gte KRat | Gte KMoney | Gte KDate | Gte KDuration -> (ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2) - | Gte _ -> - failwith - "[Z3 encoding] application of non-integer or money binary \ - operator Gte not supported" | Eq -> (ctx, Boolean.mk_eq ctx.ctx_z3 e1 e2) | Neq -> (ctx, Boolean.mk_not ctx.ctx_z3 (Boolean.mk_eq ctx.ctx_z3 e1 e2)) From e2963bd7f30531774477bf2f265b0629221667b7 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 24 Mar 2022 17:22:16 +0100 Subject: [PATCH 02/10] Add a duration_to_nb_days function to runtime --- compiler/runtime.ml | 2 ++ compiler/runtime.mli | 1 + 2 files changed, 3 insertions(+) diff --git a/compiler/runtime.ml b/compiler/runtime.ml index 49a91c94..92795786 100644 --- a/compiler/runtime.ml +++ b/compiler/runtime.ml @@ -187,6 +187,8 @@ let duration_to_string (d : duration) : string = let duration_to_years_months_days (d : duration) : int * int * int = CalendarLib.Date.Period.ymd d +let duration_to_nb_days (d : duration) : int = CalendarLib.Date.Period.nb_days d + let handle_default : 'a. (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) -> 'a = fun exceptions just cons -> diff --git a/compiler/runtime.mli b/compiler/runtime.mli index be16be9c..12cb7f4c 100644 --- a/compiler/runtime.mli +++ b/compiler/runtime.mli @@ -129,6 +129,7 @@ val date_of_numbers : int -> int -> int -> date val duration_of_numbers : int -> int -> int -> duration val duration_to_years_months_days : duration -> int * int * int +val duration_to_nb_days : duration -> int val duration_to_string : duration -> string (**{1 Defaults} *) From 2c247128d1f97f743d4be43da6032b60cfc89067 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 24 Mar 2022 17:22:31 +0100 Subject: [PATCH 03/10] [Z3encoding] Add support for duration literals --- compiler/verification/z3backend.real.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 5f5254c3..2f39279f 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -376,7 +376,8 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = (* Encoding a date as an integer corresponding to the number of days since Jan 1, 1900 *) | LDate d -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int d) - | LDuration _ -> failwith "[Z3 encoding] LDuration literals not supported" + | LDuration d -> + Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.duration_to_nb_days d) (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration corresponding to the variable [v]. If no such function declaration exists From 55dd389819d1efe4aff4e213aaf066cea9aa167a Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 24 Mar 2022 17:23:31 +0100 Subject: [PATCH 04/10] [Z3encoding] Add good unit tests for duration --- tests/test_proof/good/duration.catala_en | 12 ++++++++++++ .../test_proof/good/output/duration.catala_en.Proof | 4 ++++ 2 files changed, 16 insertions(+) create mode 100644 tests/test_proof/good/duration.catala_en create mode 100644 tests/test_proof/good/output/duration.catala_en.Proof diff --git a/tests/test_proof/good/duration.catala_en b/tests/test_proof/good/duration.catala_en new file mode 100644 index 00000000..d28df109 --- /dev/null +++ b/tests/test_proof/good/duration.catala_en @@ -0,0 +1,12 @@ +## Test + +```catala +declaration scope A: + context x content duration + context y content boolean + +scope A: + definition x equals 94 day + definition y under condition (x +^ x) >^ 100 day consequence equals true + definition y under condition (x +^ x) <=^ 100 day consequence equals false +``` diff --git a/tests/test_proof/good/output/duration.catala_en.Proof b/tests/test_proof/good/output/duration.catala_en.Proof new file mode 100644 index 00000000..ebe1a223 --- /dev/null +++ b/tests/test_proof/good/output/duration.catala_en.Proof @@ -0,0 +1,4 @@ +[RESULT] [A.y] This variable never returns an empty error +[RESULT] [A.y] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable From cca2e00d4214b09cae7160c0561b3ab39a6fd3a8 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 24 Mar 2022 17:27:03 +0100 Subject: [PATCH 05/10] [Z3encoding] Add bad unit tests for duration --- tests/test_proof/bad/duration-empty.catala_en | 11 +++++++++++ tests/test_proof/bad/duration-overlap.catala_en | 12 ++++++++++++ .../bad/output/duration-empty.catala_en.Proof | 10 ++++++++++ .../bad/output/duration-overlap.catala_en.Proof | 10 ++++++++++ 4 files changed, 43 insertions(+) create mode 100644 tests/test_proof/bad/duration-empty.catala_en create mode 100644 tests/test_proof/bad/duration-overlap.catala_en create mode 100644 tests/test_proof/bad/output/duration-empty.catala_en.Proof create mode 100644 tests/test_proof/bad/output/duration-overlap.catala_en.Proof diff --git a/tests/test_proof/bad/duration-empty.catala_en b/tests/test_proof/bad/duration-empty.catala_en new file mode 100644 index 00000000..e506b9f5 --- /dev/null +++ b/tests/test_proof/bad/duration-empty.catala_en @@ -0,0 +1,11 @@ +## Test + +```catala +declaration scope A: + context x content duration + context y content boolean + +scope A: + definition x equals 94 day + definition y under condition (x +^ x) >^ 100 day consequence equals true +``` diff --git a/tests/test_proof/bad/duration-overlap.catala_en b/tests/test_proof/bad/duration-overlap.catala_en new file mode 100644 index 00000000..655c443d --- /dev/null +++ b/tests/test_proof/bad/duration-overlap.catala_en @@ -0,0 +1,12 @@ +## Test + +```catala +declaration scope A: + context x content duration + context y content boolean + +scope A: + definition x equals 94 day + definition y under condition (x +^ x) >=^ 100 day consequence equals true + definition y under condition (x +^ x) <=^ 100 day consequence equals false +``` diff --git a/tests/test_proof/bad/output/duration-empty.catala_en.Proof b/tests/test_proof/bad/output/duration-empty.catala_en.Proof new file mode 100644 index 00000000..7cc33eb7 --- /dev/null +++ b/tests/test_proof/bad/output/duration-empty.catala_en.Proof @@ -0,0 +1,10 @@ +[ERROR] [A.y] This variable might return an empty error: + --> tests/test_proof/bad/duration-empty.catala_en + | +6 | context y content boolean + | ^ + + Test +Counterexample generation is disabled so none was generated. +[RESULT] [A.y] No two exceptions to ever overlap for this variable +[RESULT] [A.x] This variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable diff --git a/tests/test_proof/bad/output/duration-overlap.catala_en.Proof b/tests/test_proof/bad/output/duration-overlap.catala_en.Proof new file mode 100644 index 00000000..c3b0444c --- /dev/null +++ b/tests/test_proof/bad/output/duration-overlap.catala_en.Proof @@ -0,0 +1,10 @@ +[RESULT] [A.y] This variable never returns an empty error +[ERROR] [A.y] At least two exceptions overlap for this variable: + --> tests/test_proof/bad/duration-overlap.catala_en + | +6 | context y content boolean + | ^ + + Test +Counterexample generation is disabled so none was generated. +[RESULT] [A.x] This variable never returns an empty error +[RESULT] [A.x] No two exceptions to ever overlap for this variable From ce7e756af1efed4154d496760a4ecc87dd3d8ac0 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Mon, 28 Mar 2022 14:43:38 +0200 Subject: [PATCH 06/10] Nice error messages for empty structs and enums --- compiler/surface/name_resolution.ml | 12 ++++++++++++ compiler/surface/parser.messages | 11 +++++------ compiler/surface/parser.mly | 2 +- tests/test_enum/bad/empty.catala_en | 8 ++++++++ tests/test_enum/bad/output/empty.catala_en.Typecheck | 7 +++++++ tests/test_struct/bad/empty_struct.catala_en | 8 ++++++++ .../bad/output/empty_struct.catala_en.Typecheck | 7 +++++++ 7 files changed, 48 insertions(+), 7 deletions(-) create mode 100644 tests/test_enum/bad/empty.catala_en create mode 100644 tests/test_enum/bad/output/empty.catala_en.Typecheck create mode 100644 tests/test_struct/bad/empty_struct.catala_en create mode 100644 tests/test_struct/bad/output/empty_struct.catala_en.Typecheck diff --git a/compiler/surface/name_resolution.ml b/compiler/surface/name_resolution.ml index f191f230..4bf3dee4 100644 --- a/compiler/surface/name_resolution.ml +++ b/compiler/surface/name_resolution.ml @@ -377,6 +377,12 @@ let process_struct_decl (ctxt : context) (sdecl : Ast.struct_decl) : context = let s_uid = Desugared.Ast.IdentMap.find (fst sdecl.struct_decl_name) ctxt.struct_idmap in + if List.length sdecl.struct_decl_fields = 0 then + Errors.raise_spanned_error + (Pos.get_position sdecl.struct_decl_name) + "The struct %s does not have any fields; give it some for Catala to be \ + able to accept it." + (Pos.unmark sdecl.struct_decl_name); List.fold_left (fun ctxt (fdecl, _) -> let f_uid = @@ -420,6 +426,12 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context = let e_uid = Desugared.Ast.IdentMap.find (fst edecl.enum_decl_name) ctxt.enum_idmap in + if List.length edecl.enum_decl_cases = 0 then + Errors.raise_spanned_error + (Pos.get_position edecl.enum_decl_name) + "The enum %s does not have any cases; give it some for Catala to be able \ + to accept it." + (Pos.unmark edecl.enum_decl_name); List.fold_left (fun ctxt (cdecl, cdecl_pos) -> let c_uid = diff --git a/compiler/surface/parser.messages b/compiler/surface/parser.messages index 34df2002..68b62cfe 100644 --- a/compiler/surface/parser.messages +++ b/compiler/surface/parser.messages @@ -2,8 +2,7 @@ source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON ALT CONSTRUCTOR CONTE ## ## Ends in an error in state: 358. ## -## nonempty_list(enum_decl_line) -> enum_decl_line . [ SCOPE END_CODE DECLARATION ] -## nonempty_list(enum_decl_line) -> enum_decl_line . nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] +## list(enum_decl_line) -> enum_decl_line . list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] ## ## The known suffix of the stack is as follows: ## enum_decl_line @@ -51,7 +50,7 @@ source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR COLON YEAR ## ## Ends in an error in state: 350. ## -## code_item -> DECLARATION ENUM constructor COLON . nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] +## code_item -> DECLARATION ENUM constructor COLON . list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] ## ## The known suffix of the stack is as follows: ## DECLARATION ENUM constructor COLON @@ -63,7 +62,7 @@ source_file: BEGIN_CODE DECLARATION ENUM CONSTRUCTOR YEAR ## ## Ends in an error in state: 349. ## -## code_item -> DECLARATION ENUM constructor . COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] +## code_item -> DECLARATION ENUM constructor . COLON list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] ## ## The known suffix of the stack is as follows: ## DECLARATION ENUM constructor @@ -75,7 +74,7 @@ source_file: BEGIN_CODE DECLARATION ENUM YEAR ## ## Ends in an error in state: 348. ## -## code_item -> DECLARATION ENUM . constructor COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] +## code_item -> DECLARATION ENUM . constructor COLON list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] ## ## The known suffix of the stack is as follows: ## DECLARATION ENUM @@ -264,7 +263,7 @@ source_file: BEGIN_CODE DECLARATION YEAR ## ## code_item -> DECLARATION . STRUCT constructor COLON list(struct_scope) [ SCOPE END_CODE DECLARATION ] ## code_item -> DECLARATION . SCOPE constructor COLON nonempty_list(scope_decl_item) [ SCOPE END_CODE DECLARATION ] -## code_item -> DECLARATION . ENUM constructor COLON nonempty_list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] +## code_item -> DECLARATION . ENUM constructor COLON list(enum_decl_line) [ SCOPE END_CODE DECLARATION ] ## ## The known suffix of the stack is as follows: ## DECLARATION diff --git a/compiler/surface/parser.mly b/compiler/surface/parser.mly index c77ada03..ddf35032 100644 --- a/compiler/surface/parser.mly +++ b/compiler/surface/parser.mly @@ -617,7 +617,7 @@ code_item: scope_decl_context = context; }, Pos.from_lpos $sloc) } -| DECLARATION ENUM c = constructor COLON cases = nonempty_list(enum_decl_line) { +| DECLARATION ENUM c = constructor COLON cases = list(enum_decl_line) { (EnumDecl { enum_decl_name = c; enum_decl_cases = cases; diff --git a/tests/test_enum/bad/empty.catala_en b/tests/test_enum/bad/empty.catala_en new file mode 100644 index 00000000..e4b60af8 --- /dev/null +++ b/tests/test_enum/bad/empty.catala_en @@ -0,0 +1,8 @@ +## Test + +```catala +declaration enumeration Foo: + +declaration scope Bar: + internal foo content Foo +``` diff --git a/tests/test_enum/bad/output/empty.catala_en.Typecheck b/tests/test_enum/bad/output/empty.catala_en.Typecheck new file mode 100644 index 00000000..24b3677b --- /dev/null +++ b/tests/test_enum/bad/output/empty.catala_en.Typecheck @@ -0,0 +1,7 @@ +[ERROR] The enum Foo does not have any cases; give it some for Catala to be able to accept it. + + --> tests/test_enum/bad/empty.catala_en + | +4 | declaration enumeration Foo: + | ^^^ + + Test diff --git a/tests/test_struct/bad/empty_struct.catala_en b/tests/test_struct/bad/empty_struct.catala_en new file mode 100644 index 00000000..f5a63e9d --- /dev/null +++ b/tests/test_struct/bad/empty_struct.catala_en @@ -0,0 +1,8 @@ +## Test + +```catala +declaration structure Foo: + +declaration scope Bar: + internal foo content Foo +``` diff --git a/tests/test_struct/bad/output/empty_struct.catala_en.Typecheck b/tests/test_struct/bad/output/empty_struct.catala_en.Typecheck new file mode 100644 index 00000000..1b4fcf3d --- /dev/null +++ b/tests/test_struct/bad/output/empty_struct.catala_en.Typecheck @@ -0,0 +1,7 @@ +[ERROR] The struct Foo does not have any fields; give it some for Catala to be able to accept it. + + --> tests/test_struct/bad/empty_struct.catala_en + | +4 | declaration structure Foo: + | ^^^ + + Test From 5d36af01e32f0a9734dbac6b948e5af7eeba0c04 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Mon, 28 Mar 2022 15:16:03 +0200 Subject: [PATCH 07/10] Restore the trace parameter functionality in the web interpreter --- compiler/catala_web_interpreter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/catala_web_interpreter.ml b/compiler/catala_web_interpreter.ml index cc842a5d..6f1ea48d 100644 --- a/compiler/catala_web_interpreter.ml +++ b/compiler/catala_web_interpreter.ml @@ -19,7 +19,7 @@ let _ = backend = "Interpret"; language = Some (Js.to_string language); max_prec_digits = None; - trace = false; + trace; disable_counterexamples = false; optimize = false; ex_scope = Some (Js.to_string scope); From 2b0206a5a8975f1bbc338b5a730b500419bef85a Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Mon, 28 Mar 2022 18:47:13 +0200 Subject: [PATCH 08/10] Restrict duration z3 encoding to days only --- compiler/verification/z3backend.real.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 2f39279f..7d9e4abe 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -377,6 +377,11 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = 1, 1900 *) | LDate d -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int d) | LDuration d -> + let y, m, _ = Runtime.duration_to_years_months_days d in + if y <> 0 || m <> 0 then + failwith + "[Z3 encoding]: Duration literals containing years or months not \ + supported"; Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.duration_to_nb_days d) (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration From 158d49fe86b5e96b04ae387dc013f980295c2a18 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Mon, 28 Mar 2022 18:59:53 +0200 Subject: [PATCH 09/10] Removed unnecessary extra runtime function --- compiler/runtime.ml | 2 -- compiler/runtime.mli | 1 - compiler/verification/z3backend.real.ml | 4 ++-- 3 files changed, 2 insertions(+), 5 deletions(-) diff --git a/compiler/runtime.ml b/compiler/runtime.ml index 92795786..49a91c94 100644 --- a/compiler/runtime.ml +++ b/compiler/runtime.ml @@ -187,8 +187,6 @@ let duration_to_string (d : duration) : string = let duration_to_years_months_days (d : duration) : int * int * int = CalendarLib.Date.Period.ymd d -let duration_to_nb_days (d : duration) : int = CalendarLib.Date.Period.nb_days d - let handle_default : 'a. (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) -> 'a = fun exceptions just cons -> diff --git a/compiler/runtime.mli b/compiler/runtime.mli index 12cb7f4c..be16be9c 100644 --- a/compiler/runtime.mli +++ b/compiler/runtime.mli @@ -129,7 +129,6 @@ val date_of_numbers : int -> int -> int -> date val duration_of_numbers : int -> int -> int -> duration val duration_to_years_months_days : duration -> int * int * int -val duration_to_nb_days : duration -> int val duration_to_string : duration -> string (**{1 Defaults} *) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 7d9e4abe..9b92ec4a 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -377,12 +377,12 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = 1, 1900 *) | LDate d -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int d) | LDuration d -> - let y, m, _ = Runtime.duration_to_years_months_days d in + let y, m, d = Runtime.duration_to_years_months_days d in if y <> 0 || m <> 0 then failwith "[Z3 encoding]: Duration literals containing years or months not \ supported"; - Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.duration_to_nb_days d) + Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 d (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration corresponding to the variable [v]. If no such function declaration exists From 5e3274f00a718930ac884f50d921ffbf7a286117 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Mon, 28 Mar 2022 19:09:00 +0200 Subject: [PATCH 10/10] Restore nix no-web patch --- .nix/no-web.patch | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.nix/no-web.patch b/.nix/no-web.patch index 32a3cba7..54b345d7 100644 --- a/.nix/no-web.patch +++ b/.nix/no-web.patch @@ -25,7 +25,7 @@ index cc842a5d..00000000 - backend = "Interpret"; - language = Some (Js.to_string language); - max_prec_digits = None; -- trace = false; +- trace; - disable_counterexamples = false; - optimize = false; - ex_scope = Some (Js.to_string scope); @@ -39,7 +39,7 @@ index 2c5a1996..f6c38809 100644 @@ -19,16 +19,6 @@ (libraries calendar zarith zarith_stubs_js) (modules runtime)) - + -(executable - (name catala_web_interpreter) - (modes byte js)