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

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

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

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)@]"

compiler/heptagon/heptagon.ml

@@ -67,6 +67,7 @@ and op =
   | Earray_fill
   | Eselect
   | Eselect_dyn
+  | Eselect_trunc
   | Eselect_slice
   | Eupdate
   | Econcat

compiler/heptagon/parsing/hept_lexer.mll

@@ -144,6 +144,8 @@ rule token = parse
   | "^"             {POWER}
   | "["             {LBRACKET}
   | "]"             {RBRACKET}
+  | "[>"            {LBRACKETGREATER}
+  | "<]"            {LESSRBRACKET}
   | "@"             {AROBASE}
   | ".."            {DOUBLE_DOT}
   | "<<"            {DOUBLE_LESS}

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

compiler/heptagon/parsing/hept_parsetree.ml

@@ -92,6 +92,7 @@ and op =
   | Earray_fill
   | Eselect
   | Eselect_dyn
+  | Eselect_trunc
   | Eselect_slice
   | Eupdate
   | Econcat

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)
 

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

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 *)

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

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 *)
 

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

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)@]"

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

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)

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