From 3e71f25bfef709b844586a5a2d723639f0ac6f84 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= Date: Sat, 6 Aug 2022 17:49:06 +0200 Subject: [PATCH] Post merge fixes on using dates_calc --- compiler/dcalc/interpreter.ml | 23 +++++++++++------------ compiler/verification/z3backend.real.ml | 16 ++++++++-------- runtimes/ocaml/runtime.mli | 4 ++-- 3 files changed, 21 insertions(+), 22 deletions(-) diff --git a/compiler/dcalc/interpreter.ml b/compiler/dcalc/interpreter.ml index 1ba6a92e..f4e9663e 100644 --- a/compiler/dcalc/interpreter.ml +++ b/compiler/dcalc/interpreter.ml @@ -108,13 +108,13 @@ let rec evaluate_operator A.ELit (LDuration Runtime.(d1 -@ d2)) | A.Binop (A.Add KDate), [ELit (LDate d1); ELit (LDuration d2)] -> A.ELit (LDate Runtime.(d1 +@ d2)) - | A.Binop (A.Div KDuration), [ELit (LDuration d1); ELit (LDuration d2)] -> - apply_div_or_raise_err (fun _ -> - try A.ELit (LRat Runtime.(d1 /^ d2)) - with Runtime.IndivisableDurations -> - Errors.raise_multispanned_error (get_binop_args_pos args) - "Cannot divide durations that cannot be converted to a precise \ - number of days") + (* | A.Binop (A.Div KDuration), [ELit (LDuration d1); ELit (LDuration d2)] -> + * apply_div_or_raise_err (fun _ -> + * try A.ELit (LRat Runtime.(d1 /^ d2)) + * with Runtime.IndivisableDurations -> + * Errors.raise_multispanned_error (get_binop_args_pos args) + * "Cannot divide durations that cannot be converted to a precise \ + * number of days") *) | A.Binop (A.Mult KDuration), [ELit (LDuration d1); ELit (LInt i1)] -> A.ELit (LDuration Runtime.(d1 *^ i1)) | A.Binop (A.Lt KInt), [ELit (LInt i1); ELit (LInt i2)] -> @@ -253,10 +253,10 @@ let rec evaluate_operator | A.Unop A.GetMonth, [ELit (LDate d)] -> A.ELit (LInt Runtime.(month_number_of_date d)) | A.Unop A.GetYear, [ELit (LDate d)] -> A.ELit (LInt Runtime.(year_of_date d)) - | A.Unop A.FirstDayOfMonth, [ELit (LDate d)] -> - A.ELit (LDate Runtime.(first_day_of_month d)) - | A.Unop A.LastDayOfMonth, [ELit (LDate d)] -> - A.ELit (LDate Runtime.(first_day_of_month d)) + (* | A.Unop A.FirstDayOfMonth, [ELit (LDate d)] -> + * A.ELit (LDate Runtime.(first_day_of_month d)) + * | A.Unop A.LastDayOfMonth, [ELit (LDate d)] -> + * A.ELit (LDate Runtime.(first_day_of_month d)) *) | A.Unop A.IntToRat, [ELit (LInt i)] -> A.ELit (LRat Runtime.(decimal_of_integer i)) | A.Unop A.MoneyToRat, [ELit (LMoney i)] -> @@ -323,7 +323,6 @@ let rec evaluate_operator args) "Operator applied to the wrong arguments\n\ (should not happen if the term was well-typed)" ->>>>>>> master and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : 'm A.marked_expr = diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index eb074c8d..3c8c649c 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -19,6 +19,7 @@ open Dcalc open Ast open Z3 module StringMap : Map.S with type key = String.t = Map.Make (String) +module Runtime = Runtime_ocaml.Runtime type context = { ctx_z3 : Z3.context; @@ -95,7 +96,7 @@ let add_z3constraint (e : Expr.expr) (ctx : context) : context = (** For the Z3 encoding of Catala programs, we define the "day 0" as Jan 1, 1900 **) -let base_day = CalendarLib.Date.make 1900 1 1 +let base_day = Dates_calc.Dates.make_date ~year:1900 ~month:1 ~day:1 (** [unique_name] returns the full, unique name corresponding to variable [v], as given by Bindlib **) @@ -107,11 +108,10 @@ let unique_name (v : 'm var) : string = let date_to_int (d : Runtime.date) : int = (* Alternatively, could expose this from Runtime as a (noop) coercion, but would allow to break abstraction more easily elsewhere *) - let date : CalendarLib.Date.t = - CalendarLib.Printer.Date.from_string (Runtime.date_to_string d) - in - let period = CalendarLib.Date.sub date base_day in - CalendarLib.Date.Period.nb_days period + let period = Runtime.( -@ ) d base_day in + let y, m, d = Runtime.duration_to_string period in + assert (y = 0 && m = 0); + d (** [date_of_year] translates a [year], represented as an integer into an OCaml date corresponding to Jan 1st of the same year *) @@ -120,8 +120,8 @@ let date_of_year (year : int) = Runtime.date_of_numbers year 1 1 (** Returns the date (as a string) corresponding to nb days after the base day, defined here as Jan 1, 1900 **) let nb_days_to_date (nb : int) : string = - CalendarLib.Printer.Date.to_string - (CalendarLib.Date.add base_day (CalendarLib.Date.Period.day nb)) + Runtime.date_to_string + (Runtime.( +@ ) base_day (Runtime.duration_of_numbers 0 0 nb)) (** [print_z3model_expr] pretty-prints the value [e] given by a Z3 model according to the Catala type [ty], corresponding to [e] **) diff --git a/runtimes/ocaml/runtime.mli b/runtimes/ocaml/runtime.mli index d978f3bd..f518455b 100644 --- a/runtimes/ocaml/runtime.mli +++ b/runtimes/ocaml/runtime.mli @@ -252,8 +252,8 @@ val date_of_numbers : int -> int -> int -> date @raise ImpossibleDate *) -val first_day_of_month : date -> date -val last_day_of_month : date -> date +(* val first_day_of_month : date -> date + * val last_day_of_month : date -> date *) (**{2 Durations} *)