From 0abb050a23ca67bd6e88b9ced33599c16ebb233a Mon Sep 17 00:00:00 2001 From: Adrien Guatto Date: Thu, 9 Feb 2012 16:23:36 +0100 Subject: [PATCH] Changed linear typing for merge. The new rule accepts that some branches of a linearly typed merge have linear type Top, provided that at least one has type "lin". E.g.: node f(x : int at r) returns (o : int at r) var ck : bool; let ck = true; o = merge ck (x whenot ck) 0; tel is now deemed valid. --- compiler/heptagon/analysis/linear_typing.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/compiler/heptagon/analysis/linear_typing.ml b/compiler/heptagon/analysis/linear_typing.ml index 6bad16d..1b13d4f 100644 --- a/compiler/heptagon/analysis/linear_typing.ml +++ b/compiler/heptagon/analysis/linear_typing.ml @@ -802,8 +802,18 @@ and expect env lin e = found_lin, env | Emerge (_, c_e_list) -> - let env = List.fold_left (fun env (_, e) -> safe_expect env lin e) env c_e_list in - lin, env + (* Idea: one of the branches should be of linear type [lin], the others can be of linear type + Top *) + (* TODO: Cedric, avis ?*) + let type_clause (env, no_lin) (_, e) = + try + let _, env = expect env lin e in env, false + with _ -> + safe_expect env Ltop e, no_lin + in + let env, no_lin = List.fold_left type_clause (env, true) c_e_list in + if no_lin then message e.e_loc (Eunify_failed_one lin); + lin, env | Ewhen (e, _, _) -> expect env lin e