From 100c08ee365cd94ecdd4ee1e74fea927c5aeb90b Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Thu, 21 Sep 2017 16:09:19 +0100 Subject: [PATCH] Bug correction in normalization of merge: fix propagation of type annotations Minils.CtrlNbacGen relies on such type annotations to generat Controllable-Nbac nodes. This fix allows the use of ReaX to enforce contracts of nodes involving merge operations on tuples over multiple data types, such as: (a, b) = merge c (true -> ((true when c), (0 when c))) (false -> ((false whenot c), (2 whenot c))); This kind of code previously led to erroneous Controllable-Nbac code. --- compiler/heptagon/transformations/normalize.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 25c8a9c..7563aee 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -278,8 +278,6 @@ and merge context e x c_e_list = (tag, e), context in let mk_merge x c_list e_lists = - let ty = (List.hd (List.hd e_lists)).e_ty in - let lin = (List.hd (List.hd e_lists)).e_linearity in let rec build_c_e_list c_list e_lists = match c_list, e_lists with | [], [] -> [], [] @@ -293,7 +291,9 @@ and merge context e x c_e_list = | []::_ -> [] | _ ::_ -> let c_e_list, e_lists = build_c_e_list c_list e_lists in - let e_merge = mk_exp ~loc:e.e_loc (Emerge(x, c_e_list)) ty ~linearity:lin in + let c_e1 = List.hd c_e_list in + let { e_loc = loc; e_ty; e_linearity = linearity } = snd c_e1 in + let e_merge = mk_exp ~loc (Emerge(x, c_e_list)) e_ty ~linearity in let e_merge_list = build_merge_list c_list e_lists in e_merge::e_merge_list in build_merge_list c_list e_lists