Fixed bug in unicity check in linear typing
Test case included
This commit is contained in:
parent
3269a04052
commit
1aac6f7be4
2 changed files with 23 additions and 2 deletions
|
@ -774,8 +774,9 @@ and expect env lin e =
|
|||
let l, env = match e.e_desc with
|
||||
| Evar x ->
|
||||
let actual_lin = lin_of_ident x env in
|
||||
let env = check_linearity_exp env e lin in
|
||||
unify_lin lin actual_lin, env
|
||||
let found_lin = unify_lin lin actual_lin in
|
||||
let env = check_linearity_exp env e found_lin in
|
||||
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
|
||||
|
|
20
test/bad/linear_fun.ept
Normal file
20
test/bad/linear_fun.ept
Normal file
|
@ -0,0 +1,20 @@
|
|||
const n:int = 100
|
||||
|
||||
type tab = float^n
|
||||
|
||||
node f(x : tab at r) returns (o : tab at r)
|
||||
let
|
||||
o = x;
|
||||
tel
|
||||
|
||||
node main() returns (o:float)
|
||||
var u : tab at r;
|
||||
z1 : tab; z2 : tab at r;
|
||||
let
|
||||
init<<r>> u = (0.0)^n;
|
||||
|
||||
z1 = f(u);
|
||||
z2 = f(u);
|
||||
|
||||
o = 0.0;
|
||||
tel
|
Loading…
Reference in a new issue