Middlend Fixes by DCupello1 · Pull Request #216 · Wasm-DSL/spectec

DCupello1 · 2026-02-10T13:49:59Z

This pull request is for some middlend fixes/changes that were done in the Rocq backend (#207) and are now being backported.

Fixes include:

Exposing wf relations, uncase removal projection functions, type families via hints in order to produce a better output in rocq.
In undep, made List IterE's with no iteration into a ListE in order for validation to work.
ImproveIds now actually tracks atoms in order to disambiguate them from variables.
New functionality in free (inter func)
New functionality in iter (now has visit arg func)
New functionality in walk (now has collect path func)
Small fix in sub which was missing a traversal in the expression of the coercion function.
After IL change, improveids did not have the correct transformation for mixops. This has now been fixed, along with changes to transforming ids with '#' which was added with the new fresh variables generation library.
Improveids: Added small fix for LetPrs to work.
Typefamilyremoval: Small fix to generated types to not clash with the base tf type.
Sidecondtitions: Only preserves the iteration of new inferred sideconditions whenever it has a ListN
Undep: Now has new ways to place wfness premises: put whenever we encounter a term or variable that needs it (ALL), only place whenever the term or variable is not in the conclusion or function body (MINIMAL), or no placement at all (NONE)
- With the new change, this required providing a new proof obligation: for any function that constructs a term that has a correspoding wf relation, if its arguments are well formed, then the function call must also be well-formed
Typefamilyremoval: Small fix to inferral of the call expression, which was sometimes not returning the correct substituted result.
Sideconditions: removed an error message for relations that have fixed parameters. Was not necessary as it is should be valid.
Improveids: made it so the ids for hintdefs are also modified, which should have been the case in the beginning. This was only an issue if I wanted to leverage the hint system in the rendering process.

…structors/fields.

… a bind is part of a free variable set.

… a ListE)

DCupello1 · 2026-02-23T11:44:19Z

Rebased this to account for new IL changes. Still leaves improve ids not entirely fixed, will be done in a separate pull request.

DCupello1 · 2026-02-24T12:20:36Z

@nomeata could you look into this PR please? Since the IL refactor is done, these PRs can finally go in.

This one in particular is just really small changes so it shouldn't take long I hope.

nomeata · 2026-02-24T13:06:55Z

Hmm, I've paged out spectec stuff a bit these days, so I'm not eager and probably not able to give a good review. Maybe someone else whose currently playing with this could?

DCupello1 · 2026-02-24T13:17:05Z

Ah no worries then!

…ome more misc changes to naming and letpr.

… type family ones.

…milies

…nimal.

…t have the correct substitution.

… if it is ListN.

…s wfness

DCupello1 · 2026-05-25T10:39:07Z

@rossberg can you take a look on this one?

rossberg

Reviewed with a somewhat superficial understanding. :)

rossberg · 2026-05-26T09:20:24Z

  { p with it = match p.it with
    | ExpP (id, typ) -> ExpP (t.transform_var_id id, transform_typ t typ)
-    | TypP id -> TypP (t.transform_typ_id id)
+    | TypP id -> TypP (t.transform_var_id id)


Hm, this is odd. The id is a type identifier.

Hmm, aren't type parameters considered type variables? Maybe I should have a separate transform function for type variables, but I don't think theres a way to distinguish between type variables and type identifiers in arguments.

Well, no distinction is made between type names and type variables, it didn't seem necessary so far. The "sort" merely indicates the namespace, i.e., which component of the context binds it. I've exclusively used "var" for expression variables.

Hmm, I tend to want to seperate them as they generally have different naming conventions. I'll keep it as t.transform_typ_id in order for it to make more sense.

Made the change, now improveids makes even more of a disctinction between user defined types and relations, and type constructors, so that i.e. the type variable X does not clash with the type constructor X (from shape) :)

Sorry, meant to say a term constructor. Either way, it clashes when it gets to Rocq, especially when you use X when pattern matching, it gets confused with the type variable X and the term constructor X. For example, in the function relaxed2:

def $relaxed2(relaxed2, syntax X, X, X) : X hint(show $relaxed(%1)#`[%3,%4]) def $relaxed2(i, syntax X, X_1, X_2) = (X_1 X_2)[i] -- if $ND def $relaxed2(i, syntax X, X_1, X_2) = (X_1 X_2)[0] -- otherwise

would get converted as follows:

Definition fun_relaxed2 (v_relaxed2 : relaxed2) (v_X : eqType) (v_X_0 : v_X) (v_X_1 : v_X) {_ : Inhabited v_X} : v_X := match v_relaxed2, v_X, v_X_0, v_X_1 return v_X with | i, X, X_1, X_2 => (if (ND ) then ([::X_1; X_2][| (i :> nat) |]) else ([::X_1; X_2][| 0 |])) end.

Where shape is defined as:

Inductive shape : Type := | X (v_lanetype : lanetype) (v_dim : dim) : shape.

Pretty sure rocq would complain that the X in the pattern must have two arguments or something like that.
(This might be simply a rocq-specific clash though)

Ah, okay, so Is the improveid meant to remove all potential name clashes between different name spaces? It would be worth documenting that (and the renaming strategy) in the MLI.

Ah you are right! I should document that on the MLI. Yes, the idea is to remove potential name clashes between name spaces (an obvious one being functions ids and type ids being able to have the same name, etc.). I'll document it soon!

rossberg · 2026-05-26T09:32:51Z

+      (* NOTE: for let since we only have expressions we cannot modify the env ever. *)
+      let _, new_quant_map = extend_quant_set env quant_map quants in


Maybe make that an assertion?

rossberg · 2026-05-26T09:34:27Z

 *)

 val transform : Il.Ast.script -> Il.Ast.script
