From ec4a81c843f9d4ede62e429d3c4ff8f00170c1b5 Mon Sep 17 00:00:00 2001
From: DJ <f52985@gmail.com>
Date: Tue, 30 Jul 2024 17:59:16 +0900
Subject: [PATCH] Test promote

---
 spectec/src/backend-prose/render.ml |  3 +++
 spectec/test-latex/TEST.md          |  2 +-
 spectec/test-prose/TEST.md          | 10 +++++-----
 3 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml
index 21c3315818..299bf80d80 100644
--- a/spectec/src/backend-prose/render.ml
+++ b/spectec/src/backend-prose/render.ml
@@ -365,6 +365,9 @@ and render_expr' env expr =
       (render_expr env elhs)
       (render_math "=")
       (render_expr env erhs)
+  | Al.Ast.LenE e ->
+    let se = render_expr env e in
+    sprintf "the length of %s" se
   | Al.Ast.IterE (e, ids, iter) when al_to_el_expr e = None ->
     let se = render_expr env e in
     let ids = Al.Al_util.tupE (List.map Al.Al_util.varE ids) in
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 10452cfc69..47648dfe62 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -1634,7 +1634,7 @@ $$
 $$
 \begin{array}{@{}lcl@{}l@{}}
 {\bigoplus}\, \epsilon &=& \epsilon \\
-{\bigoplus}\, ({w^\ast})~{({{w'}^\ast})^\ast} &=& {w^\ast}~{\bigoplus}\, {({{w'}^\ast})^\ast} \\
+{\bigoplus}\, ({w^{n}})~{({{w'}^{n}})^\ast} &=& {w^{n}}~{\bigoplus}\, {({{w'}^{n}})^\ast} \\
 \end{array}
 $$
 
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 07678be1a6..39dafe5a39 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -5416,11 +5416,11 @@ concat_ X_u0*
 2. Let [w*] ++ w'** be X_u0*.
 3. Return w* ++ $concat_(w'**).
 
-concatn X_u0* n
+concatn_ X_u0* n
 1. If (X_u0* is []), then:
   a. Return [].
-2. Let [w*] ++ w'** be X_u0*.
-3. Return w* ++ $concatn(w'**, n).
+2. Let [w^n] ++ w'^n* be X_u0*.
+3. Return w^n ++ $concatn_(w'^n*, n).
 
 disjoint_ X_u0*
 1. If (X_u0* is []), then:
@@ -8342,8 +8342,8 @@ execution_of_ARRAY.NEW_DATA x y
 8. Let (mut, zt) be arraytype_0.
 9. If ((i + ((n · $zsize(zt)) / 8)) > |$data(z, y).BYTES|), then:
   a. Trap.
-10. Assert: Due to validation, (|$concatn_0^-1(($zsize(zt) / 8), $data(z, y).BYTES[i : ((n · $zsize(zt)) / 8)])| is n).
-11. Let tmp* be $concatn_0^-1(($zsize(zt) / 8), $data(z, y).BYTES[i : ((n · $zsize(zt)) / 8)]).
+10. Assert: Due to validation, (|$concatn__0^-1(($zsize(zt) / 8), $data(z, y).BYTES[i : ((n · $zsize(zt)) / 8)])| is n).
+11. Let tmp* be $concatn__0^-1(($zsize(zt) / 8), $data(z, y).BYTES[i : ((n · $zsize(zt)) / 8)]).
 12. Let c* be $zbytes__1^-1(zt, tmp)*.
 13. Push the values $const($cunpack(zt), $cunpacknum_(zt, c))^n to the stack.
 14. Execute the instruction (ARRAY.NEW_FIXED x n).