From 517e71d72220c883a0e2ce9fea0a88f28ca126a0 Mon Sep 17 00:00:00 2001 From: Wonho Date: Wed, 31 Jul 2024 17:35:04 +0900 Subject: [PATCH] Minor changes --- spectec/src/exe-watsup/main.ml | 2 + spectec/src/il2al/translate.ml | 2 +- spectec/test-prose/TEST.md | 108 ------------------ spectec/test-prose/doc/exec/modules-in.rst | 4 - spectec/test-prose/doc/syntax/values-in.rst | 4 - .../test-prose/doc/valid/conventions-in.rst | 12 -- spectec/test-prose/doc/valid/types-in.rst | 4 - spectec/test-splice/TEST.md | 9 -- 8 files changed, 3 insertions(+), 142 deletions(-) diff --git a/spectec/src/exe-watsup/main.ml b/spectec/src/exe-watsup/main.ml index a57f48d263..c407c2231a 100644 --- a/spectec/src/exe-watsup/main.ml +++ b/spectec/src/exe-watsup/main.ml @@ -221,8 +221,10 @@ let () = Printf.printf "%s\n%!" (List.filter (match_algo_name !print_al_o) al |> List.map Al.Print.string_of_algorithm |> String.concat "\n"); + (* WIP log "AL Validation..."; Al.Valid.valid al; + *) (match !target with | Check -> () diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 7d5b2d581d..5d6ed2e4e5 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -763,7 +763,7 @@ and handle_special_lhs lhs rhs free_ids = | ListE es -> let bindings, es' = extract_non_names es in if List.length es >= 2 then (* TODO: remove this. This is temporarily for a pure function returning stores *) - letI (listE es' ~at:lhs.at ~note:lhs.note, lhs) ~at:at :: translate_bindings free_ids bindings + letI (listE es' ~at:lhs.at ~note:lhs.note, rhs) ~at:at :: translate_bindings free_ids bindings else [ ifI diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index a3a8d4e451..578650e8e8 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -445,24 +445,6 @@ fone N canon_ N 1. Return (2 ^ ($signif(N) - 1)). -utf8 char_u0* -1. If (|char_u0*| is 1), then: - a. Let [ch] be char_u0*. - b. If (ch < 128), then: - 1) Let b be ch. - 2) Return [b]. - c. If ((128 ≤ ch) and ((ch < 2048) and (ch ≥ (b_2 - 128)))), then: - 1) Let ((2 ^ 6) · (b_1 - 192)) be (ch - (b_2 - 128)). - 2) Return [b_1, b_2]. - d. If ((((2048 ≤ ch) and (ch < 55296)) or ((57344 ≤ ch) and (ch < 65536))) and (ch ≥ (b_3 - 128))), then: - 1) Let (((2 ^ 12) · (b_1 - 224)) + ((2 ^ 6) · (b_2 - 128))) be (ch - (b_3 - 128)). - 2) Return [b_1, b_2, b_3]. - e. If ((65536 ≤ ch) and ((ch < 69632) and (ch ≥ (b_4 - 128)))), then: - 1) Let ((((2 ^ 18) · (b_1 - 240)) + ((2 ^ 12) · (b_2 - 128))) + ((2 ^ 6) · (b_3 - 128))) be (ch - (b_4 - 128)). - 2) Return [b_1, b_2, b_3, b_4]. -2. Let ch* be char_u0*. -3. Return $concat_($utf8([ch])*). - size valtype_u0 1. If (valtype_u0 is I32), then: a. Return 32. @@ -2110,24 +2092,6 @@ fone N canon_ N 1. Return (2 ^ ($signif(N) - 1)). -utf8 char_u0* -1. If (|char_u0*| is 1), then: - a. Let [ch] be char_u0*. - b. If (ch < 128), then: - 1) Let b be ch. - 2) Return [b]. - c. If ((128 ≤ ch) and ((ch < 2048) and (ch ≥ (b_2 - 128)))), then: - 1) Let ((2 ^ 6) · (b_1 - 192)) be (ch - (b_2 - 128)). - 2) Return [b_1, b_2]. - d. If ((((2048 ≤ ch) and (ch < 55296)) or ((57344 ≤ ch) and (ch < 65536))) and (ch ≥ (b_3 - 128))), then: - 1) Let (((2 ^ 12) · (b_1 - 224)) + ((2 ^ 6) · (b_2 - 128))) be (ch - (b_3 - 128)). - 2) Return [b_1, b_2, b_3]. - e. If ((65536 ≤ ch) and ((ch < 69632) and (ch ≥ (b_4 - 128)))), then: - 1) Let ((((2 ^ 18) · (b_1 - 240)) + ((2 ^ 12) · (b_2 - 128))) + ((2 ^ 6) · (b_3 - 128))) be (ch - (b_4 - 128)). - 2) Return [b_1, b_2, b_3, b_4]. -2. Let ch* be char_u0*. -3. Return $concat_($utf8([ch])*). - size valtype_u0 1. If (valtype_u0 is I32), then: a. Return 32. @@ -5481,26 +5445,6 @@ cont b 2. Assert: Due to validation, (b < 192). 3. Return (b - 128). -utf8 char_u0* -1. Let ch* be char_u0*. -2. Return $concat_($utf8([ch])*). -3. Assert: Due to validation, (|char_u0*| is 1). -4. Let [ch] be char_u0*. -5. If (ch < 128), then: - a. Let b be ch. - b. Return [b]. -6. If ((128 ≤ ch) and ((ch < 2048) and (ch ≥ $cont(b_2)))), then: - a. Let ((2 ^ 6) · (b_1 - 192)) be (ch - $cont(b_2)). - b. Return [b_1, b_2]. -7. If ((((2048 ≤ ch) and (ch < 55296)) or ((57344 ≤ ch) and (ch < 65536))) and (ch ≥ $cont(b_3))), then: - a. Let (((2 ^ 12) · (b_1 - 224)) + ((2 ^ 6) · $cont(b_2))) be (ch - $cont(b_3)). - b. Return [b_1, b_2, b_3]. -8. Assert: Due to validation, (65536 ≤ ch). -9. Assert: Due to validation, (ch < 69632). -10. Assert: Due to validation, (ch ≥ $cont(b_4)). -11. Let ((((2 ^ 18) · (b_1 - 240)) + ((2 ^ 12) · $cont(b_2))) + ((2 ^ 6) · $cont(b_3))) be (ch - $cont(b_4)). -12. Return [b_1, b_2, b_3, b_4]. - ANYREF 1. Return (REF (NULL ?(())) ANY). @@ -7372,58 +7316,6 @@ growmem meminst n b. Let meminst' be { TYPE: (PAGE (i', j)); BYTES: b* ++ 0^(n · (64 · $Ki())); }. c. Return meminst'. -with_locals C localidx_u0* localtype_u1* -1. If ((localidx_u0* is []) and (localtype_u1* is [])), then: - a. Return C. -2. Assert: Due to validation, (|localtype_u1*| ≥ 1). -3. Let [lct_1] ++ lct* be localtype_u1*. -4. Assert: Due to validation, (|localidx_u0*| ≥ 1). -5. Let [x_1] ++ x* be localidx_u0*. -6. Return $with_locals(C with .LOCALS[x_1] replaced by lct_1, x*, lct*). - -clos_deftypes deftype_u0* -1. If (deftype_u0* is []), then: - a. Return []. -2. Let dt* ++ [dt_n] be deftype_u0*. -3. Let dt'* be $clos_deftypes(dt*). -4. Return dt'* ++ [$subst_all_deftype(dt_n, dt'*)]. - -clos_valtype C t -1. Let dt* be $clos_deftypes(C.TYPES). -2. Return $subst_all_valtype(t, dt*). - -clos_deftype C dt -1. Let dt'* be $clos_deftypes(C.TYPES). -2. Return $subst_all_deftype(dt, dt'*). - -clos_moduletype C mmt -1. Let dt* be $clos_deftypes(C.TYPES). -2. Return $subst_all_moduletype(mmt, dt*). - -before typeuse_u0 x i -1. If the type of typeuse_u0 is deftype, then: - a. Return true. -2. If typeuse_u0 is of the case _IDX, then: - a. Let (_IDX typeidx) be typeuse_u0. - b. Return (typeidx < x). -3. Assert: Due to validation, typeuse_u0 is of the case REC. -4. Let (REC j) be typeuse_u0. -5. Return (j < i). - -unrollht C heaptype_u0 -1. If the type of heaptype_u0 is deftype, then: - a. Let deftype be heaptype_u0. - b. Return $unrolldt(deftype). -2. If heaptype_u0 is of the case _IDX, then: - a. Let (_IDX typeidx) be heaptype_u0. - b. Return $unrolldt(C.TYPES[typeidx]). -3. Assert: Due to validation, heaptype_u0 is of the case REC. -4. Let (REC i) be heaptype_u0. -5. Return C.RECS[i]. - -funcidx_nonfuncs YetE (`%%%%%`_nonfuncs(global*{global : global}, table*{table : table}, mem*{mem : mem}, elem*{elem : elem}, data*{data : data})) -1. Return $funcidx_module((MODULE [] [] [] global* table* mem* elem* data* ?() [])). - blocktype_ blocktype_u0 1. If blocktype_u0 is of the case _IDX, then: a. Let (_IDX x) be blocktype_u0. diff --git a/spectec/test-prose/doc/exec/modules-in.rst b/spectec/test-prose/doc/exec/modules-in.rst index c39aad42ca..be70a34007 100644 --- a/spectec/test-prose/doc/exec/modules-in.rst +++ b/spectec/test-prose/doc/exec/modules-in.rst @@ -276,10 +276,6 @@ $${definition: with_local} .. _def-with_locals: -$${definition-prose: with_locals} - -\ - $${definition: with_locals} .. _def-with_global: diff --git a/spectec/test-prose/doc/syntax/values-in.rst b/spectec/test-prose/doc/syntax/values-in.rst index af6d398a31..b17e1d766a 100644 --- a/spectec/test-prose/doc/syntax/values-in.rst +++ b/spectec/test-prose/doc/syntax/values-in.rst @@ -101,8 +101,4 @@ $${syntax+: .. _def-utf8: -$${definition-prose: utf8} - -\ - $${definition: utf8} diff --git a/spectec/test-prose/doc/valid/conventions-in.rst b/spectec/test-prose/doc/valid/conventions-in.rst index 6c11f3d3bd..549191530d 100644 --- a/spectec/test-prose/doc/valid/conventions-in.rst +++ b/spectec/test-prose/doc/valid/conventions-in.rst @@ -274,10 +274,6 @@ $${definition: unrolldt} .. _def-unrollht: -$${definition-prose: unrollht} - -\ - $${definition: unrollht} .. _def-expanddt: @@ -319,16 +315,8 @@ $${syntax: context} .. _def-clos_deftype: -$${definition-prose: clos_deftype} - -\ - $${definition: clos_deftype} .. _def-clos_deftypes: -$${definition-prose: clos_deftypes} - -\ - $${definition: clos_deftypes} diff --git a/spectec/test-prose/doc/valid/types-in.rst b/spectec/test-prose/doc/valid/types-in.rst index 88127079d8..847536af61 100644 --- a/spectec/test-prose/doc/valid/types-in.rst +++ b/spectec/test-prose/doc/valid/types-in.rst @@ -99,10 +99,6 @@ Recursive Types .. _def-before: -$${definition-prose: before} - -\ - $${definition: before} .. _syntax-oktypeidx: diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 453e2818e8..27bcd2d681 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -1754,14 +1754,9 @@ warning: definition prose `alloctable` was never spliced warning: definition prose `alloctables` was never spliced warning: definition prose `alloctypes` was never spliced warning: definition prose `arrayinst` was never spliced -warning: definition prose `before` was never spliced warning: definition prose `binop_` was never spliced warning: definition prose `blocktype_` was never spliced warning: definition prose `canon_` was never spliced -warning: definition prose `clos_deftype` was never spliced -warning: definition prose `clos_deftypes` was never spliced -warning: definition prose `clos_moduletype` was never spliced -warning: definition prose `clos_valtype` was never spliced warning: definition prose `concat_` was never spliced warning: definition prose `concatn_` was never spliced warning: definition prose `const` was never spliced @@ -1844,7 +1839,6 @@ warning: definition prose `free_valtype` was never spliced warning: definition prose `free_vectype` was never spliced warning: definition prose `func` was never spliced warning: definition prose `funcidx_module` was never spliced -warning: definition prose `funcidx_nonfuncs` was never spliced warning: definition prose `funcinst` was never spliced warning: definition prose `funcsxt` was never spliced warning: definition prose `funcsxv` was never spliced @@ -1949,9 +1943,7 @@ warning: definition prose `unpack` was never spliced warning: definition prose `unpackfield_` was never spliced warning: definition prose `unpackshape` was never spliced warning: definition prose `unrolldt` was never spliced -warning: definition prose `unrollht` was never spliced warning: definition prose `unrollrt` was never spliced -warning: definition prose `utf8` was never spliced warning: definition prose `var` was never spliced warning: definition prose `vbinop_` was never spliced warning: definition prose `vcvtop__` was never spliced @@ -1970,7 +1962,6 @@ warning: definition prose `with_data` was never spliced warning: definition prose `with_elem` was never spliced warning: definition prose `with_global` was never spliced warning: definition prose `with_local` was never spliced -warning: definition prose `with_locals` was never spliced warning: definition prose `with_mem` was never spliced warning: definition prose `with_meminst` was never spliced warning: definition prose `with_struct` was never spliced