+val uncase_proj_hint_id : string


Nit: newline

rossberg · 2026-05-26T09:37:02Z

+  | ALL     (* Places wf premises whenever it encounters a term/variable that needs well-formedness check*)
+  | MINIMAL (* Places only wf premises in terms in relations and functions that do not appear in the conclusion *)
+  | NONE    (* Does not place any wf premises in relations/functions *)


Nit: OCaml constructor name conventions are capitalisation but not all-caps.

rossberg · 2026-05-26T09:37:57Z

-(* flag that deactivates adding wellformedness predicates to relations *)
-let deactivate_wfness = false
+(* State that indicates what the placement algorithm should do *)
+let wf_state = MINIMAL


Should this perhaps be a (exported) ref, so that it's actually configurable?

DCupello1 · 2026-05-26T13:03:40Z

Have done all of the changes, they all seem reasonable! Will update tests when all seems good.

rossberg · 2026-05-26T15:58:49Z

+  | All     (* Places wf premises whenever it encounters a term/variable that needs well-formedness check*)
+  | Minimal (* Places only wf premises in terms in relations and functions that do not appear in the conclusion *)
+  | Wfnone    (* Does not place any wf premises in relations/functions *)


Nit: Perhaps prefix the constructors consistently?

…for wfstate consistent.

DCupello1 added 7 commits February 23, 2026 11:21

small fix on sub to allow for nested sub transformation.

3ba88f9

Expose uncase removal projection functions via hints

451fce1

Improve ids change: Now ensures variables don't have same name as con…

30363ce

…structors/fields.

Exposing wf relations via hints

6f7daf9

Expose type families via hints and added utility function to check if…

ba34c3d

… a bind is part of a free variable set.

Small IL changes adding more functionality to free, iter, and walk

61dfecd

Fix tests (only changes a list IterE with no iteration variables into…

5c2fd8f

… a ListE)

DCupello1 force-pushed the middlend-fixes branch from 0a04fab to 5c2fd8f Compare February 23, 2026 11:43

DCupello1 added 12 commits February 26, 2026 12:04

Improve-ids: fixed transform mixop to have the intended effect, and s…

1f2b5e0

…ome more misc changes to naming and letpr.

Make type families have a default name if there are no quantifiers.

2cdcfc6

Undep: deactivating wfness now does not remove essential ones such as…

7c03ab8

… type family ones.

Undep: the wfness filter now checks the entire expression for type fa…

96b907f

…milies

Undep: Implemented three modes for wfness placement, all, none and mi…

6f2ef13

…nimal.

Type family removal: Fixed a bug that made types of function calls no…

c46c42b

…t have the correct substitution.

Sideconditions: Only preserve the iteration of the generated premises…

14d0cc5

… if it is ListN.

Undep: Create wf lemmas for functions that construct a term that need…

dd919fd

…s wfness

Improve ids: modify names for hints as well.

4ebf89a

Sideconditions: Don't error on relations with parameters.

a9c44b7

Merge branch 'main' into middlend-fixes

27188a3

Fix tests

63cc556

rossberg reviewed May 26, 2026

View reviewed changes

CR changes

296fa93

rossberg reviewed May 26, 2026

View reviewed changes

Improved the documentation for improveids, and made term constructor …

c3f36ba

…for wfstate consistent.

DCupello1 added 4 commits May 27, 2026 11:00

Fix tests

c2821da

Merge branch 'main' into middlend-fixes

dcda467

Fix tests (again)

67d45be

Fix tests

5f7ed5c

		(* NOTE: for let since we only have expressions we cannot modify the env ever. *)
		let _, new_quant_map = extend_quant_set env quant_map quants in

Conversation

DCupello1 commented Feb 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

DCupello1 commented Feb 23, 2026

Uh oh!

DCupello1 commented Feb 24, 2026

Uh oh!

nomeata commented Feb 24, 2026

Uh oh!

DCupello1 commented Feb 24, 2026

Uh oh!

DCupello1 commented May 25, 2026

Uh oh!

rossberg left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

DCupello1 May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

DCupello1 May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

DCupello1 commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

DCupello1 commented Feb 10, 2026 •

edited

Loading

DCupello1 May 26, 2026 •

edited

Loading

DCupello1 May 26, 2026 •

edited

Loading

DCupello1 commented May 26, 2026 •

edited

Loading