Skip to content

[spectec] Fix prose of the rule instr_const#2161

Merged
rossberg merged 2 commits intomainfrom
const.prose.fix
May 8, 2026
Merged

[spectec] Fix prose of the rule instr_const#2161
rossberg merged 2 commits intomainfrom
const.prose.fix

Conversation

@f52985
Copy link
Copy Markdown
Collaborator

@f52985 f52985 commented May 8, 2026

This PR fixes the prose for the instr_const rule, where the variable val was incorrectly used instead of instr, resolving #2144.

The root cause was that the rule unification logic only considered the first two rules (CONST and VCONST) and incorrectly assumed the unified variable type should be val. It now considers all cases and correctly generates the unified variable with type instr.

Comment thread spectec/src/il2al/unify.ml Outdated
(* HARDCODE: Prevent falsely unifying mixture of instr and val into `__unify:val` *)
and generalize_unified_wasm_val env u e =
if Il2al_util.is_val u && not (Il2al_util.is_val e) then (
let new_var = VarE ("instr" $ no_region) $$ no_region % e.note in
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would it be possible to avoid hard-coding the variable name? Could it invoke gen_new_unified without a prefix here right away?

(Btw, looking at gen_new_unified just now, I noticed that

  let var =
    match prefix with
    | Some prefix -> introduce_fresh_variable ~prefix env.frees ty
    | _ -> introduce_fresh_variable env.frees ty in

can be simplified to

  let var = introduce_fresh_variable ?prefix env.frees ty

)

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense. Fixed it accordingly.

@rossberg rossberg merged commit 28b9f84 into main May 8, 2026
10 checks passed
@rossberg rossberg deleted the const.prose.fix branch May 8, 2026 09:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants