jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Bug correction in normalization of merge: fix propagation of type annotations

Browse source 
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.
This commit is contained in:
Nicolas Berthier 2017-09-21 16:09:19 +01:00
parent 15b2c09425
commit 100c08ee36
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
compiler/heptagon/transformations/normalize.ml
View file

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