[asl] Use double brackets for array declarations

asllib/PP.ml

@@ -143,9 +143,9 @@ let rec pp_expr f e =
       fprintf f "@[<hv>%a {@ %a@;<1 -2>}@]" pp_ty ty (pp_comma_list pp_one) li
   | E_Tuple es -> fprintf f "@[<hv 2>(%a)@]" pp_expr_list es
   | E_Array { length; value } ->
-      fprintf f "@[<hv 2>array[%a] of %a@]" pp_expr length pp_expr value
+      fprintf f "@[<hv 2>array[[%a]] of %a@]" pp_expr length pp_expr value
   | E_EnumArray { enum; value } ->
-      fprintf f "@[<hv 2>array[%s] of %a@]" enum pp_expr value
+      fprintf f "@[<hv 2>array[[%s]] of %a@]" enum pp_expr value
   | E_Arbitrary ty -> fprintf f "@[<h>ARBITRARY :@ %a@]" pp_ty ty
   | E_Pattern (e, p) -> fprintf f "@[<hv 2>%a@ IN %a@]" pp_expr e pp_pattern p
 
@@ -192,9 +192,9 @@ and pp_ty f t =
         enum_ty
   | T_Tuple ty_list -> fprintf f "@[(%a)@]" (pp_comma_list pp_ty) ty_list
   | T_Array (ArrayLength_Expr e, elt_type) ->
-      fprintf f "@[array [%a] of %a@]" pp_expr e pp_ty elt_type
+      fprintf f "@[array [[%a]] of %a@]" pp_expr e pp_ty elt_type
   | T_Array (ArrayLength_Enum (enum, _), elt_type) ->
-      fprintf f "@[array [%s] of %a@]" enum pp_ty elt_type
+      fprintf f "@[array [[%s]] of %a@]" enum pp_ty elt_type
   | T_Record record_ty ->
       fprintf f "@[<hv 2>record {@ %a@;<1 -2>}@]" pp_fields record_ty
   | T_Exception record_ty ->

asllib/Parser.mly

@@ -388,7 +388,7 @@ let ty :=
     | BITS; ~=pared(expr); ~=bitfields_opt;             < T_Bits      >
     | l=plist(ty);                                      < T_Tuple     >
     | name=IDENTIFIER;                                  < T_Named     >
-    | ARRAY; e=bracketed(expr); OF; t=ty;               { T_Array (ArrayLength_Expr e, t) }
+    | ARRAY; LLBRACKET; e=expr; RRBRACKET; OF; t=ty;    { T_Array (ArrayLength_Expr e, t) }
   )
 
 let ty_decl := ty |

asllib/doc/Syntax.tex

@@ -584,7 +584,7 @@ \section{ASL Grammar\label{sec:ASLGrammar}}
             |\ & \Tbits \parsesep \Tlpar \parsesep \Nexpr \parsesep \Trpar \parsesep \option{\Nbitfields} &\\
             |\ & \Plist{\Nty} &\\
             |\ & \Tidentifier &\\
-            |\ & \Tarray \parsesep \Tlbracket \parsesep \Nexpr \parsesep \Trbracket \parsesep \Tof \parsesep \Nty &
+            |\ & \Tarray \parsesep \Tllbracket \parsesep \Nexpr \parsesep \Trrbracket \parsesep \Tof \parsesep \Nty &
 \end{flalign*}
 
 \hypertarget{def-ntydecl}{}

asllib/doc/Types.tex

@@ -628,7 +628,7 @@ \section{Array Types\label{sec:ArrayTypes}}
 
 \subsection{Syntax}
 \begin{flalign*}
-\Nty \derives\ & \Tarray \parsesep \Tlbracket \parsesep \Nexpr \parsesep \Trbracket \parsesep \Tof \parsesep \Nty &
+\Nty \derives\ & \Tarray \parsesep \Tllbracket \parsesep \Nexpr \parsesep \Trrbracket \parsesep \Tof \parsesep \Nty &
 \end{flalign*}
 
 \subsection{Abstract Syntax}
@@ -640,7 +640,7 @@ \subsection{Abstract Syntax}
 \subsubsection{ASTRule.Ty.TArray}
 \begin{mathpar}
 \inferrule{}{
-  \buildty(\Nty(\Tarray, \Tlbracket, \punnode{\Nexpr}, \Trbracket, \Tof, \punnode{\Nty})) \astarrow
+  \buildty(\Nty(\Tarray, \Tllbracket, \punnode{\Nexpr}, \Trrbracket, \Tof, \punnode{\Nty})) \astarrow
   \overname{\TArray(\ArrayLengthExpr(\astof{\vexpr}), \astof{\tty})}{\vastnode}
 }
 \end{mathpar}

