Post merge fixes on using dates_calc

This commit is contained in:
Raphaël Monat 2022-08-06 17:49:06 +02:00
parent ffd2e1dec3
commit 3e71f25bfe
3 changed files with 21 additions and 22 deletions

View File

@ -108,13 +108,13 @@ let rec evaluate_operator
A.ELit (LDuration Runtime.(d1 -@ d2)) A.ELit (LDuration Runtime.(d1 -@ d2))
| A.Binop (A.Add KDate), [ELit (LDate d1); ELit (LDuration d2)] -> | A.Binop (A.Add KDate), [ELit (LDate d1); ELit (LDuration d2)] ->
A.ELit (LDate Runtime.(d1 +@ d2)) A.ELit (LDate Runtime.(d1 +@ d2))
| A.Binop (A.Div KDuration), [ELit (LDuration d1); ELit (LDuration d2)] -> (* | A.Binop (A.Div KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
apply_div_or_raise_err (fun _ -> * apply_div_or_raise_err (fun _ ->
try A.ELit (LRat Runtime.(d1 /^ d2)) * try A.ELit (LRat Runtime.(d1 /^ d2))
with Runtime.IndivisableDurations -> * with Runtime.IndivisableDurations ->
Errors.raise_multispanned_error (get_binop_args_pos args) * Errors.raise_multispanned_error (get_binop_args_pos args)
"Cannot divide durations that cannot be converted to a precise \ * "Cannot divide durations that cannot be converted to a precise \
number of days") * number of days") *)
| A.Binop (A.Mult KDuration), [ELit (LDuration d1); ELit (LInt i1)] -> | A.Binop (A.Mult KDuration), [ELit (LDuration d1); ELit (LInt i1)] ->
A.ELit (LDuration Runtime.(d1 *^ i1)) A.ELit (LDuration Runtime.(d1 *^ i1))
| A.Binop (A.Lt KInt), [ELit (LInt i1); ELit (LInt i2)] -> | 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.Unop A.GetMonth, [ELit (LDate d)] ->
A.ELit (LInt Runtime.(month_number_of_date 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.GetYear, [ELit (LDate d)] -> A.ELit (LInt Runtime.(year_of_date d))
| A.Unop A.FirstDayOfMonth, [ELit (LDate d)] -> (* | A.Unop A.FirstDayOfMonth, [ELit (LDate d)] ->
A.ELit (LDate Runtime.(first_day_of_month d)) * A.ELit (LDate Runtime.(first_day_of_month d))
| A.Unop A.LastDayOfMonth, [ELit (LDate d)] -> * | A.Unop A.LastDayOfMonth, [ELit (LDate d)] ->
A.ELit (LDate Runtime.(first_day_of_month d)) * A.ELit (LDate Runtime.(first_day_of_month d)) *)
| A.Unop A.IntToRat, [ELit (LInt i)] -> | A.Unop A.IntToRat, [ELit (LInt i)] ->
A.ELit (LRat Runtime.(decimal_of_integer i)) A.ELit (LRat Runtime.(decimal_of_integer i))
| A.Unop A.MoneyToRat, [ELit (LMoney i)] -> | A.Unop A.MoneyToRat, [ELit (LMoney i)] ->
@ -323,7 +323,6 @@ let rec evaluate_operator
args) args)
"Operator applied to the wrong arguments\n\ "Operator applied to the wrong arguments\n\
(should not happen if the term was well-typed)" (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 and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) : 'm A.marked_expr
= =

View File

@ -19,6 +19,7 @@ open Dcalc
open Ast open Ast
open Z3 open Z3
module StringMap : Map.S with type key = String.t = Map.Make (String) module StringMap : Map.S with type key = String.t = Map.Make (String)
module Runtime = Runtime_ocaml.Runtime
type context = { type context = {
ctx_z3 : Z3.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 (** 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], (** [unique_name] returns the full, unique name corresponding to variable [v],
as given by Bindlib **) as given by Bindlib **)
@ -107,11 +108,10 @@ let unique_name (v : 'm var) : string =
let date_to_int (d : Runtime.date) : int = let date_to_int (d : Runtime.date) : int =
(* Alternatively, could expose this from Runtime as a (noop) coercion, but (* Alternatively, could expose this from Runtime as a (noop) coercion, but
would allow to break abstraction more easily elsewhere *) would allow to break abstraction more easily elsewhere *)
let date : CalendarLib.Date.t = let period = Runtime.( -@ ) d base_day in
CalendarLib.Printer.Date.from_string (Runtime.date_to_string d) let y, m, d = Runtime.duration_to_string period in
in assert (y = 0 && m = 0);
let period = CalendarLib.Date.sub date base_day in d
CalendarLib.Date.Period.nb_days period
(** [date_of_year] translates a [year], represented as an integer into an OCaml (** [date_of_year] translates a [year], represented as an integer into an OCaml
date corresponding to Jan 1st of the same year *) 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, (** Returns the date (as a string) corresponding to nb days after the base day,
defined here as Jan 1, 1900 **) defined here as Jan 1, 1900 **)
let nb_days_to_date (nb : int) : string = let nb_days_to_date (nb : int) : string =
CalendarLib.Printer.Date.to_string Runtime.date_to_string
(CalendarLib.Date.add base_day (CalendarLib.Date.Period.day nb)) (Runtime.( +@ ) base_day (Runtime.duration_of_numbers 0 0 nb))
(** [print_z3model_expr] pretty-prints the value [e] given by a Z3 model (** [print_z3model_expr] pretty-prints the value [e] given by a Z3 model
according to the Catala type [ty], corresponding to [e] **) according to the Catala type [ty], corresponding to [e] **)

View File

@ -252,8 +252,8 @@ val date_of_numbers : int -> int -> int -> date
@raise ImpossibleDate *) @raise ImpossibleDate *)
val first_day_of_month : date -> date (* val first_day_of_month : date -> date
val last_day_of_month : date -> date * val last_day_of_month : date -> date *)
(**{2 Durations} *) (**{2 Durations} *)