From 6fb6ca8be9f8b7702f24668bdec26b703157697f Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 12 Jul 2025 13:35:32 +0200 Subject: [PATCH] [spectec] Require explicit declaration of builtins; adjust all specs Co-authored by @zilinc --- specification/wasm-1.0/3-numerics.spectec | 56 +++++++++++++ specification/wasm-2.0/3-numerics.spectec | 79 +++++++++++++++++- .../wasm-3.0/1.0-syntax.profiles.spectec | 2 +- .../wasm-3.0/3.0-numerics.relaxed.spectec | 18 ++-- .../wasm-3.0/3.1-numerics.scalar.spectec | 77 +++++++++++++++++ .../wasm-3.0/3.2-numerics.vector.spectec | 3 + spectec/doc/example/output/NanoWasm.pdf | Bin 245205 -> 245205 bytes .../src/backend-interpreter/interpreter.ml | 46 ++++++++-- spectec/src/frontend/elab.ml | 12 ++- spectec/src/il2al/il2al_util.ml | 3 +- spectec/test-latex/TEST.md | 8 -- 11 files changed, 271 insertions(+), 33 deletions(-) diff --git a/specification/wasm-1.0/3-numerics.spectec b/specification/wasm-1.0/3-numerics.spectec index 72543411b3..c1d352b3ca 100644 --- a/specification/wasm-1.0/3-numerics.spectec +++ b/specification/wasm-1.0/3-numerics.spectec @@ -40,10 +40,23 @@ def $promote__(M, N, fN(M)) : fN(N)* def $convert__(M, N, sx, iN(M)) : fN(N) hint(show $convert__(%,%)^(%)#((%))) def $reinterpret__(valtype_1, valtype_2, val_(valtype_1)) : val_(valtype_2) +;; TODO(3, rossberg): implement numerics internally +def $wrap__ hint(builtin) +def $extend__ hint(builtin) +def $trunc__ hint(builtin) +def $demote__ hint(builtin) +def $promote__ hint(builtin) +def $convert__ hint(builtin) +def $reinterpret__ hint(builtin) + def $ibytes_(N, iN(N)) : byte* hint(show $bytes_(I#%,%)) def $fbytes_(N, fN(N)) : byte* hint(show $bytes_(F#%,%)) def $bytes_(valtype, val_(valtype)) : byte* +def $ibytes_ hint(builtin) +def $fbytes_ hint(builtin) +def $bytes_ hint(builtin) + def $invibytes_(N, byte*) : iN(N) def $invfbytes_(N, byte*) : fN(N) @@ -79,16 +92,36 @@ def $ige_(N, sx, iN(N), iN(N)) : u32 hint(show $ige_(%)^(%)#((%,%))) def $iadd_(N, i_1, i_2) = $((i_1 + i_2) \ 2^N) def $isub_(N, i_1, i_2) = $((2^N + i_1 - i_2) \ 2^N) def $imul_(N, i_1, i_2) = $((i_1 * i_2) \ 2^N) + +def $idiv_ hint(builtin) +def $irem_ hint(builtin) +def $inot_ hint(builtin) +def $iand_ hint(builtin) +def $ior_ hint(builtin) +def $ixor_ hint(builtin) +def $ishl_ hint(builtin) +def $ishr_ hint(builtin) +def $irotl_ hint(builtin) +def $irotr_ hint(builtin) +def $iclz_ hint(builtin) +def $ictz_ hint(builtin) +def $ipopcnt_ hint(builtin) + def $ieqz_(N, i_1) = $bool(i_1 = 0) def $inez_(N, i_1) = $bool(i_1 =/= 0) + def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2) def $ine_(N, i_1, i_2) = $bool(i_1 =/= i_2) + def $ilt_(N, U, i_1, i_2) = $bool(i_1 < i_2) def $ilt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) < $signed_(N, i_2)) + def $igt_(N, U, i_1, i_2) = $bool(i_1 > i_2) def $igt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) > $signed_(N, i_2)) + def $ile_(N, U, i_1, i_2) = $bool(i_1 <= i_2) def $ile_(N, S, i_1, i_2) = $bool($signed_(N, i_1) <= $signed_(N, i_2)) + def $ige_(N, U, i_1, i_2) = $bool(i_1 >= i_2) def $ige_(N, S, i_1, i_2) = $bool($signed_(N, i_1) >= $signed_(N, i_2)) @@ -113,6 +146,29 @@ def $fgt_(N, fN(N), fN(N)) : u32 def $fle_(N, fN(N), fN(N)) : u32 def $fge_(N, fN(N), fN(N)) : u32 +def $fadd_ hint(builtin) +def $fsub_ hint(builtin) +def $fmul_ hint(builtin) +def $fdiv_ hint(builtin) +def $fmin_ hint(builtin) +def $fmax_ hint(builtin) + +def $fcopysign_ hint(builtin) +def $fabs_ hint(builtin) +def $fneg_ hint(builtin) +def $fsqrt_ hint(builtin) +def $fceil_ hint(builtin) +def $ffloor_ hint(builtin) +def $ftrunc_ hint(builtin) +def $fnearest_ hint(builtin) + +def $feq_ hint(builtin) +def $fne_ hint(builtin) +def $flt_ hint(builtin) +def $fgt_ hint(builtin) +def $fle_ hint(builtin) +def $fge_ hint(builtin) + def $binop_(Inn, ADD, iN_1, iN_2) = $iadd_($size(Inn), iN_1, iN_2) def $binop_(Inn, SUB, iN_1, iN_2) = $isub_($size(Inn), iN_1, iN_2) diff --git a/specification/wasm-2.0/3-numerics.spectec b/specification/wasm-2.0/3-numerics.spectec index 4ca0404f84..abf566967d 100644 --- a/specification/wasm-2.0/3-numerics.spectec +++ b/specification/wasm-2.0/3-numerics.spectec @@ -64,6 +64,24 @@ def $fbytes_(N, fN(N)) : byte* hint(show $bytes_(F#%,%)) def $nbytes_(numtype, num_(numtype)) : byte* hint(show $bytes_(%,%)) def $vbytes_(vectype, vec_(vectype)) : byte* hint(show $bytes_(%,%)) +;; TODO(3, rossberg): implement numerics internally +def $wrap__ hint(builtin) +def $extend__ hint(builtin) +def $trunc__ hint(builtin) +def $trunc_sat__ hint(builtin) +def $demote__ hint(builtin) +def $promote__ hint(builtin) +def $convert__ hint(builtin) +def $narrow__ hint(builtin) +def $reinterpret__ hint(builtin) + +def $ibits_ hint(builtin) +def $fbits_ hint(builtin) +def $ibytes_ hint(builtin) +def $fbytes_ hint(builtin) +def $nbytes_ hint(builtin) +def $vbytes_ hint(builtin) + def $invibytes_(N, byte*) : iN(N) def $invfbytes_(N, byte*) : fN(N) @@ -108,30 +126,63 @@ def $isub_sat_(N, sx, iN(N), iN(N)) : iN(N) hint(show $isub__sat_(%)^(%)#((% def $iavgr_(N, sx, iN(N), iN(N)) : iN(N) hint(show $iavgr_(%)^(%)#((%,%))) def $iq15mulr_sat_(N, sx, iN(N), iN(N)) : iN(N) hint(show $iq15mulr__sat_(%)^(%)#((%,%))) -;; TODO(3, rossberg): implement numerics internally def $iadd_(N, i_1, i_2) = $((i_1 + i_2) \ 2^N) def $isub_(N, i_1, i_2) = $((2^N + i_1 - i_2) \ 2^N) def $imul_(N, i_1, i_2) = $((i_1 * i_2) \ 2^N) + +def $idiv_ hint(builtin) +def $irem_ hint(builtin) +def $inot_ hint(builtin) +def $irev_ hint(builtin) +def $iand_ hint(builtin) +def $iandnot_ hint(builtin) +def $ior_ hint(builtin) +def $ixor_ hint(builtin) +def $ishl_ hint(builtin) +def $ishr_ hint(builtin) +def $irotl_ hint(builtin) +def $irotr_ hint(builtin) +def $iclz_ hint(builtin) +def $ictz_ hint(builtin) +def $ipopcnt_ hint(builtin) + def $ieqz_(N, i_1) = $bool(i_1 = 0) def $inez_(N, i_1) = $bool(i_1 =/= 0) + def $ieq_(N, i_1, i_2) = $bool(i_1 = i_2) def $ine_(N, i_1, i_2) = $bool(i_1 =/= i_2) + def $ilt_(N, U, i_1, i_2) = $bool(i_1 < i_2) def $ilt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) < $signed_(N, i_2)) + def $igt_(N, U, i_1, i_2) = $bool(i_1 > i_2) def $igt_(N, S, i_1, i_2) = $bool($signed_(N, i_1) > $signed_(N, i_2)) + def $ile_(N, U, i_1, i_2) = $bool(i_1 <= i_2) def $ile_(N, S, i_1, i_2) = $bool($signed_(N, i_1) <= $signed_(N, i_2)) + def $ige_(N, U, i_1, i_2) = $bool(i_1 >= i_2) def $ige_(N, S, i_1, i_2) = $bool($signed_(N, i_1) >= $signed_(N, i_2)) + +def $ibitselect_ hint(builtin) + def $iabs_(N, i_1) = i_1 -- if $signed_(N, i_1) >= 0 def $iabs_(N, i_1) = $ineg_(N, i_1) -- otherwise + +def $imin_ hint(builtin) +def $imax_ hint(builtin) + def $ineg_(N, i_1) = $invsigned_(N, $(- $signed_(N, i_1))) + def $iadd_sat_(N, U, i_1, i_2) = $sat_u_(N, $(i_1 + i_2)) def $iadd_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) + $signed_(N, i_2)))) + def $isub_sat_(N, U, i_1, i_2) = $sat_u_(N, $(i_1 - i_2)) def $isub_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) - $signed_(N, i_2)))) +def $iavgr_ hint(builtin) +def $iq15mulr_sat_ hint(builtin) + def $fadd_(N, fN(N), fN(N)) : fN(N)* def $fsub_(N, fN(N), fN(N)) : fN(N)* def $fmul_(N, fN(N), fN(N)) : fN(N)* @@ -155,6 +206,31 @@ def $fgt_(N, fN(N), fN(N)) : u32 def $fle_(N, fN(N), fN(N)) : u32 def $fge_(N, fN(N), fN(N)) : u32 +def $fadd_ hint(builtin) +def $fsub_ hint(builtin) +def $fmul_ hint(builtin) +def $fdiv_ hint(builtin) +def $fmin_ hint(builtin) +def $fmax_ hint(builtin) +def $fpmin_ hint(builtin) +def $fpmax_ hint(builtin) + +def $fcopysign_ hint(builtin) +def $fabs_ hint(builtin) +def $fneg_ hint(builtin) +def $fsqrt_ hint(builtin) +def $fceil_ hint(builtin) +def $ffloor_ hint(builtin) +def $ftrunc_ hint(builtin) +def $fnearest_ hint(builtin) + +def $feq_ hint(builtin) +def $fne_ hint(builtin) +def $flt_ hint(builtin) +def $fgt_ hint(builtin) +def $fle_ hint(builtin) +def $fge_ hint(builtin) + def $binop_(Inn, ADD, iN_1, iN_2) = $iadd_($sizenn(Inn), iN_1, iN_2) def $binop_(Inn, SUB, iN_1, iN_2) = $isub_($sizenn(Inn), iN_1, iN_2) def $binop_(Inn, MUL, iN_1, iN_2) = $imul_($sizenn(Inn), iN_1, iN_2) @@ -229,6 +305,7 @@ def $unpacknum_(packtype, c) = $extend__($psize(packtype), $size($unpack(packtyp ;; Vectors def $lanes_(shape, vec_(V128)) : lane_($lanetype(shape))* +def $lanes_ hint(builtin) def $invlanes_(shape, lane_($lanetype(shape))*) : vec_(V128) hint(show $lanes^(-1)#_%#(%,%)) diff --git a/specification/wasm-3.0/1.0-syntax.profiles.spectec b/specification/wasm-3.0/1.0-syntax.profiles.spectec index 55ae7a4cd9..f5a6fafe13 100644 --- a/specification/wasm-3.0/1.0-syntax.profiles.spectec +++ b/specification/wasm-3.0/1.0-syntax.profiles.spectec @@ -2,4 +2,4 @@ ;; Profiles ;; -def $ND : bool ;; non-determinism +def $ND : bool hint(builtin) ;; non-determinism diff --git a/specification/wasm-3.0/3.0-numerics.relaxed.spectec b/specification/wasm-3.0/3.0-numerics.relaxed.spectec index 5f0f87c5ce..212c948ba0 100644 --- a/specification/wasm-3.0/3.0-numerics.relaxed.spectec +++ b/specification/wasm-3.0/3.0-numerics.relaxed.spectec @@ -15,12 +15,12 @@ def $relaxed4(i, syntax X, X_1, X_2, X_3, X_4) = (X_1 X_2 X_3 X_4)[i] -- if $ND def $relaxed4(i, syntax X, X_1, X_2, X_3, X_4) = (X_1 X_2 X_3 X_4)[0] -- otherwise -def $R_fmadd : relaxed2 -def $R_fmin : relaxed4 -def $R_fmax : relaxed4 -def $R_idot : relaxed2 -def $R_iq15mulr : relaxed2 -def $R_trunc_u : relaxed4 -def $R_trunc_s : relaxed2 -def $R_swizzle : relaxed2 -def $R_laneselect : relaxed2 +def $R_fmadd : relaxed2 hint(builtin) +def $R_fmin : relaxed4 hint(builtin) +def $R_fmax : relaxed4 hint(builtin) +def $R_idot : relaxed2 hint(builtin) +def $R_iq15mulr : relaxed2 hint(builtin) +def $R_trunc_u : relaxed4 hint(builtin) +def $R_trunc_s : relaxed2 hint(builtin) +def $R_swizzle : relaxed2 hint(builtin) +def $R_laneselect : relaxed2 hint(builtin) diff --git a/specification/wasm-3.0/3.1-numerics.scalar.spectec b/specification/wasm-3.0/3.1-numerics.scalar.spectec index 005e376eb5..07b2c07bd8 100644 --- a/specification/wasm-3.0/3.1-numerics.scalar.spectec +++ b/specification/wasm-3.0/3.1-numerics.scalar.spectec @@ -18,6 +18,16 @@ def $vbytes_(vectype, vec_(vectype)) : byte* hint(show $bytes_(%,%)) def $zbytes_(storagetype, lit_(storagetype)) : byte* hint(show $bytes_(%,%)) def $cbytes_(Cnn, lit_(Cnn)) : byte* hint(show $bytes_(%,%)) +;; TODO(3, rossberg): implement numerics internally +def $ibits_ hint(builtin) +def $fbits_ hint(builtin) +def $ibytes_ hint(builtin) +def $fbytes_ hint(builtin) +def $nbytes_ hint(builtin) +def $vbytes_ hint(builtin) +def $zbytes_ hint(builtin) +def $cbytes_ hint(builtin) + def $invibytes_(N, byte*) : iN(N) hint(show $bytes_($IN(%))^(-1)#((%))) def $invfbytes_(N, byte*) : fN(N) hint(show $bytes_($FN(%))^(-1)#((%))) @@ -122,10 +132,13 @@ def $ineg_(N, i_1) = $invsigned_(N, $(- $signed_(N, i_1))) def $iabs_(N, i_1) = i_1 -- if $signed_(N, i_1) >= 0 def $iabs_(N, i_1) = $ineg_(N, i_1) -- otherwise +def $iclz_ hint(builtin) ;;def $iclz_(N, i_1) = k -- if $ibits_(N, i_1) = (0)^k 1 d* +def $ictz_ hint(builtin) ;;def $ictz_(N, i_1) = k -- if $ibits_(N, i_1) = d* 1 (0)^k +def $ipopcnt_ hint(builtin) ;;def $ipopcnt_(N, i_1) = k -- if $ibits_(N, i_1) = (0* 1)^k 0* def $iextend_(N, M, U, i) = $(i \ 2^M) @@ -138,23 +151,27 @@ def $isub_(N, i_1, i_2) = $((2^N + i_1 - i_2) \ 2^N) def $imul_(N, i_1, i_2) = $((i_1 * i_2) \ 2^N) +def $idiv_ hint(builtin) ;;def $idiv_(N, U, i_1, 0) = eps ;;def $idiv_(N, U, i_1, i_2) = $($int(i_1 / i_2)) ;;def $idiv_(N, S, i_1, 0) = eps ;;def $idiv_(N, S, i_1, i_2) = eps -- if $($signed_(N, i_1) / $signed_(N, i_2)) = 2^(N-1) ;;def $idiv_(N, S, i_1, i_2) = $($invsigned_(N, $int($signed_(N, i_1) / $signed_(N, i_2)))) +def $irem_ hint(builtin) ;;def $irem_(N, U, i_1, 0) = eps ;;def $irem_(N, U, i_1, i_2) = $(i_1 - i_2 * $int(i_1 / i_2)) ;;def $irem_(N, S, i_1, 0) = eps ;;def $irem_(N, S, i_1, i_2) = $($invsigned_(N, j_1 - j_2 * $int(j_1 / f_2))) ;; -- if j_1 = $signed_(N, i_1) /\ j_2 = $signed_(N, i_2) +def $imin_ hint(builtin) ;;def $imin_(N, U, i_1, i_2) = i_1 -- if i_1 <= i_2 ;;def $imin_(N, U, i_1, i_2) = i_2 -- otherwise ;;def $imin_(N, S, i_1, i_2) = i_1 -- if $signed_(N, i_1) <= $signed_(N, i_2) ;;def $imin_(N, S, i_1, i_2) = i_2 -- otherwise +def $imax_ hint(builtin) ;;def $imax_(N, U, i_1, i_2) = i_1 -- if i_1 >= i_2 ;;def $imax_(N, U, i_1, i_2) = i_2 -- otherwise ;;def $imax_(N, S, i_1, i_2) = i_1 -- if $signed_(N, i_1) >= $signed_(N, i_2) @@ -166,6 +183,24 @@ def $iadd_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) + def $isub_sat_(N, U, i_1, i_2) = $sat_u_(N, $(i_1 - i_2)) def $isub_sat_(N, S, i_1, i_2) = $invsigned_(N, $sat_s_(N, $($signed_(N, i_1) - $signed_(N, i_2)))) +def $iq15mulr_sat_ hint(builtin) +def $irelaxed_q15mulr_ hint(builtin) +def $iavgr_ hint(builtin) + +def $inot_ hint(builtin) +def $irev_ hint(builtin) +def $iand_ hint(builtin) +def $iandnot_ hint(builtin) +def $ior_ hint(builtin) +def $ixor_ hint(builtin) +def $ishl_ hint(builtin) +def $ishr_ hint(builtin) +def $irotl_ hint(builtin) +def $irotr_ hint(builtin) + +def $ibitselect_ hint(builtin) +def $irelaxed_laneselect_ hint(builtin) + def $ieqz_(N, i_1) = $bool(i_1 = 0) @@ -224,6 +259,36 @@ def $frelaxed_nmadd_(N, fN(N), fN(N), fN(N)) : fN(N)* hint(show $frelaxed__nma ;; TODO(3, rossberg): implement numerics internally +def $fabs_ hint(builtin) +def $fneg_ hint(builtin) +def $fsqrt_ hint(builtin) +def $fceil_ hint(builtin) +def $ffloor_ hint(builtin) +def $ftrunc_ hint(builtin) +def $fnearest_ hint(builtin) + +def $fadd_ hint(builtin) +def $fsub_ hint(builtin) +def $fmul_ hint(builtin) +def $fdiv_ hint(builtin) +def $fmin_ hint(builtin) +def $fmax_ hint(builtin) +def $fpmin_ hint(builtin) +def $fpmax_ hint(builtin) +def $frelaxed_min_ hint(builtin) +def $frelaxed_max_ hint(builtin) +def $fcopysign_ hint(builtin) + +def $feq_ hint(builtin) +def $fne_ hint(builtin) +def $flt_ hint(builtin) +def $fgt_ hint(builtin) +def $fle_ hint(builtin) +def $fge_ hint(builtin) + +def $frelaxed_madd_ hint(builtin) +def $frelaxed_nmadd_ hint(builtin) + ;; Conversions @@ -242,6 +307,18 @@ def $reinterpret__(numtype_1, numtype_2, num_(numtype_1)) : num_(numtype_2) ;; TODO(3, rossberg): implement numerics internally +def $wrap__ hint(builtin) +def $extend__ hint(builtin) +def $trunc__ hint(builtin) +def $trunc_sat__ hint(builtin) +def $relaxed_trunc__ hint(builtin) +def $demote__ hint(builtin) +def $promote__ hint(builtin) +def $convert__ hint(builtin) +def $narrow__ hint(builtin) + +def $reinterpret__ hint(builtin) + ;; Packed numbers diff --git a/specification/wasm-3.0/3.2-numerics.vector.spectec b/specification/wasm-3.0/3.2-numerics.vector.spectec index 4295ba8e94..22cc845e32 100644 --- a/specification/wasm-3.0/3.2-numerics.vector.spectec +++ b/specification/wasm-3.0/3.2-numerics.vector.spectec @@ -9,6 +9,9 @@ def $lanes_(shape, vec_(V128)) : lane_($lanetype(shape))* +;; TODO(3, rossberg): implement numerics internally +def $lanes_ hint(builtin) + def $invlanes_(shape, lane_($lanetype(shape))*) : vec_(V128) hint(show $lanes_(%)^(-1)#((%))) def $invlanes_(sh, c*) = vc -- if c* = $lanes_(sh, vc) diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf index 1250e307f793bb03acbf5150e179053a3b379a99..4b6520a0690bc74000381a72432822aa4c878a09 100644 GIT binary patch delta 145 zcmccmoA2sxz6~0}f;!>e0+USU$JbOxpV80m_X%&d6mGW^W&~oU?UusK_ZG4n85$c| z8kx>TGIm>SAo*Xs2L9 MNXhmqyOR delta 145 zcmccmoA2sxz6~0}f@i|L1tyuykFTkYKBJ$V?Gx5)Dco);%m~Cx+bxBe?=56EG&D0Y zHZqtlx0P82#@X(;l{tXb*~Qq&$kM>f*}%ZX!qCmg$i&UX$i&>m#mUjk#K6_X%ud0E Nkdp0Jb}=(D0|4O8D9Qi; diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml index 502f4b3725..85298dc1ee 100644 --- a/spectec/src/backend-interpreter/interpreter.ml +++ b/spectec/src/backend-interpreter/interpreter.ml @@ -32,6 +32,22 @@ let try_with_error fname at stringifier f step = | Exception.FreeVar _) as e -> error at (prefix ^ Printexc.to_string e) (stringifier step) | Failure msg -> error at (prefix ^ msg) (stringifier step) +let warn msg = print_endline ("warning: " ^ msg) + + +(* Hints *) + +(* Try to find a hint `hintid` on a spectec function definition `fname`. *) +let find_hint fname hintid = + let open Il.Ast in + let open Il2al.Il2al_util in + List.find_map (fun hintdef -> + match hintdef.it with + | DecH (id', hints) when fname = id'.it -> + List.find_opt (fun hint -> hint.hintid.it = hintid) hints + | _ -> None + ) !hintdefs + (* Matrix operations *) @@ -257,7 +273,7 @@ and eval_expr env expr = let el = remove_typargs al in (* TODO: refactor numerics function name *) let args = List.map (eval_arg env) el in - (match call_func ("inverse_of_"^fname') args with + (match call_func ("inverse_of_"^fname') args with | Some v -> v | _ -> raise (Exception.MissingReturnValue fname) ) @@ -753,14 +769,26 @@ and create_context (name: string) (args: value list) : AlContext.mode = AlContext.al (name, params, body, env, 0) and call_func (name: string) (args: value list) : value option = - (* Function *) - if bound_func name then - [create_context name args] - |> run - |> AlContext.get_return_value - (* Numerics *) - else if Numerics.mem name then - Some (Numerics.call_numerics name args) + let builtin_name, is_builtin = + match find_hint name "builtin" with + | None -> name, false + | Some hint -> + match hint.hintexp.it with + | SeqE [] -> name, true (* hint(builtin) *) + | TextE fname -> fname, true (* hint(builtin "g") *) + | _ -> failwith (sprintf "ill-formed builtin hint for definition `%s`" name) + in + (* Function *) + if bound_func name && not is_builtin then + [create_context name args] + |> run + |> AlContext.get_return_value + (* Numerics *) + else if Numerics.mem builtin_name then ( + if not (is_builtin || String.starts_with ~prefix: "inverse_of_" name) then + warn (sprintf "Numeric function `%s` is not defined within SpecTec, consider adding a hint(builtin)" name); + Some (Numerics.call_numerics builtin_name args) + ) (* Relation *) else if Relation.mem name then ( if bound_rule name then diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml index 43137ec936..758b156672 100644 --- a/spectec/src/frontend/elab.ml +++ b/spectec/src/frontend/elab.ml @@ -2410,6 +2410,13 @@ let check_dots env = ) env.grams +let populate_hint env hd' = + match hd'.it with + | Il.TypH (id, _) -> ignore (find "syntax type" env.typs id) + | Il.RelH (id, _) -> ignore (find "relation" env.rels id) + | Il.DecH (id, _) -> ignore (find "definition" env.defs id) + | Il.GramH (id, _) -> ignore (find "grammar" env.grams id) + let populate_def env d' : Il.def = Debug.(log_in "el.populate_def" dline); Debug.(log_in_at "el.populate_def" d'.at (Fun.const "")); @@ -2431,9 +2438,8 @@ let populate_def env d' : Il.def = | Il.GramD (id, ps', t', []) -> let _, _, _, prods' = find "grammar" env.grams id in Il.GramD (id, ps', t', prods') $ d'.at - | Il.HintD _ -> d' - | _ -> - assert false + | Il.HintD hd' -> populate_hint env hd'; d' + | _ -> assert false (* Scripts *) diff --git a/spectec/src/il2al/il2al_util.ml b/spectec/src/il2al/il2al_util.ml index cad10953d7..bcdccd7f19 100644 --- a/spectec/src/il2al/il2al_util.ml +++ b/spectec/src/il2al/il2al_util.ml @@ -142,8 +142,7 @@ let rec typ_to_var_name ty = match ty.it with (* TODO: guess this for "var" in el? *) | Il.Ast.VarT (id, args) -> - let hintdefs = !hintdefs in - (match find_hint id hintdefs with + (match find_hint id !hintdefs with | None -> id.it | Some hint -> let _, t = subst_hint hint.hintexp args in t ) diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md index e018ea95b8..2d0a3aab2e 100644 --- a/spectec/test-latex/TEST.md +++ b/spectec/test-latex/TEST.md @@ -8011,10 +8011,6 @@ $$ \end{array} $$ -\vspace{1ex} - -\vspace{1ex} - $$ \begin{array}[t]{@{}lcl@{}l@{}} {{{{\mathrm{iextend}}}_{N, M}^{\mathsf{u}}}}{(i)} & = & i \mathbin{\mathrm{mod}} {2^{M}} \\ @@ -8042,10 +8038,6 @@ $$ \end{array} $$ -\vspace{1ex} - -\vspace{1ex} - $$ \begin{array}[t]{@{}lcl@{}l@{}} {{{{\mathrm{iadd\_sat}}}_{N}^{\mathsf{u}}}}{(i_1, i_2)} & = & {{\mathrm{sat\_u}}}_{N}(i_1 + i_2) \\