asllib/tests/ASLSemanticsReference.t/SemanticsRule.EArbitraryArray.asl

@@ -1,9 +1,9 @@
 type Enum of enumeration {A, B, C};
-type Arr of array[Enum] of integer;
+type Arr of array[[Enum]] of integer;
 
 func main () => integer
 begin
-  var int_array = ARBITRARY : array[3] of integer;
+  var int_array = ARBITRARY : array[[3]] of integer;
   int_array[[2]] = 1;
   assert int_array[[2]] == 1;
 

asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetArray.asl

@@ -1,6 +1,6 @@
-type MyArrayType of array [3] of integer;
+type MyArrayType of array [[3]] of integer;
 
-var my_array : MyArrayType;  
+var my_array : MyArrayType;
 
 func main () => integer
 begin
@@ -9,4 +9,4 @@ begin
   assert my_array[[2]]==42;
 
   return 0;
-end; 
+end;

asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetArrayTooSmall.asl

@@ -1,4 +1,4 @@
-type MyArrayType of array [3] of integer;
+type MyArrayType of array [[3]] of integer;
 
 var my_array : MyArrayType;
 

asllib/tests/ASLSemanticsReference.t/SemanticsRule.EGetEnumArray.asl

@@ -1,5 +1,5 @@
 type Enum of enumeration {A, B, C};
-type Arr of array[Enum] of integer;
+type Arr of array[[Enum]] of integer;
 
 func main () => integer
 begin

asllib/tests/ASLSemanticsReference.t/SemanticsRule.LESetArray.asl

@@ -1,7 +1,7 @@
 func main () => integer
 begin
 
-  var my_array: array [42] of integer;
+  var my_array: array [[42]] of integer;
   my_array[[3]] = 53;
   assert my_array[[3]] == 53;
 

asllib/tests/ASLSyntaxReference.t/expr1.asl

@@ -9,12 +9,12 @@ begin
 
   var b0 = '1111 1000'[3:1, 0]; // E_Slice 1: a bitvector slice.
   var b1 = 0xF8[3:1, 0]; // E_Slice 2: an integer slice.
-  var bits_arr : array [1] of bits(4);
+  var bits_arr : array [[1]] of bits(4);
   // E_Binop 1: b0 == b1 is a binary expression for ==.
   // E_Cond 1: the right-hand side of the assignment is
   //           a conditional expression.
   bits_arr[[0]] = if (b0 == b1) then '1000' else '0000';
-  // E_Slice 3: bits_arr[0] stands for an array access
+  // E_Slice 3: bits_arr[[0]] stands for an array access
   assert b0 == bits_arr[[0]];
   // E_Unop 1: (NOT b8) negates the bits of b8.
   // E_Binop 2: the right-hand side of the assignment is

asllib/tests/ASLTypingReference.t/TypingRule.BuiltinAggregateTypes.asl

@@ -1,8 +1,8 @@
 type Pair of (integer, boolean);
 
-type T of array [3] of real;
+type T of array [[3]] of real;
 type Coord of enumeration { CX, CY, CZ };
-type PointArray of array [Coord] of real;
+type PointArray of array [[Coord]] of real;
 
 type PointRecord of record
   { x : real, y : real, z : real };

asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl

@@ -1,11 +1,11 @@
-// Declare an array of reals from arr1[0] to arr1[3]
-type arr1 of array [4] of real;
+// Declare an array of reals from arr1[[0]] to arr1[[3]]
+type arr1 of array [[4]] of real;
 
-// Declare an array with two entries arr2[big] and arr2[little]
+// Declare an array with two entries arr2[[big]] and arr2[[little]]
 type labels of enumeration {big, little};
-type arr2 of array [labels] of bits(4);
+type arr2 of array [[labels]] of bits(4);
 
-func foo(x: array [4] of integer) => array [4] of integer
+func foo(x: array [[4]] of integer) => array [[4]] of integer
 begin
   var y = x;
   y[[3]] = 2;
@@ -14,10 +14,10 @@ end;
 
 func main () => integer
 begin
-  var x: array [4] of integer;
+  var x: array [[4]] of integer;
   x[[1]] = 1;
 
-  x = foo (x as array [4] of integer);
-  let y: array [4] of integer = x;
+  x = foo (x as array [[4]] of integer);
+  let y: array [[4]] of integer = x;
   return 0;
 end;

asllib/tests/atcs.t

