From 2fdf2855d395ddffe544c2f97d7d674fac4e1853 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Tue, 22 Mar 2011 22:12:59 +0100 Subject: [PATCH] Added a new truncated select operator a[>e<] returns the element in the array at index e, a[0] if e < 0 and a[n-1] if e >= n --- compiler/heptagon/analysis/causality.ml | 2 +- compiler/heptagon/analysis/typing.ml | 7 +++++ compiler/heptagon/hept_printer.ml | 6 +++++ compiler/heptagon/heptagon.ml | 1 + compiler/heptagon/parsing/hept_lexer.mll | 2 ++ compiler/heptagon/parsing/hept_parser.mly | 11 ++++++-- compiler/heptagon/parsing/hept_parsetree.ml | 1 + compiler/heptagon/parsing/hept_scoping.ml | 1 + compiler/main/hept2mls.ml | 1 + compiler/main/mls2obc.ml | 27 ++++++++++++++++++-- compiler/minils/analysis/clocking.ml | 4 +++ compiler/minils/minils.ml | 1 + compiler/minils/mls_compare.ml | 4 +-- compiler/minils/mls_printer.ml | 6 +++++ compiler/minils/transformations/normalize.ml | 5 ++++ lib/pervasives.epi | 1 + test/good/array1.ept | 5 ++++ 17 files changed, 78 insertions(+), 7 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index f4582d1..975406a 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -136,7 +136,7 @@ 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) -> + | Eselect_dyn | Eselect_trunc | Eselect _ | Earray_fill) -> ctuplelist (List.map typing e_list) | (Earray | Etuple) -> candlist (List.map typing e_list) diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index c5b47eb..3fd18bb 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -716,6 +716,13 @@ and typing_app const_env h app e_list = typing_array_subscript_dyn const_env h idx_list t1 in ty, app, typed_e1::typed_defe::typed_idx_list + | Eselect_trunc -> + let e1, idx_list = assert_1min e_list in + let typed_e1, t1 = typing const_env h e1 in + let ty, typed_idx_list = + typing_array_subscript_dyn const_env h idx_list t1 in + ty, app, typed_e1::typed_idx_list + | Eupdate -> let e1, e2, idx_list = assert_2min e_list in let typed_e1, t1 = typing const_env h e1 in diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 35cc659..e6795a1 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -83,6 +83,9 @@ and print_index ff idx = and print_dyn_index ff idx = fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx +and print_trunc_index ff idx = + fprintf ff "@[<2>%a@]" (print_list print_exp "[>""<][>""<]") idx + and print_exps ff e_list = print_list_r print_exp "(" "," ")" ff e_list @@ -169,6 +172,9 @@ and print_app ff (app, args) = let r, d, e = assert_2min args in fprintf ff "%a%a default %a" print_exp r print_dyn_index e print_exp d + | Eselect_trunc -> + let e, idx_list = assert_1min args in + fprintf ff "%a%a" print_exp e print_trunc_index idx_list | Eupdate -> let e1, e2, idx = assert_2min args in fprintf ff "@[<2>(%a with %a =@ %a)@]" diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 0be0ad2..84d09b6 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -67,6 +67,7 @@ and op = | Earray_fill | Eselect | Eselect_dyn + | Eselect_trunc | Eselect_slice | Eupdate | Econcat diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 36686eb..e370f0d 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -144,6 +144,8 @@ rule token = parse | "^" {POWER} | "[" {LBRACKET} | "]" {RBRACKET} + | "[>" {LBRACKETGREATER} + | "<]" {LESSRBRACKET} | "@" {AROBASE} | ".." {DOUBLE_DOT} | "<<" {DOUBLE_LESS} diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 27044d6..f816dbc 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -41,8 +41,8 @@ open Hept_parsetree %token WITH %token WHEN MERGE %token POWER -%token LBRACKET -%token RBRACKET +%token LBRACKET LBRACKETGREATER +%token RBRACKET LESSRBRACKET %token DOUBLE_DOT %token AROBASE %token DOUBLE_LESS DOUBLE_GREATER @@ -497,6 +497,8 @@ _exp: { mk_call ~params:$2 Eselect [$1] } | simple_exp DOT indexes DEFAULT exp { mk_call Eselect_dyn ([$1; $5]@$3) } + | a=simple_exp idx=trunc_indexes + { mk_call Eselect_trunc (a::idx) } | LBRACKET exp WITH indexes EQUAL exp RBRACKET { mk_call Eupdate ($2::$6::$4) } | simple_exp LBRACKET exp DOUBLE_DOT exp RBRACKET @@ -537,6 +539,11 @@ indexes: | LBRACKET exp RBRACKET indexes { $2::$4 } ; +trunc_indexes: + LBRACKETGREATER exp LESSRBRACKET { [$2] } + | LBRACKETGREATER exp LESSRBRACKET trunc_indexes { $2::$4 } +; + qualified(X): | m=modul DOT x=X { Q { qual = m; name = x } } diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index ed16e30..95c9259 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -92,6 +92,7 @@ and op = | Earray_fill | Eselect | Eselect_dyn + | Eselect_trunc | Eselect_slice | Eupdate | Econcat diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index e496151..ec6a780 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -288,6 +288,7 @@ and translate_op = function | Eselect_slice -> Heptagon.Eselect_slice | Econcat -> Heptagon.Econcat | Eselect_dyn -> Heptagon.Eselect_dyn + | Eselect_trunc -> Heptagon.Eselect_trunc | Efun ln -> Heptagon.Efun (qualify_value ln) | Enode ln -> Heptagon.Enode (qualify_value ln) diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 65a0668..b5cdd05 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -207,6 +207,7 @@ let rec translate_op = function | Heptagon.Eselect_dyn -> Eselect_dyn | Heptagon.Eupdate -> Eupdate | Heptagon.Eselect_slice -> Eselect_slice + | Heptagon.Eselect_trunc -> Eselect_trunc | Heptagon.Econcat -> Econcat | Heptagon.Earray -> Earray | Heptagon.Etuple -> Etuple diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 0548b08..009d818 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -34,7 +34,20 @@ let rec pattern_of_idx_list p l = | Tarray (ty',_), idx :: l -> mk_pattern ty' (Larray (aux ty' l, idx)) | _ -> internal_error "mls2obc" 1 in - aux p.pat_ty l + aux p.pat_ty (List.rev l) + +let rec pattern_of_trunc_idx_list p l = + let mk_between idx se = + mk_exp_int (Eop (mk_pervasives "between", + [idx; mk_exp se.se_ty (Econst se)])) + in + let rec aux ty l = match ty, l with + | _, [] -> p + | Tarray (ty', se), idx :: l -> + mk_pattern ty' (Larray (aux ty' l, mk_between idx se)) + | _ -> internal_error "mls2obc" 1 + in + aux p.pat_ty (List.rev l) let array_elt_of_exp idx e = match e.e_desc, Modules.unalias_type e.e_ty with @@ -104,7 +117,8 @@ let rec translate map e = Epattern (pattern_of_idx_list (pattern_of_exp e) idx_list) (* Already treated cases when translating the [eq] *) | Minils.Eiterator _ | Minils.Emerge _ | Minils.Efby _ - | Minils.Eapp ({Minils.a_op=(Minils.Enode _|Minils.Efun _|Minils.Econcat|Minils.Eupdate|Minils.Eselect_dyn + | Minils.Eapp ({Minils.a_op=(Minils.Enode _|Minils.Efun _|Minils.Econcat + |Minils.Eupdate|Minils.Eselect_dyn|Minils.Eselect_trunc |Minils.Eselect_slice|Minils.Earray_fill|Minils.Efield_update|Minils.Eifthenelse |Minils.Etuple)}, _, _) -> (*Format.eprintf "%aThis should not be treated as an exp in mls2obc : %a@." @@ -185,6 +199,15 @@ and translate_act map pat let false_act = Aassgn (x, translate map e2) in let cond = bound_check_expr idx bounds in [ Acase (cond, [ ptrue, mk_block [true_act]; pfalse, mk_block [false_act] ]) ] + + | Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_trunc }, e1::idx, _) -> + let x = Control.var_from_name map x in + let bounds = Mls_utils.bounds_list e1.Minils.e_ty in + let e1 = translate map e1 in + let idx = List.map (translate map) idx in + let p = pattern_of_trunc_idx_list (pattern_of_exp e1) idx in + [Aassgn (x, mk_exp p.pat_ty (Epattern p))] + | Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eupdate }, e1::e2::idx, _) -> let x = Control.var_from_name map x in (** TODO: remplacer par if 0 < e && e < n then for () ; o[e] = v; for () else o = a *) diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 981cf27..296419a 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -90,6 +90,10 @@ and typing_op op e_list h e ck = match op with let e1, defe, idx = assert_2min e_list in let ct = skeleton ck e1.e_ty in (List.iter (expect h ct) (e1::defe::idx); ct) + | Eselect_trunc -> + let e1, idx = assert_1min e_list in + let ct = skeleton ck e1.e_ty + in (List.iter (expect h ct) (e1::idx); ct) | Eupdate -> let e1, e2, idx = assert_2min e_list in let ct = skeleton ck e.e_ty diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 2f8c694..d18b5f1 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -79,6 +79,7 @@ and op = | Eselect (** arg1[a_params] *) | Eselect_slice (** arg1[a_param1..a_param2] *) | Eselect_dyn (** arg1.[arg3...] default arg2 *) + | Eselect_trunc (** arg1[>arg_2 ...<]*) | Eupdate (** [ arg1 with arg3..arg_n = arg2 ] *) | Econcat (** arg1@@arg2 *) diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index b9b9a77..84cb8b5 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -91,8 +91,8 @@ and app_compare app1 app2 = | x, y when x = y -> 0 (* all constructors can be compared with P.compare *) | (Eequal | Etuple | Efun _ | Enode _ | Eifthenelse | Efield | Efield_update), _ -> -1 - | (Earray | Earray_fill | Eselect | Eselect_slice | Eselect_dyn | Eupdate - | Econcat ), _ -> 1 in + | (Earray | Earray_fill | Eselect | Eselect_slice | Eselect_dyn + | Eselect_trunc | Eupdate | Econcat ), _ -> 1 in if cr <> 0 then cr else list_compare static_exp_compare app1.a_params app2.a_params diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 346f5eb..e318861 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -77,6 +77,9 @@ and print_index ff idx = and print_dyn_index ff idx = fprintf ff "@[<2>%a@]" (print_list print_exp "[""][""]") idx +and print_trunc_index ff idx = + fprintf ff "@[<2>%a@]" (print_list print_exp "[>""<][>""<]") idx + and print_exp ff e = if !Compiler_options.full_type_info then fprintf ff "(%a : %a :: %a)" @@ -151,6 +154,9 @@ and print_app ff (app, args) = let r, d, e = assert_2min args in fprintf ff "%a%a default %a" print_exp r print_dyn_index e print_exp d + | Eselect_trunc -> + let e, idx_list = assert_1min args in + fprintf ff "%a%a" print_exp e print_trunc_index idx_list | Eupdate -> let e1, e2, idx = assert_2min args in fprintf ff "@[<2>(%a with %a =@ %a)@]" diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index e07cf94..e5e7339 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -261,6 +261,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 + | Eselect_trunc -> + let e1, idx = assert_1min e_list in + let context, e1 = translate VRef context e1 in + let context, idx = translate_list Exp context idx in + context, e1::idx | Eupdate -> let e1, e2, idx = assert_2min e_list in let context, e1 = translate VRef context e1 in diff --git a/lib/pervasives.epi b/lib/pervasives.epi index 8446fb4..c8e7442 100644 --- a/lib/pervasives.epi +++ b/lib/pervasives.epi @@ -28,3 +28,4 @@ val fun (xor)(bool;bool) returns (bool) val fun (~-)(int) returns (int) val fun (~-.)(float) returns (float) val fun do_stuff(int) returns (int) +val between(int;int) returns (int) diff --git a/test/good/array1.ept b/test/good/array1.ept index 526ec44..4ec9c26 100644 --- a/test/good/array1.ept +++ b/test/good/array1.ept @@ -51,3 +51,8 @@ let (z,t) = concatenate(x,y); (r1,r2) = slicing(x); tel + +node elt_trunc (a:int^m^m; i,j:int) returns (o : int) +let + o = a[>i<][>j<]; +tel \ No newline at end of file