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

Made Eupdate dynamic

Browse source 
Modifying an array with
 [ a with [i] = v ]
should expected a dynamic (not static) value
for i (nothing happens if i is in the wrong range).
This is the same behaviour as in Scade and it is 
useful eg to modify an array in a foldi.
This commit is contained in:
Cédric Pasteur 2010-07-28 12:34:07 +02:00
parent 3f0005dba1
commit 8f4220e08d
9 changed files with 34 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
compiler/heptagon/analysis/causality.ml
View file

@ -125,14 +125,18 @@ and apply op e_list =
let i3 = typing e3 in
cseq t1 (cor i2 i3)
| (Eequal | Efun _| Enode _ | Econcat | Eselect_slice
| Eselect_dyn | Eselect _ | Earray_fill), e_list ->
| Eselect_dyn| Eselect _ | Earray_fill), e_list ->
ctuplelist (List.map typing e_list)
| (Earray | Etuple), e_list ->
candlist (List.map typing e_list)
| (Eupdate _ | Efield_update _), [e1;e2] ->
| Efield_update, [e1;e2] ->
let t1 = typing e1 in
let t2 = typing e2 in
cseq t2 t1
| Eupdate , e1::e_list ->
let t1 = typing e1 in
let t2 = ctuplelist (List.map typing e_list) in
cseq t2 t1
let rec typing_pat = function
| Evarpat(x) -> cwrite(x)

8
compiler/heptagon/analysis/typing.ml
View file

@ -714,12 +714,12 @@ and typing_app const_env h op e_list =
typing_array_subscript_dyn const_env h idx_list t1 in
ty, op, typed_e1::typed_defe::typed_idx_list
| { a_op = Eupdate; a_params = idx_list }, [e1;e2] ->
| { a_op = Eupdate}, e1::e2::idx_list ->
let typed_e1, t1 = typing const_env h e1 in
let typed_idx_list, ty =
typing_array_subscript const_env h idx_list t1 in
let ty, typed_idx_list =
typing_array_subscript_dyn const_env h idx_list t1 in
let typed_e2 = expect const_env h ty e2 in
t1, { op with a_params = typed_idx_list }, [typed_e1; typed_e2]
t1, op, typed_e1::typed_e2::typed_idx_list
| { a_op = Eselect_slice; a_params = [idx1; idx2] }, [e] ->
let typed_idx1 = expect_static_exp const_env (Tid Initial.pint) idx1 in

4
compiler/heptagon/hept_printer.ml
View file

@ -141,11 +141,11 @@ and print_op ff op params e_list =
print_list_r print_exp "[" "][" "] default " ff idx_list;
print_exp ff defe;
fprintf ff ")@]"
| Eupdate, idx_list, [e1;e2] ->
| Eupdate, _, e1::e2::idx_list ->
fprintf ff "(@[";
print_exp ff e1;
fprintf ff " with ";
print_list_r print_static_exp "[" "][" "]" ff idx_list;
print_list_r print_exp "[" "][" "]" ff idx_list;
fprintf ff " = ";
print_exp ff e2;
fprintf ff ")@]"

2
compiler/heptagon/parsing/hept_parser.mly
View file

@ -456,7 +456,7 @@ _exp:
| simple_exp DOT indexes DEFAULT exp
{ mk_call Eselect_dyn ([$1; $5]@$3) }
| LBRACKET exp WITH indexes EQUAL exp RBRACKET
{ mk_call ~params:$4 Eupdate [$2; $6] }
{ mk_call Eupdate ($2::$6::$4) }
| simple_exp LBRACKET exp DOUBLE_DOT exp RBRACKET
{ mk_call ~params:[$3; $5] Eselect_slice [$1] }
| exp AROBASE exp

14
compiler/main/mls2obc.ml
View file

@ -225,14 +225,16 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
v, si, j, (control map ck action) :: s
| Minils.Evarpat x,
Minils.Eapp ({ Minils.a_op = Minils.Eupdate;
Minils.a_params = idx }, [e1; e2], _) ->
Minils.Eapp ({ Minils.a_op = Minils.Eupdate },
e1::e2::idx, _) ->
let x = var_from_name map x in
let copy = Aassgn (x, translate map (si, j, s) e1) in
let idx = List.map (fun idx -> mk_exp (Econst idx)) idx in
let bounds = Mls_utils.bounds_list e1.Minils.e_ty in
let idx = List.map (translate map (si, j, s)) idx in
let action = Aassgn (lhs_of_idx_list x idx,
translate map (si, j, s) e2)
in
translate map (si, j, s) e2) in
let cond = bound_check_expr idx bounds in
let action = Acase (cond, [ Name "true", mk_block [action] ]) in
let copy = Aassgn (x, translate map (si, j, s) e1) in
v, si, j, (control map ck copy) :: (control map ck action) :: s
| Minils.Evarpat x,

4
compiler/minils/analysis/clocking.ml
View file

@ -81,9 +81,9 @@ and typing_op op args h e ck = match op, args with
| Eselect_dyn, e1::defe::idx -> (* TODO defe not treated ? *)
let ct = skeleton ck e1.e_ty
in (expect h ct e1; List.iter (expect h ct) idx; ct)
| Eupdate, [e1; e2] ->
| Eupdate, e1::e2::idx ->
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct)
| Eselect_slice, [e] -> typing h e
| Econcat, [e1; e2] ->
let ct = skeleton ck e.e_ty

4
compiler/minils/mls_printer.ml
View file

@ -133,9 +133,9 @@ and print_app ff (app, args) = match app.a_op, app.a_params, args with
| Eselect_dyn, _, r::d::e ->
fprintf ff "%a%a default %a"
print_exp r print_dyn_index e print_exp d
| Eupdate, idx, [e1; e2] ->
| Eupdate, _, e1::e2::idx ->
fprintf ff "@[<2>(%a with %a =@ %a)@]"
print_exp e1 print_index idx print_exp e2
print_exp e1 print_dyn_index idx print_exp e2
| Econcat, _,[e1; e2] ->
fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2
| Elambda(inp, outp, _, eq_list), _, e_list ->

5
compiler/minils/transformations/normalize.ml
View file

@ -242,10 +242,11 @@ and translate_app kind context op e_list =
let context, idx = translate_list Exp context idx in
let context, e2 = translate Exp context e2 in
context, e1::e2::idx
| Eupdate, [e1; e2] ->
| Eupdate, e1::e2::idx ->
let context, e1 = translate VRef context e1 in
let context, idx = translate_list Exp context idx in
let context, e2 = translate Exp context e2 in
context, [e1; e2]
context, e1::e2::idx
| Eselect_slice, [e'] ->
let context, e' = translate VRef context e' in
context, [e']

8
test/good/array1.ept
View file

@ -6,7 +6,7 @@ let
o1 = a @ b;
o2 = b @ a;
tel
(*
node slicing (a:int^n) returns (u1,u2 : int^3)
let
u1 = a[0 .. 2];
@ -20,6 +20,11 @@ let
o = [ a with [1] = x ];
tel
node upd_dyn(a:int^m; i:int) returns (o:int^m)
let
o = [ a with [i] = a[0] ];
tel
node elt_dyn (a:int^m; i:int) returns (o:int^m)
var x : int;
let
@ -36,4 +41,3 @@ node constant(a,b:int) returns (o:int^4)
let
o = [a,b,a,b];
tel
*)