merge

.github/workflows/acl2.yml

@@ -72,6 +72,7 @@ jobs:
             for dir in ${canonicalization_errors[@]};
             do
               cat tmp/tgc/$dir/canonicalization_result.out
+              cat tmp/tgc/$dir/canonicalization-theorem.lisp
             done;
             exit 1
           fi

docs/rfc/007-type-aliases.md

@@ -28,7 +28,7 @@ Many programming languages provide the ability to create aliases (i.e. synonyms)
 The purpose may be to abbreviate a longer type,
 such as an alias `matrix` for `[i32; (3, 3)]` in an application in which 3x3 matrices of 32-bit integers are relevant
 (e.g. for 3-D rotations, even though fractional numbers may be more realistic).
-The purpose may also be to clarify the purpose and use of an existing type,
+The purpose may also be to clarify the intent and use of an existing type,
 such as an alias `balance` for `u64` in an application that keeps track of balances.
 
 The initial motivation that inspired this RFC (along with other RFCs)
@@ -42,7 +42,7 @@ With the array types of unspecified size proposed in RFC 006,
 ## Syntax
 
 The ABNF grammar changes as follows:
-```ts
+```
 ; modified rule:
 keyword = ...
         / %s"true"
@@ -59,12 +59,63 @@ declaration = import-declaration
             / circuit-declaration
             / constant-declaration
             / type-alias-declaration ; new
+
+
 ```
 
 A type alias declaration introduces the identifier to stand for the type.
 Only top-level type alias declarations are supported;
 they are not supported inside functions or circuit types.
 
+In addition, the following changes to the grammar are appropriate.
+
+First, the rule
+```
+circuit-type = identifier / self-type ; replace with the one below
+```
+should be replaced with the rule
+```
+circuit-or-alias-type = identifier / self-type
+```
+The reason is that, at parsing time, an identifier is not necessarily a circuit type;
+it may be a type alias that may expand to a (circuit or non-circuit type).
+Thus, the nomenclature `circuit-or-alias-type` is appropriate.
+Consequently, references to `circuit-type` in the following rules must be replaced with `circuit-or-alias-type`:
+```
+; modified rule:
+circuit-construction = circuit-or-alias-type "{" ; modified
+                       circuit-inline-element
+                       *( "," circuit-inline-element ) [ "," ]
+                       "}"
+
+; modified rule:
+postfix-expression = primary-expression
+                   / postfix-expression "." natural
+                   / postfix-expression "." identifier
+                   / identifier function-arguments
+                   / postfix-expression "." identifier function-arguments
+                   / circuit-or-alias-type "::" identifier function-arguments ; modified
+                   / postfix-expression "[" expression "]"
+                   / postfix-expression "[" [expression] ".." [expression] "]"
+```
+
+Second, the rule
+```
+aggregate-type = tuple-type / array-type / circuit-type
+```
+should be removed, because if we replaced `circuit-type` with `circuit-or-alias-type` there,
+the identifier could be a type alias, not necessarily an aggregate type.
+(The notion of aggregate type remains at a semantic level, but has no longer a place in the grammar.)
+Consequently, the rule
+```
+type = scalar-type / aggregate-type
+```
+should be rephrased as
+```
+type = scalar-type / tuple-type / array-type / circuit-or-alias-type
+```
+which "inlines" the previous `aggregate-type` with `circuit-type` replaced with `circuit-or-alias-type`.
+
 ## Semantics
 
 There must be no direct or indirect circularity in the type aliases.

tests/compiler/char/nonprinting.leo

@@ -37,7 +37,7 @@ function main(
     in30: char,
     in31: char,
     in32: char,
-    in32: char,
+    in33: char,
 ) -> ([char; 33], bool) {
     let str = [
         in1,
@@ -72,8 +72,8 @@ function main(
         in30,
         in31,
         in32,
-        in32,
+        in33,
     ];
     console.log("{}", str);
     return (str, in1 == '\x00');
-}
+}

tests/expectations/compiler/compiler/char/nonprinting.leo.out

@@ -4,21 +4,21 @@ expectation: Pass
 outputs:
   - circuit:
       num_public_variables: 0
-      num_private_variables: 35
+      num_private_variables: 36
       num_constraints: 3
-      at: 27242eeb2faf33996c0329ac2ec3b337434f78d392ff29465d3508084de6c721
-      bt: 4727127f178bb02895a615bf38a4aa3c5cb9d2b076eca15ebe6fea741b48ce98
-      ct: cae904ba23a045f4438177f10211a50ae29eee49d08211c731aee88353dc0cfb
+      at: 25579220a31118007fe071d3083ad5a5503f7dc6bd4d51abf15f1a7778a99c86
+      bt: 8f5bf097224289e45b78e01a711900a993240585fe13744f9ab71a9c5c4d9111
+      ct: df019f90846f94966d481bfb6d579bee9c47d281176e210ccd973210afc957a1
     output:
       - input_file: inputs/nonprinting.in
         output:
           registers:
             r0:
               type: "[char; 33]"
-              value: "\"\\u{0}\\u{1}\\u{2}\\u{3}\\u{4}\\u{5}\\u{6}\\u{7}\\u{8}\\t\\n\\u{b}\\u{c}\\r\\u{e}\\u{f}\\u{10}\\u{11}\\u{12}\\u{13}\\u{14}\\u{15}\\u{16}\\u{17}\\u{18}\\u{19}\\u{1a}\\u{1b}\\u{1c}\\u{1d}\\u{1e}\\u{1f}\\u{1f}\""
+              value: "\"\\u{0}\\u{1}\\u{2}\\u{3}\\u{4}\\u{5}\\u{6}\\u{7}\\u{8}\\t\\n\\u{b}\\u{c}\\r\\u{e}\\u{f}\\u{10}\\u{11}\\u{12}\\u{13}\\u{14}\\u{15}\\u{16}\\u{17}\\u{18}\\u{19}\\u{1a}\\u{1b}\\u{1c}\\u{1d}\\u{1e}\\u{1f} \""
             r1:
               type: bool
               value: "true"
-    initial_ast: b03b0ea8ad821952fa64e477900b43c830e9fbd9693478018ad4b13abd12b027
-    canonicalized_ast: b03b0ea8ad821952fa64e477900b43c830e9fbd9693478018ad4b13abd12b027
-    type_inferenced_ast: 4ded1909fcd3fa1edf7de8111d3f7b97fced37b5b2d18b316f9fee3aad246f5e
+    initial_ast: 4e9ef2d8121eabed385e2d358e2d9ed1dc64d88894c3dbfc078d5da34902ce4c
+    canonicalized_ast: 4e9ef2d8121eabed385e2d358e2d9ed1dc64d88894c3dbfc078d5da34902ce4c
+    type_inferenced_ast: 489e02b2ed42362bf493fe2fb58cf03ab06cfb95abd49b7ba0329a8e8d7c3daa