@@ -91,8 +91,8 @@ ATCs on other types
   > func main () => integer
   > begin
   >     let x: A = B { a = 0 };
-  >     var a: array[10] of B;
-  >     let b = a as array[10] of A;
+  >     var a: array[[10]] of B;
+  >     let b = a as array[[10]] of A;
   >     return 0;
   > end;
   > EOF

asllib/tests/explicit-parameters.t/explicit-parameters.asl

@@ -60,7 +60,7 @@ end;
 
 
 // We can parametrise accessors
-var _R : array [31] of bits(64);
+var _R : array [[31]] of bits(64);
 
 getter X{N}(regno: integer) => bits(N)
 begin

asllib/tests/lca.t

@@ -182,14 +182,14 @@
   > type T1 of integer;
   > func main () => integer
   > begin
-  >   var a: array[4] of integer;
-  >   var b: array[4] of T1;
+  >   var a: array[[4]] of integer;
+  >   var b: array[[4]] of T1;
   >   let x = if ARBITRARY: boolean then a else b;
   >   let -: real = x;
   > end;
   > EOF
 
   $ aslref lca14.asl
   File lca14.asl, line 7, characters 2 to 18:
-  ASL Typing error: a subtype of real was expected, provided array [4] of T1.
+  ASL Typing error: a subtype of real was expected, provided array [[4]] of T1.
   [1]

asllib/tests/regressions.t/array-index-error.asl

@@ -1,6 +1,6 @@
 func main () => integer
 begin
-  var arr: array[5] of integer;
+  var arr: array[[5]] of integer;
 
   // Legal
   arr[[2]] = 0;
@@ -10,4 +10,4 @@ begin
 
   return 1;
 end;
-  
+

asllib/tests/regressions.t/array-lca.asl

@@ -2,8 +2,8 @@ type A of integer;
 func main() => integer
 begin
     var b = ARBITRARY: boolean;
-    var a : array[5] of integer;
-    var c : array[5] of A;
+    var a : array[[5]] of integer;
+    var c : array[[5]] of A;
     var x = if (b) then a else c;
     return 0;
 end;

asllib/tests/regressions.t/array-with-enums.asl

@@ -4,7 +4,7 @@ type MyEnum of enumeration {
   MyEnumC,
 };
 
-type MyArray of array [ MyEnum ] of integer;
+type MyArray of array [[ MyEnum ]] of integer;
 
 var myArray : MyArray;
 

asllib/tests/regressions.t/array.asl

@@ -1,4 +1,4 @@
-type a of array [4] of integer;
+type a of array [[4]] of integer;
 
 var global_a: a;
 

asllib/tests/regressions.t/enum-array.asl

@@ -1,6 +1,6 @@
 type MyEnum of enumeration { A, B, C };
 
-type MyArray of array [ MyEnum ] of integer;
+type MyArray of array [[ MyEnum ]] of integer;
 
 func main () => integer
 begin

asllib/tests/regressions.t/run.t

@@ -6,8 +6,8 @@ Hello world should work:
 Type-checking errors:
 
   $ aslref subtype-satisfaction-arrray-illegal.asl
-  File subtype-satisfaction-arrray-illegal.asl, line 4, characters 0 to 36:
-  ASL Typing error: a subtype of m was expected, provided array [10] of n.
+  File subtype-satisfaction-arrray-illegal.asl, line 4, characters 0 to 38:
+  ASL Typing error: a subtype of m was expected, provided array [[10]] of n.
   [1]
 
   $ aslref anonymous-types-example.asl

asllib/tests/regressions.t/subtype-satisfaction-arrray-illegal.asl

@@ -1,7 +1,7 @@
 type l of bits(64) { [1] x, [2] y, [3] z };
-type m of array[10] of l;
+type m of array[[10]] of l;
 type n of bits(64) { [1] x, [2] y, [3] z };
-type o of array[10] of n subtypes m;
+type o of array[[10]] of n subtypes m;
 
 func main () => integer
 begin

asllib/tests/typing.t/HExample8.asl

@@ -8,6 +8,6 @@ end;
 
 func FunctWithConstraint{M}(result : bits(M), x : integer{1,2,3,4}) => bits(M)
 begin
-    var y : array[x] of integer;
+    var y : array[[x]] of integer;
     return result;
 end;

herd/tests/instructions/ASL/enum-array.litmus

@@ -1,7 +1,7 @@
 ASL enum-arrays
 {}
 type Enum of enumeration {A, B, C};
-type Arr of array[Enum] of integer;
+type Arr of array[[Enum]] of integer;
 func main () => integer
 begin
   var arr: Arr;