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

Removed unnecessary extra runtime function

Browse Source
This commit is contained in:
Denis Merigoux 2022-03-28 18:59:53 +02:00
parent 2b0206a5a8
commit 158d49fe86
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
3 changed files with 2 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/runtime.ml
View File

@ -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 ->

1
compiler/runtime.mli
View File

@ -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} *)

4
compiler/verification/z3backend.real.ml
View File

@ -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