Enable array size polymorphism

Makefile

@@ -17,10 +17,10 @@ OPAM := opam
 LIT := lit
 
 # Control verbosity of testing
-LIT_VERBOSITY = --succinct
-# LIT_VERBOSITY = --verbose
-DUNE_VERBOSITY = ALCOTEST_COMPACT=1
-# DUNE_VERBOSITY =
+# LIT_VERBOSITY = --succinct
+LIT_VERBOSITY = --verbose
+# DUNE_VERBOSITY = ALCOTEST_COMPACT=1
+DUNE_VERBOSITY =
 
 build::
 	$(DUNE) build

libASL/asl_fmt.ml

@@ -226,7 +226,7 @@ let rec ty (fmt : PP.formatter) (x : AST.ty) : unit =
   | Type_Array (ixty, ety) ->
       kw_array fmt;
       nbsp fmt;
-      brackets fmt (fun _ -> ixtype fmt ixty);
+      ixtype fmt ixty;
       nbsp fmt;
       kw_of fmt;
       nbsp fmt;
@@ -295,7 +295,7 @@ and change (fmt : PP.formatter) (x : AST.change) : unit =
 and ixtype (fmt : PP.formatter) (x : AST.ixtype) : unit =
   match x with
   | Index_Enum tc -> tycon fmt tc
-  | Index_Int sz -> expr fmt sz
+  | Index_Int sz -> brackets fmt (fun _ -> expr fmt sz)
 
 and expr (fmt : PP.formatter) (x : AST.expr) : unit =
   ( match x with

libASL/asl_parser.messages

@@ -266,7 +266,7 @@ Malformed array type.
 The syntax of array types is
     "array [ <expression> ] of <type>"
 or
-    "array [ <enumeration type name> ] of <type>"
+    "array <enumeration type name> of <type>"
 
 expr_command_start: ID AS ARRAY LBRACK WHILE
 ##
@@ -1266,7 +1266,7 @@ Missing "]" in array type.
 The syntax of array types is
     "array [ <expression> ] of <type>"
 or
-    "array [ <enumeration type name> ] of <type>"
+    "array <enumeration type name> of <type>"
 
 expr_command_start: ID AS ARRAY LBRACK BITSLIT RBRACK WHILE
 ##
@@ -1282,7 +1282,7 @@ Missing "]" in array type.
 The syntax of array types is
     "array [ <expression> ] of <type>"
 or
-    "array [ <enumeration type name> ] of <type>"
+    "array <enumeration type name> of <type>"
 
 expr_command_start: ID AS ARRAY LBRACK BITSLIT RBRACK OF WHILE
 ##
@@ -1298,31 +1298,6 @@ Missing "of" in array type.
 The syntax of array types is
     "array [ $2 ] of <type>"
 
-expr_command_start: ID AS ARRAY LBRACK ID WHILE
-##
-## Ends in an error in state: 122.
-##
-## aexpr -> ident . [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ]
-## aexpr -> ident . LPAREN loption(separated_nonempty_list(COMMA,arg)) RPAREN throws [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ]
-## aexpr -> ident . QUERY LPAREN loption(separated_nonempty_list(COMMA,arg)) RPAREN [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ]
-## aexpr -> ident . LPAREN loption(separated_nonempty_list(COMMA,arg)) RPAREN LBRACE separated_nonempty_list(COMMA,field_assignment) RBRACE [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ]
-## aexpr -> ident . LBRACE separated_nonempty_list(COMMA,field_assignment) RBRACE [ XOR STAR SLASH REM RBRACK QUOT PLUS_PLUS PLUS OR MOD MINUS_MINUS_GT MINUS LT_MINUS_GT LT_LT LT_EQ LT LBRACK IN GT_GT GT_EQ GT EQ_EQ DOT DIVRM DIV CARET BAR_BAR BANG_EQ AS AND AMPERSAND_AMPERSAND ]
-## ixtype -> ident . [ RBRACK ]
-##
-## The known suffix of the stack is as follows:
-## ident
-##
-
-Malformed expression starting with identifier.
-The syntax of expressions that start with an identifier is
-    "$0"                                      - variable read or call getter function
-or
-    "$0(<expressions>)"                       - function call
-or
-    "$0{<field assignments>}"                 - record expression
-or
-    "$0(<expressions>){<field assignments>}"  - record expression
-
 expr_command_start: LBRACK ID COMMA ID RPAREN
 ##
 ## Ends in an error in state: 197.

libASL/asl_parser.mly

@@ -236,7 +236,7 @@ variable_declaration:
     { Decl_Const(v, ty, e, Range($symbolstartpos, $endpos)) }
 
 ixtype:
-| ident = ident { Index_Enum(ident) }
+| TYPE ident = ident { Index_Enum(ident) }
 | expr = expr { Index_Int(expr) }
 
 throws:

libASL/tcheck.ml

@@ -1072,6 +1072,9 @@ let rec synthesize_type
   | Type_Constructor (tc1, es1), Type_Constructor (tc2, es2) when tc1 = tc2 ->
       assert (List.length es1 = List.length es2);
       List.iter2 (synthesize_equality s) es1 es2
+  | Type_Array (Index_Int n1, elty1), Type_Array (Index_Int n2, elty2) ->
+      synthesize_equality s n1 n2;
+      synthesize_type env loc s elty1 elty2
   | Type_Array (_, elty1), Type_Array (_, elty2) ->
       synthesize_type env loc s elty1 elty2
   | Type_Tuple tys1, Type_Tuple tys2 ->

tests/asl_test.ml

@@ -236,7 +236,7 @@ let tests : unit Alcotest.test_case list =
            var (h : integer, i : boolean) = (1, TRUE);
            var (j : integer, - : boolean) = (1, TRUE);
            var arr1 : array [8] of integer;
-           var arr2 : array [boolean] of integer;
+           var arr2 : array [type boolean] of integer;
 
            let m : bits(8*N) = UNKNOWN : bits(8*N);
            let n : bits(8*N) = Zeros(8*N);

tests/lit/tcheck/array_param_00.asl

@@ -0,0 +1,17 @@
+// RUN: %asli --batchmode %s
+// Copyright (C) 2025-2025 Intel Corporation
+
+func F(x : array [size] of integer) => integer
+begin
+    var sum = 0;
+    for i = 0 to size-1 do
+        sum = sum + x[i];
+    end
+    return sum;
+end
+
+func main() => integer
+begin
+    let x : integer = (F(array (1,2,3)));
+    let y : integer = (F(array (1)));
+end