From e49b6d558bffde6a44641d156603b4a6e1cf013d Mon Sep 17 00:00:00 2001 From: "xavier.thirioux" <xavier.thirioux@enseeiht.fr> Date: Tue, 14 Feb 2017 12:11:31 +0100 Subject: [PATCH] nice bug correction wrt constants with a large number of digits. Would raise exception when comparing these constants --- src/corelang.ml | 15 ++++++++++++++- src/normalization.ml | 10 +++++----- 2 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/corelang.ml b/src/corelang.ml index 6aa86700..6618e3e2 100755 --- a/src/corelang.ml +++ b/src/corelang.ml @@ -473,8 +473,21 @@ let rec dimension_of_expr expr = let sort_handlers hl = List.sort (fun (t, _) (t', _) -> compare t t') hl +let num_10 = Num.num_of_int 10 + +let rec is_eq_const c1 c2 = + match c1, c2 with + | Const_real (n1, i1, _), Const_real (n2, i2, _) + -> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in + let n2 = n2 // (num_10 **/ (num_of_int i2)) in + eq_num n1 n2) + | Const_struct lcl1, Const_struct lcl2 + -> List.length lcl1 = List.length lcl2 + && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2 + | _ -> c1 = c2 + let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with - | Expr_const c1, Expr_const c2 -> c1 = c2 + | Expr_const c1, Expr_const c2 -> is_eq_const c1 c2 | Expr_ident i1, Expr_ident i2 -> i1 = i2 | Expr_array el1, Expr_array el2 | Expr_tuple el1, Expr_tuple el2 -> diff --git a/src/normalization.ml b/src/normalization.ml index 040606c3..c8de574e 100644 --- a/src/normalization.ml +++ b/src/normalization.ml @@ -80,8 +80,8 @@ let mk_fresh_var node loc ty ck = let get_expr_alias defs expr = try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs) with - Not_found -> None - + | Not_found -> None + (* Replace [expr] with (tuple of) [locals] *) let replace_expr locals expr = match locals with @@ -156,13 +156,13 @@ let mk_expr_alias_opt opt node (defs, vars) expr = taking propagated [offsets] into account in order to change expression type *) let mk_norm_expr offsets ref_e norm_d = -(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) + (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*) let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in { ref_e with expr_desc = norm_d; expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } - + (* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *) let rec normalize_list alias node offsets norm_element defvars elist = List.fold_right @@ -172,7 +172,7 @@ let rec normalize_list alias node offsets norm_element defvars elist = ) elist (defvars, []) let rec normalize_expr ?(alias=true) node offsets defvars expr = -(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) + (*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) match expr.expr_desc with | Expr_const _ | Expr_ident _ -> defvars, unfold_offsets expr offsets -- GitLab